theory Corres_D

lemma corres_handle2':
  "corres_underlying R False nf' (dc \<oplus> r) P P' m m' \<Longrightarrow>
   corres_underlying R False nf' (dc \<oplus> r) P P' m (m' <handle2> (throwError \<circ> e))" apply (clarsimp simp: corres_underlying_def) apply (rule conjI) prefer 2 apply (clarsimp simp: handleE'_def bind_def) apply (drule (1) bspec, clarsimp) apply (drule (1) bspec, clarsimp) apply (clarsimp simp: return_def throwError_def split: sum.splits) apply clarsimp apply (drule (1) bspec, clarsimp) apply (clarsimp simp: handleE'_def bind_def) apply (drule (1) bspec, clarsimp) apply (fastforce simp: return_def throwError_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying R False nf' (dc \<oplus> r) P P' m m' \<Longrightarrow> corres_underlying R False nf' (dc \<oplus> r) P P' m (m' <handle2> throwError \<circ> e) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd ((m' <handle2> throwError \<circ> e) b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'
 2. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd ((m' <handle2> throwError \<circ> e) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd ((m' <handle2> throwError \<circ> e) b)
 2. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> \<not> snd (m' s'); (a, b) \<in> R; P a; P' b; nf'\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (m' b). \<not> snd (case x of (x, xa) \<Rightarrow> (case x of Inl x \<Rightarrow> (throwError \<circ> e) x | Inr v' \<Rightarrow> return (Inr v')) xa)) \<and> \<not> snd (m' b)
 2. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> R; P a; P' b; nf'; (aa, ba) \<in> fst (m' b); \<forall>x\<in>fst (m' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; \<not> snd (m' b); snd ((case aa of Inl x \<Rightarrow> (throwError \<circ> e) x | Inr v' \<Rightarrow> return (Inr v')) ba)\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; nf'; (aa, ba) \<in> fst (m' b); \<not> snd (m' b); snd ((case aa of Inl x \<Rightarrow> (throwError \<circ> e) x | Inr v' \<Rightarrow> return (Inr v')) ba); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((m' <handle2> throwError \<circ> e) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r' proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>\<forall>x\<in>R. case x of (s, s') \<Rightarrow> P s \<and> P' s' \<longrightarrow> (\<forall>x\<in>fst (m' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m s). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' s')); (a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst ((m' <handle2> throwError \<circ> e) b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst ((m' <handle2> throwError \<circ> e) b); \<forall>x\<in>fst (m' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; nf' \<longrightarrow> \<not> snd (m' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; \<forall>x\<in>fst (m' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r'; nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m' b); (aa, ba) \<in> fst ((case ab of Inl x \<Rightarrow> (throwError \<circ> e) x | Inr v' \<Rightarrow> return (Inr v')) bb)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba ab bb ac bc. \<lbrakk>(a, b) \<in> R; P a; P' b; nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m' b); (aa, ba) \<in> fst ((case ab of Inl x \<Rightarrow> (throwError \<circ> e) x | Inr v' \<Rightarrow> return (Inr v')) bb); (ac, bc) \<in> fst (m a); (bc, bb) \<in> R; (dc \<oplus> r) ac ab\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m a). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal:
No subgoals!