theory Tcb_DR

lemma corres_underlying_returnOk_ignored:
  "corres_underlying sr nf nf' (erel \<oplus> dc) P P' f (g >>=E (\<lambda>_. returnOk v))
    = corres_underlying sr nf nf' (erel \<oplus> dc) P P' f g" apply (clarsimp simp: corres_underlying_def) apply (rule ball_cong[OF refl], rename_tac ss) apply (case_tac ss, rename_tac s s', clarsimp) apply (rule imp_cong[OF refl]) apply (clarsimp simp: bindE_def bind_def returnOk_def return_def lift_def throwError_def
                 split: prod.splits sum.splits) apply (rule imp_cong[OF refl], rule conj_cong[OF _ refl], rule ball_cong[OF refl], rename_tac rr) by (case_tac rr; rename_tac rvs' t'; case_tac rvs'; rename_tac rv'; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr nf nf' (erel \<oplus> dc) P P' f (doE _ <- g;
returnOk v
odE) = corres_underlying sr nf nf' (erel \<oplus> dc) 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 ((doE _ <- g;
returnOk v
odE) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd ((doE _ <- g;
returnOk v
odE) s'))) = (\<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 (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd (g s'))) proof (prove)
goal (1 subgoal):
 1. \<And>ss. ss \<in> sr \<Longrightarrow> (case ss of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst ((doE _ <- g;
returnOk v
odE) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd ((doE _ <- g;
returnOk v
odE) s'))) = (case ss 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 (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd (g s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. (s, s') \<in> sr \<Longrightarrow> (P s \<and> P' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst ((doE _ <- g;
returnOk v
odE) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd ((doE _ <- g;
returnOk v
odE) s'))) = (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 (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd (g s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s \<and> P' s'\<rbrakk> \<Longrightarrow> ((nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst ((doE _ <- g;
returnOk v
odE) s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd ((doE _ <- g;
returnOk v
odE) s'))) = ((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 (r, t) \<Rightarrow> (t, t') \<in> sr \<and> (erel \<oplus> dc) r r') \<and> (nf' \<longrightarrow> \<not> snd (g s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> ((nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>y\<in>fst (g s'). \<forall>x1. (\<forall>x1a. x1 = Inl x1a \<longrightarrow> (\<forall>x2. y = (Inl x1a, x2) \<longrightarrow> (\<exists>x\<in>fst (f s). \<forall>x1 x2a. x = (x1, x2a) \<longrightarrow> (x2a, x2) \<in> sr \<and> (\<exists>x'. x1 = Inl x' \<and> erel x' x1a)))) \<and> (\<forall>x2. x1 = Inr x2 \<longrightarrow> (\<forall>x2a. y = (Inr x2, x2a) \<longrightarrow> (\<exists>x\<in>fst (f s). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (x2, x2a) \<in> sr \<and> (\<exists>x'. x1 = Inr x'))))) \<and> (nf' \<longrightarrow> \<not> snd (g s'))) = ((nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (g s'). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (\<exists>x\<in>fst (f s). \<forall>x1a x2a. x = (x1a, x2a) \<longrightarrow> (x2a, x2) \<in> sr \<and> (erel \<oplus> dc) x1a x1)) \<and> (nf' \<longrightarrow> \<not> snd (g s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' rr. \<lbrakk>(s, s') \<in> sr; P s; P' s'; nf \<longrightarrow> \<not> snd (f s); rr \<in> fst (g s')\<rbrakk> \<Longrightarrow> (\<forall>x1. (\<forall>x1a. x1 = Inl x1a \<longrightarrow> (\<forall>x2. rr = (Inl x1a, x2) \<longrightarrow> (\<exists>x\<in>fst (f s). \<forall>x1 x2a. x = (x1, x2a) \<longrightarrow> (x2a, x2) \<in> sr \<and> (\<exists>x'. x1 = Inl x' \<and> erel x' x1a)))) \<and> (\<forall>x2. x1 = Inr x2 \<longrightarrow> (\<forall>x2a. rr = (Inr x2, x2a) \<longrightarrow> (\<exists>x\<in>fst (f s). \<forall>x1 x2. x = (x1, x2) \<longrightarrow> (x2, x2a) \<in> sr \<and> (\<exists>x'. x1 = Inr x'))))) = (\<forall>x1 x2. rr = (x1, x2) \<longrightarrow> (\<exists>x\<in>fst (f s). \<forall>x1a x2a. x = (x1a, x2a) \<longrightarrow> (x2a, x2) \<in> sr \<and> (erel \<oplus> dc) x1a x1))