theory Corres_UL_C

lemma ccorres_Call:
  assumes ge: "\<Gamma> f = Some (Catch bdy Skip)"
  and    cul: "ccorres_underlying sr \<Gamma> r xf r xf P P' (Skip # hs) a bdy"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Call f)" using ge cul apply - apply (rule ccorresI') apply (erule exec_handlers.cases) apply clarsimp apply (erule exec_Normal_elim_cases | simp)+ apply clarsimp apply (erule exec_Normal_elim_cases | simp)+ apply (erule (4) ccorresE) apply (erule EHAbrupt, rule EHOther) apply (rule exec.Skip) apply simp apply (simp add: unif_rrel_simps) apply fastforce apply (erule (4) ccorresE) apply (erule (1) EHOther) apply (simp add: unif_rrel_simps) apply fastforce apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Call f) proof (prove)
using this:
\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END)
ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Call f) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs a (Call f) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>Call f # 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 hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z h sa za hsa na t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # 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 (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # 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 (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa za na t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>Call f,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 (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (na = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # 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 (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z h sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); s' = sa; Call f = h; n = length hs; z = t; \<Gamma>\<turnstile> \<langle>h,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')
 2. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma>\<turnstile> \<langle>Call f,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')
 2. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa t s'. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt s'; t = Normal s'\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, s') \<in> sr \<and> unif_rrel True r xf arrel axf ra s'
 2. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 3. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 4. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s sa t s'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt s'; t = Normal s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>bdy # SKIP # hs,sa\<rangle> \<Rightarrow> (?n40 s sa t s', ?x40 s sa t s')
 2. \<And>s sa t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt s'; t = Normal s'; ?x40 s sa t s' = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n40 s sa t s' = length (SKIP # hs)) r xf r xf ra t'; ?n40 s sa t s' \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, s') \<in> sr \<and> unif_rrel True r xf arrel axf ra s'
 3. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 4. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 5. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (6 subgoals):
 1. \<And>s sa t s'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); t = Normal s'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>SKIP,Normal s'\<rangle> \<Rightarrow> ?x40 s sa t s'
 2. \<And>s sa t s'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); t = Normal s'\<rbrakk> \<Longrightarrow> \<not> isAbr (?x40 s sa t s')
 3. \<And>s sa t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt s'; t = Normal s'; ?x40 s sa t s' = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length hs = length (SKIP # hs)) r xf r xf ra t'; length hs \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, s') \<in> sr \<and> unif_rrel True r xf arrel axf ra s'
 4. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 5. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 6. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (5 subgoals):
 1. \<And>s sa t s'. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); t = Normal s'\<rbrakk> \<Longrightarrow> \<not> isAbr (Normal s')
 2. \<And>s sa t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt s'; t = Normal s'; Normal s' = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length hs = length (SKIP # hs)) r xf r xf ra t'; length hs \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, s') \<in> sr \<and> unif_rrel True r xf arrel axf ra s'
 3. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 4. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 5. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt s'; t = Normal s'; Normal s' = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length hs = length (SKIP # hs)) r xf r xf ra t'; length hs \<le> length (SKIP # hs)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, s') \<in> sr \<and> unif_rrel True r xf arrel axf ra s'
 2. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 3. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 4. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Abrupt t'; t = Normal t'; s' = t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; r ra (xf t')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra (xf t')
 2. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 3. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 4. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa t. \<lbrakk>ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,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')
 2. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 3. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (4 subgoals):
 1. \<And>s sa t. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>bdy # SKIP # hs,sa\<rangle> \<Rightarrow> (?n142 s sa t, ?x142 s sa t)
 2. \<And>s sa t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t; ?x142 s sa t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n142 s sa t = length (SKIP # hs)) r xf r xf ra t'; ?n142 s sa t \<le> length (SKIP # 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 True r xf arrel axf ra t')
 3. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 4. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length (SKIP # hs) = length (SKIP # hs)) r xf r xf ra t'; length (SKIP # hs) \<le> length (SKIP # 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 True r xf arrel axf ra t')
 2. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 3. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (3 subgoals):
 1. \<And>s sa t t' ra ta. \<lbrakk>(s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); \<Gamma>\<turnstile> \<langle>bdy,Normal sa\<rangle> \<Rightarrow> Normal t'; t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; r ra (xf t')\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> r ra (xf t')
 2. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 3. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (2 subgoals):
 1. \<And>s sa t. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, sa) \<in> sr; P s; sa \<in> P'; \<not> snd (a s); \<not> isAbr t; t = Stuck; \<Gamma> f = None\<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')
 2. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z sa. \<lbrakk>\<Gamma> f = Some (TRY
  bdy
CATCH SKIP
END); ccorresG sr \<Gamma> r xf P P' (SKIP # hs) a bdy; (s, s') \<in> sr; P s; s' \<in> P'; \<not> snd (a s); s' = sa; Call f # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (a s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!