kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_UL

lemma unit_dc_is_eq:
  "(dc::unit\<Rightarrow>_\<Rightarrow>_) = (=)" by (fastforce simp: dc_def)

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

lemma corres_split_norE:
  "\<lbrakk> corres_underlying sr nf nf' (f \<oplus> dc) P P' a c; corres_underlying sr nf nf' (f \<oplus> r) R R' b d;
     \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>x. R\<rbrace>, \<lbrace>\<top>\<top>\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>x. R'\<rbrace>,\<lbrace>\<top>\<top>\<rbrace> \<rbrakk>
  \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (a >>=E (\<lambda>rv. b)) (c >>=E (\<lambda>rv. d))" apply (rule corres_splitEE, assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' (f \<oplus> dc) P P' a c; corres_underlying sr nf nf' (f \<oplus> r) R R' b d; \<lbrace>Q\<rbrace> a \<lbrace>\<lambda>x. R\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<lbrace>Q'\<rbrace> c \<lbrace>\<lambda>x. R'\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (f \<oplus> r) (P and Q) (P' and Q') (doE rv <- a;
b
odE) (doE rv <- c;
d
odE) proof (prove)
goal:
No subgoals!
theory Corres_UL

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

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

lemma corres_split_mapr:
  assumes y: "corres_underlying sr nf nf' ((=) \<circ> f) P P' a c"
  assumes x: "\<And>rv. corres_underlying sr nf nf' r (R rv) (R' (f rv)) (b rv) (d (f 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 y _ z]) apply simp apply (simp add: x) 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'. ((=) \<circ> f) rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (R rv) (R' rv') (b rv) (d rv') proof (prove)
goal (1 subgoal):
 1. \<And>rv. corres_underlying sr nf nf' r (R rv) (R' (f rv)) (b rv) (d (f rv)) proof (prove)
goal:
No subgoals!
theory Corres_UL

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

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

