theory Corres_C

lemma ccorres_split_nothrowE:
  fixes R' :: "cstate set"
  assumes ac: "ccorres_underlying sr \<Gamma>
                    (f' \<currency> r') (liftxf es ef' vf' xf')
                    (f' \<currency> r') (liftxf es ef' vf' xf')
                    P P' hs a c"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     bd: "\<And>rv rv'. \<lbrakk> r' rv (vf' rv'); ef' rv' = scast EXCEPTION_NONE \<rbrakk>
            \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv')"
  and    err: "\<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> scast EXCEPTION_NONE; f' err (ef' rv') err' \<rbrakk>
            \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs
                     (throwError err) (d' rv')"
  and  valid: "\<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>,\<lbrace>QE\<rbrace>"
  and valid': "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' c ({s. (ef' (xf' s) = scast EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv (xf' s))) \<and>
  (ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' err (xf' s) (es s)))})" (is "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> R' c {s. ?Q'' s}")
  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="case_sum QE Q"
             and R'="\<lambda>rv. {s. s \<in> case_sum QE' QR' rv (xf' s)}" for QE' QR'
           in ccorres_master_split_hs) apply (rule ac) apply (rule ccorres_abstract[OF ceqv]) apply (case_tac rv, simp_all add: lift_def) apply (rule ccorres_abstract[where xf'=es, OF ceqv_refl]) apply (rule ccorres_gen_asm2) apply (rule ccorres_gen_asm2) apply (rule_tac err'=rv'a in err) apply assumption+ apply (rule ccorres_gen_asm2) apply (rule ccorres_gen_asm2) apply (erule(1) bd) apply (rule ccorres_empty[where P=\<top>]) apply (rule hoare_strengthen_post, rule valid[unfolded validE_def]) apply (simp split: sum.split_asm) apply (rule exec_handlers_Hoare_Post,
         rule exec_handlers_Hoare_from_vcg_nofail[OF valid', where A="{}"]) apply (auto simp: ccHoarePost_def split: sum.split) 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. ccorres_underlying sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P P' hs a c
 2. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) {s. s \<in> (case rv of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)} hs (Nondet_Monad.lift b rv) d
 3. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (Nondet_Monad.lift b rv) SKIP
 4. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 5. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost ?r' ?xf' (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost ?arrel' ?axf' (\<lambda>a b. ?E' a)} proof (prove)
goal (4 subgoals):
 1. \<And>rv. ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) {s. s \<in> (case rv of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)} hs (Nondet_Monad.lift b rv) d
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (Nondet_Monad.lift b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv'. ccorres_underlying sr \<Gamma> r xf arrel axf (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) ((case rv of Inl a \<Rightarrow> ?QE'3 a | Inr a \<Rightarrow> ?QR'3 a) rv') hs (Nondet_Monad.lift b rv) (d' rv')
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (Nondet_Monad.lift b rv) SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' a. rv = Inl a \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?QE'3 a rv') hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 4. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 5. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' a rv'a. rv = Inl a \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?G'16 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 4. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 5. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'16 b a (es s)} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?G'19 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 4. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 5. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'19 b a (es s) \<inter> \<lbrace>?P20 b a (es s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a; ?P24 rv' a rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE a) (?G'23 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 4. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 5. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'23 b a (es s) \<inter> \<lbrace>?P24 b a (es s)\<rbrace> \<inter> \<lbrace>?P20 b a (es s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a; ?P24 rv' a rv'a\<rbrakk> \<Longrightarrow> ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE
 2. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P20 rv' a rv'a; ?P24 rv' a rv'a\<rbrakk> \<Longrightarrow> f' a (ef' rv') rv'a
 3. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 4. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 5. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 6. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>?P24 b a (es s)\<rbrace> \<inter> \<lbrace>?P20 b a (es s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' ba. \<lbrakk>rv = Inr ba; ?P30 rv' ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'29 rv' ba) hs (b ba) (d' rv')
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. ?G'29 rv' b \<inter> \<lbrace>?P30 rv' b\<rbrace>) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' ba. \<lbrakk>rv = Inr ba; ?P30 rv' ba; ?P34 rv' ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'33 rv' ba) hs (b ba) (d' rv')
 2. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 3. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 4. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. ?G'33 rv' b \<inter> \<lbrace>?P34 rv' b\<rbrace> \<inter> \<lbrace>?P30 rv' b\<rbrace>) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (3 subgoals):
 1. \<And>rv. hs \<noteq> [] \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> b v') SKIP
 2. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and ?E rv\<rbrace>
 3. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. ?E' a)} proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and (\<lambda>_. True)\<rbrace>
 2. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (2 subgoals):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> QE e s | Inr r \<Rightarrow> Q r s \<Longrightarrow> ((case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) and (\<lambda>_. True)) s
 2. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (1 subgoal):
 1. exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (2 subgoals):
 1. {s. (ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv (xf' s))) \<and> (ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' err (xf' s) (es s)))} \<subseteq> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (es s) \<inter> \<lbrace>f' a (ef' b) (es s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. Q' b rv' \<inter> \<lbrace>ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' b (vf' rv')\<rbrace>) (xf' s)})
 2. {} \<subseteq> {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal:
No subgoals!