theory Corres_UL_C

lemma ccorres_handlers_weaken:
  assumes cul: "ccorres_underlying sr \<Gamma> rrel xf arrel axf P P' [] a c"
  shows   "ccorres_underlying sr \<Gamma> rrel xf arrel axf P P' hs a c" using cul apply - apply (rule ccorresI') apply (frule (5) ccorres_empty_handler_abrupt') apply (erule exec_handlers.cases) apply clarsimp apply (erule (4) ccorresE) apply (erule EHAbrupt [OF _ EHEmpty]) apply simp apply clarsimp apply (erule (4) ccorresE) apply (erule (1) EHOther) apply clarsimp apply (erule bexI [rotated], simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> rrel xf arrel axf P P' hs a c proof (prove)
using this:
ccorres_underlying sr \<Gamma> rrel xf arrel axf P P' [] a c

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