kings-crown/FVELER_Isabelle huggingface dataset:
theory HaskellLemmaBucket

lemma set_tails_set: "(set (tails v) \<subseteq> {x. set x \<subseteq> S}) = (set v \<subseteq> S)" apply (induct v, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (set (tails v) \<subseteq> {x. set x \<subseteq> S}) = (set v \<subseteq> S) proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma filter_assocs_Cons:
  fixes v :: "('a :: len) word" shows
  "\<lbrakk> f (v, g v); \<forall>x < v. \<not> f (x, g x) \<rbrakk> \<Longrightarrow>
     filter f (assocs g) = (v, g v) # tl (filter f (assocs g))" apply (simp add: assocs_def) apply (cut_tac v=v in enum_word_div) apply clarsimp apply (subst map_cong [OF _ refl], assumption)+ apply (simp(no_asm)) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (v, g v); \<forall>x<v. \<not> f (x, g x)\<rbrakk> \<Longrightarrow> filter f (assocs g) = (v, g v) # tl (filter f (assocs g)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (v, g v); \<forall>x<v. \<not> f (x, g x)\<rbrakk> \<Longrightarrow> filter f (map (\<lambda>x. (x, g x)) enum) = (v, g v) # tl (filter f (map (\<lambda>x. (x, g x)) enum)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f (v, g v); \<forall>x<v. \<not> f (x, g x); \<exists>xs ys. enum = xs @ [v] @ ys \<and> (\<forall>x\<in>set xs. x < v) \<and> (\<forall>y\<in>set ys. v < y)\<rbrakk> \<Longrightarrow> filter f (map (\<lambda>x. (x, g x)) enum) = (v, g v) # tl (filter f (map (\<lambda>x. (x, g x)) enum)) proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>f (v, g v); \<forall>x<v. \<not> f (x, g x); enum = xs @ v # ys; \<forall>x\<in>set xs. x < v; \<forall>y\<in>set ys. v < y\<rbrakk> \<Longrightarrow> filter f (map (\<lambda>x. (x, g x)) enum) = (v, g v) # tl (filter f (map (\<lambda>x. (x, g x)) enum)) proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>f (v, g v); \<forall>x<v. \<not> f (x, g x); enum = xs @ v # ys; \<forall>x\<in>set xs. x < v; \<forall>y\<in>set ys. v < y\<rbrakk> \<Longrightarrow> filter f (map (\<lambda>x. (x, g x)) (xs @ v # ys)) = (v, g v) # tl (filter f (map (\<lambda>x. (x, g x)) (xs @ v # ys))) proof (prove)
goal (1 subgoal):
 1. \<And>xs ys. \<lbrakk>f (v, g v); \<forall>x<v. \<not> f (x, g x); enum = xs @ v # ys; \<forall>x\<in>set xs. x < v; \<forall>y\<in>set ys. v < y\<rbrakk> \<Longrightarrow> (f (v, g v) \<longrightarrow> filter f (map (\<lambda>x. (x, g x)) xs) @ (v, g v) # filter f (map (\<lambda>x. (x, g x)) ys) = (v, g v) # tl (filter f (map (\<lambda>x. (x, g x)) xs) @ (v, g v) # filter f (map (\<lambda>x. (x, g x)) ys))) \<and> (\<not> f (v, g v) \<longrightarrow> filter f (map (\<lambda>x. (x, g x)) xs) @ filter f (map (\<lambda>x. (x, g x)) ys) = (v, g v) # tl (filter f (map (\<lambda>x. (x, g x)) xs) @ filter f (map (\<lambda>x. (x, g x)) ys))) proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma snd_stateAssert_after:
  "\<not> snd ((do _ \<leftarrow> f; stateAssert R vs od) s) \<Longrightarrow>
  \<not>snd (f s) \<and> (\<forall>(rv, s') \<in> fst (f s). R s')" apply (clarsimp simp: bind_def stateAssert_def get_def assert_def
      return_def fail_def split_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> snd ((do _ <- f;
stateAssert R vs
od) s) \<Longrightarrow> \<not> snd (f s) \<and> (\<forall>(rv, s')\<in>fst (f s). R s') proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma oblivious_stateAssert [simp]:
  "oblivious f (stateAssert g xs) = (\<forall>s. g (f s) = g s)" apply (simp add: oblivious_def stateAssert_def exec_get
                   assert_def return_def fail_def split: if_split) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious f (stateAssert g xs) = (\<forall>s. g (f s) = g s) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. (g (f s) \<longrightarrow> g s) \<and> (\<not> g (f s) \<longrightarrow> \<not> g s)) = (\<forall>s. g (f s) = g s) proof (prove)
goal:
No subgoals!
theory HaskellLemmaBucket

lemma stateAssert_def2:
  "stateAssert f xs = do v \<leftarrow> gets f; if v then return () else fail od" by (simp add: stateAssert_def gets_def assert_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. stateAssert f xs = do v <- gets f;
if v then return () else fail
od
theory Corres_UL

lemma corres_underlyingI:
  assumes rv: "\<And>s t rv' t'. \<lbrakk>(s, t) \<in> R; P s; P' t; (rv', t') \<in> fst (c t)\<rbrakk>
                            \<Longrightarrow> \<exists>(rv, s') \<in> fst (a s). (s', t') \<in> R \<and> r rv rv'"
  and     nf: "\<And>s t. \<lbrakk>(s, t) \<in> R; P s; P' t; nf'\<rbrakk> \<Longrightarrow> \<not> snd (c t)"
  shows  "corres_underlying R nf nf' r P P' a c" unfolding corres_underlying_def using rv nf by (auto simp: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying R nf nf' r P P' a c proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>R. P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (c s'). \<exists>(ra, t)\<in>fst (a s). (t, t') \<in> R \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s')) proof (prove)
using this:
\<lbrakk>(?s, ?t) \<in> R; P ?s; P' ?t; (?rv', ?t') \<in> fst (c ?t)\<rbrakk> \<Longrightarrow> \<exists>(rv, s')\<in>fst (a ?s). (s', ?t') \<in> R \<and> r rv ?rv'
\<lbrakk>(?s, ?t) \<in> R; P ?s; P' ?t; nf'\<rbrakk> \<Longrightarrow> \<not> snd (c ?t)

goal (1 subgoal):
 1. \<forall>(s, s')\<in>R. P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (c s'). \<exists>(ra, t)\<in>fst (a s). (t, t') \<in> R \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s'))
theory Corres_UL

lemma corres_underlyingE:
  assumes cul: "corres_underlying R nf nf' r P P' a c"
  and     xin: "(s, t) \<in> R" "P s" "P' t" "(rv', t') \<in> fst (c t)"
  and      rl: "\<And>s' rv. \<lbrakk>nf' \<longrightarrow> \<not> snd (c t); (rv, s') \<in> fst (a s); (s', t') \<in> R; r rv rv'\<rbrakk> \<Longrightarrow> Q"
  and      nf: "nf \<longrightarrow> \<not> snd (a s)"
  shows   "Q" using cul xin nf unfolding corres_underlying_def by (fastforce simp: split_def intro: rl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q proof (prove)
using this:
corres_underlying R nf nf' r P P' a c
(s, t) \<in> R
P s
P' t
(rv', t') \<in> fst (c t)
nf \<longrightarrow> \<not> snd (a s)

goal (1 subgoal):
 1. Q proof (prove)
using this:
\<forall>(s, s')\<in>R. P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (a s)) \<longrightarrow> (\<forall>(r', t')\<in>fst (c s'). \<exists>(ra, t)\<in>fst (a s). (t, t') \<in> R \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (c s'))
(s, t) \<in> R
P s
P' t
(rv', t') \<in> fst (c t)
nf \<longrightarrow> \<not> snd (a s)

goal (1 subgoal):
 1. Q
theory Corres_UL

lemma corres_underlyingD:
  "\<lbrakk> corres_underlying R nf nf' rs P P' f f'; (s,s') \<in> R; P s; P' s'; nf \<longrightarrow> \<not> snd (f s) \<rbrakk>
  \<Longrightarrow> (\<forall>(r',t')\<in>fst (f' s'). \<exists>(r,t)\<in>fst (f s). (t, t') \<in> R \<and> rs r r') \<and> (nf' \<longrightarrow> \<not> snd (f' s'))" by (fastforce simp: corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying R nf nf' rs P P' f f'; (s, s') \<in> R; P s; P' s'; nf \<longrightarrow> \<not> snd (f s)\<rbrakk> \<Longrightarrow> (\<forall>(r', t')\<in>fst (f' s'). \<exists>(r, t)\<in>fst (f s). (t, t') \<in> R \<and> rs r r') \<and> (nf' \<longrightarrow> \<not> snd (f' s'))
theory Corres_UL

lemma corres_underlyingD2:
  "\<lbrakk> corres_underlying R nf nf' rs P P' f f'; (s,s') \<in> R; P s; P' s'; (r',t')\<in>fst (f' s'); nf \<longrightarrow> \<not> snd (f s) \<rbrakk>
  \<Longrightarrow> \<exists>(r,t)\<in>fst (f s). (t, t') \<in> R \<and> rs r r'" by (fastforce dest: corres_underlyingD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying R nf nf' rs P P' f f'; (s, s') \<in> R; P s; P' s'; (r', t') \<in> fst (f' s'); nf \<longrightarrow> \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>(r, t)\<in>fst (f s). (t, t') \<in> R \<and> rs r r'
theory Corres_UL

lemma propagate_no_fail:
  "\<lbrakk> corres_underlying S nf True R P P' f f';
        no_fail P f; \<forall>s'. P' s' \<longrightarrow> (\<exists>s. P s \<and> (s,s') \<in> S) \<rbrakk>
  \<Longrightarrow> no_fail P' f'" apply (clarsimp simp: corres_underlying_def no_fail_def) apply (erule allE, erule (1) impE) apply clarsimp apply (drule (1) bspec, clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying S nf True R P P' f f'; no_fail P f; \<forall>s'. P' s' \<longrightarrow> (\<exists>s. P s \<and> (s, s') \<in> S)\<rbrakk> \<Longrightarrow> no_fail P' f' proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r') \<and> \<not> snd (f' s'); \<forall>s. P s \<longrightarrow> \<not> snd (f s); \<forall>s'. P' s' \<longrightarrow> (\<exists>s. P s \<and> (s, s') \<in> S); P' s; snd (f' s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r') \<and> \<not> snd (f' s'); \<forall>s. P s \<longrightarrow> \<not> snd (f s); P' s; snd (f' s); \<exists>sa. P sa \<and> (sa, s) \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>\<forall>x\<in>S. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> S \<and> R r r') \<and> \<not> snd (f' s'); \<forall>s. P s \<longrightarrow> \<not> snd (f s); P' s; snd (f' s); P sa; (sa, s) \<in> S\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_singleton:
 "corres_underlying sr nf nf' r P P' (\<lambda>s. ({(R s, S s)},x)) (\<lambda>s. ({(R' s, S' s)},False))
  = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<and> (nf \<longrightarrow> \<not> x)
          \<longrightarrow> ((S s, S' s') \<in> sr \<and> r (R s) (R' s')))" by (auto simp: corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (\<lambda>s. ({(R s, S s)}, x)) (\<lambda>s. ({(R' s, S' s)}, False)) = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<and> (nf \<longrightarrow> \<not> x) \<longrightarrow> (S s, S' s') \<in> sr \<and> r (R s) (R' s'))
theory Corres_UL

lemma corres_return[simp, corres_no_simp]:
  "corres_underlying sr nf nf' r P P' (return a) (return b) =
   ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r a b)" by (simp add: return_def corres_singleton)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (return a) (return b) = ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r a b)
theory Corres_UL

lemma corres_get[simp, corres_no_simp]:
 "corres_underlying sr nf nf' r P P' get get = (\<forall> s s'. (s, s') \<in> sr \<and> P s \<and> P' s' \<longrightarrow> r s s')" by (fastforce simp: get_def corres_singleton)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' get get = (\<forall>s s'. (s, s') \<in> sr \<and> P s \<and> P' s' \<longrightarrow> r s s')
theory Corres_UL

lemma corres_gets[simp, corres_no_simp]:
 "corres_underlying sr nf nf' r P P' (gets a) (gets b) =
  (\<forall> s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (a s) (b s'))" by (simp add: simpler_gets_def corres_singleton)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (gets a) (gets b) = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (a s) (b s'))
theory Corres_UL

lemma corres_throwError[simp, corres_no_simp]:
  "corres_underlying sr nf nf' r P P' (throwError a) (throwError b) =
   ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r (Inl a) (Inl b))" by (simp add: throwError_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (throwError a) (throwError b) = ((\<exists>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr) \<longrightarrow> r (Inl a) (Inl b))
