kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_UL

lemma corres_stateAssert_r:
  "corres_underlying sr nf nf' r P Q f (g ()) \<Longrightarrow>
   corres_underlying sr nf nf' r P (Q and P') f (stateAssert P' [] >>= g)" apply (clarsimp simp: bind_assoc stateAssert_def) apply (rule corres_symb_exec_r [OF _ get_sp]) apply (rule corres_assert_assume) apply (rule corres_assume_pre) apply (erule corres_guard_imp, clarsimp+) apply (wp | rule no_fail_pre)+ done

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

lemma corres_assert:
  "corres_underlying sr nf nf' dc (%_. P) (%_. Q) (assert P) (assert Q)" by (clarsimp simp add: corres_underlying_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' dc (\<lambda>_. P) (\<lambda>_. Q) (assert P) (assert Q)
theory Corres_UL

lemma corres_split2:
  assumes corr: "corres_underlying sr nf nf' (\<lambda>(a, b).\<lambda>(a', b'). r a a' b b') P P'
                        (do a \<leftarrow> F; b \<leftarrow> G; return (a, b) od)
                        (do a' \<leftarrow> F'; b' \<leftarrow> G'; return (a', b') od)"
  and     corr': "\<And>a a' b b'. \<lbrakk> r a a' b b'\<rbrakk>
                     \<Longrightarrow> corres_underlying sr nf nf' r1 (P1 a b) (P1' a' b') (H a b) (H' a' b')"
  and       h1: "\<lbrace>P\<rbrace> do fx \<leftarrow> F; gx \<leftarrow> G; return (fx, gx) od \<lbrace>\<lambda>rv. P1 (fst rv) (snd rv)\<rbrace>"
  and       h2: "\<lbrace>P'\<rbrace> do fx \<leftarrow> F'; gx \<leftarrow> G'; return (fx, gx) od \<lbrace>\<lambda>rv. P1' (fst rv) (snd rv)\<rbrace>"
  shows "corres_underlying sr nf nf' r1 P P'
                (do a \<leftarrow> F; b \<leftarrow> G; H a b od)
                (do a' \<leftarrow> F'; b' \<leftarrow> G'; H' a' b' od)" proof - have "corres_underlying sr nf nf' r1 P P'
               (do a \<leftarrow> F; b \<leftarrow> G; rv \<leftarrow> return (a, b); H (fst rv) (snd rv) od)
               (do a' \<leftarrow> F'; b' \<leftarrow> G'; rv' \<leftarrow> return (a', b'); H' (fst rv') (snd rv') od)" by (rule corres_underlying_split [OF corr corr', simplified bind_assoc, OF _ h1 h2])
   (simp add: split_beta split_def) thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- F;
G >>= H a
od) (do a' <- F';
G' >>= H' a'
od) proof (state)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- F;
G >>= H a
od) (do a' <- F';
G' >>= H' a'
od) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- F;
b <- G;
rv <- return (a, b);
H (fst rv) (snd rv)
od) (do a' <- F';
b' <- G';
rv' <- return (a', b');
H' (fst rv') (snd rv')
od) proof (state)
this:
corres_underlying sr nf nf' r1 P P' (do a <- F;
b <- G;
rv <- return (a, b);
H (fst rv) (snd rv)
od) (do a' <- F';
b' <- G';
rv' <- return (a', b');
H' (fst rv') (snd rv')
od)

goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- F;
G >>= H a
od) (do a' <- F';
G' >>= H' a'
od) proof (prove)
using this:
corres_underlying sr nf nf' r1 P P' (do a <- F;
b <- G;
rv <- return (a, b);
H (fst rv) (snd rv)
od) (do a' <- F';
b' <- G';
rv' <- return (a', b');
H' (fst rv') (snd rv')
od)

goal (1 subgoal):
 1. corres_underlying sr nf nf' r1 P P' (do a <- F;
G >>= H a
od) (do a' <- F';
G' >>= H' a'
od) proof (state)
this:
corres_underlying sr nf nf' r1 P P' (do a <- F;
G >>= H a
od) (do a' <- F';
G' >>= H' a'
od)

