theory Corres_C

lemma ccorres_return_C_errorE:
  assumes xfc: "\<And>s. xf (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s)) = v s"
  and     esc: "\<And>s. es (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s)) = es s"
  and     xfu: "\<And>s f. globals (xfu f s) = globals s"
  and     wfh: "wfhandlers hs"
  shows   "ccorres_underlying rf_sr \<Gamma> rvr rvxf (f \<currency> r) (liftxf es sf vf xf)
    \<top> {s. sf (v s) \<noteq> scast EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} hs
    (throwError rv) (return_C xfu v)" apply (rule ccorres_guard_imp2, rule ccorres_return_C_errorE') apply (rule xfc) apply (rule esc) apply (rule wfh) apply (simp add: xfu rf_sr_def cong: cstate_relation_only_t_hrs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> rvr rvxf (f \<currency> r) (liftxf es sf vf xf) (\<lambda>_. True) {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} hs (throwError rv) (return_C xfu v) proof (prove)
goal (5 subgoals):
 1. \<And>s. xf (xfu (\<lambda>_. v s) s\<lparr>global_exn_var_' := Return\<rparr>) = v s
 2. \<And>s. es (xfu (\<lambda>_. v s) s\<lparr>global_exn_var_' := Return\<rparr>) = es s
 3. wfhandlers hs
 4. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} proof (prove)
goal (4 subgoals):
 1. \<And>s. es (xfu (\<lambda>_. v s) s\<lparr>global_exn_var_' := Return\<rparr>) = es s
 2. wfhandlers hs
 3. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} proof (prove)
goal (3 subgoals):
 1. wfhandlers hs
 2. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} proof (prove)
goal (2 subgoals):
 1. \<And>s s'. (s, s') \<in> rf_sr \<Longrightarrow> (s, xfu (\<lambda>_. v s') s'\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)} proof (prove)
goal:
No subgoals!