kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_More_VCG

lemma bindE_split_recursive_asm:
  assumes x: "\<And>x s'. \<lbrakk> (Inr x, s') \<in> mres (f s) \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. B x s \<and> s = s'\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>"
  shows      "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>" apply (clarsimp simp: validE_def valid_def bindE_def in_bind lift_def) apply (erule allE, erule(1) impE) apply (drule(1) bspec, simp) apply (clarsimp simp: in_throwError split: sum.splits) apply (drule x) apply (clarsimp simp: validE_def valid_def) apply (drule(1) bspec, simp split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>st. A st \<and> st = s\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x. \<lbrakk>\<forall>s. A s \<longrightarrow> (\<forall>x\<in>mres (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> B ra s'); A s; (x, s'') \<in> mres (f s); (a, b) \<in> mres ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s'')\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> C r b proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x. \<lbrakk>A s; (x, s'') \<in> mres (f s); (a, b) \<in> mres ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s''); \<forall>x\<in>mres (f s). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> B ra s'\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> C r b proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x. \<lbrakk>A s; (x, s'') \<in> mres (f s); (a, b) \<in> mres ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s''); case x of Inl e \<Rightarrow> E e s'' | Inr r \<Rightarrow> B r s''\<rbrakk> \<Longrightarrow> case a of Inl e \<Rightarrow> E e b | Inr r \<Rightarrow> C r b proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x2. \<lbrakk>B x2 s''; A s; (Inr x2, s'') \<in> mres (f s); (a, b) \<in> mres (g x2 s'')\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> C x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x2. \<lbrakk>B x2 s''; A s; (a, b) \<in> mres (g x2 s''); \<lbrace>\<lambda>s. B x2 s \<and> s = s''\<rbrace> g x2 \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> C x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>a b s'' x2. \<lbrakk>B x2 s''; A s; (a, b) \<in> mres (g x2 s''); \<forall>x\<in>mres (g x2 s''). case x of (Inl e, s') \<Rightarrow> E e s' | (Inr ra, s') \<Rightarrow> C ra s'\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> C x2 b) proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma validE_R_abstract_rv:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" by (erule hoare_post_imp_R, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>rv'. Q rv' s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Trace_More_VCG

lemma validE_cases_valid:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q (Inr rv) s\<rbrace>,\<lbrace>\<lambda>rv s. Q (Inl rv) s\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (simp add: validE_def) apply (erule hoare_strengthen_post) apply (simp split: sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. Q (Inr rv)\<rbrace>, \<lbrace>\<lambda>rv. Q (Inl rv)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> Q (Inl e) s | Inr r \<Rightarrow> Q (Inr r) s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> Q (Inl e) s | Inr r \<Rightarrow> Q (Inr r) s \<Longrightarrow> Q rv s proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma liftM_pre:
  assumes rl: "\<lbrace>\<lambda>s. \<not> P s \<rbrace> a \<lbrace> \<lambda>_ _. False \<rbrace>"
  shows "\<lbrace>\<lambda>s. \<not> P s \<rbrace> liftM f a \<lbrace> \<lambda>_ _. False \<rbrace>" unfolding liftM_def apply (rule seq) apply (rule rl) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> liftM f a \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> do x <- a;
return (f x)
od \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>\<lambda>s. \<not> P s\<rbrace> a \<lbrace>?B\<rbrace>
 2. \<And>x. ?P x \<Longrightarrow> \<lbrace>?C\<rbrace> return (f x) \<lbrace>\<lambda>_ _. False\<rbrace>
 3. \<And>x s. ?B x s \<Longrightarrow> ?P x \<and> ?C s proof (prove)
goal (2 subgoals):
 1. \<And>x. ?P x \<Longrightarrow> \<lbrace>?C\<rbrace> return (f x) \<lbrace>\<lambda>_ _. False\<rbrace>
 2. \<And>x s. False \<Longrightarrow> ?P x \<and> ?C s proof (prove)
goal (1 subgoal):
 1. \<And>x s. False \<Longrightarrow> ?P x \<and> False proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma hoare_gen_asm':
  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace>" apply (auto intro: hoare_assume_pre) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P' and (\<lambda>_. P)\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma hoare_gen_asm_conj:
  "(P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P' s \<and> P\<rbrace> f \<lbrace>Q\<rbrace>
theory Trace_More_VCG

lemma valid_rv_lift:
  "\<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P'\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. P \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> P \<and> Q rv s\<rbrace>
theory Trace_More_VCG

lemma valid_imp_ex:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. rv \<longrightarrow> Q rv s x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>x. Q rv s x)\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>x. rv \<longrightarrow> Q rv s x\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (\<exists>x. Q rv s x)\<rbrace>
theory Trace_More_VCG

lemma valid_rv_split:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not>rv \<longrightarrow> Q' s\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> Q' s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. if rv then Q s else Q' s\<rbrace>
theory Trace_More_VCG

lemma hoare_rv_split:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> (Q rv s)\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. (\<not>rv) \<longrightarrow> (Q rv s)\<rbrace>\<rbrakk>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def split_def) by (metis (full_types) fst_eqD snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv \<longrightarrow> Q rv s\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<not> rv \<longrightarrow> Q rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>mres (f s). fst x \<longrightarrow> Q True (snd x)); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>mres (f s). \<not> fst x \<longrightarrow> Q False (snd x)); P s; (a, b) \<in> mres (f s)\<rbrakk> \<Longrightarrow> Q a b
theory Trace_More_VCG

lemma combine_validE:
  "\<lbrakk> \<lbrace> P \<rbrace> x \<lbrace> Q \<rbrace>,\<lbrace> E \<rbrace>; \<lbrace> P' \<rbrace> x \<lbrace> Q' \<rbrace>,\<lbrace> E' \<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace> P and P' \<rbrace> x \<lbrace> \<lambda>r. (Q r) and (Q' r) \<rbrace>,\<lbrace>\<lambda>r. (E r) and (E' r) \<rbrace>" apply (clarsimp simp: validE_def valid_def split: sum.splits) apply (erule allE, erule (1) impE)+ apply (drule (1) bspec)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<lbrace>P'\<rbrace> x \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> x \<lbrace>\<lambda>r. Q r and Q' r\<rbrace>, \<lbrace>\<lambda>r. E r and E' r\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P' s \<longrightarrow> (\<forall>x\<in>mres (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E' x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q' x2 s')); \<forall>s. P s \<longrightarrow> (\<forall>x\<in>mres (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s')); (a, b) \<in> mres (x s); P s; P' s\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b \<and> E' x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b \<and> Q' x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> mres (x s); P s; P' s; \<forall>x\<in>mres (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E' x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q' x2 s'); \<forall>x\<in>mres (x s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s')\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b \<and> E' x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b \<and> Q' x2 b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> mres (x s); P s; P' s; case (a, b) of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E' x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q' x2 s'); case (a, b) of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> E x1 s') \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> Q x2 s')\<rbrakk> \<Longrightarrow> (\<forall>x1. a = Inl x1 \<longrightarrow> E x1 b \<and> E' x1 b) \<and> (\<forall>x2. a = Inr x2 \<longrightarrow> Q x2 b \<and> Q' x2 b) proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma valid_case_prod:
  "\<lbrakk> \<And>x y. valid (P x y) (f x y) Q \<rbrakk> \<Longrightarrow> valid (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrace>P x y\<rbrace> f x y \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>case v of (x, xa) \<Rightarrow> P x xa\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>Q\<rbrace>
