kings-crown/FVELER_Isabelle huggingface dataset:
theory StateMonad

lemma seq_ext:
  assumes "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>" "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>"
  shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" using assms by (blast intro: seq_ext')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace> proof (prove)
using this:
\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>
\<lbrace>B ?x\<rbrace> g ?x \<lbrace>C\<rbrace>

goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>
theory StateMonad

lemma seqE:
  assumes "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>" "\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>"
  shows "\<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" using assms by(blast intro: seqE')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
using this:
\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>
\<lbrace>B ?x\<rbrace> g ?x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>

goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>
theory StateMonad

lemma get_sp:
  "\<lbrace>P\<rbrace> get \<lbrace>\<lambda>a s. s = a \<and> P s\<rbrace>" by (simp add:get_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>a s. s = a \<and> P s\<rbrace>
theory StateMonad

lemma put_sp:
  "\<lbrace>\<top>\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>" by (simp add:put_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> put a \<lbrace>\<lambda>_ s. s = a\<rbrace>
theory StateMonad

lemma return_sp:
  "\<lbrace>P\<rbrace> return a \<lbrace>\<lambda>b s. b = a \<and> P s\<rbrace>" by (simp add:return_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> return a \<lbrace>\<lambda>b s. b = a \<and> P s\<rbrace>
theory StateMonad

lemma hoare_post_conj [intro!]:
  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> Q \<rbrace>; \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> a \<lbrace> Q and R \<rbrace>" by (simp add:valid_def split_def pred_conj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>Q and R\<rbrace>
theory StateMonad

lemma hoare_pre_disj [intro!]:
  "\<lbrakk> \<lbrace> P \<rbrace> a \<lbrace> R \<rbrace>; \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> P or Q \<rbrace> a \<lbrace> R \<rbrace>" by (simp add:valid_def pred_disj_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P or Q\<rbrace> a \<lbrace>R\<rbrace>
theory StateMonad

lemma hoare_post_taut [iff]: "\<lbrace> P \<rbrace> a \<lbrace> \<top>\<top> \<rbrace>" by (simp add:valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_ _. True\<rbrace>
theory StateMonad

lemma hoare_pre_cont [iff]: "\<lbrace> \<bottom> \<rbrace> a \<lbrace> P \<rbrace>" by (simp add:valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. False\<rbrace> a \<lbrace>P\<rbrace>
theory StateMonad

lemma hoare_return [intro!]: "\<And>x. P x \<Longrightarrow> \<lbrace> Q \<rbrace> return x \<lbrace> \<guillemotleft>P,Q\<guillemotright> \<rbrace>" by (simp add:valid_def return_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x. P x \<Longrightarrow> \<lbrace>Q\<rbrace> return x \<lbrace>\<guillemotleft>P,Q\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_return_drop [iff]: "\<lbrace> Q \<rbrace> return x \<lbrace> \<guillemotleft>\<top>,Q\<guillemotright> \<rbrace>" by (simp add:valid_def return_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> return x \<lbrace>\<guillemotleft>\<lambda>_. True,Q\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_return_drop_var [iff]: "\<lbrace> Q \<rbrace> return x \<lbrace> \<lambda>r. Q \<rbrace>" by (simp add:valid_def return_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> return x \<lbrace>\<lambda>r. Q\<rbrace>
theory StateMonad

lemma hoare_return_only [intro!]: "\<And>x. P x \<Longrightarrow> \<lbrace> Q \<rbrace> return x \<lbrace> \<guillemotleft>P,\<top>\<guillemotright> \<rbrace>" by (simp add:valid_def return_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x. P x \<Longrightarrow> \<lbrace>Q\<rbrace> return x \<lbrace>\<guillemotleft>P,\<lambda>_. True\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_get [iff]: "\<lbrace> P \<rbrace> get \<lbrace> \<guillemotleft>P,P\<guillemotright> \<rbrace>" by (simp add:valid_def get_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> get \<lbrace>\<guillemotleft>P,P\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_gets [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) s \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> gets f \<lbrace> Q \<rbrace>" by (simp add:valid_def gets_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> Q (f s) s) \<Longrightarrow> \<lbrace>P\<rbrace> gets f \<lbrace>Q\<rbrace>
theory StateMonad

lemma hoare_modify [iff]: "\<lbrace> P o f \<rbrace> modify f \<lbrace> \<guillemotleft>\<top>,P\<guillemotright> \<rbrace>" by (simp add:valid_def modify_def pred_lift_exact_def put_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P \<circ> f\<rbrace> modify f \<lbrace>\<guillemotleft>\<lambda>_. True,P\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_modifyE [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> modify f \<lbrace> \<guillemotleft>\<top>,Q\<guillemotright> \<rbrace>" by (simp add:valid_def modify_def pred_lift_exact_def put_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> Q (f s)) \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<guillemotleft>\<lambda>_. True,Q\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_modifyE_var [intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> modify f \<lbrace> \<lambda>r s. Q s \<rbrace>" by (simp add:valid_def modify_def pred_lift_exact_def put_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> Q (f s)) \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>r. Q\<rbrace>
theory StateMonad

lemma hoare_put [intro!]: "P x \<Longrightarrow> \<lbrace> Q \<rbrace> put x \<lbrace> \<guillemotleft>\<top>,P\<guillemotright>\<rbrace>" by (simp add:valid_def put_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P x \<Longrightarrow> \<lbrace>Q\<rbrace> put x \<lbrace>\<guillemotleft>\<lambda>_. True,P\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_if [intro!]:
  "\<lbrakk> P \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> R \<rbrace>; \<not> P \<Longrightarrow> \<lbrace> Q \<rbrace> b \<lbrace> R \<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace> Q \<rbrace> if P then a else b \<lbrace> R \<rbrace>" by (simp add:valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<not> P \<Longrightarrow> \<lbrace>Q\<rbrace> b \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> if P then a else b \<lbrace>R\<rbrace>
theory StateMonad

lemma hoare_unless [intro!]:
  "\<lbrakk> \<And>s. \<lbrakk> P; Q s \<rbrakk> \<Longrightarrow> R s; \<lbrakk> \<not> P \<rbrakk> \<Longrightarrow> \<lbrace> Q \<rbrace> a \<lbrace> \<guillemotleft>\<top>,R\<guillemotright> \<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace> Q \<rbrace> unless P a \<lbrace> \<guillemotleft>\<top>,R\<guillemotright> \<rbrace>" by (simp add:valid_def unless_def split_def when_def return_def pred_lift_exact_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. \<lbrakk>P; Q s\<rbrakk> \<Longrightarrow> R s; \<not> P \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>\<guillemotleft>\<lambda>_. True,R\<guillemotright>\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> unless P a \<lbrace>\<guillemotleft>\<lambda>_. True,R\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_pre_subst: "\<lbrakk> A = B; \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>B\<rbrace> a \<lbrace>C\<rbrace>" by (clarsimp simp:valid_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A = B; \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>B\<rbrace> a \<lbrace>C\<rbrace>
theory StateMonad

lemma hoare_post_subst: "\<lbrakk> B = C; \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace>" by (clarsimp simp:valid_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B = C; \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace>
theory StateMonad

lemma hoare_return_var[intro!]: "\<lbrakk> \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> (\<And>x. P x \<Longrightarrow> \<lbrace>R\<rbrace> return x \<lbrace>\<guillemotleft>Q,R\<guillemotright>\<rbrace>)" by (rule hoare_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> (\<And>x. P x \<Longrightarrow> \<lbrace>R\<rbrace> return x \<lbrace>\<guillemotleft>Q,R\<guillemotright>\<rbrace>)
theory StateMonad

lemma hoare_return_drop_imp[intro!]: "\<lbrakk> \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> return x \<lbrace>\<guillemotleft>\<top>,Q\<guillemotright>\<rbrace>" by (simp add:valid_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> Q s) \<Longrightarrow> \<lbrace>P\<rbrace> return x \<lbrace>\<guillemotleft>\<lambda>_. True,Q\<guillemotright>\<rbrace>
theory StateMonad

lemma hoare_pre_imp: "\<lbrakk> \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<And>s. P s \<Longrightarrow> Q s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" by (simp add:valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>
theory StateMonad

lemma "isSkip f \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> \<guillemotleft>\<top>,P\<guillemotright> \<rbrace>" apply (clarsimp simp: valid_def split_def isSkip_def) apply (rename_tac s) apply (case_tac "f s") apply (erule_tac x=s in allE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isSkip f \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<guillemotleft>\<lambda>_. True,P\<guillemotright>\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. \<exists>r. f s = (r, s); P s\<rbrakk> \<Longrightarrow> P (snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. \<exists>r. f s = (r, s); P s\<rbrakk> \<Longrightarrow> P (snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. \<exists>r. f s = (r, s); P s; f s = (a, b)\<rbrakk> \<Longrightarrow> P (snd (f s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; f s = (a, b); \<exists>r. f s = (r, s)\<rbrakk> \<Longrightarrow> P (snd (f s)) proof (prove)
goal:
No subgoals!
theory LexordList

lemma lexord_not_less_Nil [simp]: "\<not> x < lexord_list []" by (simp add: lexord_list_less_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> x < lexord_list []
theory LexordList

lemma lexord_Nil_less_Cons [simp]: "lexord_list [] < lexord_list (a # x)" by (simp add: lexord_list_less_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lexord_list [] < lexord_list (a # x)
theory LexordList

lemma lexord_Cons_less_Cons [simp]: "lexord_list (a # x) < lexord_list (b # y) \<longleftrightarrow> a < b \<or> a = b \<and> lexord_list x < lexord_list y" by (simp add: lexord_list_less_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lexord_list (a # x) < lexord_list (b # y)) = (a < b \<or> a = b \<and> lexord_list x < lexord_list y)
theory LexordList

lemma lexord_le_Nil [simp]: "x \<le> lexord_list [] \<longleftrightarrow> x = lexord_list []" unfolding lexord_list_le_def by (cases x) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x \<le> lexord_list []) = (x = lexord_list []) proof (prove)
goal (1 subgoal):
 1. (x < lexord_list [] \<or> x = lexord_list []) = (x = lexord_list [])
theory LexordList

lemma lexord_Nil_le_Cons [simp]: "lexord_list [] \<le> x" unfolding lexord_list_le_def apply (cases x, rename_tac x', case_tac x') by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lexord_list [] \<le> x proof (prove)
goal (1 subgoal):
 1. lexord_list [] < x \<or> lexord_list [] = x proof (prove)
goal (2 subgoals):
 1. \<And>x'. \<lbrakk>x = lexord_list x'; x' = []\<rbrakk> \<Longrightarrow> lexord_list [] < x \<or> lexord_list [] = x
 2. \<And>x' a list. \<lbrakk>x = lexord_list x'; x' = a # list\<rbrakk> \<Longrightarrow> lexord_list [] < x \<or> lexord_list [] = x
theory LexordList

lemma lexord_Cons_le_Cons [simp]: "lexord_list (a # x) \<le> lexord_list (b # y) \<longleftrightarrow> a < b \<or> a = b \<and> lexord_list x \<le> lexord_list y" unfolding lexord_list_le_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lexord_list (a # x) \<le> lexord_list (b # y)) = (a < b \<or> a = b \<and> lexord_list x \<le> lexord_list y) proof (prove)
goal (1 subgoal):
 1. (lexord_list (a # x) < lexord_list (b # y) \<or> lexord_list (a # x) = lexord_list (b # y)) = (a < b \<or> a = b \<and> (lexord_list x < lexord_list y \<or> lexord_list x = lexord_list y))
theory LexordList

lemma lexord_less_list_code [code]:
  "xs < lexord_list ([]::'a::{equal, order} list) \<longleftrightarrow> False"
  "lexord_list [] < lexord_list ((x::'a::{equal, order}) # xs') \<longleftrightarrow> True"
  "lexord_list ((x::'a::{equal, order}) # xs') < lexord_list (y # ys') \<longleftrightarrow> x < y \<or> x = y \<and> lexord_list xs' < lexord_list ys'" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (xs < lexord_list []) = False &&& (lexord_list [] < lexord_list (x # xs')) = True &&& (lexord_list (x # xs') < lexord_list (y # ys')) = (x < y \<or> x = y \<and> lexord_list xs' < lexord_list ys')
theory LexordList

lemma lexord_less_eq_list_code [code]:
  "lexord_list (x # xs') \<le> lexord_list ([]::'a::{equal, order} list) \<longleftrightarrow> False"
  "lexord_list [] \<le> (xs::'a::{equal, order} lexord_list) \<longleftrightarrow> True"
  "lexord_list ((x::'a::{equal, order}) # xs') \<le> lexord_list (y # ys') \<longleftrightarrow> x < y \<or> x = y \<and> lexord_list xs' \<le> lexord_list ys'" by simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (lexord_list (x # xs') \<le> lexord_list []) = False &&& (lexord_list [] \<le> xs) = True &&& (lexord_list (x # xs') \<le> lexord_list (y # ys')) = (x < y \<or> x = y \<and> lexord_list xs' \<le> lexord_list ys')
theory LexordList

lemma "lexord_list [1, 2, 3, 4] < lexord_list [1, 2, 3, 5 :: int]" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3, 4] < lexord_list [1, 2, 3, 5]
theory LexordList

lemma "\<not> (lexord_list [1, 2, 3, 5] < lexord_list [1, 2, 3, 4, 5 :: int])" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> lexord_list [1, 2, 3, 5] < lexord_list [1, 2, 3, 4, 5]
theory LexordList

lemma "lexord_list [1, 2, 3, 4] \<le> lexord_list [1, 2, 3, 5 :: int]" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3, 4] \<le> lexord_list [1, 2, 3, 5]
theory LexordList

lemma "lexord_list [1, 2, 3] < lexord_list [1, 3 :: nat]" apply (fails \<open>solves \<open>simp only: lexord_list_simps\<close>\<close>) apply (fails \<open>solves \<open>simp only: rel_simps\<close>\<close>) by (simp only: lexord_list_simps rel_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3] < lexord_list [1, 3] proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3] < lexord_list [1, 3] proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3] < lexord_list [1, 3]
theory LexordList

lemma "lexord_list [1, 2, 3] \<le> lexord_list [1, 3 :: nat]" apply (fails \<open>solves \<open>simp only: lexord_list_simps\<close>\<close>) apply (fails \<open>solves \<open>simp only: rel_simps\<close>\<close>) by (simp only: lexord_list_simps rel_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3] \<le> lexord_list [1, 3] proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3] \<le> lexord_list [1, 3] proof (prove)
goal (1 subgoal):
 1. lexord_list [1, 2, 3] \<le> lexord_list [1, 3]
theory LexordList

lemma "\<not> (lexord_list [1, 2, 3] < lexord_list [1, 2, 3 :: nat])" by (simp only: lexord_list_simps rel_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> lexord_list [1, 2, 3] < lexord_list [1, 2, 3]
theory ML_Goal_Test

lemma uses_our_new_magic_simp_rule:
  "magic = 1 + 4" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. magic = 1 + 4
theory Heap_List

lemma card_set_UNIV:
  fixes xs :: "'a::finite list"
  assumes "x \<notin> set xs"
  shows "card (set xs) < card(UNIV::'a set)" proof - have "finite (UNIV::'a set)" by simp moreover from assms have "set xs \<subset> UNIV" by blast ultimately show ?thesis by (rule psubset_card_mono) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. card (set xs) < CARD('a) proof (state)
goal (1 subgoal):
 1. card (set xs) < CARD('a) proof (prove)
goal (1 subgoal):
 1. finite UNIV proof (state)
this:
finite UNIV

goal (1 subgoal):
 1. card (set xs) < CARD('a) proof (state)
this:
finite UNIV

goal (1 subgoal):
 1. card (set xs) < CARD('a) proof (chain)
picking this:
x \<notin> set xs proof (prove)
using this:
x \<notin> set xs

goal (1 subgoal):
 1. set xs \<subset> UNIV proof (state)
this:
set xs \<subset> UNIV

goal (1 subgoal):
 1. card (set xs) < CARD('a) proof (chain)
picking this:
finite UNIV
set xs \<subset> UNIV proof (prove)
using this:
finite UNIV
set xs \<subset> UNIV

goal (1 subgoal):
 1. card (set xs) < CARD('a) proof (state)
this:
card (set xs) < CARD('a)

goal:
No subgoals!
theory Heap_List

lemma heap_path_None[simp]:
  "heap_path hp None xs end = (xs = [] \<and> end = None)" by (cases xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_path hp None xs end = (xs = [] \<and> end = None)
theory Heap_List

lemma heap_ls_unique:
  "\<lbrakk> heap_ls hp x xs; heap_ls hp x ys \<rbrakk> \<Longrightarrow> xs = ys" by (induct xs arbitrary: ys x; simp) (case_tac ys; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp x xs; heap_ls hp x ys\<rbrakk> \<Longrightarrow> xs = ys
theory Heap_List

lemma heap_ls_distinct:
  "heap_ls hp x xs \<Longrightarrow> distinct xs" by (induct xs arbitrary: x; clarsimp simp: heap_ls_hd_not_in_tl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_ls hp x xs \<Longrightarrow> distinct xs
theory Heap_List

lemma heap_ls_is_walk':
  "\<lbrakk> heap_ls hp x xs; set xs \<inter> set ys = {} \<rbrakk> \<Longrightarrow> heap_walk hp x ys = ys @ xs" by (frule heap_ls_distinct) (induct xs arbitrary: x ys; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_ls hp x xs; set xs \<inter> set ys = {}\<rbrakk> \<Longrightarrow> heap_walk hp x ys = ys @ xs
theory Heap_List

lemma heap_path_end_unique:
  "heap_path hp x xs y \<Longrightarrow> heap_path hp x xs y' \<Longrightarrow> y = y'" by (induct xs arbitrary: x; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp x xs y; heap_path hp x xs y'\<rbrakk> \<Longrightarrow> y = y'
theory Heap_List

lemma heap_path_head':
  "heap_path hp st xs y \<Longrightarrow> xs \<noteq> [] \<longrightarrow> st = Some (hd xs)" by (induct xs arbitrary: st; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_path hp st xs y \<Longrightarrow> xs \<noteq> [] \<longrightarrow> st = Some (hd xs)
theory Heap_List

lemma heap_ls_next_of_hd:
  "\<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls\<rbrakk> \<Longrightarrow> hp a = Some (hd (tl ls))" apply (cut_tac hp=hp and xs="[]" and z=a and ys="tl ls" in heap_path_non_nil_lookup_next) apply (prop_tac "ls \<noteq> []", fastforce) apply fastforce apply (cases "tl ls"; clarsimp) apply (cases ls; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls\<rbrakk> \<Longrightarrow> hp a = Some (hd (tl ls)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls\<rbrakk> \<Longrightarrow> heap_path hp ?x ([] @ a # tl ls) ?y
 2. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls; hp a = (case tl ls of [] \<Rightarrow> ?y | a # list \<Rightarrow> Some (hd (tl ls)))\<rbrakk> \<Longrightarrow> hp a = Some (hd (tl ls)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls; ls \<noteq> []\<rbrakk> \<Longrightarrow> heap_path hp ?x ([] @ a # tl ls) ?y
 2. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls; hp a = (case tl ls of [] \<Rightarrow> ?y | a # list \<Rightarrow> Some (hd (tl ls)))\<rbrakk> \<Longrightarrow> hp a = Some (hd (tl ls)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls; hp a = (case tl ls of [] \<Rightarrow> None | a # list \<Rightarrow> Some (hd (tl ls)))\<rbrakk> \<Longrightarrow> hp a = Some (hd (tl ls)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = hd ls; heap_ls hp st ls; Suc 0 < length ls; hp (hd ls) = None; tl ls = []\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Heap_List

lemma heap_path_prefix:
  "heap_path hp st ls ed \<Longrightarrow> \<forall>xs\<le>ls. heap_path hp st xs (if xs = [] then st else hp (last xs))" apply clarsimp apply (erule Prefix_Order.prefixE) by (metis append_butlast_last_id heap_path_append heap_path_non_nil_lookup_next list.case(1))

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_path hp st ls ed \<Longrightarrow> \<forall>xs\<le>ls. heap_path hp st xs (if xs = [] then st else hp (last xs)) proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>heap_path hp st ls ed; xs \<noteq> []; xs \<le> ls\<rbrakk> \<Longrightarrow> heap_path hp st xs (hp (last xs)) proof (prove)
goal (1 subgoal):
 1. \<And>xs zs. \<lbrakk>heap_path hp st ls ed; xs \<noteq> []; ls = xs @ zs\<rbrakk> \<Longrightarrow> heap_path hp st xs (hp (last xs))
theory Heap_List

lemma heap_path_butlast:
  "heap_path hp st ls ed \<Longrightarrow> ls \<noteq> [] \<Longrightarrow> heap_path hp st (butlast ls) (Some (last ls))" by (induct ls rule: rev_induct; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>heap_path hp st ls ed; ls \<noteq> []\<rbrakk> \<Longrightarrow> heap_path hp st (butlast ls) (Some (last ls))