kings-crown/FVELER_Isabelle huggingface dataset:
theory EquivValid

lemma gets_ev':
  shows "equiv_valid_inv I A (\<lambda> s. \<forall> t. I s t \<and> A s t \<longrightarrow> f s = f t) (gets f)" apply (simp add: equiv_valid_def2) apply (auto intro: equiv_valid_rv_guard_imp[OF gets_evrv']) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. \<forall>t. I s t \<and> A s t \<longrightarrow> f s = f t) (gets f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (=) (\<lambda>s. \<forall>t. I s t \<and> A s t \<longrightarrow> f s = f t) (gets f) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gets_the_evrv:
  "equiv_valid_rv_inv I A R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))) (gets_the f)" unfolding gets_the_def apply (rule equiv_valid_rv_bind) apply(rule equiv_valid_rv_guard_imp[OF gets_evrv]) apply simp apply(rule assert_opt_ev2) apply simp apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))) (gets_the f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))) (gets f >>= assert_opt) proof (prove)
goal (3 subgoals):
 1. equiv_valid_rv_inv I A ?W (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))) (gets f)
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (?Q rv) (?Q rv') (assert_opt rv) (assert_opt rv')
 3. \<lbrace>K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))\<rbrace> gets f \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t))) s \<Longrightarrow> K (\<forall>s t. I s t \<and> A s t \<longrightarrow> ?W (f s) (f t)) s
 2. \<And>rv rv'. ?W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (?Q rv) (?Q rv') (assert_opt rv) (assert_opt rv')
 3. \<lbrace>K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))\<rbrace> gets f \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. R (the rv) (the rv') \<Longrightarrow> equiv_valid_2 I A A R (?Q rv) (?Q rv') (assert_opt rv) (assert_opt rv')
 2. \<lbrace>K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))\<rbrace> gets f \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv rv' a a'. \<lbrakk>R (the rv) (the rv'); rv = Some a; rv' = Some a'\<rbrakk> \<Longrightarrow> R a a'
 2. \<lbrace>K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))\<rbrace> gets f \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (the (f s)) (the (f t)))\<rbrace> gets f \<lbrace>\<lambda>rv _. True\<rbrace> proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gets_the_ev:
  "equiv_valid_inv I A (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t)) (gets_the f)" unfolding equiv_valid_def2 apply(rule equiv_valid_rv_guard_imp[OF gets_the_evrv]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t)) (gets_the f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (=) (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t)) (gets_the f) proof (prove)
goal (1 subgoal):
 1. \<And>s. K (\<forall>s t. I s t \<and> A s t \<longrightarrow> f s = f t) s \<Longrightarrow> K (\<forall>s t. I s t \<and> A s t \<longrightarrow> the (f s) = the (f t)) s
theory EquivValid

