kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_In_Monad

lemma in_assertE:
  "(r, s') \<in> mres (assertE P s) = (P \<and> r = Inr () \<and> s' = s)" by (simp add: assertE_def returnOk_def return_def fail_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (assertE P s)) = (P \<and> r = Inr () \<and> s' = s)
theory Trace_In_Monad

lemma in_assert_opt:
  "(r, s') \<in> mres (assert_opt v s) = (v = Some r \<and> s' = s)" by (auto simp: assert_opt_def in_fail in_return split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (assert_opt v s)) = (v = Some r \<and> s' = s)
theory Trace_In_Monad

lemma in_get:
  "(r, s') \<in> mres (get s) = (r = s \<and> s' = s)" by (simp add: get_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (get s)) = (r = s \<and> s' = s)
theory Trace_In_Monad

lemma in_gets:
  "(r, s') \<in> mres (gets f s) = (r = f s \<and> s' = s)" by (simp add: simpler_gets_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (gets f s)) = (r = f s \<and> s' = s)
theory Trace_In_Monad

lemma in_put:
  "(r, s') \<in> mres (put x s) = (s' = x \<and> r = ())" by (simp add: put_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (put x s)) = (s' = x \<and> r = ())
theory Trace_In_Monad

lemma in_when:
  "(v, s') \<in> mres (when P f s) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not>P \<longrightarrow> v = () \<and> s' = s))" by (simp add: when_def in_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (when P f s)) = ((P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (\<not> P \<longrightarrow> v = () \<and> s' = s))
theory Trace_In_Monad

lemma in_unless:
  "(v, s') \<in> mres (unless P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))" by (simp add: unless_def in_when)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (unless P f s)) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))
theory Trace_In_Monad

lemma in_unlessE:
  "(v, s') \<in> mres (unlessE P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))" by (simp add: unlessE_def in_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (unlessE P f s)) = ((\<not> P \<longrightarrow> (v, s') \<in> mres (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))
theory Trace_In_Monad

lemma inl_unlessE:
  "((Inl x, s') \<in> mres (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> mres (f s))" by (auto simp add: in_unlessE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inl x, s') \<in> mres (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> mres (f s))
theory Trace_In_Monad

lemma in_modify:
  "(v, s') \<in> mres (modify f s) = (s'=f s \<and> v = ())" by (auto simp add: modify_def bind_def get_def put_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> mres (modify f s)) = (s' = f s \<and> v = ())
theory Trace_In_Monad

lemma in_alternative:
  "(r,s') \<in> mres ((f \<sqinter> g) s) = ((r,s') \<in> mres (f s) \<or> (r,s') \<in> mres (g s))" by (auto simp add: alternative_def mres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres ((f \<sqinter> g) s)) = ((r, s') \<in> mres (f s) \<or> (r, s') \<in> mres (g s))
theory Trace_In_Monad

lemma in_liftM:
  "((r, s') \<in> mres (liftM t f s)) = (\<exists>r'. (r', s') \<in> mres (f s) \<and> r = t r')" by (simp add: liftM_def in_return in_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> mres (liftM t f s)) = (\<exists>r'. (r', s') \<in> mres (f s) \<and> r = t r')
theory Trace_In_Monad

lemma in_bindE:
  "(rv, s') \<in> mres ((f >>=E (\<lambda>rv'. g rv')) s) =
   ((\<exists>ex. rv = Inl ex \<and> (Inl ex, s') \<in> mres (f s)) \<or>
    (\<exists>rv' s''. (rv, s') \<in> mres (g rv' s'') \<and> (Inr rv', s'') \<in> mres (f s)))" apply (clarsimp simp: bindE_def in_bind lift_def in_throwError) apply (safe del: disjCI; strengthen subst[where P="\<lambda>x. x \<in> mres (f s)", mk_strg I _ E];
         auto simp: in_throwError split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> mres ((f >>=E g) s)) = ((\<exists>ex. rv = Inl ex \<and> (Inl ex, s') \<in> mres (f s)) \<or> (\<exists>rv' s''. (rv, s') \<in> mres (g rv' s'') \<and> (Inr rv', s'') \<in> mres (f s))) proof (prove)
goal (1 subgoal):
 1. (\<exists>s'' x. (x, s'') \<in> mres (f s) \<and> (rv, s') \<in> mres ((case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> g v') s'')) = ((\<exists>ex. rv = Inl ex \<and> (Inl ex, s') \<in> mres (f s)) \<or> (\<exists>rv' s''. (rv, s') \<in> mres (g rv' s'') \<and> (Inr rv', s'') \<in> mres (f s))) proof (prove)
goal:
No subgoals!
theory Trace_In_Monad

lemma bind_det_exec:
  "mres (a s) = {(r,s')} \<Longrightarrow> mres ((a >>= b) s) = mres (b r s')" by (simp add: in_bind set_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres (a s) = {(r, s')} \<Longrightarrow> mres ((a >>= b) s) = mres (b r s')
theory Trace_In_Monad

lemma in_bind_det_exec:
  "mres (a s) = {(r,s')} \<Longrightarrow> (s'' \<in> mres ((a >>= b) s)) = (s'' \<in> mres (b r s'))" by (cases s'', simp add: in_bind)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres (a s) = {(r, s')} \<Longrightarrow> (s'' \<in> mres ((a >>= b) s)) = (s'' \<in> mres (b r s'))
theory Trace_In_Monad

lemma exec_put:
  "(put s' >>= m) s = m () s'" by (simp add: bind_def put_def mres_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (put s' >>= m) s = m () s'
theory Trace_VCG

lemma valid_make_schematic_post:
  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>) \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>" by (auto simp add: valid_def split: prod.splits)

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

lemma validE_make_schematic_post:
  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>) \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
        \<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>" by (auto simp add: validE_def valid_def split: prod.splits sum.splits)

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

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

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

lemma hoare_vcg_precond_impE_R: (* FIXME lib: rename to hoare_weaken_preE_R *)
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,-; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" unfolding validE_R_def by (rule hoare_vcg_precond_impE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>x y. True\<rbrace>; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>x y. True\<rbrace>
theory Trace_VCG

lemma hoare_weaken_preE_E:
  "\<lbrakk> \<lbrace>P'\<rbrace> f -,\<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>" by (fastforce simp add: validE_E_def validE_def valid_def)

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

lemma wpc_helper_valid:
  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>
theory Trace_VCG

lemma wpc_helper_validE:
  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>
theory Trace_VCG

lemma wpc_helper_validE_R:
  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -
theory Trace_VCG

lemma wpc_helper_validR_R:
  "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f -, \<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>
theory Trace_VCG

lemma bind_wp[wp_split]:
  "\<lbrakk> \<And>r. \<lbrace>Q' r\<rbrace> g r \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= (\<lambda>rv. g rv) \<lbrace>Q\<rbrace>" by (fastforce simp: valid_def bind_def' mres_def intro: image_eqI[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace> g r \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>
theory Trace_VCG

lemma seq':
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<forall>x s. B x s \<longrightarrow> P x \<and> C s \<rbrakk> \<Longrightarrow>
   \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" apply (erule bind_wp[rotated]) apply (clarsimp simp: valid_def) apply (fastforce elim: rev_bexI image_eqI[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<forall>x s. B x s \<longrightarrow> P x \<and> C s\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r. \<lbrakk>\<forall>x. P x \<longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<forall>x s. B x s \<longrightarrow> P x \<and> C s\<rbrakk> \<Longrightarrow> \<lbrace>B r\<rbrace> g r \<lbrace>D\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r s a b. \<lbrakk>\<forall>x. P x \<longrightarrow> (\<forall>s. C s \<longrightarrow> (\<forall>x\<in>mres (g x s). case x of (x, xa) \<Rightarrow> D x xa)); \<forall>x s. B x s \<longrightarrow> P x \<and> C s; B r s; (a, b) \<in> mres (g r s)\<rbrakk> \<Longrightarrow> D a b proof (prove)
goal:
No subgoals!
theory Trace_VCG

lemma seq:
  assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>"
  assumes g_valid: "\<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>"
  assumes bind:  "\<And>x s. B x s \<Longrightarrow> P x \<and> C s"
  shows "\<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" apply (insert f_valid g_valid bind) apply (blast intro: seq') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<And>x s. B x s \<Longrightarrow> P x \<and> C s\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_VCG

lemma seq_ext':
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" by (metis bind_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>
theory Trace_VCG

lemma seq_ext:
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>C\<rbrace>" by (rule bind_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>
theory Trace_VCG

lemma seqE':
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>A\<rbrace> doE x \<leftarrow> f; g x odE \<lbrace>C\<rbrace>,\<lbrace>E\<rbrace>" apply (simp add: bindE_def validE_def) apply (erule seq_ext') apply (auto simp: lift_def valid_def throwError_def return_def mres_def
             split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> B r s\<rbrace>; \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> C r s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= lift g \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> C r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>x. \<lbrace>B x\<rbrace> g x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> C r s\<rbrace> \<Longrightarrow> \<forall>x. \<lbrace>\<lambda>s. case x of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> B r s\<rbrace> lift g x \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> C r s\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_VCG

lemma seqE:
  assumes f_valid: "\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>,\<lbrace>E\<rbrace>"
  assumes g_valid: "\<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>" apply (insert f_valid g_valid) apply (blast intro: seqE') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>, \<lbrace>E\<rbrace>; \<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>=E g \<lbrace>C\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_VCG

lemma hoare_TrueI:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. \<top>\<rbrace>" by (simp add: valid_def)

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

lemma hoareE_TrueI:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. \<top>\<rbrace>, \<lbrace>\<lambda>r. \<top>\<rbrace>" by (simp add: validE_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r _. True\<rbrace>
theory Trace_VCG

lemma hoare_True_E_R[simp]:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_ s. True\<rbrace>, -" by (auto 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>_ s. True\<rbrace>, -
theory Trace_VCG

lemma hoare_post_conj[intro]:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>" by (fastforce simp: valid_def)

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

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

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

lemma hoare_conj:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P and P'\<rbrace> f \<lbrace>Q and Q'\<rbrace>" unfolding valid_def by auto

(* 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 and P'\<rbrace> f \<lbrace>Q and Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q r s'); \<forall>s. P' s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). Q' r s')\<rbrakk> \<Longrightarrow> \<forall>s. (P and P') s \<longrightarrow> (\<forall>(r, s')\<in>mres (f s). (Q and Q') r s')
theory Trace_VCG

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

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

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 mres_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 Trace_VCG

lemma hoare_modifyE_var:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> Q (f s) \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> modify f \<lbrace>\<lambda>_ s. Q s\<rbrace>" by(simp add: valid_def modify_def put_def get_def bind_def mres_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>_. Q\<rbrace>
theory Trace_VCG

lemma hoare_if:
  "\<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 Trace_VCG

lemma hoare_post_subst:
  "\<lbrakk> B = C; \<lbrace>A\<rbrace> a \<lbrace>B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> a \<lbrace>C\<rbrace>" by (erule subst)

(* 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 Trace_VCG

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

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

lemma hoare_post_impErr': (* FIXME lib: eliminate *)
  "\<lbrakk> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<forall>rv s. Q rv s \<longrightarrow> R rv s; \<forall>e s. E e s \<longrightarrow> F e s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>" unfolding validE_def valid_def by (fastforce split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<forall>rv s. Q rv s \<longrightarrow> R rv s; \<forall>e s. E e s \<longrightarrow> F e s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>, \<lbrace>F\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (a s). case r of Inl e \<Rightarrow> E e s' | Inr r \<Rightarrow> Q r s'); \<forall>rv s. Q rv s \<longrightarrow> R rv s; \<forall>e s. E e s \<longrightarrow> F e s\<rbrakk> \<Longrightarrow> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>mres (a s). case r of Inl e \<Rightarrow> F e s' | Inr r \<Rightarrow> R r s')
theory Trace_VCG

lemma hoare_post_impErr:
  "\<lbrakk> \<lbrace>P\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<And>rv s. Q rv s \<Longrightarrow> R rv s; \<And>e s. E e s \<Longrightarrow> F e s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>,\<lbrace>F\<rbrace>" by (blast intro: hoare_post_impErr')

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