kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_No_Fail

lemma no_fail_undefined[simp, wp]:
  "no_fail \<bottom> undefined" by (simp add: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) undefined
theory Trace_No_Fail

lemma no_fail_assume_pre:
  "(\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f" by (simp add: no_fail_def)

\<^cancel>\<open>lemma no_fail_liftM_eq[simp]:
  "no_fail P (liftM f m) = no_fail P m"
  by (auto simp: liftM_def no_fail_def bind_def return_def)\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail P f
theory Trace_No_Fail

lemma no_fail_liftM[wp]:
  "no_fail P m \<Longrightarrow> no_fail P (liftM f m)" unfolding liftM_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P m \<Longrightarrow> no_fail P (liftM f m) proof (prove)
goal (1 subgoal):
 1. no_fail P m \<Longrightarrow> no_fail P (do x <- m;
return (f x)
od)
theory Trace_No_Fail

lemma no_fail_pre_and:
  "no_fail P f \<Longrightarrow> no_fail (P and Q) f" by (erule no_fail_pre) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail (P and Q) f
theory Trace_No_Fail

lemma no_fail_spec:
  "\<lbrakk> \<And>s. no_fail (((=) s) and P) f \<rbrakk> \<Longrightarrow> no_fail P f" by (simp add: no_fail_def)

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

lemma no_fail_assertE[wp]:
  "no_fail (\<lambda>_. P) (assertE P)" by (simp add: assertE_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. P) (assertE P)
theory Trace_No_Fail

lemma no_fail_spec_pre:
  "\<lbrakk> no_fail (((=) s) and P') f; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> no_fail (((=) s) and P) f" by (erule no_fail_pre, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail ((=) s and P') f; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> no_fail ((=) s and P) f
theory Trace_No_Fail

lemma no_fail_unlessE[wp]:
  "\<lbrakk> \<not> G \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)" by (simp add: unlessE_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. \<not> G \<longrightarrow> P s) (unlessE G f)
theory Trace_No_Fail

lemma no_fail_throwError[wp]:
  "no_fail \<top> (throwError e)" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (throwError e)
theory Trace_No_Fail

lemma no_fail_liftE[wp]:
  "no_fail P f \<Longrightarrow> no_fail P (liftE f)" unfolding liftE_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail P (liftE f) proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail P (do r <- f;
return (Inr r)
od)
theory Trace_No_Fail

lemma no_fail_gets_the[wp]:
  "no_fail (\<lambda>s. f s \<noteq> None) (gets_the f)" unfolding gets_the_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s \<noteq> None) (gets_the f) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s \<noteq> None) (gets f >>= assert_opt)
theory Trace_No_Fail

lemma no_fail_lift:
  "(\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not>isl x \<longrightarrow> P s) (lift f x)" unfolding lift_def by (wpsimp wp: no_fail_throwError split: sum.splits | assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not> isl x \<longrightarrow> P s) (lift f x) proof (prove)
goal (1 subgoal):
 1. (\<And>y. x = Inr y \<Longrightarrow> no_fail P (f y)) \<Longrightarrow> no_fail (\<lambda>s. \<not> isl x \<longrightarrow> P s) (case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> f v')
theory Trace_No_Fail

lemma validE_R_valid_eq:
  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace>" unfolding validE_R_def validE_def valid_def by (fastforce split: sum.splits prod.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - = \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv s. \<not> isl rv \<longrightarrow> R (projr rv) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>s. Q s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). case r of Inl e \<Rightarrow> True | Inr r \<Rightarrow> R r s')) = (\<forall>s. Q s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). \<not> isl r \<longrightarrow> R (projr r) s'))
theory Trace_No_Fail

lemma no_fail_bindE[wp]:
  "\<lbrakk> no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<rbrakk>
     \<Longrightarrow> no_fail (P and Q) (f >>=E g)" unfolding bindE_def by (wpsimp wp: no_fail_lift simp: validE_R_valid_eq | assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>=E g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; \<And>rv. no_fail (R rv) (g rv); \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, -\<rbrakk> \<Longrightarrow> no_fail (P and Q) (f >>= lift g)
theory Trace_No_Fail

lemma no_fail_False[simp]:
  "no_fail (\<lambda>_. False) X" by (clarsimp simp: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. False) X
theory Trace_No_Fail

lemma no_fail_gets_map[wp]:
  "no_fail (\<lambda>s. f s p \<noteq> None) (gets_map f p)" unfolding gets_map_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s p \<noteq> None) (gets_map f p) proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>s. f s p \<noteq> None) (do m <- gets f;
assert_opt (m p)
od)
theory Trace_No_Fail

lemma no_fail_or:
  "\<lbrakk>no_fail P a; no_fail Q a\<rbrakk> \<Longrightarrow> no_fail (P or Q) a" by (clarsimp simp: no_fail_def)

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

