kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_D

lemma OR_choiceE_OR[simp]: "(OR_choiceE c (f :: ('a + 'b,unit) s_monad) g) = (f \<sqinter> g)" apply (clarsimp simp: OR_choiceE_def bindE_def liftE_def) apply (clarsimp simp: alternative_def get_def select_def return_def bind_def select_f_def
                            mk_ef_def wrap_ext_unit_def wrap_ext_bool_unit_def image_def
                 split: if_split_asm) apply (rule ext, rename_tac s) apply (case_tac "f s") apply (case_tac "g s") apply clarsimp by (intro conjI set_eqI; clarsimp?; blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. OR_choiceE c f g = (f \<sqinter> g) proof (prove)
goal (1 subgoal):
 1. do r <- get;
(rv, uu_) <- select_f (mk_ef (wrap_ext_bool c r));
if rv then f else g
od = (f \<sqinter> g) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. (\<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)}, \<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s))) = (\<lambda>s. (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s))) proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)}, \<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s)) = (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. f s = (a, b) \<Longrightarrow> (\<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)}, \<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s)) = (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>f s = (a, b); g s = (aa, ba)\<rbrakk> \<Longrightarrow> (\<Union> {y. \<exists>b x. (x \<longrightarrow> (y, b) = f s) \<and> (\<not> x \<longrightarrow> (y, b) = g s)}, \<exists>a x. (x \<longrightarrow> (a, True) = f s) \<and> (\<not> x \<longrightarrow> (a, True) = g s)) = (fst (f s) \<union> fst (g s), snd (f s) \<or> snd (g s)) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>f s = (a, b); g s = (aa, ba)\<rbrakk> \<Longrightarrow> \<Union> {y. \<exists>bb x. (x \<longrightarrow> y = a \<and> bb = b) \<and> (\<not> x \<longrightarrow> y = aa \<and> bb = ba)} = a \<union> aa \<and> (\<exists>ab x. (x \<longrightarrow> ab = a \<and> b) \<and> (\<not> x \<longrightarrow> ab = aa \<and> ba)) = (b \<or> ba)
theory Corres_D

lemma corres_group_bind_rhs:
  "corres_underlying sr nf nf' rvr P P' a (do y\<leftarrow>(do f; g od); h y od)
    \<Longrightarrow> corres_underlying sr nf nf' rvr P P' a (do x \<leftarrow> f; y \<leftarrow> g; h y od)" by (simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' rvr P P' a (do f;
g
od >>= h) \<Longrightarrow> corres_underlying sr nf nf' rvr P P' a (do x <- f;
g >>= h
od)
theory Corres_D

lemma corres_expand_bind_rhs:
  "dcorres rvr P P' a (do z \<leftarrow> f; y \<leftarrow> g z; h y od)
    \<Longrightarrow> dcorres rvr P P' a (do y\<leftarrow> do z\<leftarrow>f; g z od; h y od)" by (simp add: bind_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres rvr P P' a (do z <- f;
g z >>= h
od) \<Longrightarrow> dcorres rvr P P' a (f >>= g >>= h)
theory Corres_D

lemma corres_bind_ignore_ret_rhs:
  "corres_underlying sr nf nf' rvr P P' a (do f; g od)
    \<Longrightarrow> corres_underlying sr nf nf' rvr P P' a (do y\<leftarrow> f;g od)" by (simp add: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' rvr P P' a (do f;
g
od) \<Longrightarrow> corres_underlying sr nf nf' rvr P P' a (do y <- f;
g
od)
theory Corres_D