lemma throwError_ev_pre:
  "equiv_valid_inv I A P (throwError e)" by (auto simp: throwError_def return_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (throwError e)
theory EquivValid

lemma returnOk_ev_pre:
  "equiv_valid_inv I A P (returnOk v)" by (auto simp: returnOk_def return_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (returnOk v)
theory EquivValid

lemma bindE_ev:
  assumes reads_res_2: "\<And> rv. equiv_valid_inv I A (Q rv) (g rv)"
  assumes reads_res_1: "equiv_valid_inv I A P' f"
  assumes hoare: "\<lbrace> P'' \<rbrace> f \<lbrace> Q \<rbrace>,-"
  shows "equiv_valid_inv I A (\<lambda>s. P' s \<and> P'' s) (f >>=E g)" unfolding bindE_def apply (rule bind_ev) prefer 3 apply(rule hoare[unfolded validE_R_def validE_def]) apply(simp split: sum.split add: lift_def throwError_ev) apply(blast intro!: reads_res_2) apply(rule reads_res_1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. P' s \<and> P'' s) (f >>=E g) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. P' s \<and> P'' s) (f >>= lift g) proof (prove)
goal (3 subgoals):
 1. \<And>rv. equiv_valid_inv I A (?Q rv) (lift g rv)
 2. equiv_valid_inv I A P' f
 3. \<lbrace>P''\<rbrace> f \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>P''\<rbrace> f \<lbrace>?Q\<rbrace>
 2. \<And>rv. equiv_valid_inv I A (?Q rv) (lift g rv)
 3. equiv_valid_inv I A P' f proof (prove)
goal (2 subgoals):
 1. \<And>rv. equiv_valid_inv I A (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s) (lift g rv)
 2. equiv_valid_inv I A P' f proof (prove)
goal (2 subgoals):
 1. \<And>rv. \<forall>x2. rv = Inr x2 \<longrightarrow> equiv_valid_inv I A (Q x2) (g x2)
 2. equiv_valid_inv I A P' f proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P' f proof (prove)
goal:
No subgoals!
theory EquivValid

lemma liftE_bindE_ev:
  assumes r2: "\<And> val. equiv_valid_inv I A (Q val) (g val)"
  assumes r1: "equiv_valid_inv I A P f"
  assumes hoare: "\<lbrace> R \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "equiv_valid_inv I A (\<lambda> s. P s \<and> R s) (liftE f >>=E g)" using assms by (blast intro: liftE_bindE_ev_general)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. P s \<and> R s) (liftE f >>=E g) proof (prove)
using this:
equiv_valid_inv I A (Q ?val) (g ?val)
equiv_valid_inv I A P f
\<lbrace>R\<rbrace> f \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. P s \<and> R s) (liftE f >>=E g)
theory EquivValid

lemma liftM_ev:
  assumes reads_res: "equiv_valid I A B P g"
  shows "equiv_valid I A B P (liftM f g)" apply (simp add: liftM_def) apply (rule bind_ev_general[THEN equiv_valid_guard_imp, OF return_ev reads_res wp_post_taut]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P (liftM f g) proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P (do x <- g;
return (f x)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> True proof (prove)
goal:
No subgoals!
theory EquivValid

lemma liftME_ev:
  assumes reads_res: "equiv_valid_inv I A P g"
  shows "equiv_valid_inv I A P (liftME f g)" apply(simp add: liftME_def) apply (rule bindE_ev_pre[OF returnOk_ev reads_res]) apply (rule hoare_True_E_R) apply fast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (liftME f g) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (doE x <- g;
returnOk (f x)
odE) proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> g \<lbrace>\<lambda>x _. True\<rbrace>, -
 2. \<And>s. P s \<Longrightarrow> P s \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> P s \<and> ?P'' s proof (prove)
goal:
No subgoals!
theory EquivValid

lemma whenE_ev:
  assumes a: "b \<Longrightarrow> equiv_valid_inv I A P m"
  shows "equiv_valid_inv I A (\<lambda>s. b \<longrightarrow> P s) (whenE b m)" unfolding whenE_def by (auto intro: a returnOk_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. b \<longrightarrow> P s) (whenE b m) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>s. b \<longrightarrow> P s) (if b then m else returnOk ())
theory EquivValid

lemma whenE_throwError_bindE_ev:
  assumes "\<And> rv. \<not> b \<Longrightarrow> equiv_valid_inv I A P (g rv)"
  shows "equiv_valid_inv I A P (whenE b (throwError e) >>=E g)" apply (rule_tac Q="\<lambda> rv. P and (\<lambda> s. \<not> b)" in bindE_ev_pre) apply (rule gen_asm_ev) apply (blast intro: assms) apply (rule whenE_ev) apply (rule throwError_ev) apply (wp whenE_throwError_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (whenE b (throwError e) >>=E g) proof (prove)
goal (4 subgoals):
 1. \<And>rv. equiv_valid_inv I A (P and (\<lambda>s. \<not> b)) (g rv)
 2. equiv_valid_inv I A ?P' (whenE b (throwError e))
 3. \<lbrace>?P''\<rbrace> whenE b (throwError e) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<not> b)\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<not> b \<Longrightarrow> equiv_valid_inv I A P (g rv)
 2. equiv_valid_inv I A ?P' (whenE b (throwError e))
 3. \<lbrace>?P''\<rbrace> whenE b (throwError e) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<not> b)\<rbrace>, -
 4. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. equiv_valid_inv I A ?P' (whenE b (throwError e))
 2. \<lbrace>?P''\<rbrace> whenE b (throwError e) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<not> b)\<rbrace>, -
 3. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (3 subgoals):
 1. b \<Longrightarrow> equiv_valid_inv I A ?P10 (throwError e)
 2. \<lbrace>?P''\<rbrace> whenE b (throwError e) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<not> b)\<rbrace>, -
 3. \<And>s. P s \<Longrightarrow> (b \<longrightarrow> ?P10 s) \<and> ?P'' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''\<rbrace> whenE b (throwError e) \<lbrace>\<lambda>rv. P and (\<lambda>s. \<not> b)\<rbrace>, -
 2. \<And>s. P s \<Longrightarrow> (b \<longrightarrow> True) \<and> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (b \<longrightarrow> True) \<and> (\<not> b \<longrightarrow> (P and (\<lambda>s. \<not> b)) s) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma K_bind_ev:
  "equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (K_bind f x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (K_bind f x)
