theory CNode_DR

lemma corres_bindE_throwError:
  assumes f:"\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>"
  assumes nf: "sf \<Longrightarrow> no_fail P' f"
  shows "corres_underlying sr af sf (dc \<oplus> r) P P' (Monads_D.throw) (doE x \<leftarrow> f; throwError (e x) odE)" apply (clarsimp simp: corres_underlying_def) apply (rule conjI) apply (clarsimp simp: in_monad bindE_def throwError_def return_def) apply (drule_tac P="(=) b" in use_valid [OF _ f], simp) apply (clarsimp simp: lift_def throwError_def return_def split: sum.splits) apply (rule impI, drule nf) apply (simp add: no_fail_def) apply (clarsimp simp: bindE_def bind_def throwError_def return_def lift_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr af sf (dc \<oplus> r) P P' throw (doE x <- f;
throwError (e x)
odE) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst ((doE x <- f;
throwError (e x)
odE) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> (dc \<oplus> r) ra r') \<and> (sf \<longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst ((doE x <- f;
throwError (e x)
odE) b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (throw a). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> (dc \<oplus> r) ra r'
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> sf \<longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> sr; P a; P' b; (x, s'') \<in> fst (f b); (aa, ba) \<in> fst (lift (\<lambda>x s. ({(Inl (e x), s)}, False)) x s'')\<rbrakk> \<Longrightarrow> (a, ba) \<in> sr \<and> (\<exists>y'. aa = Inl y')
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> sf \<longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba s'' x. \<lbrakk>(a, b) \<in> sr; P a; P' b; (aa, ba) \<in> fst (lift (\<lambda>x s. ({(Inl (e x), s)}, False)) x s''); b = s''\<rbrakk> \<Longrightarrow> (a, ba) \<in> sr \<and> (\<exists>y'. aa = Inl y')
 2. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> sf \<longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a)\<rbrakk> \<Longrightarrow> sf \<longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a); no_fail P' f\<rbrakk> \<Longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> sr; P a; P' b; af \<longrightarrow> \<not> snd (throw a); \<forall>s. P' s \<longrightarrow> \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<not> snd ((doE x <- f;
throwError (e x)
odE) b) proof (prove)
goal:
No subgoals!