theory Corres_C

lemma ccorres_return_C':
  assumes xfc: "\<And>s. (xf (global_exn_var_'_update (\<lambda>_. Return) (xfu (\<lambda>_. v s) s))) = v 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> r rvxf arrel xf \<top> {s. arrel rv (v s)} hs
               (return 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 (frule exec_handlers_less2, clarsimp) apply (clarsimp simp: return_def unif_rrel_def xfc) apply (auto 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> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return rv) (return_C xfu v) proof (prove)
using this:
wfhandlers hs

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return rv) (return_C xfu v) proof (prove)
using this:
wfhandlers hs

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return 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> r rvxf arrel xf (\<lambda>_. True) {s. arrel rv (v s)} hs (return 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. arrel rv (v 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 (return rv s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel 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. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t. \<lbrakk>wfhandlers hs; (s, sa) \<in> sr; arrel rv (v sa); \<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)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (return rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r rvxf arrel xf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t. \<lbrakk>wfhandlers hs; (s, sa) \<in> sr; arrel rv (v sa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (return rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r rvxf arrel xf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; arrel rv (v sa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t)\<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; arrel rv (v sa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); 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 (return rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 4. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; arrel rv (v sa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); 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 (return rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r rvxf arrel xf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; arrel rv (v sa); \<Gamma>\<turnstile>\<^sub>h \<langle>hs,xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>\<rangle> \<Rightarrow> (na, t); t = Normal (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>); \<exists>v. length hs - na = Suc v\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (return rv s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r rvxf arrel xf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa na va. \<lbrakk>(s, sa) \<in> sr; arrel rv (v sa); \<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>)); length hs - na = Suc va\<rbrakk> \<Longrightarrow> (na = length hs \<longrightarrow> (s, xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>) \<in> sr \<and> r rv (rvxf (xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>))) \<and> (na \<noteq> length hs \<longrightarrow> (s, xfu (\<lambda>_. v sa) sa\<lparr>global_exn_var_' := Return\<rparr>) \<in> sr)
 2. \<And>s s' n z h sa t hsa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 3. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel 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. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t')
 2. \<And>s s' n z sa. \<lbrakk>wfhandlers hs; (s, s') \<in> sr; True; s' \<in> {s. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel 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. arrel rv (v s)}; \<not> snd (return 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 (return rv s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r rvxf arrel xf ra t') proof (prove)
goal:
No subgoals!