theory CNode_DR

lemma boolean_exception_corres:
  "\<lbrakk>dcorres (boolean_exception) P P' a b\<rbrakk>
    \<Longrightarrow> dcorres (dc\<oplus>dc) P P' (doE r \<leftarrow> a; unlessE r Monads_D.throw odE) b" apply (clarsimp simp:bindE_def lift_def unlessE_def corres_underlying_def bind_def) apply (erule allE, erule impE, rule conjI, assumption, assumption) apply (drule_tac x = "(aa,baa)" in bspec) apply simp apply clarsimp apply (rule bexI) prefer 2 apply assumption apply (clarsimp simp: boolean_exception_def validE_def valid_def lift_def
                        throwError_def returnOk_def return_def
                  split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres boolean_exception P P' a b \<Longrightarrow> dcorres (dc \<oplus> dc) P P' (doE r <- a;
unlessE r throw
odE) b proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa. \<lbrakk>\<forall>ba. P (transform ba) \<and> P' ba \<longrightarrow> (\<forall>x\<in>fst (b ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a (transform ba)). case x of (r, t) \<Rightarrow> transform t' = t \<and> boolean_exception r r'); (aa, baa) \<in> fst (b ba); P (transform ba); P' ba\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a (transform ba)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; \<forall>x\<in>fst (b ba). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (a (transform ba)). case x of (r, t) \<Rightarrow> transform t' = t \<and> boolean_exception r r'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a (transform ba)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal (2 subgoals):
 1. \<And>ba a baa. \<lbrakk>(a, baa) \<in> fst (b ba); P (transform ba); P' ba\<rbrakk> \<Longrightarrow> (a, baa) \<in> fst (b ba)
 2. \<And>ba aa baa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; case (aa, baa) of (r', t') \<Rightarrow> \<exists>x\<in>fst (a (transform ba)). case x of (r, t) \<Rightarrow> transform t' = t \<and> boolean_exception r r'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a (transform ba)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; case (aa, baa) of (r', t') \<Rightarrow> \<exists>x\<in>fst (a (transform ba)). case x of (r, t) \<Rightarrow> transform t' = t \<and> boolean_exception r r'\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a (transform ba)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa aaa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; (aaa, transform baa) \<in> fst (a (transform ba)); boolean_exception aaa aa\<rbrakk> \<Longrightarrow> \<exists>y\<in>fst (a (transform ba)). \<exists>x\<in>fst (case y of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal (2 subgoals):
 1. \<And>ba aa baa aaa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; (aaa, transform baa) \<in> fst (a (transform ba)); boolean_exception aaa aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ?y49 ba aa baa aaa of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa
 2. \<And>ba aa baa aaa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; (aaa, transform baa) \<in> fst (a (transform ba)); boolean_exception aaa aa\<rbrakk> \<Longrightarrow> ?y49 ba aa baa aaa \<in> fst (a (transform ba)) proof (prove)
goal (2 subgoals):
 1. \<And>ba aa baa aaa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; (aaa, transform baa) \<in> fst (a (transform ba)); boolean_exception aaa aa\<rbrakk> \<Longrightarrow> ?y49 ba aa baa aaa \<in> fst (a (transform ba))
 2. \<And>ba aa baa aaa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; (aaa, transform baa) \<in> fst (a (transform ba)); boolean_exception aaa aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case ?y49 ba aa baa aaa of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal (1 subgoal):
 1. \<And>ba aa baa aaa. \<lbrakk>(aa, baa) \<in> fst (b ba); P (transform ba); P' ba; (aaa, transform baa) \<in> fst (a (transform ba)); boolean_exception aaa aa\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (case (aaa, transform baa) of (x, xa) \<Rightarrow> lift (\<lambda>r. if r then returnOk () else throw) x xa). case x of (r, t) \<Rightarrow> transform baa = t \<and> (dc \<oplus> dc) r aa proof (prove)
goal:
No subgoals!