theory Corres_C

lemma ccorres_split_nothrow_call_novcgE:
  assumes ac: "ccorres (f' \<currency> r') (liftxf errstate ef' vf' xf'') P P' [] a (Call f)"
  and     gg: "\<And>x y s. globals (g x y s) = globals s"
  and   xfxf: "\<And>a s t. xf' (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t"
  and     gi: "\<And>s. globals (i s) = globals s"
  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 rf_sr \<Gamma> (fl \<currency> 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 rf_sr \<Gamma> (fl \<currency> 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>"
  shows "ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (P and R) ({s. i s \<in> P'} \<inter>
  {s. \<forall>t.  (ef' (xf'' t) = scast EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and>
            (ef' (xf'' t) \<noteq> scast EXCEPTION_NONE \<longrightarrow>
              (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))}
  ) hs (a >>=E b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y));;
 d)" (is "ccorres_underlying rf_sr \<Gamma> ?r ?xf arrel axf ?P (?Q1 \<inter> ?Q2) hs ?A ?B") 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_nohs) apply (rule ccorres_callE [OF ac]) apply (rule gg) apply (rule errstate_state_update) apply (simp add: gg)+ apply (rule xfxf) apply (rule gi) apply (rule ccorres_abstract[OF ceqv]) apply (case_tac rv, simp_all add: lift_def) apply (rule_tac xf'=errstate in ccorres_abstract[OF ceqv_refl]) apply (rule ccorres_gen_asm2) apply (rule ccorres_gen_asm2) apply (erule_tac err'1=rv'a in err, assumption) apply (rule ccorres_gen_asm2) apply (rule ccorres_gen_asm2) apply (erule(1) bd) apply (rule hoare_strengthen_post) apply (rule valid [unfolded validE_def]) apply (simp split: sum.split_asm) apply (rule exec_handlers_Hoare_call_Basic) apply (clarsimp simp: ccHoarePost_def xfxf gg errstate_def
                  split: sum.split) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))}) hs (a >>=E b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y));;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (P and R) ({s. i s \<in> P'} \<inter> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))}) hs (a >>= Nondet_Monad.lift b) (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y));;
d) proof (prove)
goal (4 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> ?r' ?xf' ?arrel' ?axf' P {s. i s \<in> P'} [] a (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)))
 2. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # 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)})) UNIV proof (prove)
goal (7 subgoals):
 1. \<And>x y s. globals (g x y s) = globals s
 2. \<And>a s t. errstate (g a t (s\<lparr>globals := globals t\<rparr>)) = errstate t
 3. \<And>a s t. ?xf'4 (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 4. \<And>s. globals (i s) = globals s
 5. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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
 6. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 7. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' ?xf'4) (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (6 subgoals):
 1. \<And>a s t. errstate (g a t (s\<lparr>globals := globals t\<rparr>)) = errstate t
 2. \<And>a s t. ?xf'4 (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 3. \<And>s. globals (i s) = globals s
 4. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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
 5. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 6. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' ?xf'4) (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (8 subgoals):
 1. \<And>a s t sa. current_fault_' (globals (g a sa (s\<lparr>globals := globals sa\<rparr>))) = current_fault_' (globals sa)
 2. \<And>a s t sa. current_lookup_fault_' (globals (g a sa (s\<lparr>globals := globals sa\<rparr>))) = current_lookup_fault_' (globals sa)
 3. \<And>a s t sa. current_syscall_error_' (globals (g a sa (s\<lparr>globals := globals sa\<rparr>))) = current_syscall_error_' (globals sa)
 4. \<And>a s t. ?xf'4 (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 5. \<And>s. globals (i s) = globals s
 6. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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
 7. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 8. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' ?xf'4) (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (5 subgoals):
 1. \<And>a s t. ?xf'4 (g a t (s\<lparr>globals := globals t\<rparr>)) = xf'' t
 2. \<And>s. globals (i s) = globals s
 3. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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
 4. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 5. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' ?xf'4) (\<lambda>a b. {s. s \<in> (case a of Inl x \<Rightarrow> ?QE'3 x | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (4 subgoals):
 1. \<And>s. globals (i s) = globals s
 2. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate 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)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate 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)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv rv'. ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate 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)})) UNIV proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a. rv = Inl a \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> 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 rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate 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)})) UNIV proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a rv'a. rv = Inl a \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (QE a) (?G'31 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'31 b a (errstate s)} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P34 rv' a rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (QE a) (?G'33 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'33 b a (errstate s) \<inter> \<lbrace>?P34 b a (errstate s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (4 subgoals):
 1. \<And>rv rv' a rv'a. \<lbrakk>rv = Inl a; ?P34 rv' a rv'a; ?P38 rv' a rv'a\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (QE a) (?G'37 rv' a rv'a) hs (throwError a) (d' rv')
 2. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 3. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 4. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> ?G'37 b a (errstate s) \<inter> \<lbrace>?P38 b a (errstate s)\<rbrace> \<inter> \<lbrace>?P34 b a (errstate s)\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ba. rv = Inr ba \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?QR'3 ba rv') hs (b ba) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr x \<Rightarrow> ?QR'3 x) (xf' s)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ba. \<lbrakk>rv = Inr ba; ?P46 rv' ba\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?G'45 rv' ba) hs (b ba) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. ?G'45 rv' b \<inter> \<lbrace>?P46 rv' b\<rbrace>) (xf' s)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<And>rv rv' ba. \<lbrakk>rv = Inr ba; ?P46 rv' ba; ?P50 rv' ba\<rbrakk> \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> (fl \<currency> r) xf arrel axf (Q ba) (?G'49 rv' ba) hs (b ba) (d' rv')
 2. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 3. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate s)\<rbrace> \<inter> \<lbrace>ef' b \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE\<rbrace>} | Inr b \<Rightarrow> \<lambda>rv'. ?G'49 rv' b \<inter> \<lbrace>?P50 rv' b\<rbrace> \<inter> \<lbrace>?P46 rv' b\<rbrace>) (xf' s)})) UNIV proof (prove)
goal (2 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>case_sum QE Q\<rbrace>
 2. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate 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)})) UNIV proof (prove)
