kings-crown/FVELER_Isabelle huggingface dataset:
theory EquivValid

lemma equiv_valid_2_guard_imp:
  assumes reads_res: "equiv_valid_2 D A B R Q Q' f f'"
  assumes guard_imp: "\<And> s. P s \<Longrightarrow> Q s"
  assumes guard_imp': "\<And> s. P' s \<Longrightarrow> Q' s"
  shows "equiv_valid_2 D A B R P P' f f'" using assms by (fastforce simp: equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A B R P P' f f' proof (prove)
using this:
equiv_valid_2 D A B R Q Q' f f'
P ?s \<Longrightarrow> Q ?s
P' ?s \<Longrightarrow> Q' ?s

goal (1 subgoal):
 1. equiv_valid_2 D A B R P P' f f'
theory EquivValid

lemma equiv_valid_2_bind_pre:
  assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes r1: "equiv_valid_2 D A A R' P P' f f'"
  assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes hoare': "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
  assumes guard_imp: "\<And> s. T s \<Longrightarrow> P s \<and> S s"
  assumes guard_imp': "\<And> s. T' s \<Longrightarrow> P' s \<and> S' s"
  shows "equiv_valid_2 D A A R T T' (f >>= g) (f' >>= g')" using assms by (blast intro: equiv_valid_2_bind[THEN equiv_valid_2_guard_imp])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A A R T T' (f >>= g) (f' >>= g') proof (prove)
using this:
R' ?rv ?rv' \<Longrightarrow> equiv_valid_2 D A A R (Q ?rv) (Q' ?rv') (g ?rv) (g' ?rv')
equiv_valid_2 D A A R' P P' f f'
\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>
\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>
T ?s \<Longrightarrow> P ?s \<and> S ?s
T' ?s \<Longrightarrow> P' ?s \<and> S' ?s

goal (1 subgoal):
 1. equiv_valid_2 D A A R T T' (f >>= g) (f' >>= g')
theory EquivValid

lemma equiv_valid_2_liftE_bindE:
  assumes r2: "\<And> rv rv'. R' rv rv' \<Longrightarrow> equiv_valid_2 D A A R (Q rv) (Q' rv') (g rv) (g' rv')"
  assumes hoare: "\<lbrace> S \<rbrace> f \<lbrace> Q \<rbrace>"
  assumes hoare':  "\<lbrace> S' \<rbrace> f' \<lbrace> Q' \<rbrace>"
  assumes r1: "equiv_valid_2 D A A R' P P' f f'"
  shows "equiv_valid_2 D A A R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g')" using assms by(blast intro: equiv_valid_2_liftE_bindE_general)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 D A A R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g') proof (prove)
using this:
R' ?rv ?rv' \<Longrightarrow> equiv_valid_2 D A A R (Q ?rv) (Q' ?rv') (g ?rv) (g' ?rv')
\<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>
\<lbrace>S'\<rbrace> f' \<lbrace>Q'\<rbrace>
equiv_valid_2 D A A R' P P' f f'

goal (1 subgoal):
 1. equiv_valid_2 D A A R (P and S) (P' and S') (liftE f >>=E g) (liftE f' >>=E g')
theory EquivValid

lemma equiv_valid_2_rvrel_imp:
  "\<lbrakk>equiv_valid_2 I A A R P P' f f'; \<And> s t. R s t \<Longrightarrow> R' s t\<rbrakk> \<Longrightarrow>
   equiv_valid_2 I A A R' P P' f f'" apply(fastforce simp: equiv_valid_2_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid_2 I A A R P P' f f'; \<And>s t. R s t \<Longrightarrow> R' s t\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A R' P P' f f' proof (prove)
goal:
No subgoals!
theory EquivValid

lemma equiv_valid_def2:
  "equiv_valid I A B P f = equiv_valid_2 I A B (=) P P f f" by (simp add: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f = equiv_valid_2 I A B (=) P P f f
theory EquivValid

lemma bind_ev_general:
  assumes reads_res_2: "\<And>rv. equiv_valid I B C (Q rv) (g rv)"
  assumes reads_res_1: "equiv_valid I A B P' f"
  assumes hoare: "\<lbrace> P'' \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "equiv_valid I A C (\<lambda>s. P' s \<and> P'' s) (f >>= g)" unfolding equiv_valid_def2 apply (rule equiv_valid_2_bind_general[where R'="(=)"]) apply (auto intro: reads_res_1[unfolded equiv_valid_def2] reads_res_2[unfolded equiv_valid_def2])[2] apply (rule hoare) apply (rule hoare) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A C (\<lambda>s. P' s \<and> P'' s) (f >>= g) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A C (=) (\<lambda>s. P' s \<and> P'' s) (f >>= g) proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> equiv_valid_2 I ?B C (=) (?Q rv) (?Q' rv') (g rv) (g rv')
 2. equiv_valid_rv I A ?B (=) P' f
 3. \<lbrace>P''\<rbrace> f \<lbrace>?Q\<rbrace>
 4. \<lbrace>P''\<rbrace> f \<lbrace>?Q'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory EquivValid

lemma bind_ev:
  assumes reads_res_2: "\<And>rv. equiv_valid I A A (Q rv) (g rv)"
  assumes reads_res_1: "equiv_valid I A A P' f"
  assumes hoare: "\<lbrace> P'' \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "equiv_valid I A A (\<lambda>s. P' s \<and> P'' s) (f >>= g)" using assms by (blast intro: bind_ev_general)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A A (\<lambda>s. P' s \<and> P'' s) (f >>= g) proof (prove)
using this:
equiv_valid I A A (Q ?rv) (g ?rv)
equiv_valid I A A P' f
\<lbrace>P''\<rbrace> f \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. equiv_valid I A A (\<lambda>s. P' s \<and> P'' s) (f >>= g)
theory EquivValid

lemma equiv_valid_weaken_pre:
  "\<lbrakk> equiv_valid I A' B P f; \<forall>st t. I st t \<and> A st t \<longrightarrow> A' st t \<rbrakk>
     \<Longrightarrow> equiv_valid I A B P f" by (fastforce simp: equiv_valid_def spec_equiv_valid_def equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid I A' B P f; \<forall>st t. I st t \<and> A st t \<longrightarrow> A' st t\<rbrakk> \<Longrightarrow> equiv_valid I A B P f
theory EquivValid

lemma equiv_valid_guard_imp:
  assumes reads_res: "equiv_valid I A B Q f"
  assumes guard_imp: "\<And> s. P s \<Longrightarrow> Q s"
  shows "equiv_valid I A B P f" using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

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

goal (1 subgoal):
 1. equiv_valid I A B P f
theory EquivValid

lemma gen_asm_ev':
  assumes "Q \<Longrightarrow> equiv_valid D A B P f"
  shows "equiv_valid D A B (P and K Q) f" using assms by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid D A B (P and K Q) f proof (prove)
using this:
Q \<Longrightarrow> equiv_valid D A B P f

goal (1 subgoal):
 1. equiv_valid D A B (P and K Q) f
theory EquivValid

lemma get_evrv:
  "equiv_valid_rv_inv I A (I and A) \<top> get" by(auto simp: equiv_valid_2_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A (I and A) (\<lambda>_. True) get
theory EquivValid

lemma equiv_valid_rv_bind_general:
  assumes ev1:
  "equiv_valid_rv I A B W P f"
  assumes ev2:
  "\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I B C R (Q rv) (Q rv') (g rv) (g rv')"
  assumes hoare:
  "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "equiv_valid_rv I A C R P (f >>= g)" apply(rule equiv_valid_2_guard_imp) apply(rule equiv_valid_2_bind_general[OF ev2]) apply(assumption) apply(rule ev1) apply(rule hoare) apply(rule hoare) apply(simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A C R P (f >>= g) proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 I A C R ?Q ?Q' (f >>= g) (f >>= g)
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. P s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. ?R'4 rv rv' \<Longrightarrow> W rv rv'
 2. equiv_valid_2 I A B ?R'4 ?P4 ?P'4 f f
 3. \<lbrace>?S4\<rbrace> f \<lbrace>Q\<rbrace>
 4. \<lbrace>?S'4\<rbrace> f \<lbrace>Q\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?P4 s \<and> ?S4 s
 6. \<And>s. P s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 I A B W ?P4 ?P'4 f f
 2. \<lbrace>?S4\<rbrace> f \<lbrace>Q\<rbrace>
 3. \<lbrace>?S'4\<rbrace> f \<lbrace>Q\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ?P4 s \<and> ?S4 s
 5. \<And>s. P s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S4\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<lbrace>?S'4\<rbrace> f \<lbrace>Q\<rbrace>
 3. \<And>s. P s \<Longrightarrow> P s \<and> ?S4 s
 4. \<And>s. P s \<Longrightarrow> P s \<and> ?S'4 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?S'4\<rbrace> f \<lbrace>Q\<rbrace>
 2. \<And>s. P s \<Longrightarrow> P s \<and> P s
 3. \<And>s. P s \<Longrightarrow> P s \<and> ?S'4 s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> P s \<and> P s
 2. \<And>s. P s \<Longrightarrow> P s \<and> P s proof (prove)
goal:
No subgoals!
theory EquivValid

lemma equiv_valid_rv_bind:
  assumes ev1:
  "equiv_valid_rv_inv I A W P f"
  assumes ev2:
  "\<And> rv rv'. W rv rv' \<Longrightarrow> equiv_valid_2 I A A R (Q rv) (Q rv') (g rv) (g rv')"
  assumes hoare:
  "\<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>"
  shows "equiv_valid_rv_inv I A R P (f >>= g)" using assms by(blast intro: equiv_valid_rv_bind_general)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv_inv I A R P (f >>= g) proof (prove)
using this:
equiv_valid_rv_inv I A W P f
W ?rv ?rv' \<Longrightarrow> equiv_valid_2 I A A R (Q ?rv) (Q ?rv') (g ?rv) (g ?rv')
\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>

goal (1 subgoal):
 1. equiv_valid_rv_inv I A R P (f >>= g)
theory EquivValid

lemma modify_ev2:
  assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I (f s) (f' t) \<and> B (f s) (f' t)"
  shows
  "equiv_valid_2 I A B R P P' (modify f) (modify f')" apply(clarsimp simp: equiv_valid_2_def in_monad) using assms by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' (modify f) (modify f') proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R () () \<and> I (f s) (f' t) \<and> B (f s) (f' t) proof (prove)
using this:
\<lbrakk>I ?s ?t; A ?s ?t; P ?s; P' ?t\<rbrakk> \<Longrightarrow> R () () \<and> I (f ?s) (f' ?t) \<and> B (f ?s) (f' ?t)

goal (1 subgoal):
 1. \<And>s t. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R () () \<and> I (f s) (f' t) \<and> B (f s) (f' t)
theory EquivValid

lemma modify_ev:
  "equiv_valid I A B
     (\<lambda> s. \<forall> s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t))
     (modify f)" apply(clarsimp simp:equiv_valid_def2) apply(rule modify_ev2) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B (\<lambda>s. \<forall>s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) (modify f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A B (=) (\<lambda>s. \<forall>s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) (modify f) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>I s t; A s t; \<forall>s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t); \<forall>s t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)\<rbrakk> \<Longrightarrow> () = () \<and> I (f s) (f t) \<and> B (f s) (f t)
theory EquivValid

lemma modify_ev':
  "equiv_valid I A B
     (\<lambda> s. \<forall> t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t))
     (modify f)" apply(clarsimp simp:equiv_valid_def2) apply(rule modify_ev2) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B (\<lambda>s. \<forall>t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) (modify f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A B (=) (\<lambda>s. \<forall>t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t)) (modify f) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>I s t; A s t; \<forall>t. I s t \<and> A s t \<longrightarrow> I (f s) (f t) \<and> B (f s) (f t); \<forall>ta. I t ta \<and> A t ta \<longrightarrow> I (f t) (f ta) \<and> B (f t) (f ta)\<rbrakk> \<Longrightarrow> () = () \<and> I (f s) (f t) \<and> B (f s) (f t)
theory EquivValid

lemma modify_ev'':
  assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P t\<rbrakk> \<Longrightarrow> I (f s) (f t) \<and> B (f s) (f t)"
  shows "equiv_valid I A B P (modify f)" apply(clarsimp simp:equiv_valid_def2) apply(rule modify_ev2) using assms by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P (modify f) proof (prove)
goal (1 subgoal):
 1. equiv_valid_rv I A B (=) P (modify f) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>I s t; A s t; P s; P t\<rbrakk> \<Longrightarrow> () = () \<and> I (f s) (f t) \<and> B (f s) (f t) proof (prove)
using this:
\<lbrakk>I ?s ?t; A ?s ?t; P ?s; P ?t\<rbrakk> \<Longrightarrow> I (f ?s) (f ?t) \<and> B (f ?s) (f ?t)

goal (1 subgoal):
 1. \<And>s t. \<lbrakk>I s t; A s t; P s; P t\<rbrakk> \<Longrightarrow> () = () \<and> I (f s) (f t) \<and> B (f s) (f t)
theory EquivValid

lemma put_ev2:
  assumes "\<And> s t. \<lbrakk>I s t; A s t; P s; P' t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x'"
  shows
  "equiv_valid_2 I A B R P P' (put x) (put x')" apply(clarsimp simp: equiv_valid_2_def in_monad) using assms by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' (put x) (put x') proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x' proof (prove)
