theory Corres_UL_C

lemma ccorres_master_splitE:
  fixes a :: "('s, 'e + 'a) nondet_monad"
  and xf' :: "'t \<Rightarrow> 'b"
  assumes pre: "ccorres_underlying sr \<Gamma> (inr_rrel r') xf' (inl_rrel arrel) axf P P' hs' a c"
  assumes hsw: "hs' \<noteq> [] \<Longrightarrow> hs' = hs"
  assumes ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  assumes post: "\<And>rv rv'. r' rv rv'
                    \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')"
  assumes hoare: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>,-"
                 "exec_handlers_Hoare \<Gamma> R' (c # hs)
                    (ccHoarePost (inr_rrel r' :: ('e + 'a \<Rightarrow> 'b \<Rightarrow> bool)) xf' (\<lambda>v. Q' (theRight v))) UNIV"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs
             (a >>=E (\<lambda>rv. b rv)) (c ;; d)" unfolding bindE_def apply (rule_tac R="\<lambda>rv s. (case rv of Inl _ \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s)"
             and R'="\<lambda>rv. {s. s \<in> (Q' (theRight rv) (xf' s) \<inter> {s'. inr_rrel r' rv (xf' s)})}"
              and E="\<lambda>rv. \<top>"
             and E'="\<lambda>rv. {s. s \<in> ({s'. inl_rrel arrel rv (axf s')}
                                    \<inter> {s'. inl_rrel arrel rv (axf s)})}"
                in ccorres_master_split [OF pre]) apply (erule hsw) apply (rule ccorres_abstract[OF ceqv]) apply (rule ccorres_gen_asm2) apply (clarsimp elim!: inl_inrE simp: lift_def) apply (erule post) apply (rule_tac xf'=axf in ccorres_abstract, rule ceqv_refl) apply (rule ccorres_gen_asm2) apply (clarsimp simp: lift_def throwError_def
                   elim!: inl_inrE) apply (rule ccorres_return_Skip'[simplified]) apply (rule hoare_strengthen_post, rule hoare[unfolded validE_R_def validE_def]) apply simp apply (simp add: ccHoarePost_def inl_rrel_def split: sum.split) apply (rule hoare[unfolded ccHoarePost_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>=E b) (c;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>= Nondet_Monad.lift b) (c;;
d) proof (prove)
goal (5 subgoals):
 1. hs' \<noteq> [] \<Longrightarrow> hs' = hs
 2. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) {s. s \<in> Q' (theRight rv) (xf' s) \<inter> \<lbrace>inr_rrel r' rv (xf' s)\<rbrace>} hs (Nondet_Monad.lift b rv) d
 3. \<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s. s \<in> {s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv (axf s)\<rbrace>} [] (Nondet_Monad.lift b rv) SKIP
 4. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 5. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) {s. s \<in> Q' (theRight rv) (xf' s) \<inter> \<lbrace>inr_rrel r' rv (xf' s)\<rbrace>} hs (Nondet_Monad.lift b rv) d
 2. \<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s. s \<in> {s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv (axf s)\<rbrace>} [] (Nondet_Monad.lift b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) (Q' (theRight rv) rv' \<inter> \<lbrace>inr_rrel r' rv rv'\<rbrace>) hs (Nondet_Monad.lift b rv) (d' rv')
 2. \<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s. s \<in> {s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv (axf s)\<rbrace>} [] (Nondet_Monad.lift b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. inr_rrel r' rv rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) (Q' (theRight rv) rv') hs (Nondet_Monad.lift b rv) (d' rv')
 2. \<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s. s \<in> {s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv (axf s)\<rbrace>} [] (Nondet_Monad.lift b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (4 subgoals):
 1. \<And>rv' ra. r' ra rv' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ra) (Q' ra rv') hs (b ra) (d' rv')
 2. \<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s. s \<in> {s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv (axf s)\<rbrace>} [] (Nondet_Monad.lift b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (3 subgoals):
 1. \<And>rv. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s. s \<in> {s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv (axf s)\<rbrace>} [] (Nondet_Monad.lift b rv) SKIP
 2. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 3. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. hs' \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) ({s'. inl_rrel arrel rv (axf s')} \<inter> \<lbrace>inl_rrel arrel rv rv'\<rbrace>) [] (Nondet_Monad.lift b rv) SKIP
 2. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 3. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. \<lbrakk>hs' \<noteq> []; inl_rrel arrel rv rv'\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s'. inl_rrel arrel rv (axf s')} [] (Nondet_Monad.lift b rv) SKIP
 2. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 3. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (3 subgoals):
 1. \<And>rv' e. \<lbrakk>hs' \<noteq> []; arrel (Inl e) rv'\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (\<lambda>_. True) {s'. arrel (Inl e) (axf s')} [] (return (Inl e)) SKIP
 2. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 3. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)\<rbrace>
 2. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (2 subgoals):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> Q r s \<Longrightarrow> ((\<lambda>s. case rv of Inl x \<Rightarrow> True | Inr rv' \<Rightarrow> Q rv' s) and (\<lambda>_. True)) s
 2. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (1 subgoal):
 1. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (inr_rrel r') xf' (\<lambda>a b. {s. s \<in> Q' (theRight a) (xf' s) \<inter> \<lbrace>inr_rrel r' a (xf' s)\<rbrace>})) {s. hs' \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (inl_rrel arrel) axf (\<lambda>a b. {s. s \<in> {s'. inl_rrel arrel a (axf s')} \<inter> \<lbrace>inl_rrel arrel a (axf s)\<rbrace>})} proof (prove)
goal (1 subgoal):
 1. exec_handlers_Hoare \<Gamma> R' (c # hs) {s. \<forall>rv. inr_rrel r' rv (xf' s) \<longrightarrow> s \<in> Q' (theRight rv) (xf' s)} UNIV proof (prove)
goal:
No subgoals!