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 <handle2> (\<lambda>x. Monads_D.throw)) m'" apply (clarsimp simp: corres_underlying_def) apply (rule conjI) prefer 2 apply fastforce apply clarsimp apply (drule (1) bspec, clarsimp) apply (drule (1) bspec, clarsimp) apply (clarsimp simp: handleE'_def) apply (simp add: bind_def) apply (rule bexI) prefer 2 apply assumption apply (simp add: return_def throwError_def split: sum.splits) apply fastforce 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 <handle2> (\<lambda>x. throw)) m' 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' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m <handle2> (\<lambda>x. throw)) a). case x of (ra, t) \<Rightarrow> (t, t') \<in> R \<and> (dc \<oplus> r) ra r') \<and> (nf' \<longrightarrow> \<not> snd (m' 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' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m <handle2> (\<lambda>x. throw)) 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' 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' 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' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m <handle2> (\<lambda>x. throw)) 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' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst ((m <handle2> (\<lambda>x. throw)) 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' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((m <handle2> (\<lambda>x. throw)) 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' 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 <handle2> (\<lambda>x. throw)) 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; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((m <handle2> (\<lambda>x. throw)) 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; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((do v <- m;
case v of Inl e \<Rightarrow> throw | Inr v' \<Rightarrow> return (Inr v')
od) 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; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (m a). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> (case x of Inl e \<Rightarrow> throw | Inr v' \<Rightarrow> return (Inr v')) xa). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ?y51 a b aa ba ab bb of (x, xa) \<Rightarrow> (case x of Inl e \<Rightarrow> throw | Inr v' \<Rightarrow> return (Inr v')) xa). case x of (ra, t) \<Rightarrow> (t, ba) \<in> R \<and> (dc \<oplus> r) ra aa
 2. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> ?y51 a b aa ba ab bb \<in> fst (m a) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> ?y51 a b aa ba ab bb \<in> fst (m a)
 2. \<And>a b aa ba ab bb. \<lbrakk>(a, b) \<in> R; P a; P' b; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ?y51 a b aa ba ab bb of (x, xa) \<Rightarrow> (case x of Inl e \<Rightarrow> throw | Inr v' \<Rightarrow> return (Inr v')) xa). 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; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case (ab, bb) of (x, xa) \<Rightarrow> (case x of Inl e \<Rightarrow> throw | Inr v' \<Rightarrow> return (Inr v')) xa). 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; (aa, ba) \<in> fst (m' b); nf' \<longrightarrow> \<not> snd (m' b); (ab, bb) \<in> fst (m a); (bb, ba) \<in> R; (dc \<oplus> r) ab aa\<rbrakk> \<Longrightarrow> ((\<exists>x1. ab = Inl x1) \<longrightarrow> (\<exists>y'. aa = Inl y')) \<and> (\<forall>x2. ab = Inr x2 \<longrightarrow> (\<exists>y'. aa = Inr y' \<and> r x2 y')) proof (prove)
goal:
No subgoals!