theory Trace_More_VCG

lemma validE_case_prod:
  "\<lbrakk> \<And>x y. validE (P x y) (f x y) Q E \<rbrakk> \<Longrightarrow> validE (case_prod P v) (case_prod (\<lambda>x y. f x y) v) Q E" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrace>P x y\<rbrace> f x y \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>case v of (x, xa) \<Rightarrow> P x xa\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_More_VCG

lemma valid_pre_satisfies_post:
  "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>" by (clarsimp simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s r' s'. P s \<Longrightarrow> Q r' s') \<Longrightarrow> \<lbrace>P\<rbrace> m \<lbrace>Q\<rbrace>
theory Trace_More_VCG

lemma validE_pre_satisfies_post:
  "\<lbrakk> \<And>s r' s'. P s \<Longrightarrow> Q r' s'; \<And>s r' s'. P s \<Longrightarrow> R r' s' \<rbrakk> \<Longrightarrow> \<lbrace> P \<rbrace> m \<lbrace> Q \<rbrace>,\<lbrace> R \<rbrace>" by (clarsimp simp: validE_def2 split: sum.splits)

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

lemma hoare_validE_R_conjI:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - ; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, - \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -" by (fastforce simp: Ball_def validE_R_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, -
theory Trace_More_VCG

lemma hoare_validE_E_conjI:
  "\<lbrakk> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace> ; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace> \<rbrakk>  \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" by (fastforce simp: Ball_def validE_E_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f -, \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>
theory Trace_More_VCG

lemma validE_R_post_conjD1:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" by (fastforce simp: validE_R_def validE_def valid_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. Q r s \<and> R r s\<rbrace>, - \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -
theory Trace_More_VCG

lemma throw_opt_wp[wp]:
  "\<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" unfolding throw_opt_def by wpsimp auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if v = None then E ex else Q (the v)\<rbrace> throw_opt ex v \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if v = None then E ex else Q (the v)\<rbrace> case v of None \<Rightarrow> throwError ex | Some v \<Rightarrow> returnOk v \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_More_VCG

lemma hoare_name_pre_state2:
  "(\<And>s. \<lbrace>P and ((=) s)\<rbrace> f \<lbrace>Q\<rbrace>) \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (auto simp: valid_def intro: hoare_name_pre_state)

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

lemma returnOk_E': "\<lbrace>P\<rbrace> returnOk r -,\<lbrace>E\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk r -, \<lbrace>E\<rbrace>
theory Trace_More_VCG

lemma throwError_R': "\<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>,-" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>, -
theory Trace_Monad_Equations

lemma assert_def2:
  "assert v = assert_opt (if v then Some () else None)" by (cases v; simp add: assert_def assert_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. assert v = assert_opt (if v then Some () else None)
theory Trace_Monad_Equations

lemma return_returnOk:
  "return (Inr x) = returnOk x" unfolding returnOk_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. return (Inr x) = returnOk x proof (prove)
goal (1 subgoal):
 1. return (Inr x) = (return \<circ> Inr) x
theory Trace_Monad_Equations

lemma exec_modify:
  "(modify f >>= g) s = g () (f s)" by (simp add: bind_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (modify f >>= g) s = g () (f s)
theory Trace_Monad_Equations

lemma bind_return_eq:
  "(a >>= return) = (b >>= return) \<Longrightarrow> a = b" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a >>= return = b >>= return \<Longrightarrow> a = b
theory Trace_Monad_Equations

lemma bindE_bind_linearise:
  "((f >>=E g) >>= h) =
   (f >>= case_sum (h o Inl) (\<lambda>rv. g rv >>= h))" apply (simp add: bindE_def bind_assoc) apply (rule ext, rule bind_apply_cong, rule refl) apply (simp add: lift_def throwError_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>=E g >>= h = f >>= case_sum (h \<circ> Inl) (\<lambda>rv. g rv >>= h) proof (prove)
goal (1 subgoal):
 1. do x <- f;
lift g x >>= h
od = f >>= case_sum (h \<circ> Inl) (\<lambda>rv. g rv >>= h) proof (prove)
goal (1 subgoal):
 1. \<And>x rv st. (rv, st) \<in> mres (f x) \<Longrightarrow> (lift g rv >>= h) st = (case rv of Inl x \<Rightarrow> (h \<circ> Inl) x | Inr rv \<Rightarrow> g rv >>= h) st proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma throwError_bind:
  "(throwError e >>= f) = (f (Inl e))" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. throwError e >>= f = f (Inl e)
theory Trace_Monad_Equations

lemma bind_bindE_assoc:
  "((f >>= g) >>=E h)
   = f >>= (\<lambda>rv. g rv >>=E h)" by (simp add: bindE_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>= g >>=E h = do rv <- f;
g rv >>=E h
od
theory Trace_Monad_Equations

lemma liftE_bind:
  "(liftE m >>= m') = (m >>= (\<lambda>rv. m' (Inr rv)))" by (simp add: liftE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE m >>= m' = do rv <- m;
m' (Inr rv)
od
theory Trace_Monad_Equations

lemma catch_throwError: "catch (throwError ft) g = g ft" by (simp add: catch_def throwError_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (throwError ft <catch> g) = g ft
theory Trace_Monad_Equations

lemma cart_singleton_image:
  "S \<times> {s} = (\<lambda>v. (v, s)) ` S" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<times> {s} = (\<lambda>v. (v, s)) ` S
theory Trace_Monad_Equations

lemma liftE_bindE_handle:
  "((liftE f >>=E (\<lambda>x. g x)) <handle> h)
   = f >>= (\<lambda>x. g x <handle> h)" by (simp add: liftE_bindE handleE_def handleE'_def
                bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE f >>=E g <handle> h) = do x <- f;
g x <handle> h
od
theory Trace_Monad_Equations

lemma catch_liftE_bindE:
  "catch (liftE g >>=E (\<lambda>x. f x)) h = g >>= (\<lambda>x. catch (f x) h)" by (simp add: liftE_bindE catch_def bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE g >>=E f <catch> h) = do x <- g;
f x <catch> h
od
theory Trace_Monad_Equations

lemma returnOk_catch_bind:
  "catch (returnOk v) h >>= g = g v" by (simp add: returnOk_liftE catch_liftE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (returnOk v <catch> h) >>= g = g v
theory Trace_Monad_Equations

lemma liftE_bindE_assoc:
  "(liftE f >>=E g) >>= h = f >>= (\<lambda>x. g x >>= h)" by (simp add: liftE_bindE bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. liftE f >>=E g >>= h = do x <- f;
g x >>= h
od
theory Trace_Monad_Equations

lemma unlessE_throw_catch_If:
  "catch (unlessE P (throwError e) >>=E f) g
   = (if P then catch (f ()) g else g e)" by (simp add: unlessE_def catch_throwError split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (unlessE P (throwError e) >>=E f <catch> g) = (if P then f () <catch> g else g e)
theory Trace_Monad_Equations

lemma whenE_bindE_throwError_to_if:
  "whenE P (throwError e) >>=E (\<lambda>_. b) = (if P then (throwError e) else b)" unfolding whenE_def bindE_def by (auto simp: lift_def throwError_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doE _ <- whenE P (throwError e);
b
odE = (if P then throwError e else b) proof (prove)
goal (1 subgoal):
 1. (if P then throwError e else returnOk ()) >>= lift (\<lambda>_. b) = (if P then throwError e else b)
theory Trace_Monad_Equations

lemma alternative_liftE_returnOk:
  "(liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)" by (simp add: liftE_def alternative_def returnOk_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (liftE m \<sqinter> returnOk v) = liftE (m \<sqinter> return v)
theory Trace_Monad_Equations

lemma gets_the_return:
  "(return x = gets_the f) = (\<forall>s. f s = Some x)" apply (subst fun_eq_iff) apply (simp add: return_def gets_the_def exec_gets
                   assert_opt_def fail_def
            split: option.split) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (return x = gets_the f) = (\<forall>s. f s = Some x) proof (prove)
goal (1 subgoal):
 1. (\<forall>xa. return x xa = gets_the f xa) = (\<forall>s. f s = Some x) proof (prove)
goal (1 subgoal):
 1. (\<forall>xa. (\<exists>y. f xa = Some y) \<and> (\<forall>x2. f xa = Some x2 \<longrightarrow> x = x2)) = (\<forall>s. f s = Some x) proof (prove)
goal:
No subgoals!
theory Trace_Monad_Equations

lemma gets_the_returns:
  "(return x = gets_the f) = (\<forall>s. f s = Some x)"
  "(returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x))"
  "(throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))" by (simp_all add: returnOk_def throwError_def
                    gets_the_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (return x = gets_the f) = (\<forall>s. f s = Some x) &&& (returnOk x = gets_the g) = (\<forall>s. g s = Some (Inr x)) &&& (throwError x = gets_the h) = (\<forall>s. h s = Some (Inl x))