using this:
\<lbrakk>I ?s ?t; A ?s ?t; P ?s; P' ?t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x'

goal (1 subgoal):
 1. \<And>s t. \<lbrakk>P s; P' t; I s t; A s t\<rbrakk> \<Longrightarrow> R () () \<and> I x x' \<and> B x x'
theory EquivValid

lemma get_bind_ev2:
  assumes "\<And> rv rv'. \<lbrakk>I rv rv'; A rv rv'\<rbrakk> \<Longrightarrow> equiv_valid_2 I A B R (P and ((=) rv)) (P' and ((=) rv')) (f rv) (f' rv')"
  shows "equiv_valid_2 I A B R P P' (get >>= f) (get >>= f')" apply(rule equiv_valid_2_guard_imp) apply(rule_tac R'="I and A" in equiv_valid_2_bind_general) apply(rule assms, simp+) apply(rule get_evrv) apply(wp get_sp)+ by(auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' (get >>= f) (get >>= f') proof (prove)
goal (3 subgoals):
 1. equiv_valid_2 I A B R ?Q ?Q' (get >>= f) (get >>= f')
 2. \<And>s. P s \<Longrightarrow> ?Q s
 3. \<And>s. P' s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. \<And>rv rv'. (I and A) rv rv' \<Longrightarrow> equiv_valid_2 I ?B4 B R (?Q4 rv) (?Q'4 rv') (f rv) (f' rv')
 2. equiv_valid_2 I A ?B4 (I and A) ?P4 ?P'4 get get
 3. \<lbrace>?S4\<rbrace> get \<lbrace>?Q4\<rbrace>
 4. \<lbrace>?S'4\<rbrace> get \<lbrace>?Q'4\<rbrace>
 5. \<And>s. P s \<Longrightarrow> ?P4 s \<and> ?S4 s
 6. \<And>s. P' s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (5 subgoals):
 1. equiv_valid_2 I A A (I and A) ?P4 ?P'4 get get
 2. \<lbrace>?S4\<rbrace> get \<lbrace>\<lambda>rv. P and (=) rv\<rbrace>
 3. \<lbrace>?S'4\<rbrace> get \<lbrace>\<lambda>rv'. P' and (=) rv'\<rbrace>
 4. \<And>s. P s \<Longrightarrow> ?P4 s \<and> ?S4 s
 5. \<And>s. P' s \<Longrightarrow> ?P'4 s \<and> ?S'4 s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?S4\<rbrace> get \<lbrace>\<lambda>rv. P and (=) rv\<rbrace>
 2. \<lbrace>?S'4\<rbrace> get \<lbrace>\<lambda>rv'. P' and (=) rv'\<rbrace>
 3. \<And>s. P s \<Longrightarrow> True \<and> ?S4 s
 4. \<And>s. P' s \<Longrightarrow> True \<and> ?S'4 s proof (prove)
goal (2 subgoals):
 1. \<And>s. P s \<Longrightarrow> True \<and> (P and (=) s) s
 2. \<And>s. P' s \<Longrightarrow> True \<and> (P' and (=) s) s