lemma no_fail_state_assert[wp]:
  "no_fail P (state_assert P)" unfolding state_assert_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P (state_assert P) proof (prove)
goal (1 subgoal):
 1. no_fail P (do s <- get;
assert (P s)
od)
theory Trace_No_Fail

lemma no_fail_condition[wp]:
  "\<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) (condition C A B)" unfolding condition_def no_fail_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail Q A; no_fail R B\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s)) condition C
  A
  B proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. Q s \<longrightarrow> \<not> failed (A s); \<forall>s. R s \<longrightarrow> \<not> failed (B s)\<rbrakk> \<Longrightarrow> \<forall>s. (C s \<longrightarrow> Q s) \<and> (\<not> C s \<longrightarrow> R s) \<longrightarrow> \<not> failed (if C s then A s else B s)
theory Trace_No_Fail

lemma no_fail_ex_lift:
  "(\<And>x. no_fail (P x) f) \<Longrightarrow> no_fail (\<lambda>s. \<exists>x. P x s) f" by (fastforce simp: no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_fail (P x) f) \<Longrightarrow> no_fail (\<lambda>s. \<exists>x. P x s) f
theory Trace_No_Fail

lemma no_fail_grab_asm:
  "(G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f" by (cases G; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (G \<Longrightarrow> no_fail P f) \<Longrightarrow> no_fail (\<lambda>s. G \<and> P s) f
theory Trace_No_Fail

lemma no_fail_put_trace_elem[wp]:
  "no_fail \<top> (put_trace_elem x)" by (clarsimp simp: put_trace_elem_def no_fail_def failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (put_trace_elem x)
theory Trace_No_Fail

lemma no_fail_put_trace[wp]:
  "no_fail \<top> (put_trace xs)" by (induct xs; wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) (put_trace xs)
theory Trace_No_Fail

lemma no_fail_interference[wp]:
  "no_fail \<top> interference" by (wpsimp simp: interference_def commit_step_def env_steps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (\<lambda>_. True) interference
theory Trace_No_Fail

lemma no_fail_Await[wp]:
  "\<exists>s. c s \<Longrightarrow> no_fail \<top> (Await c)" by (wpsimp simp: Await_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>s. c s \<Longrightarrow> no_fail (\<lambda>_. True) (Await c)
theory Trace_No_Fail

lemma parallel_failed:
  "failed (parallel f g s) \<Longrightarrow> failed (f s) \<and> failed (g s)" by (auto simp: parallel_def2 failed_def image_def intro!: bexI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. failed (parallel f g s) \<Longrightarrow> failed (f s) \<and> failed (g s)
theory Trace_No_Fail

lemma no_fail_parallel[wp]:
  "\<lbrakk> no_fail P f \<or> no_fail Q g \<rbrakk> \<Longrightarrow> no_fail (P and Q) (parallel f g)" by (auto simp: no_fail_def dest!: parallel_failed)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<or> no_fail Q g \<Longrightarrow> no_fail (P and Q) (parallel f g)
theory Trace_More_VCG

lemma hoare_take_disjunct:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> (False \<or> P'' rv s)\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>P''\<rbrace>" by (erule hoare_strengthen_post, simp)

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

lemma hoare_post_add:
  "\<lbrace>P\<rbrace> S \<lbrace>\<lambda>r s. R r s \<and> Q r s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> S \<lbrace>Q\<rbrace>" by (erule hoare_strengthen_post, simp)

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

lemma hoare_post_addE:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. R s \<and> Q s\<rbrace>, \<lbrace>T\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. Q s\<rbrace>, \<lbrace>T\<rbrace>" by (erule hoare_post_impErr; simp)

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

lemma hoare_pre_add:
  "(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>)" apply (subst iff_conv_conj_imp) by(intro conjI impI; rule hoare_weaken_pre, assumption, clarsimp)

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

lemma hoare_pre_addE:
  "(\<forall>s. P s \<longrightarrow> R s) \<Longrightarrow> (\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace> \<longleftrightarrow> \<lbrace>P and R\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>S\<rbrace>)" apply (subst iff_conv_conj_imp) by(intro conjI impI; rule hoare_weaken_preE, assumption, clarsimp)

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

lemma hoare_name_pre_state:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (clarsimp simp: valid_def)

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

lemma hoare_name_pre_stateE:
  "\<lbrakk>\<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by (clarsimp simp: validE_def2)

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

lemma hoare_vcg_imp_lift_pre_add:
  "\<lbrakk> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. R rv s\<rbrace>; f \<lbrace>\<lambda>s. \<not> Q s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace>" apply (rule hoare_weaken_pre) apply (rule hoare_vcg_imp_lift') apply fastforce apply fastforce apply (clarsimp simp: pred_conj_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> f \<lbrace>\<lambda>rv s. Q s \<longrightarrow> R rv s\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P'3\<rbrace> f \<lbrace>\<lambda>rv s. \<not> Q s\<rbrace>
 2. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> f \<lbrace>R\<rbrace>
 3. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<not> ?P'3 s \<longrightarrow> ?Q'3 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q'3\<rbrace> f \<lbrace>R\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<not> \<not> Q s \<longrightarrow> ?Q'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>P and Q\<rbrace> f \<lbrace>R\<rbrace>; \<lbrace>\<lambda>s. \<not> Q s\<rbrace> f \<lbrace>\<lambda>_ s. \<not> Q s\<rbrace>; P s\<rbrakk> \<Longrightarrow> \<not> \<not> Q s \<longrightarrow> (P and Q) s proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma hoare_lift_Pf_pre_conj:
  assumes P: "\<And>x. \<lbrace>\<lambda>s. Q x s\<rbrace> m \<lbrace>P x\<rbrace>"
  assumes f: "\<And>P. \<lbrace>\<lambda>s. P (g s) \<and> R s\<rbrace> m \<lbrace>\<lambda>_ s. P (f s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. Q (g s) s \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. P (f s) rv s\<rbrace>" apply (clarsimp simp: valid_def) apply (rule use_valid [OF _ P], simp) apply (rule use_valid [OF _ f], simp, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Q (g s) s \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. P (f s) rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> mres (m s); Q (g s) s; R s\<rbrakk> \<Longrightarrow> P (f b) a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>(a, b) \<in> mres (m s); Q (g s) s; R s\<rbrakk> \<Longrightarrow> Q (f b) s proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma hoare_if_r_and:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace>
   = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not>R r \<longrightarrow> Q' r s)\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. if R r then Q r else Q' r\<rbrace> = \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r s. (R r \<longrightarrow> Q r s) \<and> (\<not> R r \<longrightarrow> Q' r s)\<rbrace>
theory Trace_More_VCG

lemma hoare_vcg_ex_lift_R:
  "\<lbrakk> \<And>v. \<lbrace>P v\<rbrace> f \<lbrace>Q v\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>v. P v s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>v. Q v rv s\<rbrace>,-" apply (simp add: validE_R_def validE_def) apply (rule hoare_strengthen_post, erule hoare_vcg_ex_lift) apply (auto split: sum.split) done

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

lemma hoare_case_option_wpR:
  "\<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>,-; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>,-\<rbrakk>
   \<Longrightarrow> \<lbrace>case_option P P' v\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>,-" by (cases v) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f None \<lbrace>Q\<rbrace>, -; \<And>x. \<lbrace>P' x\<rbrace> f (Some x) \<lbrace>Q' x\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>case v of None \<Rightarrow> P | Some x \<Rightarrow> P' x\<rbrace> f v \<lbrace>\<lambda>rv. case v of None \<Rightarrow> Q rv | Some x \<Rightarrow> Q' x rv\<rbrace>, -
theory Trace_More_VCG

lemma hoare_vcg_conj_liftE_R:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>P'\<rbrace>,-; \<lbrace>Q\<rbrace> f \<lbrace>Q'\<rbrace>,- \<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. P' rv s \<and> Q' rv s\<rbrace>, -" apply (simp add: validE_R_def validE_def valid_def split: sum.splits) apply blast done

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

lemma K_valid[wp]:
  "\<lbrace>K P\<rbrace> f \<lbrace>\<lambda>_. K P\<rbrace>" by (simp add: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K P\<rbrace> f \<lbrace>\<lambda>_. K P\<rbrace>
theory Trace_More_VCG

lemma hoare_ex_all:
  "(\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>" apply (rule iffI) apply (fastforce simp: valid_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace>) = \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<lbrace>\<lambda>s. \<exists>x. P x s\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<forall>x. \<lbrace>P x\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma hoare_imp_eq_substR:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. rv = x \<longrightarrow> Q x s\<rbrace>,-" by (fastforce simp add: valid_def validE_R_def validE_def split: sum.splits)

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

lemma hoare_split_bind_case_sum:
  assumes x: "\<And>rv. \<lbrace>R rv\<rbrace> g rv \<lbrace>Q\<rbrace>"
             "\<And>rv. \<lbrace>S rv\<rbrace> h rv \<lbrace>Q\<rbrace>"
  assumes y: "\<lbrace>P\<rbrace> f \<lbrace>S\<rbrace>,\<lbrace>R\<rbrace>"
  shows      "\<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace>" apply (rule hoare_seq_ext[OF _ y[unfolded validE_def]]) apply (wpsimp wp: x split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f >>= case_sum g h \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. case x of Inl e \<Rightarrow> R e s | Inr r \<Rightarrow> S r s\<rbrace> case x of Inl x \<Rightarrow> g x | Inr x \<Rightarrow> h x \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!