goal (3 subgoals):
 1. \<lbrace>R\<rbrace> a \<lbrace>?Q58\<rbrace>
 2. \<And>rv s. ?Q58 rv s \<Longrightarrow> (case rv of Inl x \<Rightarrow> QE x | Inr x \<Rightarrow> Q x) s
 3. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate 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)})) UNIV 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) s
 2. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate 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)})) UNIV proof (prove)
goal (1 subgoal):
 1. exec_handlers_Hoare \<Gamma> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} (call i f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) (\<lambda>x y. Basic (g x y)) # hs) (ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate 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)})) UNIV proof (prove)
goal (2 subgoals):
 1. \<forall>s' t x. s' \<in> {s. \<forall>t. (ef' (xf'' t) = SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>rv. r' rv (vf' (xf'' t)) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q' rv (xf'' t))) \<and> (ef' (xf'' t) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<longrightarrow> (\<forall>err. f' err (ef' (xf'' t)) (errstate t) \<longrightarrow> g s t (s\<lparr>globals := globals t\<rparr>) \<in> Q'' err (xf'' t) (errstate t)))} \<longrightarrow> g s' t (s'\<lparr>globals := globals t\<rparr>) \<in> ccHoarePost (f' \<currency> r') (liftxf errstate ef' vf' xf') (\<lambda>a b. {s. s \<in> (case a of Inl a \<Rightarrow> \<lambda>b. {s. s \<in> Q'' a b (errstate s) \<inter> \<lbrace>f' a (ef' b) (errstate 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. UNIV \<subseteq> UNIV proof (prove)
goal (1 subgoal):
 1. UNIV \<subseteq> UNIV proof (prove)
goal:
No subgoals!