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     wfh: "wfhandlers hs"
  and     srv: "\<And>s s'. (s, s') \<in> sr \<Longrightarrow> (s, global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s') s')) \<in> sr"
  shows   "ccorres_underlying 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)" using wfh unfolding creturn_def apply - apply (rule ccorresI') apply (erule exec_handlers.cases) apply clarsimp apply (clarsimp elim!: exec_Normal_elim_cases) apply (drule (1) wfhandlersD) apply simp apply (simp add: throwError_def return_def) apply (drule exec_handlers_less2, clarsimp+) apply (auto simp: unif_rrel_def xfc esc elim!: srv)[1] apply (clarsimp elim!: exec_Normal_elim_cases) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying 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)
using this:
wfhandlers hs

goal (1 subgoal):
 1. ccorres_underlying 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)
using this:
wfhandlers hs

goal (1 subgoal):
 1. ccorres_underlying 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) (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) proof (prove)
goal (1 subgoal):
 1. wfhandlers hs \<Longrightarrow> ccorres_underlying 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) (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>(Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (throwError rv s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z h sa za hsa na t. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = na; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>hsa,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t. \<lbrakk>wfhandlers hs; (s, sa) \<in> sr; \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW),Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (throwError rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t. \<lbrakk>wfhandlers hs; (s, sa) \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (throwError rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa)\<rbrakk> \<Longrightarrow> global_exn_var_' (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>) = Return
 2. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa); t = Normal (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (throwError rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 4. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa); t = Normal (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (throwError rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, Normal (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>)); sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa); t = Normal (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>)\<rbrakk> \<Longrightarrow> (s, xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>) \<in> sr \<and> unif_rrel (na = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) (Inl rv) (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>)
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na va. \<lbrakk>(s, sa) \<in> sr; sf (v sa) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE; f rv (sf (v sa)) (es sa); length hs - na = Suc va\<rbrakk> \<Longrightarrow> (s, xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>) \<in> sr \<and> unif_rrel (na = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) (Inl rv) (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>)
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = h # hsa; n = length hsa; z = t; \<Gamma>\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t')
 2. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. sf (v s) \<noteq> SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE \<and> f rv (sf (v s)) (es s)}; \<not> snd (throwError rv s); s' = sa; (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);;
(\<acute>global_exn_var :== Return;;
THROW)) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (throwError rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) rvr rvxf (f \<currency> r) (liftxf es sf vf xf) ra t') proof (prove)
goal:
No subgoals!