goal:
No subgoals!
theory Corres_UL

lemma corres_inst: "corres_underlying sr nf nf' r P P' f g \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" .

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

lemma corres_assert_opt_assume:
  assumes "\<And>x. P' = Some x \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g x)"
  assumes "\<And>s. Q s \<Longrightarrow> P' \<noteq> None"
  shows "corres_underlying sr nf nf' r P Q f (assert_opt P' >>= g)" using assms by (auto simp: bind_def assert_opt_def assert_def fail_def return_def
                 corres_underlying_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P Q f (assert_opt P' >>= g) proof (prove)
using this:
P' = Some ?x \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ?x)
Q ?s \<Longrightarrow> P' \<noteq> None

goal (1 subgoal):
 1. corres_underlying sr nf nf' r P Q f (assert_opt P' >>= g)
theory Corres_UL

lemma corres_assert_opt[corres]:
  "r x x' \<Longrightarrow>
  corres_underlying sr nf nf' (\<lambda>x x'. r (Some x) x') (\<lambda>s. x \<noteq> None) \<top> (assert_opt x) (return x')" unfolding corres_underlying_def by (clarsimp simp: assert_opt_def return_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r x x' \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>x. r (Some x)) (\<lambda>s. x \<noteq> None) (\<lambda>_. True) (assert_opt x) (return x') proof (prove)
