theory Corres_C

lemma ccorres_split_nothrow_case_sum:
  "\<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' hs a c;
    \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv');
    \<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 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 (e err) (d' rv');
    \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = scast EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s))
                                                 \<longrightarrow>  s \<in> Q' rv' (xf' s))
                                   \<and> (\<forall>ft. ef' (xf' s) \<noteq> scast EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s)
                                                 \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))} \<rbrakk>
      \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>= case_sum e b) (c;;d)" apply (erule_tac R="case_sum QE Q" and R'="case_sum QE' QR'" for QE' QR'
           in ccorres_master_split_hs) apply (case_tac rv, simp_all)[1] apply (erule ccorres_abstract) apply (rule ccorres_abstract[where xf'=es], rule ceqv_refl) apply (rule_tac P="ef' rv' \<noteq> scast EXCEPTION_NONE" in ccorres_gen_asm2) apply (rule_tac P="f' aa (ef' rv') rv'a" in ccorres_gen_asm2) apply assumption apply (erule ccorres_abstract) apply (rule_tac P="r' ba (vf' rv')" in ccorres_gen_asm2) apply (rule_tac P="ef' rv' = scast EXCEPTION_NONE" in ccorres_gen_asm2) apply assumption apply (rule ccorres_empty[where P=\<top>]) apply (simp add: validE_def) apply (erule hoare_strengthen_post, simp split: sum.split_asm) apply (drule exec_handlers_Hoare_from_vcg_nofail) apply (erule exec_handlers_Hoare_Post [OF _ _ subset_refl]) apply (clarsimp simp: ccHoarePost_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorresG sr \<Gamma> (f' \<currency> r') (liftxf es ef' vf' xf') P P' hs a c; \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (P and R) (P' \<inter> R') hs (a >>= case_sum e b) (c;;
d) proof (prove)
goal (4 subgoals):
 1. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> 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 x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x) hs (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) d
 2. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 3. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x)) {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 aa. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inl aa\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?QE'4 aa) hs (e aa) d
 2. \<And>rv ba. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 4. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl x \<Rightarrow> ?QE'4 x | Inr x \<Rightarrow> ?QR'4 x)) {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 aa rv'. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inl aa\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'16 aa rv') hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 4. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> ?G'16 a (xf' s)} | Inr x \<Rightarrow> ?QR'4 x)) {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 aa rv' rv'a. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inl aa\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'20 aa rv' rv'a) hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 4. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> ?G'20 a (xf' s) (es sa)}} | Inr x \<Rightarrow> ?QR'4 x)) {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 aa rv' rv'a. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inl aa; ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'25 aa rv' rv'a) hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 4. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> ?G'25 a (xf' s) (es sa) \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr x \<Rightarrow> ?QR'4 x)) {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 aa rv' rv'a. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inl aa; ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' aa (ef' rv') rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE aa) (?G'27 aa rv' rv'a) hs (e aa) (d' rv')
 2. \<And>rv ba. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 3. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 4. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> ?G'27 a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr x \<Rightarrow> ?QR'4 x)) {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 ba. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?QR'4 ba) hs (b ba) d
 2. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 3. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr x \<Rightarrow> ?QR'4 x)) {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 ba rv'. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'35 ba rv') hs (b ba) (d' rv')
 2. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 3. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> ?G'35 a (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 ba rv'. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba; r' ba (vf' rv')\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'38 ba rv') hs (b ba) (d' rv')
 2. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 3. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> ?G'38 a (xf' s) \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {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 ba rv'. \<lbrakk>\<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}; rv = Inr ba; r' ba (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q ba) (?G'40 ba rv') hs (b ba) (d' rv')
 2. \<And>rv. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 3. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> ?G'40 a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}; hs \<noteq> []\<rbrakk> \<Longrightarrow> ccorresG sr \<Gamma> arrel axf (?E rv) (?E' rv) [] (case rv of Inl x \<Rightarrow> e x | Inr x \<Rightarrow> b x) SKIP
 2. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> QE e s | Inr r \<Rightarrow> Q r s\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {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>ft. f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s)))}\<rbrakk> \<Longrightarrow> \<lbrace>R\<rbrace> a \<lbrace>\<lambda>rv. case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x\<rbrace>
 2. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> R' c {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))}\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>; exec_handlers_Hoare \<Gamma> R' (c # ?cs61) {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))} ?A61\<rbrakk> \<Longrightarrow> exec_handlers_Hoare \<Gamma> R' (c # hs) (ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>})) {s. hs \<noteq> [] \<longrightarrow> s \<in> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. {})} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv'); \<And>rv rv'. \<lbrakk>r' rv (vf' rv'); ef' rv' = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (Q rv) (Q' rv rv') hs (b rv) (d' rv'); \<And>err rv' err'. \<lbrakk>ef' rv' \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f' err (ef' rv') err'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf (QE err) (Q'' err rv' err') hs (e err) (d' rv'); \<lbrace>R\<rbrace> a \<lbrace>Q\<rbrace>, \<lbrace>QE\<rbrace>\<rbrakk> \<Longrightarrow> {s. (\<forall>rv'. ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> r' rv' (vf' (xf' s)) \<longrightarrow> s \<in> Q' rv' (xf' s)) \<and> (\<forall>ft. ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> f' ft (ef' (xf' s)) (es s) \<longrightarrow> s \<in> Q'' ft (xf' s) (es s))} \<subseteq> ccHoarePost (f' \<currency> r') (liftxf es ef' vf' xf') (\<lambda>a b. case a of Inl a \<Rightarrow> {s. s \<in> {sa. sa \<in> Q'' a (xf' s) (es sa) \<inter> \<lbrace>f' a (ef' (xf' s)) (es sa)\<rbrace> \<inter> \<lbrace>ef' (xf' s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>}} | Inr a \<Rightarrow> {s. s \<in> Q' a (xf' s) \<inter> \<lbrace>ef' (xf' s) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace> \<inter> \<lbrace>r' a (vf' (xf' s))\<rbrace>}) proof (prove)
goal:
No subgoals!