theory Corres_UL_C

lemma ccorres_basic_srnoop:
  assumes asm: "ccorres_underlying sr E r xf arrel axf G G' hs a c"
  and   gsr: "\<And>s s'. (s, s') \<in> sr \<Longrightarrow> (s, g s') \<in> sr"
  and   gG: "\<And>s'. s' \<in> G' \<Longrightarrow> g s' \<in> G'"
  shows "ccorres_underlying sr E r xf arrel axf G G' hs a (Basic g ;; c)" using asm apply - apply (rule ccorresI') apply clarsimp apply (erule exec_handlers.cases) apply clarsimp apply (erule exec_Normal_elim_cases) apply (erule exec_Normal_elim_cases) apply simp apply (erule (4) ccorresE [OF _ gsr _ gG]) apply (erule (1) EHAbrupt) apply clarsimp apply (erule bexI [rotated]) apply simp apply clarsimp apply (erule exec_Normal_elim_cases) apply (erule exec_Normal_elim_cases) apply simp apply (erule (4) ccorresE [OF _ gsr _ gG]) apply (erule (1) EHOther) apply clarsimp apply (erule bexI [rotated]) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs a (Basic g;;
c) proof (prove)
using this:
ccorres_underlying sr E r xf arrel axf G G' hs a c

goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs a (Basic g;;
c) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr E r xf arrel axf G G' hs a c \<Longrightarrow> ccorres_underlying sr E r xf arrel axf G G' hs a (Basic g;;
c) proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; E\<turnstile>\<^sub>h \<langle>(Basic g;;
c) # 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 (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; E\<turnstile>\<^sub>h \<langle>(Basic g;;
c) # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = na; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> Abrupt za; E\<turnstile>\<^sub>h \<langle>hsa,za\<rangle> \<Rightarrow> (na, t)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile> \<langle>Basic g;;
c,Normal sa\<rangle> \<Rightarrow> Abrupt za; E\<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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); E\<turnstile> \<langle>Basic g,Normal sa\<rangle> \<Rightarrow> s'; E\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> Abrupt za\<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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); E\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> Abrupt za; s' = Normal (g 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 = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Abrupt za; s' = Normal (g 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 = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 za na t s'. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Abrupt za; s' = Normal (g sa)\<rbrakk> \<Longrightarrow> E\<turnstile>\<^sub>h \<langle>c # hs,g sa\<rangle> \<Rightarrow> (?n22 s sa za na t s', ?x22 s sa za na t s')
 2. \<And>s sa za na t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Abrupt za; s' = Normal (g sa); ?x22 s sa za na t s' = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n22 s sa za na t s' = length hs) r xf arrel axf ra t'; ?n22 s sa za na t s' \<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 = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z h sa t hsa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 4. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, t); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Abrupt za; s' = Normal (g sa); t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf 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 = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z h sa t hsa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, Normal t'); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Abrupt za; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (na = length hs) r xf arrel axf ra t'; na \<le> length hs\<rbrakk> \<Longrightarrow> \<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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile>\<^sub>h \<langle>hs,za\<rangle> \<Rightarrow> (na, Normal t'); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Abrupt za; (ta, t') \<in> sr; unif_rrel (na = length hs) r xf arrel axf ra t'; na \<le> length hs\<rbrakk> \<Longrightarrow> case (ra, ta) 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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 hsa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = h # hsa; n = length hsa; z = t; E\<turnstile> \<langle>h,Normal sa\<rangle> \<Rightarrow> t; \<not> isAbr t\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t')
 2. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile> \<langle>Basic g;;
c,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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); \<not> isAbr t; E\<turnstile> \<langle>Basic g,Normal sa\<rangle> \<Rightarrow> s'; E\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> 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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); \<not> isAbr t; E\<turnstile> \<langle>c,s'\<rangle> \<Rightarrow> t; s' = Normal (g 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')
 2. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); \<not> isAbr t; E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> t; s' = Normal (g 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')
 2. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s'. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); \<not> isAbr t; E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> t; s' = Normal (g sa)\<rbrakk> \<Longrightarrow> E\<turnstile>\<^sub>h \<langle>c # hs,g sa\<rangle> \<Rightarrow> (?n51 s sa t s', ?x51 s sa t s')
 2. \<And>s sa t s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); \<not> isAbr t; E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> t; s' = Normal (g sa); ?x51 s sa t s' = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (?n51 s sa t s' = length hs) r xf arrel axf ra t'; ?n51 s sa t s' \<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 True r xf arrel axf ra t')
 3. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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 s' t' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); \<not> isAbr t; E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> t; s' = Normal (g sa); t = Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel (length hs = length hs) r xf arrel axf ra t'; length hs \<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 True r xf arrel axf ra t')
 2. \<And>s s' n z sa. \<lbrakk>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Normal t'; (ra, ta) \<in> fst (a s); (ta, t') \<in> sr; unif_rrel True r xf arrel axf ra t'\<rbrakk> \<Longrightarrow> \<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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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' ra ta. \<lbrakk>(s, sa) \<in> sr; G s; sa \<in> G'; \<not> snd (a s); E\<turnstile> \<langle>c,Normal (g sa)\<rangle> \<Rightarrow> Normal t'; (ta, t') \<in> sr; unif_rrel True r xf arrel axf ra t'\<rbrakk> \<Longrightarrow> case (ra, ta) 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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (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>ccorres_underlying sr E r xf arrel axf G G' hs a c; (s, s') \<in> sr; G s; s' \<in> G'; \<not> snd (a s); s' = sa; (Basic g;;
c) # hs = []; n = 0; z = Abrupt sa\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>x\<in>fst (a s). case x of (ra, t) \<Rightarrow> (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!