goal (1 subgoal):
 1. r x x' \<Longrightarrow> \<forall>(s, s')\<in>sr. x \<noteq> None \<and> True \<longrightarrow> (nf \<longrightarrow> \<not> snd (assert_opt x s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (return x' s'). \<exists>(ra, t)\<in>fst (assert_opt x s). (t, t') \<in> sr \<and> r (Some ra) r') \<and> (nf' \<longrightarrow> \<not> snd (return x' s'))
theory Corres_UL

lemma assert_opt_assert_corres[corres]:
  "(x = None) = (x' = None) \<Longrightarrow>
   corres_underlying sr nf nf' (\<lambda>y _. x = Some y) (K (x \<noteq> None)) \<top>
                     (assert_opt x) (assert (\<exists>y. x' = Some y))" by (simp add: corres_underlying_def assert_opt_def return_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x = None) = (x' = None) \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>y _. x = Some y) (K (x \<noteq> None)) (\<lambda>_. True) (assert_opt x) (assert (\<exists>y. x' = Some y))
theory Corres_UL

lemma corres_assert_opt_l:
  assumes "\<And>x. P' = Some x \<Longrightarrow> corres_underlying sr nf nf' r (P x) Q (f x) g"
  shows "corres_underlying sr nf nf' r (\<lambda>s. \<exists>x. P' = Some x \<and> P x s) Q (assert_opt P' >>= f) g" using assms by (auto simp: bind_def assert_opt_def assert_def fail_def return_def corres_underlying_def
           split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (\<lambda>s. \<exists>x. P' = Some x \<and> P x s) Q (assert_opt P' >>= f) g proof (prove)
using this:
P' = Some ?x \<Longrightarrow> corres_underlying sr nf nf' r (P ?x) Q (f ?x) g

goal (1 subgoal):
 1. corres_underlying sr nf nf' r (\<lambda>s. \<exists>x. P' = Some x \<and> P x s) Q (assert_opt P' >>= f) g
theory Corres_UL

lemma corres_gets_the_gets:
  "corres_underlying sr False nf' r P P' (gets_the f) f' \<Longrightarrow>
   corres_underlying sr nf nf' (\<lambda>x x'. x \<noteq> None \<and> r (the x) x') P P' (gets f) f'" apply (simp add: gets_the_def bind_def simpler_gets_def assert_opt_def) apply (fastforce simp: corres_underlying_def in_monad split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False nf' r P P' (gets_the f) f' \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>x x'. x \<noteq> None \<and> r (the x) x') P P' (gets f) f' proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False nf' r P P' (\<lambda>s. (case f s of None \<Rightarrow> fail | Some x \<Rightarrow> return x) s) f' \<Longrightarrow> corres_underlying sr nf nf' (\<lambda>x x'. (\<exists>y. x = Some y) \<and> r (the x) x') P P' (\<lambda>s. ({(f s, s)}, False)) f' proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_fail:
  assumes no_fail: "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P s; P' s'; nf' \<rbrakk> \<Longrightarrow> False"
  shows "corres_underlying sr nf nf' R P P' f fail" using no_fail by (auto simp add: corres_underlying_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' R P P' f fail proof (prove)
using this:
\<lbrakk>(?s, ?s') \<in> sr; P ?s; P' ?s'; nf'\<rbrakk> \<Longrightarrow> False

goal (1 subgoal):
 1. corres_underlying sr nf nf' R P P' f fail
theory Corres_UL

lemma corres_returnOk:
  "(\<And>s s'. \<lbrakk> (s,s') \<in> sr; P s; P' s' \<rbrakk> \<Longrightarrow> r x y) \<Longrightarrow>
  corres_underlying sr nf nf' (r' \<oplus> r) P P' (returnOk x) (returnOk y)" apply (rule corres_noopE) apply wp apply clarsimp apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r x y) \<Longrightarrow> corres_underlying sr nf nf' (r' \<oplus> r) P P' (returnOk x) (returnOk y) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r x y; P s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. (s, s') \<in> sr \<and> P' s'\<rbrace> returnOk y \<lbrace>\<lambda>rv s'. (s, s') \<in> sr \<and> r x rv\<rbrace>, \<lbrace>\<lambda>r s. False\<rbrace>
 2. \<And>s. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r x y; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') (returnOk y) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r x y; P s; (s, sa) \<in> sr \<and> P' sa\<rbrakk> \<Longrightarrow> (s, sa) \<in> sr \<and> r x y
 2. \<And>s. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r x y; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') (returnOk y) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> r x y; P s; nf'\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s'. (s, s') \<in> sr \<and> P' s') (returnOk y) proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_returnOkTT:
  "r x y \<Longrightarrow> corres_underlying sr nf nf' (r' \<oplus> r) \<top> \<top> (returnOk x) (returnOk y)" by (simp add: corres_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r x y \<Longrightarrow> corres_underlying sr nf nf' (r' \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (returnOk x) (returnOk y)
theory Corres_UL

lemma corres_throwErrorTT:
  "r x y \<Longrightarrow> corres_underlying sr nf nf' (r \<oplus> r') \<top> \<top> (throwError x) (throwError y)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r x y \<Longrightarrow> corres_underlying sr nf nf' (r \<oplus> r') (\<lambda>_. True) (\<lambda>_. True) (throwError x) (throwError y)
theory Corres_UL

lemma corres_False [simp, corres_no_simp]:
  "corres_underlying sr nf nf' r P \<bottom> f f'" by (simp add: corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P (\<lambda>_. False) f f'
theory Corres_UL

lemma corres_liftME[simp]:
  "corres_underlying sr nf nf' (f \<oplus> r) P P' (liftME fn m) m'
   = corres_underlying sr nf nf' (f \<oplus> (r \<circ> fn)) P P' m m'" apply (simp add: liftME_liftM) apply (rule corres_cong [OF refl refl refl refl]) apply (case_tac x, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r) P P' (liftME fn m) m' = corres_underlying sr nf nf' (f \<oplus> (r \<circ> fn)) P P' m m' proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r \<circ> case_sum Inl (Inr \<circ> fn)) P P' m m' = corres_underlying sr nf nf' (f \<oplus> (r \<circ> fn)) P P' m m' proof (prove)
goal (1 subgoal):
 1. \<And>x y s t s' t'. \<lbrakk>P s; P' t; (s', t') \<in> sr; (x, s') \<in> fst (m s); (y, t') \<in> fst (m' t)\<rbrakk> \<Longrightarrow> (f \<oplus> r \<circ> case_sum Inl (Inr \<circ> fn)) x y = (f \<oplus> (r \<circ> fn)) x y proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_liftME2[simp]:
  "corres_underlying sr nf nf' (f \<oplus> r) P P' m (liftME fn m')
   = corres_underlying sr nf nf' (f \<oplus> (\<lambda>x. r x \<circ> fn)) P P' m m'" apply (simp add: liftME_liftM) apply (rule corres_cong [OF refl refl refl refl]) apply (case_tac y, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (f \<oplus> r) P P' m (liftME fn m') = corres_underlying sr nf nf' (f \<oplus> (\<lambda>x. r x \<circ> fn)) P P' m m' proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (\<lambda>x. (f \<oplus> r) x \<circ> case_sum Inl (Inr \<circ> fn)) P P' m m' = corres_underlying sr nf nf' (f \<oplus> (\<lambda>x. r x \<circ> fn)) P P' m m' proof (prove)
goal (1 subgoal):
 1. \<And>x y s t s' t'. \<lbrakk>P s; P' t; (s', t') \<in> sr; (x, s') \<in> fst (m s); (y, t') \<in> fst (m' t)\<rbrakk> \<Longrightarrow> ((f \<oplus> r) x \<circ> case_sum Inl (Inr \<circ> fn)) y = (f \<oplus> (\<lambda>x. r x \<circ> fn)) x y proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_assertE_assume:
  "\<lbrakk>\<And>s. P s \<longrightarrow> P'; \<And>s'. Q s' \<longrightarrow> Q'\<rbrakk> \<Longrightarrow>
   corres_underlying sr nf nf' (f \<oplus> (=)) P Q (assertE P') (assertE Q')" apply (simp add: corres_underlying_def assertE_def returnOk_def
                   fail_def return_def) by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<longrightarrow> P'; \<And>s'. Q s' \<longrightarrow> Q'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> (=)) P Q (assertE P') (assertE Q') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<longrightarrow> P'; \<And>s'. Q s' \<longrightarrow> Q'\<rbrakk> \<Longrightarrow> (P' \<longrightarrow> (Q' \<longrightarrow> (\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> (s, s') \<in> sr)) \<and> (\<not> Q' \<longrightarrow> (\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> \<not> nf'))) \<and> (\<not> P' \<longrightarrow> (Q' \<longrightarrow> (\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> nf)) \<and> (\<not> Q' \<longrightarrow> (\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> Q s' \<longrightarrow> \<not> nf \<longrightarrow> \<not> nf')))
theory Corres_UL

lemma rel_prod_apply [simp]:
  "(f \<otimes> g) (a,b) (c,d) = (f a c \<and> g b d)" by (simp add: rel_prod_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<otimes> g) (a, b) (c, d) = (f a c \<and> g b d)
theory Corres_UL

lemma select_corres_eq:
  "corres_underlying sr nf nf' (=) \<top> \<top> (select UNIV) (select UNIV)" by (simp add: corres_underlying_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (=) (\<lambda>_. True) (\<lambda>_. True) (select UNIV) (select UNIV)
theory Corres_UL

lemma corres_cases:
  "\<lbrakk> R \<Longrightarrow> corres_underlying sr nf nf' r P P' f g; \<not>R \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g \<rbrakk>
  \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') f g" by (simp add: corres_underlying_def) blast

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

lemma corres_cases':
  "\<lbrakk> R \<Longrightarrow> corres_underlying sr nf nf' r P P' f g; \<not>R \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g \<rbrakk>
  \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not>R \<longrightarrow> Q s))
                                   (\<lambda>s. (R \<longrightarrow> P' s) \<and> (\<not>R \<longrightarrow> Q' s)) f g" by (cases R; simp)

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

lemma whenE_throwError_corres_initial:
  assumes P: "frel f f'"
  assumes Q: "P = P'"
  assumes R: "\<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' m m'"
  shows      "corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q'
                     (whenE P  (throwError f ) >>=E (\<lambda>_. m ))
                     (whenE P' (throwError f') >>=E (\<lambda>_. m'))" unfolding whenE_def apply (cases P) apply (simp add: P Q) apply (simp add: Q) apply (rule R) apply (simp add: Q) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' (doE _ <- whenE P (throwError f);
m
odE) (doE _ <- whenE P' (throwError f');
m'
odE) proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (2 subgoals):
 1. P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE)
 2. \<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (1 subgoal):
 1. \<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' (doE _ <- if P then throwError f else returnOk ();
m
odE) (doE _ <- if P' then throwError f' else returnOk ();
m'
odE) proof (prove)
goal (1 subgoal):
 1. \<not> P' \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' m m' proof (prove)
goal (1 subgoal):
 1. \<not> P' \<Longrightarrow> \<not> P proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma whenE_throwError_corres:
  assumes P: "frel f f'"
  assumes Q: "P = P'"
  assumes R: "\<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) Q Q' m m'"
  shows      "corres_underlying sr nf nf' (frel \<oplus> rvr) (\<lambda>s. \<not> P \<longrightarrow> Q s) (\<lambda>s. \<not> P' \<longrightarrow> Q' s)
                     (whenE P  (throwError f ) >>=E (\<lambda>_. m ))
                     (whenE P' (throwError f') >>=E (\<lambda>_. m'))" apply (rule whenE_throwError_corres_initial) apply (simp_all add: P Q R) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (frel \<oplus> rvr) (\<lambda>s. \<not> P \<longrightarrow> Q s) (\<lambda>s. \<not> P' \<longrightarrow> Q' s) (doE _ <- whenE P (throwError f);
m
odE) (doE _ <- whenE P' (throwError f');
m'
odE) proof (prove)
goal (3 subgoals):
 1. frel f f'
 2. P = P'
 3. \<not> P \<Longrightarrow> corres_underlying sr nf nf' (frel \<oplus> rvr) (\<lambda>s. \<not> P \<longrightarrow> Q s) (\<lambda>s. \<not> P' \<longrightarrow> Q' s) m m' proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma option_corres:
  assumes None: "\<lbrakk> x = None; x' = None \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' (A None) (C None)"
  assumes Some: "\<And>z z'. \<lbrakk> x = Some z; x' = Some z' \<rbrakk> \<Longrightarrow>
             corres_underlying sr nf nf' r (Q z) (Q' z') (A (Some z)) (C (Some z'))"
  assumes None_eq: "(x = None) = (x' = None)"
  shows "corres_underlying sr nf nf' r (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>z. x = Some z \<longrightarrow> Q z s))
                  (\<lambda>s. (x' = None \<longrightarrow> P' s) \<and> (\<forall>z. x' = Some z \<longrightarrow> Q' z s))
                  (A x) (C x')" apply (cases x; cases x'; simp add: assms) apply (simp add: None flip: None_eq) apply (simp flip: None_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (\<lambda>s. (x = None \<longrightarrow> P s) \<and> (\<forall>z. x = Some z \<longrightarrow> Q z s)) (\<lambda>s. (x' = None \<longrightarrow> P' s) \<and> (\<forall>z. x' = Some z \<longrightarrow> Q' z s)) (A x) (C x') proof (prove)
goal (2 subgoals):
 1. x' = None \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. P s \<and> (\<forall>z. x = Some z \<longrightarrow> Q z s)) P' (A x) (C None)
 2. \<And>a. \<lbrakk>x = Some a; x' = None\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q a) P' (A (Some a)) (C None) proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>x = Some a; x' = None\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (Q a) P' (A (Some a)) (C None) proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_bind_return:
 "corres_underlying sr nf nf' r P P' (f >>= return) g \<Longrightarrow>
  corres_underlying sr nf nf' r P P' f g" by (simp add: corres_underlying_def)

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

lemma corres_bind_return2:
  "corres_underlying sr nf nf' r P P' f (g >>= return) \<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' f (g >>= return) \<Longrightarrow> corres_underlying sr nf nf' r P P' f g