lemma corres_free_fail:
  "dcorres c P P' f fail" by (fastforce simp: corres_underlying_def bind_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' f fail
theory Corres_D

lemma corres_free_return:
  "dcorres dc P P' (return a) (return b)" by (clarsimp simp:return_def bind_def corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc P P' (return a) (return b)
theory Corres_D

lemma corres_dummy_return_pl:
  "dcorres c P P' (do return b; f od) g \<Longrightarrow> dcorres c P P' f g" by (fastforce simp: corres_underlying_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' (do return b;
f
od) g \<Longrightarrow> dcorres c P P' f g
theory Corres_D

lemma corres_dummy_return_r:
  "dcorres c P P' f (do x\<leftarrow>g;return x od) \<Longrightarrow> dcorres c P P' f g" by (fastforce simp: corres_underlying_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' f (g >>= return) \<Longrightarrow> dcorres c P P' f g
theory Corres_D

lemma corres_dummy_return_pr:
  "dcorres c P P' f (do return b; g od)  \<Longrightarrow> dcorres c P P' f g" by (fastforce simp: corres_underlying_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' f (do return b;
g
od) \<Longrightarrow> dcorres c P P' f g
theory Corres_D

lemma corres_dummy_returnOk_r:
  "dcorres c P P' f (g >>=E returnOk) \<Longrightarrow> dcorres c P P' f g" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' f (g >>=E returnOk) \<Longrightarrow> dcorres c P P' f g
theory Corres_D

lemma corres_dummy_returnOk_pl:
  "dcorres c P P' (returnOk b >>=E (\<lambda>_. f)) g \<Longrightarrow> dcorres c P P' f g" by (fastforce simp: corres_underlying_def bindE_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' (doE _ <- returnOk b;
f
odE) g \<Longrightarrow> dcorres c P P' f g
theory Corres_D

lemma corres_dummy_get_pr:
  "dcorres c P P' f (do s\<leftarrow>get;g od)\<Longrightarrow> dcorres c P P' f g" by (fastforce simp: corres_underlying_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' f (do s <- get;
g
od) \<Longrightarrow> dcorres c P P' f g
theory Corres_D

lemma corres_dummy_get_pl:
  "dcorres c P P' (do s\<leftarrow>get;g od) f \<Longrightarrow> dcorres c P P' g f" by (fastforce simp: corres_underlying_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres c P P' (do s <- get;
g
od) f \<Longrightarrow> dcorres c P P' g f
theory Corres_D

lemma dcorres_free_throw:
  assumes "\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>"
  shows "dcorres (dc \<oplus> r) P P' Monads_D.throw f" using assms apply (simp add:corres_underlying_def throwError_def return_def) apply (clarsimp simp:validE_def valid_def) apply (drule_tac x = b in meta_spec) apply (fastforce split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> r) P P' throw f proof (prove)
using this:
\<lbrace>(=) ?s\<rbrace> f \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) ?s\<rbrace>

goal (1 subgoal):
 1. dcorres (dc \<oplus> r) P P' throw f proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrace>(=) s\<rbrace> f \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>) \<Longrightarrow> \<forall>b. P (transform b) \<and> P' b \<longrightarrow> (\<forall>x\<in>fst (f b). case x of (r', t') \<Rightarrow> transform t' = transform b \<and> (\<exists>y'. r' = Inl y')) proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<And>s. \<forall>x\<in>fst (f s). case x of (Inl e, s') \<Rightarrow> s = s' | (Inr ra, s') \<Rightarrow> False; (a, ba) \<in> fst (f b); P (transform b); P' b\<rbrakk> \<Longrightarrow> transform ba = transform b \<and> (\<exists>y'. a = Inl y') proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>(a, ba) \<in> fst (f b); P (transform b); P' b; \<forall>x\<in>fst (f b). case x of (Inl e, s') \<Rightarrow> b = s' | (Inr ra, s') \<Rightarrow> False\<rbrakk> \<Longrightarrow> transform ba = transform b \<and> (\<exists>y'. a = Inl y') proof (prove)
goal:
No subgoals!
theory Corres_D

lemma  corres_split_keep_pfx:
  assumes x: "corres_underlying sr nf nf' r' P P' a c"
  assumes y: "\<And>rv rv'. r' rv rv' \<Longrightarrow> corres_underlying sr nf nf' r (P and (Q rv)) (P' and (Q' rv')) (b rv) (d rv')"
  assumes    "\<lbrace>P\<rbrace> a \<lbrace>\<lambda>x. P and (Q x)\<rbrace>" "\<lbrace>P'\<rbrace> c \<lbrace>\<lambda>x. P' and (Q' x)\<rbrace>"
  shows      "corres_underlying sr nf nf' r P P' (a >>= (\<lambda>rv. b rv)) (c >>= (\<lambda>rv'. d rv'))" using assms by (rule corres_underlying_split)

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

goal (1 subgoal):
 1. corres_underlying sr nf nf' r P P' (a >>= b) (c >>= d)
theory Corres_D

lemma dcorres_absorb_pfx:
  assumes "dcorres r (P) (P') (f) (f')"
  shows "\<And> s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f f' " using assms by (fastforce simp:corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f f' proof (prove)
using this:
dcorres r P P' f f'

goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f f'
theory Corres_D

lemma dcorres_expand_pfx:
assumes "\<And> s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') f f' "
shows "dcorres r P P' f f'" using assms by (fastforce simp:corres_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' f f' proof (prove)
using this:
\<lbrakk>?s = transform ?s'; P ?s; P' ?s'\<rbrakk> \<Longrightarrow> dcorres r ((=) ?s) ((=) ?s') f f'

goal (1 subgoal):
 1. dcorres r P P' f f'
theory Corres_D

lemma dcorres_absorb_get_l:
  assumes "!!s'. \<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g"
  shows "dcorres rv P P' (do t\<leftarrow> get; f t od)  g" apply (rule corres_symb_exec_l [where Q="%x. P and ((=) x)"]) apply (rule dcorres_expand_pfx) apply clarsimp apply (rule assms) apply (clarsimp simp: valid_def exs_valid_def get_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres rv P P' (get >>= f) g proof (prove)
goal (4 subgoals):
 1. \<And>t. dcorres rv (P and (=) t) P' (f t) g
 2. \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. False \<Longrightarrow> no_fail P get proof (prove)
goal (4 subgoals):
 1. \<And>t s s'. \<lbrakk>s = transform s'; (P and (=) t) s; P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) s) ((=) s') (f t) g
 2. \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. False \<Longrightarrow> no_fail P get proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g
 2. \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 4. False \<Longrightarrow> no_fail P get proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> P (transform s')
 2. \<And>s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> P' s'
 3. \<And>s. P s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>P\<rbrace> get \<lbrace>\<lambda>x. P and (=) x\<rbrace>
 5. False \<Longrightarrow> no_fail P get proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_expand_get_l:
  assumes "dcorres rv P P' (do t\<leftarrow>get; f t od) g"
  shows "\<lbrakk> P (transform s'); P' s'\<rbrakk> \<Longrightarrow>
         dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g" using assms by (simp add:get_def corres_underlying_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g proof (prove)
using this:
dcorres rv P P' (get >>= f) g

goal (1 subgoal):
 1. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') (f (transform s')) g
theory Corres_D

lemma dcorres_absorb_get_r:
  assumes "!!s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform s')) ((=) s') f (g s')"
  shows "dcorres rv P P' f (do t\<leftarrow> get; g t od)" apply (rule corres_symb_exec_r [where Q'="%x. P' and ((=) x)"]) apply (rule dcorres_expand_pfx) apply clarsimp apply (rule assms) apply (clarsimp simp: valid_def exs_valid_def get_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres rv P P' f (get >>= g) proof (prove)
goal (4 subgoals):
 1. \<And>t. dcorres rv P (P' and (=) t) f (g t)
 2. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace>
 3. \<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>t s s'. \<lbrakk>s = transform s'; P s; (P' and (=) t) s'\<rbrakk> \<Longrightarrow> dcorres rv ((=) s) ((=) s') f (g t)
 2. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace>
 3. \<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail P' get proof (prove)
goal (4 subgoals):
 1. \<And>t. \<lbrakk>P (transform t); P' t\<rbrakk> \<Longrightarrow> dcorres rv ((=) (transform t)) ((=) t) f (g t)
 2. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace>
 3. \<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail P' get proof (prove)
goal (5 subgoals):
 1. \<And>t. \<lbrakk>P (transform t); P' t\<rbrakk> \<Longrightarrow> P (transform t)
 2. \<And>t. \<lbrakk>P (transform t); P' t\<rbrakk> \<Longrightarrow> P' t
 3. \<lbrace>P'\<rbrace> get \<lbrace>\<lambda>x. P' and (=) x\<rbrace>
 4. \<And>s. P' s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail P' get proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_absorb_gets_the:
  assumes A: "\<And>s' obj'. \<lbrakk>P' s';  g' s' = Some obj'; P (transform s')\<rbrakk>
          \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') (f) (f' obj')"
  shows "dcorres r P P' (f) (do a\<leftarrow> gets_the (g'); f' a od)" apply (simp add: gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp :assert_opt_def split:option.splits) apply (clarsimp simp:corres_free_fail) apply (rule dcorres_expand_pfx) apply (clarsimp simp:assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' f (gets_the g' >>= f') proof (prove)
goal (1 subgoal):
 1. dcorres r P P' f (do x <- get;
assert_opt (g' x) >>= f'
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') f (assert_opt (g' s') >>= f') proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>P (transform s'); P' s'\<rbrakk> \<Longrightarrow> (g' s' = None \<longrightarrow> dcorres r ((=) (transform s')) ((=) s') f fail) \<and> (\<forall>x2. g' s' = Some x2 \<longrightarrow> dcorres r ((=) (transform s')) ((=) s') f (f' x2)) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>P (transform s'); P' s'; g' s' = Some x2\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') f (f' x2) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2 s s'a. \<lbrakk>P (transform s'); P' s'; g' s' = Some x2; s = transform s'a; transform s' = s; s' = s'a\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s'a) f (f' x2) proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_get:
  assumes A: "\<And>s s'. \<lbrakk>s = transform s';P s; P' s'\<rbrakk>
          \<Longrightarrow> dcorres r ((=) s) ((=) s') (f s) (f' s')"
  shows "dcorres r P P' (do s\<leftarrow>get;f s od) (do s'\<leftarrow> get; f' s' od)" apply (rule dcorres_expand_pfx) apply (rule_tac r'="\<lambda>r r'. s=r \<and> s'=r'" and Q="%x. (=) s" and Q'="%x. (=) s'" in corres_split_forwards') apply (clarsimp simp: corres_underlying_def get_def) apply wp+ apply (drule A) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (get >>= f) (get >>= f') proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') (get >>= f) (get >>= f') proof (prove)
goal (4 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. s = r \<and> s' = r') ((=) s) ((=) s') get get
 2. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>x. (=) s\<rbrace>
 3. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get \<lbrace>\<lambda>x. (=) s'\<rbrace>
 4. \<And>s s' rv rv'. \<lbrakk>s = transform s'; P s; P' s'; s = rv \<and> s' = rv'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') (f rv) (f' rv') proof (prove)
goal (3 subgoals):
 1. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<lbrace>\<lambda>x. (=) s\<rbrace>
 2. \<And>s s'. \<lbrakk>s = transform s'; P s; P' s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get \<lbrace>\<lambda>x. (=) s'\<rbrace>
 3. \<And>s s' rv rv'. \<lbrakk>s = transform s'; P s; P' s'; s = rv \<and> s' = rv'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') (f rv) (f' rv') proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv rv'. \<lbrakk>s = transform s'; P s; P' s'; s = rv \<and> s' = rv'\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') (f rv) (f' rv') proof (prove)
goal (3 subgoals):
 1. \<And>s s' rv rv'. \<lbrakk>P s; P' s'; s = rv \<and> s' = rv'\<rbrakk> \<Longrightarrow> P s
 2. \<And>s s' rv rv'. \<lbrakk>P s; P' s'; s = rv \<and> s' = rv'\<rbrakk> \<Longrightarrow> P' s'
 3. \<And>s s' rv rv'. \<lbrakk>P s; P' s'; s = rv \<and> s' = rv'; dcorres r ((=) s) ((=) s') (f s) (f' s')\<rbrakk> \<Longrightarrow> dcorres r ((=) s) ((=) s') (f rv) (f' rv') proof (prove)
goal:
No subgoals!
theory Corres_D

lemma wpc_helper_dcorres:
  "dcorres r Q Q' f f'
   \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (dcorres r P P' f f')" apply (clarsimp simp: wpc_helper_def) apply (erule corres_guard_imp) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r Q Q' f f' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (dcorres r P P' f f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres r Q Q' f f'; \<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''\<rbrakk> \<Longrightarrow> dcorres r P P' f f' proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P s\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P' s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> Q s; \<forall>s. P' s \<longrightarrow> Q' s; P'' \<subseteq> Q''; P' s\<rbrakk> \<Longrightarrow> Q' s proof (prove)
goal:
No subgoals!
theory Corres_D

lemma dcorres_strengthen_lhs_guard:
  "\<lbrakk> dcorres rr P P' g g'; \<And>s. P' s \<Longrightarrow> P (transform s) \<rbrakk> \<Longrightarrow> dcorres rr \<top> P' g g'" by (rule stronger_corres_guard_imp [where Q=P and Q'=P']) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dcorres rr P P' g g'; \<And>s. P' s \<Longrightarrow> P (transform s)\<rbrakk> \<Longrightarrow> dcorres rr (\<lambda>_. True) P' g g'
theory Corres_D

lemma dcorres_throw:
  "dcorres (dc \<oplus> anyrel) \<top> \<top> (Monads_D.throw) (throwError anyerror)" by (clarsimp simp:corres_underlying_def throwError_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) throw (throwError anyerror)
theory Corres_D

lemma dcorres_alternative_throw:
  "dcorres (dc \<oplus> anyrel) \<top> \<top> (any \<sqinter> Monads_D.throw) (throwError anyerror)" by (rule corres_alternate2[OF dcorres_throw])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> anyrel) (\<lambda>_. True) (\<lambda>_. True) (any \<sqinter> throw) (throwError anyerror)
theory Corres_D

lemma dcorres_returnOk:
  "r a b \<Longrightarrow>
  dcorres (dc \<oplus> r) \<top> \<top> (returnOk a) (returnOk b)" by (clarsimp simp:corres_underlying_def return_def returnOk_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. r a b \<Longrightarrow> dcorres (dc \<oplus> r) (\<lambda>_. True) (\<lambda>_. True) (returnOk a) (returnOk b)
theory Corres_D

lemma case_sum_triv_return:
  "case_sum throwError returnOk = return" apply (intro ext) apply (simp add: throwError_def returnOk_def return_def
            split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. case_sum throwError returnOk = return proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (case x of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> returnOk x) xa = return x xa proof (prove)
goal:
No subgoals!
theory Corres_D

lemma lift_returnOk_bind_triv:
  "g >>= (lift returnOk) = g" by (simp add: lift_def case_sum_triv_return cong: bind_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. g >>= lift returnOk = g
theory Corres_D

lemma dcorres_throw_wp:
assumes "\<forall>s. \<lbrace>(=) s\<rbrace>g\<lbrace>\<lambda>r. \<bottom>\<rbrace>,\<lbrace>\<lambda>e. (=) s\<rbrace>"
shows "dcorres (dc\<oplus>anyrel) \<top> P (Monads_D.throw) g" using assms apply (clarsimp simp:throwError_def corres_underlying_def return_def validE_def valid_def) apply (drule spec) apply (drule (1) bspec) apply (clarsimp split:sum.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> anyrel) (\<lambda>_. True) P throw g proof (prove)
using this:
\<forall>s. \<lbrace>(=) s\<rbrace> g \<lbrace>\<lambda>r _. False\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>

goal (1 subgoal):
 1. dcorres (dc \<oplus> anyrel) (\<lambda>_. True) P throw g proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>s. \<forall>x\<in>fst (g s). case x of (Inl e, s') \<Rightarrow> s = s' | (Inr ra, s') \<Rightarrow> False; P b; (a, ba) \<in> fst (g b)\<rbrakk> \<Longrightarrow> transform ba = transform b \<and> (\<exists>y'. a = Inl y') proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>P b; (a, ba) \<in> fst (g b); \<forall>x\<in>fst (g (?s35 b a ba)). case x of (Inl e, s') \<Rightarrow> ?s35 b a ba = s' | (Inr ra, s') \<Rightarrow> False\<rbrakk> \<Longrightarrow> transform ba = transform b \<and> (\<exists>y'. a = Inl y') proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>P b; (a, ba) \<in> fst (g b); case (a, ba) of (Inl e, s') \<Rightarrow> b = s' | (Inr ra, s') \<Rightarrow> False\<rbrakk> \<Longrightarrow> transform ba = transform b \<and> (\<exists>y'. a = Inl y') proof (prove)
goal:
No subgoals!