theory Corres_UL

lemma corres_no_failI_base:
  assumes f: "nf \<Longrightarrow> no_fail P f"
  assumes f': "nf' \<Longrightarrow> no_fail P' f'"
  assumes corres: "\<forall>(s, s') \<in> S. P s \<and> P' s' \<longrightarrow>
                     (\<forall>(r', t') \<in> fst (f' s'). \<exists>(r, t) \<in> fst (f s). (t, t') \<in> S \<and> R r r')"
  shows "corres_underlying S nf nf' R P P' f f'" using assms by (simp add: corres_underlying_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying S nf nf' R P P' f f' proof (prove)
using this:
nf \<Longrightarrow> no_fail P f
nf' \<Longrightarrow> no_fail P' f'
\<forall>(s, s')\<in>S. P s \<and> P' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (f' s'). \<exists>(r, t)\<in>fst (f s). (t, t') \<in> S \<and> R r r')

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

lemma corres_no_failI:
  assumes f': "nf' \<Longrightarrow> no_fail P' f'"
  assumes corres: "\<forall>(s, s') \<in> S. P s \<and> P' s' \<longrightarrow>
                     (\<forall>(r', t') \<in> fst (f' s'). \<exists>(r, t) \<in> fst (f s). (t, t') \<in> S \<and> R r r')"
  shows "corres_underlying S False nf' R P P' f f'" using assms by (simp add: corres_underlying_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying S False nf' R P P' f f' proof (prove)
using this:
nf' \<Longrightarrow> no_fail P' f'
\<forall>(s, s')\<in>S. P s \<and> P' s' \<longrightarrow> (\<forall>(r', t')\<in>fst (f' s'). \<exists>(r, t)\<in>fst (f s). (t, t') \<in> S \<and> R r r')

goal (1 subgoal):
 1. corres_underlying S False nf' R P P' f f'
theory Corres_UL

lemma corres_cong:
  assumes "\<And>s. P s = P' s"
  assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q s' = Q' s'"
  assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s; Q' s' \<rbrakk> \<Longrightarrow> f s = f' s"
  assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s; Q' s' \<rbrakk>  \<Longrightarrow> g s' = g' s'"
  assumes "\<And>x y s t s' t'. \<lbrakk> P' s; Q' t; (s', t') \<in> sr;
                             (x, s') \<in> fst (f' s); (y, t') \<in> fst (g' t) \<rbrakk> \<Longrightarrow> r x y = r' x y"
  shows   "corres_underlying sr nf nf' r P Q f g = corres_underlying sr nf nf' r' P' Q' f' g'" by (force simp: corres_underlying_def assms split_def)

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

lemma stronger_corres_guard_imp[corres_pre]:
  assumes x: "corres_underlying sr nf nf' r Q Q' f g"
  assumes y: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> Q s"
  assumes z: "\<And>s s'. \<lbrakk> P s; P' s'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> Q' s'"
  shows      "corres_underlying sr nf nf' r P P' f g" using x by (auto simp: y z corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' f g proof (prove)
using this:
corres_underlying sr nf nf' r Q Q' f g

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

lemma corres_guard_imp2:
  "\<lbrakk>corres_underlying sr nf nf' r Q P' f g; \<And>s. P s \<Longrightarrow> Q s\<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" by corres_pre

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

lemma corres_guard2_imp:
  "\<lbrakk>corres_underlying sr nf nf' r P Q' f g; \<And>s. P' s \<Longrightarrow> Q' s\<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r P P' f g" by corres_pre

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

lemma corres_rel_imp[corres_rrel_pre]:
  assumes x: "corres_underlying sr nf nf' r' P P' f g"
  assumes y: "\<And>x y. r' x y \<Longrightarrow> r x y"
  shows      "corres_underlying sr nf nf' r P P' f g" apply (insert x) apply (simp add: corres_underlying_def) apply clarsimp apply (drule (1) bspec, clarsimp) apply (drule (1) bspec, clarsimp) apply (blast intro: y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' f g 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 proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (g s'). case x of (r'a, t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> r' r r'a) \<and> (nf' \<longrightarrow> \<not> snd (g s')) \<Longrightarrow> \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (g s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (g s')) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (g s'). case x of (r'a, t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> r' r r'a) \<and> (nf' \<longrightarrow> \<not> snd (g s')); (a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (g b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra r') \<and> (nf' \<longrightarrow> \<not> snd (g b)) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); \<forall>x\<in>fst (g b). case x of (r'a, t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> r' r r'a; nf' \<longrightarrow> \<not> snd (g b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> sr \<and> r ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); (aa, ba) \<in> fst (g b); nf' \<longrightarrow> \<not> snd (g b); (ab, bb) \<in> fst (f a); (bb, ba) \<in> sr; r' ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> sr \<and> r ra aa proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_split_forwards:
  assumes ac: "corres_underlying sr nf nf' r' P P' a c"
  assumes valid: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>"
  assumes bd: "\<And>rv rv'. r' rv rv' \<Longrightarrow>
                        corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')"
  shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" using assms apply - apply (rule corres_split) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
using this:
corres_underlying sr nf nf' r' P P' a c
\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>
\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>
r' ?rv ?rv' \<Longrightarrow> corres_underlying sr nf nf' r (R ?rv) (R' ?rv') (b ?rv) (d ?rv')

goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' ?r'5 P P' a c
 2. \<And>rv rv'. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv'); ?r'5 rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (?R5 rv) (?R'5 rv') (b rv) (d rv')
 3. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')\<rbrakk> \<Longrightarrow> \<lbrace>Q\<rbrace> a \<lbrace>?R5\<rbrace>
 4. \<lbrakk>corres_underlying sr nf nf' r' P P' a c; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>; \<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv')\<rbrakk> \<Longrightarrow> \<lbrace>Q'\<rbrace> c \<lbrace>?R'5\<rbrace> proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma rel_sum_comb_r2[simp]:
  "(f \<oplus> g) x (Inr y) = (\<exists>x'. x = Inr x' \<and> g x' y)" apply (case_tac x, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<oplus> g) x (Inr y) = (\<exists>x'. x = Inr x' \<and> g x' y) proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma rel_sum_comb_l2[simp]:
  "(f \<oplus> g) x (Inl y) = (\<exists>x'. x = Inl x' \<and> f x' y)" apply (case_tac x, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<oplus> g) x (Inl y) = (\<exists>x'. x = Inl x' \<and> f x' y) proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_split_eqr:
  assumes x: "corres_underlying sr nf nf' (=) P P' a c"
  assumes y: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' rv) (b rv) (d rv)"
  assumes z: "\<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>" "\<lbrace>Q'\<rbrace> c \<lbrace>R'\<rbrace>"
  shows      "corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= (\<lambda>rv. b rv)) (c >>= d)" apply (rule corres_split[OF x _ z]) apply (simp add: y) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r (P and Q) (P' and Q') (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. rv = rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv') proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma dc_simp[simp]: "dc a b" by (simp add: dc_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dc a b
theory Corres_UL

lemma dc_o_simp1[simp]: "dc \<circ> f = dc" by (simp add: dc_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dc \<circ> f = dc
theory Corres_UL

lemma dc_o_simp2[simp]: "dc x \<circ> f = dc x" by (simp add: dc_def o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dc x \<circ> f = dc x