theory Corres_UL_C

lemma ccorres_throw:
  assumes abh: "ccorres_underlying sr \<Gamma> arrel axf arrel axf P P' hs a h"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf P P' (h#hs) a Throw" apply (rule ccorresI') apply (erule exec_handlers.cases, simp_all) apply (erule exec_Normal_elim_cases) apply clarsimp apply (frule exec_handlers_Cons_le) apply (rule ccorresE [OF abh], assumption+) apply (simp add: unif_rrel_def split_def) apply (erule rev_bexI, simp) apply (erule exec_Normal_elim_cases) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' (h # hs) a THROW proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>THROW # h # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length (h # hs)) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z ha sa za na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = ha; n = na; z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> Abrupt za; \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z ha sa za na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = ha; n = na; z = t; \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,za\<rangle> \<Rightarrow> (na, t); Abrupt za = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,sa\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa na t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,sa\<rangle> \<Rightarrow> (na, t); na \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa na t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,sa\<rangle> \<Rightarrow> (na, t); na \<le> length hs; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (na = length hs) arrel axf arrel axf ra t'; na \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = Suc (length hs)) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa na t t' r ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>h # hs,sa\<rangle> \<Rightarrow> (na, Normal t'); t = Normal t'; (r, ta) \<in> fst (a s); (ta, t') \<in> sr; arrel r (axf t'); na \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). (snd x, t') \<in> sr \<and> arrel (fst x) (axf t')
 2. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<Gamma>\<turnstile> \<langle>THROW,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z h sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; THROW = h; n = Suc (length hs); z = t; \<not> isAbr t; t = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. t = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel True r xf arrel axf ra t') proof (prove)
goal:
No subgoals!