kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_UL

lemma corres_add_noop_lhs:
  "corres_underlying sr nf nf' r P P' (return () >>= (\<lambda>_. f)) g
      \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (do _ <- return ();
f
od) g \<Longrightarrow> corres_underlying sr nf nf' r P P' f g
theory Corres_UL

lemma corres_add_noop_lhs2:
  "corres_underlying sr nf nf' r P P' (f >>= (\<lambda>_. return ())) g
      \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (do _ <- f;
return ()
od) g \<Longrightarrow> corres_underlying sr nf nf' r P P' f g
theory Corres_UL

lemma isLeft_case_sum:
  "isLeft v \<Longrightarrow> (case v of Inl v' \<Rightarrow> f v' | Inr v' \<Rightarrow> g v') = f (theLeft v)" by (clarsimp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isLeft v \<Longrightarrow> (case v of Inl v' \<Rightarrow> f v' | Inr v' \<Rightarrow> g v') = f (theLeft v)
theory Corres_UL

lemma corres_returnTT:
  "r a b \<Longrightarrow> corres_underlying sr nf nf' r \<top> \<top> (return a) (return b)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r a b \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>_. True) (\<lambda>_. True) (return a) (return b)
theory Corres_UL

lemma corres_assert_gen_asm:
  "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q f (assert F >>= g)" by (simp add: corres_gen_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ())) \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q f (assert F >>= g)
theory Corres_UL

