kings-crown/FVELER_Isabelle huggingface dataset:
theory Trace_More_VCG

lemma valid_return_unit:
  "\<lbrace>P\<rbrace> f >>= (\<lambda>_. return ()) \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>" by (auto simp: valid_def in_bind in_return Ball_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do _ <- f;
return ()
od \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>
theory Trace_More_VCG

lemma hoare_weak_lift_imp_conj:
  "\<lbrakk> \<lbrace>Q\<rbrace> m \<lbrace>Q'\<rbrace>; \<lbrace>R\<rbrace> m \<lbrace>R'\<rbrace> \<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. (P \<longrightarrow> Q s) \<and> R s\<rbrace> m \<lbrace>\<lambda>rv s. (P \<longrightarrow> Q' rv s) \<and> R' rv s\<rbrace>" apply (rule hoare_vcg_conj_lift) apply (rule hoare_weak_lift_imp) apply assumption+ done

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

lemma hoare_eq_P:
  assumes "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>" by (rule assms)

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

lemma hoare_validE_R_conj:
  "\<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 (simp add: valid_def validE_def validE_R_def Let_def split_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>R\<rbrace>, -\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q and R\<rbrace>, -
theory Trace_More_VCG

lemma P_bool_lift:
  assumes t: "\<lbrace>Q\<rbrace> f \<lbrace>\<lambda>r. Q\<rbrace>"
  assumes f: "\<lbrace>\<lambda>s. \<not>Q s\<rbrace> f \<lbrace>\<lambda>r s. \<not>Q s\<rbrace>"
  shows "\<lbrace>\<lambda>s. P (Q s)\<rbrace> f \<lbrace>\<lambda>r s. P (Q s)\<rbrace>" apply (clarsimp simp: valid_def) apply (rule back_subst[where P=P], assumption) apply (rule iffI) apply (erule (1) use_valid [OF _ t]) apply (rule classical) apply (drule (1) use_valid [OF _ f]) apply simp done

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

lemma gets_sp: "\<lbrace>P\<rbrace> gets f \<lbrace>\<lambda>rv. P and (\<lambda>s. f s = rv)\<rbrace>" by (wp, simp)

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

lemma post_by_hoare2:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; (r, s') \<in> mres (f s); P s \<rbrakk> \<Longrightarrow> Q r s'" by (rule post_by_hoare, assumption+)

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

lemma hoare_Ball_helper:
  assumes x: "\<And>x. \<lbrace>P x\<rbrace> f \<lbrace>Q x\<rbrace>"
  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>rv s. P (S s)\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<forall>x \<in> S s. P x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> S s. Q x rv s\<rbrace>" apply (clarsimp simp: valid_def) apply (drule bspec, erule back_subst[where P="\<lambda>A. x\<in>A" for x]) apply (erule post_by_hoare[OF y, rotated]) apply (rule refl) apply (erule (1) post_by_hoare[OF x]) done

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

lemma handy_prop_divs:
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (Q s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s)\<rbrace>"
             "\<And>P. \<lbrace>\<lambda>s. P (R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (R' rv s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (Q s \<and> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<and> R' rv s)\<rbrace>"
             "\<lbrace>\<lambda>s. P (Q s \<or> R s) \<and> S s\<rbrace> f \<lbrace>\<lambda>rv s. P (Q' rv s \<or> R' rv s)\<rbrace>" apply (clarsimp simp: valid_def
                  elim!: subst[rotated, where P=P]) apply (rule use_valid [OF _ x(1)], assumption) apply (rule use_valid [OF _ x(2)], assumption) apply simp apply (clarsimp simp: valid_def
                 elim!: subst[rotated, where P=P]) apply (rule use_valid [OF _ x(1)], assumption) apply (rule use_valid [OF _ x(2)], assumption) apply simp done

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

lemma hoare_set_preserved:
  assumes x: "\<And>x. \<lbrace>fn' x\<rbrace> m \<lbrace>\<lambda>rv. fn x\<rbrace>"
  shows      "\<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace>" apply (induct xs) apply simp apply wp apply simp apply (rule hoare_vcg_conj_lift) apply (rule x) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. set [] \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set [] \<subseteq> {x. fn x s}\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set (a # xs) \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set (a # xs) \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. True\<rbrace> m \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set (a # xs) \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set (a # xs) \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set (a # xs) \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set (a # xs) \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. fn' a s \<and> set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. fn a s \<and> set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>fn' a\<rbrace> m \<lbrace>\<lambda>rv. fn a\<rbrace>
 2. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. set xs \<subseteq> {x. fn' x s}\<rbrace> m \<lbrace>\<lambda>rv s. set xs \<subseteq> {x. fn x s}\<rbrace> proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma hoare_conj_lift_inv:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>s. P' s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv. I\<rbrace>;
    \<And>s. P s \<Longrightarrow> P' s\<rbrakk>
   \<Longrightarrow> \<lbrace>\<lambda>s. P s \<and> I s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> I s\<rbrace>" by (fastforce simp: valid_def)

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

lemma hoare_in_monad_post:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>"
  shows      "\<lbrace>\<top>\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> mres (f s)\<rbrace>" apply (clarsimp simp: valid_def) apply (rule back_subst[where P="\<lambda>s. x\<in>mres (f s)" for x], assumption) apply (simp add: state_unchanged[OF x]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> f \<lbrace>\<lambda>rv s. (rv, s) \<in> mres (f s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> mres (f s) \<Longrightarrow> (a, b) \<in> mres (f b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. (a, b) \<in> mres (f s) \<Longrightarrow> s = b proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma list_case_throw_validE_R:
  "\<lbrakk> \<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>,- \<rbrakk> \<Longrightarrow>
   \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>,-" apply (cases xs, simp_all) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>y ys. xs = y # ys \<Longrightarrow> \<lbrace>P\<rbrace> f y ys \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> case xs of [] \<Rightarrow> throwError e | x # xs \<Rightarrow> f x xs \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. xs = [] \<Longrightarrow> \<lbrace>P\<rbrace> throwError e \<lbrace>Q\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma validE_R_sp:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
  assumes y: "\<And>x. \<lbrace>Q x\<rbrace> g x \<lbrace>R\<rbrace>,-"
  shows "\<lbrace>P\<rbrace> f >>=E (\<lambda>x. g x) \<lbrace>R\<rbrace>,-" by (rule hoare_pre, wp x y, simp)

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

lemma valid_set_take_helper:
  "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (xs rv s). Q x rv s\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x \<in> set (take (n rv s) (xs rv s)). Q x rv s\<rbrace>" apply (erule hoare_strengthen_post) apply (clarsimp dest!: in_set_takeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>set (xs rv s). Q x rv s\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x\<in>set (take (n rv s) (xs rv s)). Q x rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>x\<in>set (xs rv s). Q x rv s \<Longrightarrow> \<forall>x\<in>set (take (n rv s) (xs rv s)). Q x rv s proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma whenE_throwError_sp:
  "\<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, -" apply (simp add: whenE_def validE_R_def) apply (intro conjI impI; wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> whenE Q (throwError e) \<lbrace>\<lambda>rv s. \<not> Q \<and> P s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. (Q \<longrightarrow> \<lbrace>P\<rbrace> throwError e \<lbrace>\<lambda>rv s. False\<rbrace>, \<lbrace>\<lambda>x y. True\<rbrace>) \<and> (\<not> Q \<longrightarrow> \<lbrace>P\<rbrace> returnOk () \<lbrace>\<lambda>rv. P\<rbrace>, \<lbrace>\<lambda>x y. True\<rbrace>) proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma weaker_hoare_ifE:
  assumes x: "\<lbrace>P \<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  assumes y: "\<lbrace>P'\<rbrace> b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
  shows      "\<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (rule hoare_vcg_precond_impE) apply (wp x y) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P and P'\<rbrace> if test then a else b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if test then a else b \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>s. (P and P') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (P and P') s \<Longrightarrow> (test \<longrightarrow> P s) \<and> (\<not> test \<longrightarrow> P' s) proof (prove)
goal:
No subgoals!
theory Trace_More_VCG

lemma wp_split_const_if_R:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-"
  assumes y: "\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,-"
  shows "\<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> f \<lbrace>\<lambda>rv s. (G \<longrightarrow> Q rv s) \<and> (\<not> G \<longrightarrow> Q' rv s)\<rbrace>,-" by (cases G, simp_all add: x y)

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

lemma hoare_grab_asm:
  "\<lbrakk> G \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. G \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>" by (cases G, simp+)

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

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

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

lemma hoare_grab_exs:
  assumes x: "\<And>x. P x \<Longrightarrow> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>"
  shows      "\<lbrace>\<lambda>s. \<exists>x. P x \<and> P' s\<rbrace> f \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def) apply (erule(2) use_valid [OF _ x]) done

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

lemma hoare_prop_E: "\<lbrace>\<lambda>rv. P\<rbrace> f -,\<lbrace>\<lambda>rv s. P\<rbrace>" unfolding validE_E_def by (rule hoare_pre, wp, simp)

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

lemma hoare_walk_assmsE:
  assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>" and y: "\<And>s. P s \<Longrightarrow> Q s" and z: "\<lbrace>P\<rbrace> g \<lbrace>\<lambda>rv. Q\<rbrace>"
  shows      "\<lbrace>P\<rbrace> doE x \<leftarrow> f; g odE \<lbrace>\<lambda>rv. Q\<rbrace>" apply (wp z) apply (simp add: validE_def) apply (rule hoare_strengthen_post [OF x]) apply (auto simp: y split: sum.splits) done

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

lemma univ_get_wp:
  assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. P\<rbrace>"
  shows "\<lbrace>\<lambda>s. \<forall>(rv, s') \<in> mres (f s). s = s' \<longrightarrow> Q rv s'\<rbrace> f \<lbrace>Q\<rbrace>" apply (rule hoare_pre_imp[OF _ univ_wp]) apply clarsimp apply (drule bspec, assumption, simp) apply (drule mp) apply (simp add: state_unchanged[OF x]) apply simp done

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

lemma weak_if_wp:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow>
   \<lbrace>P and P'\<rbrace> f \<lbrace>\<lambda>r. if C r then Q r else Q' r\<rbrace>" by (auto simp add: valid_def split_def)

(* 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>\<lambda>r. if C r then Q r else Q' r\<rbrace>