theory EquivValid

lemma return_ev_pre:
  "equiv_valid_inv I A P (return x)" apply (simp add: equiv_valid_def2 return_ev2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (return x) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma fail_ev2_l:
  "equiv_valid_2 I A B R P P' fail f'" by(simp add: equiv_valid_2_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' fail f'
theory EquivValid

lemma fail_ev2_r:
  "equiv_valid_2 I A B R P P' f fail" by(simp add: equiv_valid_2_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A B R P P' f fail
theory EquivValid

lemma fail_ev_pre:
  "equiv_valid I A B P fail" apply (simp add: equiv_valid_def2 fail_ev2_l) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P fail proof (prove)
goal:
No subgoals!
theory EquivValid

lemma assert_ev2:
  "R () () \<Longrightarrow> equiv_valid_2 I A A R P P' (assert a) (assert b)" apply(simp add: assert_def fail_ev2_l fail_ev2_r) apply(blast intro: return_ev2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. R () () \<Longrightarrow> equiv_valid_2 I A A R P P' (assert a) (assert b) proof (prove)
goal (1 subgoal):
 1. R () () \<Longrightarrow> a \<longrightarrow> b \<longrightarrow> equiv_valid_2 I A A R P P' (return ()) (return ()) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma liftE_ev:
  "equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (liftE f)" unfolding liftE_def apply (rule bind_ev_general[THEN equiv_valid_guard_imp, OF return_ev _ wp_post_taut]) apply fastforce+  (* schematic instantiation *)
   done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (liftE f) proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (do r <- f;
return (Inr r)
od) proof (prove)
goal (2 subgoals):
 1. equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B ?P'1 f
 2. \<And>s. \<lbrakk>equiv_valid I A B P f; P s\<rbrakk> \<Longrightarrow> ?P'1 s \<and> True proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory EquivValid

lemma if_ev:
  assumes "b \<Longrightarrow> equiv_valid I A B P f"
  assumes "\<not> b \<Longrightarrow> equiv_valid I A B Q g"
  shows "equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s)) (if b then f else g)" apply (clarsimp split: if_split) using assms by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) (if b then f else g) proof (prove)
goal (1 subgoal):
 1. (b \<longrightarrow> equiv_valid I A B P f) \<and> (\<not> b \<longrightarrow> equiv_valid I A B Q g) proof (prove)
using this:
b \<Longrightarrow> equiv_valid I A B P f
\<not> b \<Longrightarrow> equiv_valid I A B Q g

goal (1 subgoal):
 1. (b \<longrightarrow> equiv_valid I A B P f) \<and> (\<not> b \<longrightarrow> equiv_valid I A B Q g)
theory EquivValid

lemma assert_ev_pre:
  "equiv_valid_inv I A P (assert b)" apply(simp add: equiv_valid_def2 assert_ev2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A P (assert b) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma assert_opt_ev:
  "equiv_valid_inv I A \<top> (assert_opt v)" apply (simp add: assert_opt_def return_ev fail_ev
            split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (\<lambda>_. True) (assert_opt v) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma assert_opt_ev2:
  assumes "\<And> a a'. \<lbrakk>v = Some a; v' = Some a'\<rbrakk> \<Longrightarrow> R a a'"
  shows "equiv_valid_2 I A A R \<top> \<top> (assert_opt v) (assert_opt v')" apply (simp add: assert_opt_def return_ev fail_ev2_l fail_ev2_r
            split: option.split) apply(intro allI impI) apply(rule return_ev2) apply(rule assms, assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_2 I A A R (\<lambda>_. True) (\<lambda>_. True) (assert_opt v) (assert_opt v') proof (prove)
goal (1 subgoal):
 1. \<forall>x2. v = Some x2 \<longrightarrow> (\<forall>x2a. v' = Some x2a \<longrightarrow> equiv_valid_2 I A A R (\<lambda>_. True) (\<lambda>_. True) (return x2) (return x2a)) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a. \<lbrakk>v = Some x2; v' = Some x2a\<rbrakk> \<Longrightarrow> equiv_valid_2 I A A R (\<lambda>_. True) (\<lambda>_. True) (return x2) (return x2a) proof (prove)
goal (1 subgoal):
 1. \<And>x2 x2a s t. \<lbrakk>v = Some x2; v' = Some x2a; True; True; I s t; A s t\<rbrakk> \<Longrightarrow> R x2 x2a proof (prove)
goal:
No subgoals!
theory EquivValid

lemma select_f_ev:
  "equiv_valid_inv I A (K (det f)) (select_f (f x))" apply (rule gen_asm_ev) apply (simp add: select_f_def equiv_valid_def2 equiv_valid_2_def det_set_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (K (det f)) (select_f (f x)) proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> equiv_valid_inv I A (\<lambda>_. True) (select_f (f x)) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gets_evrv:
  "equiv_valid_rv_inv I A R (K (\<forall>s t. I s t \<and> A s t \<longrightarrow> R (f s) (f t))) (gets f)" apply (auto simp: equiv_valid_2_def in_monad) 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 (f s) (f t))) (gets f) proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gets_evrv':
  "equiv_valid_rv_inv I A R (\<lambda>s. (\<forall>t. I s t \<and> A s t \<longrightarrow> R (f s) (f t))) (gets f)" apply (auto simp: equiv_valid_2_def in_monad) done

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

lemma gets_evrv'':
  "\<forall>s t. I s t \<and> A s t \<and> P s \<and> P t \<longrightarrow> R (f s) (f t) \<Longrightarrow> equiv_valid_rv_inv I A R P (gets f)" apply (auto simp: equiv_valid_2_def in_monad) done

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

lemma equiv_valid_rv_guard_imp:
  "\<lbrakk>equiv_valid_rv I A B R P f; \<And> s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow>
   equiv_valid_rv I A B R Q f" apply(simp add: equiv_valid_2_def) apply fast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid_rv I A B R P f; \<And>s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> equiv_valid_rv I A B R Q f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t'); \<And>s. Q s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> \<forall>s t. Q s \<and> Q t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (f t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> I s' t' \<and> B s' t') proof (prove)
goal:
No subgoals!
theory EquivValid

lemma gets_ev:
  shows "equiv_valid_inv I A (\<lambda> s. \<forall> s 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>s 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>s t. I s t \<and> A s t \<longrightarrow> f s = f t) (gets f) proof (prove)
goal:
No subgoals!