lemma corres_assert_gen_asm_l:
  "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q (f ()) g \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q (assert F >>= f) g" by (simp add: corres_gen_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> corres_underlying sr nf nf' r P Q (f ()) g) \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>_. F)) Q (assert F >>= f) g
theory Corres_UL

lemma corres_assert_gen_asm_l2:
  "\<lbrakk> F \<Longrightarrow> corres_underlying sr nf nf' r P Q (f ()) g \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r P (Q and (\<lambda>_. F)) (assert F >>= f) g" by (simp add: corres_gen_asm2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (F \<Longrightarrow> corres_underlying sr nf nf' r P Q (f ()) g) \<Longrightarrow> corres_underlying sr nf nf' r P (Q and (\<lambda>_. F)) (assert F >>= f) g
theory Corres_UL

lemma corres_add_guard:
  "\<lbrakk>\<And>s s'. \<lbrakk>Q s; Q' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s \<and> P' s';
    corres_underlying sr nf nf' r (Q and P) (Q' and P') f g\<rbrakk> \<Longrightarrow>
    corres_underlying sr nf nf' r Q Q' f g" by (auto simp: corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>Q s; Q' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s \<and> P' s'; corres_underlying sr nf nf' r (Q and P) (Q' and P') f g\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g
theory Corres_UL

lemma corres_stateAssert_r_cross:
  assumes A: "\<forall>s s'. (s, s') \<in> sr \<longrightarrow> P' s \<longrightarrow> Q' s' \<longrightarrow> A s'"
  assumes C: "corres_underlying sr nf nf' r P Q f (g ())"
  shows
  "corres_underlying sr nf nf' r (P and P') (Q and Q') f (stateAssert A [] >>= g)" apply (clarsimp simp: bind_assoc stateAssert_def) apply corres_pre apply (rule corres_symb_exec_r) apply (rule corres_assert_gen_asm2, rule C) apply wpsimp+ apply (simp add: A) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and P') (Q and Q') f (stateAssert A [] >>= g) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and P') (Q and Q') f (do x <- get;
assert (A x) >>= g
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying sr nf nf' r ?Q ?Q' f (do x <- get;
assert (A x) >>= g
od)
 2. \<And>s s'. \<lbrakk>(P and P') s; (Q and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>(P and P') s; (Q and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (6 subgoals):
 1. \<And>x. corres_underlying sr nf nf' r ?Q (?Q'1 x) f (assert (A x) >>= g)
 2. \<lbrace>?Q'\<rbrace> get \<lbrace>?Q'1\<rbrace>
 3. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. nf' \<Longrightarrow> no_fail ?Q' get
 5. \<And>s s'. \<lbrakk>(P and P') s; (Q and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q s
 6. \<And>s s'. \<lbrakk>(P and P') s; (Q and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q'\<rbrace> get \<lbrace>\<lambda>x. Q and (\<lambda>_. A x)\<rbrace>
 2. \<And>s. ?Q' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. nf' \<Longrightarrow> no_fail ?Q' get
 4. \<And>s s'. \<lbrakk>(P and P') s; (Q and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> P s
 5. \<And>s s'. \<lbrakk>(P and P') s; (Q and Q') s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s; Q s'; Q' s'\<rbrakk> \<Longrightarrow> A s' proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_gets_trivial:
  "\<lbrakk>\<And>s s'. (s,s') \<in> sr \<Longrightarrow> f s = f' s' \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' (=) \<top> \<top> (gets f) (gets f')" unfolding corres_underlying_def gets_def get_def return_def bind_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. (s, s') \<in> sr \<Longrightarrow> f s = f' s') \<Longrightarrow> corres_underlying sr nf nf' (=) (\<lambda>_. True) (\<lambda>_. True) (gets f) (gets f') proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. (s, s') \<in> sr \<Longrightarrow> f s = f' s') \<Longrightarrow> \<forall>(s, s')\<in>sr. True \<and> True \<longrightarrow> (nf \<longrightarrow> \<not> snd (\<Union> (fst ` (\<lambda>(sa, s). ({(f sa, s)}, False)) ` fst ({(s, s)}, False)), True \<in> snd ` (\<lambda>(sa, s). ({(f sa, s)}, False)) ` fst ({(s, s)}, False) \<or> snd ({(s, s)}, False))) \<longrightarrow> (\<forall>(r', t')\<in>fst (\<Union> (fst ` (\<lambda>(sa, s). ({(f' sa, s)}, False)) ` fst ({(s', s')}, False)), True \<in> snd ` (\<lambda>(sa, s). ({(f' sa, s)}, False)) ` fst ({(s', s')}, False) \<or> snd ({(s', s')}, False)). \<exists>(r, t)\<in>fst (\<Union> (fst ` (\<lambda>(sa, s). ({(f sa, s)}, False)) ` fst ({(s, s)}, False)), True \<in> snd ` (\<lambda>(sa, s). ({(f sa, s)}, False)) ` fst ({(s, s)}, False) \<or> snd ({(s, s)}, False)). (t, t') \<in> sr \<and> r = r') \<and> (nf' \<longrightarrow> \<not> snd (\<Union> (fst ` (\<lambda>(sa, s). ({(f' sa, s)}, False)) ` fst ({(s', s')}, False)), True \<in> snd ` (\<lambda>(sa, s). ({(f' sa, s)}, False)) ` fst ({(s', s')}, False) \<or> snd ({(s', s')}, False)))
theory Corres_UL

lemma corres_underlying_fail_fail:
  "corres_underlying rf_sr nf False r \<top> \<top> fail fail" by (simp add: corres_underlying_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr nf False r (\<lambda>_. True) (\<lambda>_. True) fail fail
theory Corres_UL

lemma corres_underlying_assert_assert:
  "Q' = Q \<Longrightarrow> corres_underlying rf_sr nf False dc \<top> \<top> (assert Q) (assert Q')" by (simp add: assert_def corres_underlying_fail_fail)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q' = Q \<Longrightarrow> corres_underlying rf_sr nf False dc (\<lambda>_. True) (\<lambda>_. True) (assert Q) (assert Q')
theory Corres_UL

lemma corres_underlying_stateAssert_stateAssert:
  assumes "\<And>s s'. \<lbrakk> (s,s') \<in> rf_sr; P s; P' s' \<rbrakk> \<Longrightarrow> Q' s' = Q s"
  shows "corres_underlying rf_sr nf False dc P P' (stateAssert Q []) (stateAssert Q' [])" by (auto simp: stateAssert_def get_def Nondet_Monad.bind_def corres_underlying_def
                 assert_def return_def fail_def assms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying rf_sr nf False dc P P' (stateAssert Q []) (stateAssert Q' [])
theory Corres_UL

lemma corres_no_fail_nf:
  "\<lbrakk> no_fail P f; corres_underlying S True nf' r P Q f g \<rbrakk> \<Longrightarrow>
   corres_underlying S False nf' r P Q f g" by (simp add: corres_underlying_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_fail P f; corres_underlying S True nf' r P Q f g\<rbrakk> \<Longrightarrow> corres_underlying S False nf' r P Q f g
theory Corres_UL

lemma (in strengthen_implementation) wpfix_strengthen_corres_guard_imp:
  "(\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (Q s))
    \<Longrightarrow> (\<And>s. st (\<not> F) (\<longrightarrow>) (P' s) (Q' s))
    \<Longrightarrow> st F (\<longrightarrow>)
        (corres_underlying sr nf nf' r P P' f g)
        (corres_underlying sr nf nf' r Q Q' f g)" by (cases F; auto elim: corres_guard_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. st (\<not> F) (\<longrightarrow>) (P s) (Q s); \<And>s. st (\<not> F) (\<longrightarrow>) (P' s) (Q' s)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (corres_underlying sr nf nf' r P P' f g) (corres_underlying sr nf nf' r Q Q' f g)
theory Corres_UL

lemma corres_name_pre:
  "\<lbrakk> \<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk>
                 \<Longrightarrow> corres_underlying sr nf nf' r ((=) s) ((=) s') f g \<rbrakk>
        \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" apply (simp add: corres_underlying_def split_def
                   Ball_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r ((=) s) ((=) s') f g) \<Longrightarrow> corres_underlying sr nf nf' r P P' f g proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. \<lbrakk>P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>a b. (a, b) \<in> fst (g s') \<longrightarrow> (\<exists>x\<in>fst (f s). (snd x, b) \<in> sr \<and> r (fst x) a)) \<and> (nf' \<longrightarrow> \<not> snd (g s'))) \<Longrightarrow> \<forall>a b. (a, b) \<in> sr \<longrightarrow> P a \<and> P' b \<longrightarrow> (nf \<longrightarrow> \<not> snd (f a)) \<longrightarrow> (\<forall>aa ba. (aa, ba) \<in> fst (g b) \<longrightarrow> (\<exists>x\<in>fst (f a). (snd x, ba) \<in> sr \<and> r (fst x) aa)) \<and> (nf' \<longrightarrow> \<not> snd (g b)) proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_return_trivial:
  "corres_underlying srel nf' nf dc \<top> \<top> (return a) (return b)" by (simp add: corres_underlying_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf' nf dc (\<lambda>_. True) (\<lambda>_. True) (return a) (return b)
theory DetWPLib

lemma det_result:
  "\<lbrakk> det_wp P f; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. fst (f s) = {(rv, s)}\<rbrace>" by (fastforce simp: det_wp_def valid_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_wp P f; \<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>_. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv s. fst (f s) = {(rv, s)}\<rbrace>
theory DetWPLib

lemma det_wp_use:
  "det_wp P f \<Longrightarrow> P s \<Longrightarrow> (fst (f s) = {s'}) = (s' \<in> fst (f s))" by (fastforce simp: det_wp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_wp P f; P s\<rbrakk> \<Longrightarrow> (fst (f s) = {s'}) = (s' \<in> fst (f s))
theory DetWPLib

lemma det_wp_det:
  "det f \<Longrightarrow> det_wp \<top> f" by (clarsimp simp: det_def det_wp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> det_wp (\<lambda>_. True) f
theory DetWPLib

lemma det_wp_no_fail:
  "det_wp P f \<Longrightarrow> no_fail P f" by (fastforce simp: det_wp_def no_fail_def)

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

lemma det_wp_bind [wp]:
  "\<lbrakk> det_wp P f; \<And>rv. det_wp (Q rv) (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk> \<Longrightarrow> det_wp (P and P') (f >>= (\<lambda>rv. g rv))" apply (simp add: det_wp_def valid_def split_def bind_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>det_wp P f; \<And>rv. det_wp (Q rv) (g rv); \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> det_wp (P and P') (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<exists>a b. f s = ({(a, b)}, False)); \<And>rv. \<forall>s. Q rv s \<longrightarrow> (\<exists>a b. g rv s = ({(a, b)}, False)); \<forall>s. P' s \<longrightarrow> (\<forall>x\<in>fst (f s). Q (fst x) (snd x))\<rbrakk> \<Longrightarrow> \<forall>s. P s \<and> P' s \<longrightarrow> (\<exists>a b. (\<Union>x\<in>fst (f s). fst (g (fst x) (snd x))) = {(a, b)}) \<and> (\<forall>x\<in>fst (f s). \<not> snd (g (fst x) (snd x))) \<and> \<not> snd (f s) proof (prove)
goal:
No subgoals!
theory DetWPLib

lemma det_wp_pre:
  "det_wp P' f \<Longrightarrow> (\<And>s. P s \<Longrightarrow> P' s) \<Longrightarrow> det_wp P f" by (simp add: det_wp_def)

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

lemma det_wp_return [wp]:
  "det_wp \<top> (return x)" by (simp add: det_wp_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. True) (return x)
theory DetWPLib

lemma det_wp_case_option [wp]:
  "\<lbrakk> x = None \<Longrightarrow> det_wp P f;
     \<And>y. x = Some y \<Longrightarrow> det_wp (Q y) (g y) \<rbrakk> \<Longrightarrow>
  det_wp (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q y s)) (case_option f g x)" by (cases x) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x = None \<Longrightarrow> det_wp P f; \<And>y. x = Some y \<Longrightarrow> det_wp (Q y) (g y)\<rbrakk> \<Longrightarrow> det_wp (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>y. x = Some y \<longrightarrow> Q y s)) (case x of None \<Rightarrow> f | Some x \<Rightarrow> g x)
theory DetWPLib

lemma det_wp_get [wp]:
  "det_wp \<top> get" by (simp add: get_def det_wp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. True) get
theory DetWPLib

lemma det_wp_gets [wp]:
  "det_wp \<top> (gets f)" by (simp add: simpler_gets_def det_wp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. True) (gets f)
theory DetWPLib

lemma det_wp_fail [wp]:
  "det_wp \<bottom> fail" by (simp add: fail_def det_wp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. False) fail
theory DetWPLib

lemma det_wp_assert [wp]:
  "det_wp (\<lambda>_. P) (assert P)" by (simp add: assert_def det_wp_fail det_wp_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. P) (assert P)
theory DetWPLib

lemma det_wp_stateAssert [wp]:
  "det_wp P (stateAssert P xs)" apply (simp add: stateAssert_def) apply (rule det_wp_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp P (stateAssert P xs) proof (prove)
goal (1 subgoal):
 1. det_wp P (do s <- get;
assert (P s)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ((\<lambda>_. True) and P) s proof (prove)
goal:
No subgoals!
theory DetWPLib

lemma det_wp_select_f:
  "det_wp (\<lambda>_. P s) f \<Longrightarrow> det_wp (\<lambda>_. P s) (select_f (f s))" apply (clarsimp simp: select_f_def det_wp_def) apply (erule_tac x=s in allE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. P s) f \<Longrightarrow> det_wp (\<lambda>_. P s) (select_f (f s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; \<forall>s. \<exists>r. f s = ({r}, False)\<rbrakk> \<Longrightarrow> (\<forall>sa. \<exists>a b. fst (f s) \<times> {sa} = {(a, b)}) \<and> \<not> snd (f s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P s; \<exists>r. f s = ({r}, False)\<rbrakk> \<Longrightarrow> (\<forall>sa. \<exists>a b. fst (f s) \<times> {sa} = {(a, b)}) \<and> \<not> snd (f s) proof (prove)
goal:
No subgoals!
theory DetWPLib

lemma det_wp_modify [wp]:
  "det_wp \<top> (modify f)" by (simp add: det_wp_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. True) (modify f)
theory DetWPLib

lemma det_wp_liftM [wp]:
  "det_wp P g \<Longrightarrow> det_wp P (liftM f g)" apply (simp add: liftM_def) apply (rule det_wp_pre) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp P g \<Longrightarrow> det_wp P (liftM f g) proof (prove)
goal (1 subgoal):
 1. det_wp P g \<Longrightarrow> det_wp P (do x <- g;
return (f x)
od) proof (prove)
goal (2 subgoals):
 1. det_wp P g \<Longrightarrow> det_wp ?P' (do x <- g;
return (f x)
od)
 2. \<And>s. \<lbrakk>det_wp P g; P s\<rbrakk> \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory DetWPLib

lemma det_wp_when [wp]:
  "det_wp P f \<Longrightarrow> det_wp (\<lambda>s. Q \<longrightarrow> P s) (when Q f)" by (clarsimp simp: when_def det_wp_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp P f \<Longrightarrow> det_wp (\<lambda>s. Q \<longrightarrow> P s) (when Q f)
theory DetWPLib

lemma det_wp_unless [wp]:
  "det_wp P f \<Longrightarrow> det_wp (\<lambda>s. \<not>Q \<longrightarrow> P s) (unless Q f)" by (simp add: unless_def det_wp_when)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp P f \<Longrightarrow> det_wp (\<lambda>s. \<not> Q \<longrightarrow> P s) (unless Q f)
theory DetWPLib

lemma det_wp_assert_opt :
  "det_wp (\<lambda>_. x \<noteq> None) (assert_opt x)" apply (simp add: assert_opt_def) apply (rule det_wp_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. x \<noteq> None) (assert_opt x) proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. \<exists>y. x = Some y) (case x of None \<Rightarrow> fail | Some v \<Rightarrow> return v) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>y. x = Some y \<Longrightarrow> (x = None \<longrightarrow> False) \<and> (\<forall>y. x = Some y \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma corres_Id:
  "\<lbrakk> f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> no_fail P' g \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' r \<top> P' f g" apply (clarsimp simp: corres_underlying_def Ball_def no_fail_def) apply (rule rev_bexI, assumption) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> no_fail P' g\<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' r (\<lambda>_. True) P' f g proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> \<forall>s. P' s \<longrightarrow> \<not> snd (g s); P' a; nf \<longrightarrow> \<not> snd (g a); (aa, b) \<in> fst (g a)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (g a). case x of (ra, t) \<Rightarrow> t = b \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>f = g; \<And>rv. r rv rv; nf' \<Longrightarrow> \<forall>s. P' s \<longrightarrow> \<not> snd (g s); P' a; nf \<longrightarrow> \<not> snd (g a); (aa, b) \<in> fst (g a)\<rbrakk> \<Longrightarrow> case (aa, b) of (ra, t) \<Rightarrow> t = b \<and> r ra aa proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma select_pick_corres_underlying:
  "corres_underlying sr nf nf' r P Q (f x) g
     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g" by (fastforce simp: corres_underlying_def select_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P Q (f x) g \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g
theory ExtraCorres

lemma select_pick_corres:
  "corres_underlying sr nf nf' r P Q (f x) g
     \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g" by (fastforce simp: intro: select_pick_corres_underlying)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P Q (f x) g \<Longrightarrow> corres_underlying sr nf nf' r (P and (\<lambda>s. x \<in> S)) Q (select S >>= f) g
theory ExtraCorres

lemma corres_modify:
  assumes rl:
  "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> (f s, g s') \<in> sr"
  shows "corres_underlying sr nf nf' dc P P' (modify f) (modify g)" by (simp add: simpler_modify_def corres_singleton rl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc P P' (modify f) (modify g)
theory ExtraCorres

lemma ex_absI[intro!]:
  "(s, s') \<in> sr \<Longrightarrow> P s \<Longrightarrow> ex_abs_underlying sr P s'" by (auto simp add: ex_abs_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> sr; P s\<rbrakk> \<Longrightarrow> ex_abs_underlying sr P s'
theory ExtraCorres

lemma corres_u_nofail:
  "\<lbrakk>corres_underlying S nf True r P P' f g; nf \<Longrightarrow> no_fail P f\<rbrakk>
   \<Longrightarrow> no_fail (P' and ex_abs_underlying S P) g" by (fastforce simp: corres_underlying_def ex_abs_underlying_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying S nf True r P P' f g; nf \<Longrightarrow> no_fail P f\<rbrakk> \<Longrightarrow> no_fail (P' and ex_abs_underlying S P) g
theory ExtraCorres

lemma wp_from_corres_u:
  "\<lbrakk> corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> f' \<lbrace>\<lambda>rv' s'. \<exists>rv s. (s,s') \<in> R \<and> r rv rv' \<and> Q rv s \<and> Q' rv' s'\<rbrace>" apply (fastforce simp: corres_underlying_def valid_def no_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying R nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>; nf \<Longrightarrow> no_fail P f\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> R \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> f' \<lbrace>\<lambda>rv' s'. \<exists>rv s. (s, s') \<in> R \<and> r rv rv' \<and> Q rv s \<and> Q' rv' s'\<rbrace> proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma corres_nofail:
  "corres_underlying state_relation nf True r P P' f g \<Longrightarrow> (nf \<Longrightarrow> no_fail P f) \<Longrightarrow>
  no_fail (\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> P' s') g" by (fastforce intro: no_fail_pre corres_u_nofail simp: ex_abs_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying state_relation nf True r P P' f g; nf \<Longrightarrow> no_fail P f\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> P s \<and> P' s') g