lemma corres_if:
  "\<lbrakk> G = G'; corres_underlying sr nf nf' r P P' a c; corres_underlying sr nf nf' r Q Q' b d \<rbrakk>
    \<Longrightarrow> corres_underlying sr nf nf' r
                (if G then P else Q) (if G' then P' else Q')
                (if G then a else b) (if G' then c else d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G = G'; corres_underlying sr nf nf' r P P' a c; corres_underlying sr nf nf' r Q Q' b d\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (if G then P else Q) (if G' then P' else Q') (if G then a else b) (if G' then c else d)
theory Corres_UL

lemma corres_whenE:
  "\<lbrakk> G = G'; corres_underlying sr nf nf' (fr \<oplus> r) P P' f g; r () () \<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' (fr \<oplus> r) (\<lambda>s. G \<longrightarrow> P s) (\<lambda>s. G' \<longrightarrow> P' s) (whenE G f) (whenE G' g)" by (simp add: whenE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G = G'; corres_underlying sr nf nf' (fr \<oplus> r) P P' f g; r () ()\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' (fr \<oplus> r) (\<lambda>s. G \<longrightarrow> P s) (\<lambda>s. G' \<longrightarrow> P' s) (whenE G f) (whenE G' g)
theory Corres_UL

lemma corres_if_r:
  "\<lbrakk> corres_underlying sr nf nf' r P P' a c; corres_underlying sr nf nf' r P Q' a d \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r (P) (if G' then P' else Q')
                                     (a) (if G' then c  else d)" by (simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' r P P' a c; corres_underlying sr nf nf' r P Q' a d\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (if G' then P' else Q') a (if G' then c else d)
theory Corres_UL

lemma corres_if3:
 "\<lbrakk> G = G';
    G \<Longrightarrow> corres_underlying sr nf nf' r P P' a c;
    \<not> G' \<Longrightarrow> corres_underlying sr nf nf' r Q Q' b d \<rbrakk>
  \<Longrightarrow> corres_underlying sr nf nf' r (if G then P else Q) (if G' then P' else Q')
                                    (if G then a else b) (if G' then c else d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G = G'; G \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; \<not> G' \<Longrightarrow> corres_underlying sr nf nf' r Q Q' b d\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (if G then P else Q) (if G' then P' else Q') (if G then a else b) (if G' then c else d)
theory Corres_UL

lemma corres_if_strong:
  "\<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; R s; R' s'\<rbrakk> \<Longrightarrow> G = G';
    \<lbrakk>G; G'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' a c;
    \<lbrakk>\<not> G; \<not> G'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r Q Q' b d \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r
         (R and (if G then P else Q)) (R' and (if G' then P' else Q'))
         (if G then a else b) (if G' then c else d)" by (fastforce simp: corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; R s; R' s'\<rbrakk> \<Longrightarrow> G = G'; \<lbrakk>G; G'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; \<lbrakk>\<not> G; \<not> G'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r Q Q' b d\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (R and (if G then P else Q)) (R' and (if G' then P' else Q')) (if G then a else b) (if G' then c else d)
theory Corres_UL

lemma corres_liftM2_simp[simp]:
  "corres_underlying sr nf nf' r P P' f (liftM t g) =
   corres_underlying sr nf nf' (\<lambda>x. r x \<circ> t) P P' f g" by (fastforce simp add: corres_underlying_def in_liftM)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' f (liftM t g) = corres_underlying sr nf nf' (\<lambda>x. r x \<circ> t) P P' f g
theory Corres_UL

lemma corres_liftE_rel_sum[simp]:
 "corres_underlying sr nf nf' (f \<oplus> r) P P' (liftE m) (liftE m') =
  corres_underlying sr nf nf' r P P' m m'" by (simp add: liftE_liftM o_def)

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

lemma corres_disj_division:
  "\<lbrakk> P \<or> Q; P \<Longrightarrow> corres_underlying sr nf nf' r R S x y; Q \<Longrightarrow> corres_underlying sr nf nf' r T U x y \<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)) (\<lambda>s. (P \<longrightarrow> S s) \<and> (Q \<longrightarrow> U s)) x y" by (safe; corres_pre, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> corres_underlying sr nf nf' r R S x y; Q \<Longrightarrow> corres_underlying sr nf nf' r T U x y\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (\<lambda>s. (P \<longrightarrow> R s) \<and> (Q \<longrightarrow> T s)) (\<lambda>s. (P \<longrightarrow> S s) \<and> (Q \<longrightarrow> U s)) x y
theory Corres_UL

lemma corres_weaker_disj_division:
  "\<lbrakk> P \<or> Q; P \<Longrightarrow> corres_underlying sr nf nf' r R S x y; Q \<Longrightarrow> corres_underlying sr nf nf' r T U x y \<rbrakk>
     \<Longrightarrow> corres_underlying sr nf nf' r (R and T) (S and U) x y" by (corres_pre, rule corres_disj_division, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<or> Q; P \<Longrightarrow> corres_underlying sr nf nf' r R S x y; Q \<Longrightarrow> corres_underlying sr nf nf' r T U x y\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r (R and T) (S and U) x y
theory Corres_UL

lemma corres_symmetric_bool_cases:
  "\<lbrakk> P = P'; \<lbrakk> P; P' \<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' r Q Q' f g;
        \<lbrakk> \<not> P; \<not> P' \<rbrakk> \<Longrightarrow> corres_underlying srel nf nf' r R R' f g \<rbrakk>
      \<Longrightarrow> corres_underlying srel nf nf' r (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s))
                                          (\<lambda>s. (P' \<longrightarrow> Q' s) \<and> (\<not> P' \<longrightarrow> R' s))
                                          f g" by (cases P, simp_all)

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

lemma corres_bind_return_r:
  "corres_underlying S nf nf' (\<lambda>x y. r x (h y)) P Q f g \<Longrightarrow>
   corres_underlying S nf nf' r P Q f (do x \<leftarrow> g; return (h x) od)" by (fastforce simp: corres_underlying_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying S nf nf' (\<lambda>x y. r x (h y)) P Q f g \<Longrightarrow> corres_underlying S nf nf' r P Q f (do x <- g;
return (h x)
od)
theory Corres_UL

lemma corres_underlying_symb_exec_l:
  "\<lbrakk> corres_underlying sr nf nf' dc P P' f (return ()); \<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h;
     \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<rbrakk>
    \<Longrightarrow> corres_underlying sr nf nf' r P P' (f >>= g) h" apply (drule corres_underlying_split) apply assumption+ apply (rule return_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying sr nf nf' dc P P' f (return ()); \<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' (f >>= g) h proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; dc rv rv'\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' ?r (?Q rv) (?Q' rv') (?b rv) (?d rv')
 2. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>?Q\<rbrace>
 3. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> return () \<lbrace>?Q'\<rbrace>
 4. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; corres_underlying sr nf nf' ?r P P' (f >>= ?b) (return () >>= ?d)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' (f >>= g) h proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> return () \<lbrace>\<lambda>rv'. P'\<rbrace>
 2. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; corres_underlying sr nf nf' r P P' (f >>= g) (do rv' <- return ();
h
od)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' (f >>= g) h proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. corres_underlying sr nf nf' r (Q rv) P' (g rv) h; \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; corres_underlying sr nf nf' r P P' (f >>= g) (do rv' <- return ();
h
od)\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P P' (f >>= g) h proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_req:
  assumes x: "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P s; P' s' \<rbrakk> \<Longrightarrow> F"
  assumes y: "F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
  shows      "corres_underlying sr nf nf' r P P' f g" apply (cases "F") apply (rule y) apply assumption apply (simp add: corres_underlying_def) apply clarsimp apply (subgoal_tac "F") apply simp apply (rule x, assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' f g proof (prove)
goal (2 subgoals):
 1. F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g
 2. \<not> F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g proof (prove)
goal (2 subgoals):
 1. F \<Longrightarrow> F
 2. \<not> F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g proof (prove)
goal (1 subgoal):
 1. \<not> F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g proof (prove)
goal (1 subgoal):
 1. \<not> F \<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>\<not> F; (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 (2 subgoals):
 1. \<And>a b. \<lbrakk>\<not> F; (a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a); F\<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))
 2. \<And>a b. \<lbrakk>\<not> F; (a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> F proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<not> F; (a, b) \<in> sr; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> F proof (prove)
goal:
No subgoals!
theory Corres_UL

lemma corres_gen_asm:
  assumes x: "F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
  shows "corres_underlying sr nf nf' r (P and (\<lambda>s. F)) P' f g" apply (rule corres_req[where F=F]) apply simp apply (rule corres_guard_imp [OF x]) apply simp+ done

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

lemma corres_gen_asm2:
  assumes x: "F \<Longrightarrow> corres_underlying sr nf nf' r P P' f g"
  shows "corres_underlying sr nf nf' r P (P' and (\<lambda>s. F)) f g" apply (rule corres_req[where F=F]) apply simp apply (rule corres_guard_imp [OF x]) apply simp+ done

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

lemma corres_trivial:
 "corres_underlying sr nf nf' r \<top> \<top> f g \<Longrightarrow> corres_underlying sr nf nf' r \<top> \<top> f g" by assumption

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

lemma corres_underlying_trivial[corres]:
  "\<lbrakk> nf' \<Longrightarrow> no_fail P' f \<rbrakk> \<Longrightarrow> corres_underlying Id nf nf' (=) \<top> P' f f" by (auto simp add: corres_underlying_def Id_def no_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (nf' \<Longrightarrow> no_fail P' f) \<Longrightarrow> corres_underlying Id nf nf' (=) (\<lambda>_. True) P' f f
theory Corres_UL

lemma corres_underlying_trivial_dc[corres]:
  "(nf' \<Longrightarrow> no_fail P' f) \<Longrightarrow> corres_underlying Id nf nf' dc (\<lambda>_. True) P' f f"
  for f :: "('s, unit) nondet_monad" by (fastforce intro: corres_underlying_trivial corres_rrel_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (nf' \<Longrightarrow> no_fail P' f) \<Longrightarrow> corres_underlying Id nf nf' dc (\<lambda>_. True) P' f f
theory Corres_UL

lemma corres_assume_pre:
  assumes R: "\<And>s s'. \<lbrakk> P s; Q s'; (s,s') \<in> sr \<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P Q f g"
  shows "corres_underlying sr nf nf' r P Q f g" apply (clarsimp simp add: corres_underlying_def) apply (frule (2) R) apply (clarsimp simp add: corres_underlying_def) apply blast done

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

lemma corres_assert_assume:
  "\<lbrakk> P' \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()); \<And>s. Q s \<Longrightarrow> P' \<rbrakk> \<Longrightarrow>
  corres_underlying sr nf nf' r P Q f (assert P' >>= g)" by (auto simp: bind_def assert_def fail_def return_def
                 corres_underlying_def)

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

lemma corres_assert_gen_asm_cross:
  "\<lbrakk> \<And>s s'. \<lbrakk>(s, s') \<in> sr; P' s; Q' s'\<rbrakk> \<Longrightarrow> A;
     A \<Longrightarrow> corres_underlying sr nf nf' r P Q f (g ()) \<rbrakk>
  \<Longrightarrow> corres_underlying sr nf nf' r (P and P') (Q and Q') f (assert A >>= g)" by (metis corres_assert_assume corres_assume_pre corres_weaker_disj_division)

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