theory EquivValid

lemma wpc_helper_equiv_valid:
  "equiv_valid D A B Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (equiv_valid D A B P f)" using equiv_valid_guard_imp apply (simp add: wpc_helper_def) apply (blast) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid D A B Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (equiv_valid D A B P f) proof (prove)
using this:
\<lbrakk>equiv_valid ?I ?A ?B ?Q ?f; \<And>s. ?P s \<Longrightarrow> ?Q s\<rbrakk> \<Longrightarrow> equiv_valid ?I ?A ?B ?P ?f

goal (1 subgoal):
 1. equiv_valid D A B Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (equiv_valid D A B P f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid D A B Q f; \<And>I A B Q f P. \<lbrakk>equiv_valid I A B Q f; \<And>s. P s \<Longrightarrow> Q s\<rbrakk> \<Longrightarrow> equiv_valid I A B P f\<rbrakk> \<Longrightarrow> (\<forall>s. P s \<longrightarrow> Q s) \<and> (\<forall>s. P' s \<longrightarrow> Q' s) \<and> P'' \<subseteq> Q'' \<longrightarrow> equiv_valid D A B P f proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapM_x_ev_pre:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>"
  assumes inv_established: "\<And> s. P s \<Longrightarrow> I s"
  shows "equiv_valid_inv D A P (mapM_x m lst)" apply(subst mapM_x_mapM) apply(rule bind_ev_pre[OF return_ev mapM_ev_pre]) apply (blast intro: reads_res invariant inv_established wp_post_taut)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (mapM_x m lst) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (do x <- mapM m lst;
return ()
od) proof (prove)
goal (5 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A ?I1 (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>?I1\<rbrace> m x \<lbrace>\<lambda>_. ?I1\<rbrace>
 3. \<And>s. ?P' s \<Longrightarrow> ?I1 s
 4. \<lbrace>?P''\<rbrace> mapM m lst \<lbrace>\<lambda>x _. True\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapM_ev:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>"
  shows "equiv_valid_inv D A I (mapM m lst)" using assms by (auto intro: mapM_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A I (mapM m lst) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m ?x)
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> m ?x \<lbrace>\<lambda>_. I\<rbrace>

goal (1 subgoal):
 1. equiv_valid_inv D A I (mapM m lst)
theory EquivValid

lemma mapM_x_ev:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>"
  shows "equiv_valid_inv D A I (mapM_x m lst)" using assms by (auto intro: mapM_x_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A I (mapM_x m lst) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m ?x)
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> m ?x \<lbrace>\<lambda>_. I\<rbrace>

goal (1 subgoal):
 1. equiv_valid_inv D A I (mapM_x m lst)
theory EquivValid

lemma mapME_x_mapME:
  "mapME_x f l = mapME f l >>=E (\<lambda> y. returnOk ())" apply (simp add: mapME_x_def sequenceE_x_def mapME_def sequenceE_def) apply (induct l, simp_all add: Let_def bindE_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapME_x f l = doE y <- mapME f l;
returnOk ()
odE proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>x y. doE _ <- x;
y
odE) (map f l) (returnOk ()) = doE y <- foldr (\<lambda>p q. doE x <- p;
y <- q;
returnOk (x # y)
odE) (map f l) (returnOk []);
returnOk ()
odE proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapME_ev:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv I A P (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> P \<rbrace> m x \<lbrace> \<lambda>_. P \<rbrace>, -"
  shows "equiv_valid_inv I A P (mapME m lst)" using assms by (auto intro: mapME_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (mapME m lst) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv I A P (m ?x)
?x \<in> set lst \<Longrightarrow> \<lbrace>P\<rbrace> m ?x \<lbrace>\<lambda>_. P\<rbrace>, -

goal (1 subgoal):
 1. equiv_valid_inv I A P (mapME m lst)
theory EquivValid

lemma mapME_x_ev_pre:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>,-"
  assumes inv_established: "\<And> s. P s \<Longrightarrow> I s"
  shows "equiv_valid_inv D A P (mapME_x m lst)" unfolding mapME_x_mapME apply (wp assms mapME_ev_pre | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (mapME_x m lst) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A P (doE y <- mapME m lst;
returnOk ()
odE) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapME_x_ev:
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m x)"
  assumes invariant: "\<And> x. x \<in> set lst \<Longrightarrow> \<lbrace> I \<rbrace> m x \<lbrace> \<lambda>_. I \<rbrace>, -"
  shows "equiv_valid_inv D A I (mapME_x m lst)" using assms by (auto intro: mapME_x_ev_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A I (mapME_x m lst) proof (prove)
using this:
?x \<in> set lst \<Longrightarrow> equiv_valid_inv D A I (m ?x)
?x \<in> set lst \<Longrightarrow> \<lbrace>I\<rbrace> m ?x \<lbrace>\<lambda>_. I\<rbrace>, -

goal (1 subgoal):
 1. equiv_valid_inv D A I (mapME_x m lst)
theory EquivValid

lemma mapM_ev':
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)"
  shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapM m lst)" apply(rule mapM_ev) apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapM m lst) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>K (\<forall>x\<in>set lst. P x)\<rbrace> m x \<lbrace>\<lambda>_. K (\<forall>x\<in>set lst. P x)\<rbrace> proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapM_x_ev':
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)"
  shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapM_x m lst)" apply(rule mapM_x_ev) apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapM_x m lst) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>K (\<forall>x\<in>set lst. P x)\<rbrace> m x \<lbrace>\<lambda>_. K (\<forall>x\<in>set lst. P x)\<rbrace> proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapME_ev':
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)"
  shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapME m lst)" apply(rule mapME_ev) apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapME m lst) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>K (\<forall>x\<in>set lst. P x)\<rbrace> m x \<lbrace>\<lambda>_. K (\<forall>x\<in>set lst. P x)\<rbrace>, - proof (prove)
goal:
No subgoals!
theory EquivValid

lemma mapME_x_ev':
  assumes reads_res: "\<And> x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (P x)) (m x)"
  shows "equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapME_x m lst)" apply(rule mapME_x_ev) apply(rule equiv_valid_guard_imp[OF reads_res], simp+, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (mapME_x m lst) proof (prove)
goal (2 subgoals):
 1. \<And>x. x \<in> set lst \<Longrightarrow> equiv_valid_inv D A (K (\<forall>x\<in>set lst. P x)) (m x)
 2. \<And>x. x \<in> set lst \<Longrightarrow> \<lbrace>K (\<forall>x\<in>set lst. P x)\<rbrace> m x \<lbrace>\<lambda>_. K (\<forall>x\<in>set lst. P x)\<rbrace>, - proof (prove)
goal:
No subgoals!
theory EquivValid

lemma use_spec_ev:
  "(\<And>st. spec_equiv_valid st I A B P f) \<Longrightarrow> equiv_valid I A B P f" by (simp add: equiv_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>st. spec_equiv_valid st I A B P f) \<Longrightarrow> equiv_valid I A B P f
theory EquivValid

lemma drop_spec_ev:
  "equiv_valid I A B P f \<Longrightarrow> spec_equiv_valid st I A B P f" by (simp add: equiv_valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f \<Longrightarrow> spec_equiv_valid st I A B P f
theory EquivValid

lemma spec_equiv_valid_guard_imp:
  assumes reads_res: "spec_equiv_valid_inv s' I A P' f"
  assumes guard_imp: "\<And> s. P s \<Longrightarrow> P' s"
  shows "spec_equiv_valid_inv s' I A P f" using assms by (fastforce simp: spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A P f proof (prove)
using this:
spec_equiv_valid_inv s' I A P' f
P ?s \<Longrightarrow> P' ?s

goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A P f
theory EquivValid

lemma bindE_spec_ev:
  assumes reads_res_2: "\<And> rv s''. (Inr rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (Q rv) (g rv)"
  assumes reads_res_1: "spec_equiv_valid_inv s' I A P' f"
  assumes hoare: "\<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>,-"
  shows "spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>=E g)" unfolding bindE_def apply (rule bind_spec_ev) prefer 3 apply(rule hoare[simplified validE_R_def validE_def]) apply(simp split: sum.split add: lift_def) apply(rule conjI) apply(fastforce simp: spec_equiv_valid_def throwError_def return_ev2) apply(fastforce simp: reads_res_2) apply(rule reads_res_1) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>=E g) proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A (\<lambda>s. P' s \<and> P'' s) (f >>= lift g) proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (?Q rv) (lift g rv)
 2. spec_equiv_valid_inv s' I A P' f
 3. \<lbrace>P''\<rbrace> f \<lbrace>?Q\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>P''\<rbrace> f \<lbrace>?Q\<rbrace>
 2. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (?Q rv) (lift g rv)
 3. spec_equiv_valid_inv s' I A P' f proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> spec_equiv_valid_inv s'' I A (\<lambda>s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s) (lift g rv)
 2. spec_equiv_valid_inv s' I A P' f proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> (\<forall>x1. rv = Inl x1 \<longrightarrow> spec_equiv_valid_inv s'' I A (\<lambda>s. True) (throwError x1)) \<and> (\<forall>x2. rv = Inr x2 \<longrightarrow> spec_equiv_valid_inv s'' I A (Q x2) (g x2))
 2. spec_equiv_valid_inv s' I A P' f proof (prove)
goal (3 subgoals):
 1. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> \<forall>x1. rv = Inl x1 \<longrightarrow> spec_equiv_valid_inv s'' I A (\<lambda>s. True) (throwError x1)
 2. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> \<forall>x2. rv = Inr x2 \<longrightarrow> spec_equiv_valid_inv s'' I A (Q x2) (g x2)
 3. spec_equiv_valid_inv s' I A P' f proof (prove)
goal (2 subgoals):
 1. \<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> \<forall>x2. rv = Inr x2 \<longrightarrow> spec_equiv_valid_inv s'' I A (Q x2) (g x2)
 2. spec_equiv_valid_inv s' I A P' f proof (prove)
goal (1 subgoal):
 1. spec_equiv_valid_inv s' I A P' f proof (prove)
goal:
No subgoals!
theory EquivValid

lemma if_spec_ev:
  "\<lbrakk> G \<Longrightarrow> spec_equiv_valid_inv s' I A P f;
     \<not> G \<Longrightarrow> spec_equiv_valid_inv s' I A P' f'
   \<rbrakk>  \<Longrightarrow> spec_equiv_valid_inv s' I A (\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)) (if G then f else f')" by (cases G, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<Longrightarrow> spec_equiv_valid_inv s' I A P f; \<not> G \<Longrightarrow> spec_equiv_valid_inv s' I A P' f'\<rbrakk> \<Longrightarrow> spec_equiv_valid_inv s' I A (\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)) (if G then f else f')