theory Corres_UL_C

lemma ccorres_init_tmp_lift2:
  assumes rl: "\<And>t t'. ceqv \<Gamma> xf' rv' t t' c c'"
  and c: "ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'"
  shows "ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. xf' s = rv'}) hs m c" using c apply - apply (rule ccorresI') apply (erule (2) ccorresE) apply fastforce apply assumption apply simp apply (erule conjE)+ apply (erule (1) ceqvhD1 [OF _ _ rl]) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. xf' s = rv'}) hs m c proof (prove)
using this:
ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'

goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. xf' s = rv'}) hs m c proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c' \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G (G' \<inter> {s. xf' s = rv'}) hs m c proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c'; (s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (4 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> s' \<in> G'
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 4. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); ?x3 s s' n z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n3 s s' n z = length hs) rrel xf arrel axf r t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (3 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<not> snd (m s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 3. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); ?x3 s s' n z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n3 s s' n z = length hs) rrel xf arrel axf r t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 2. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); ?x3 s s' n z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n3 s s' n z = length hs) rrel xf arrel axf r t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<and> xf' s' = rv'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 2. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); ?x3 s s' n z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n3 s s' n z = length hs) rrel xf arrel axf r t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> srel; G s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); s' \<in> G'; xf' s' = rv'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 2. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); ?x3 s s' n z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n3 s s' n z = length hs) rrel xf arrel axf r t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<inter> {s. xf' s = rv'}; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(r, t)\<in>fst (m s). (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z t' r t. \<lbrakk>(s, s') \<in> srel; G s; s' \<in> G' \<and> xf' s' = rv'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (m s); z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (n = length hs) rrel xf arrel axf r t'; n \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (m s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> unif_rrel (n = length hs) rrel xf arrel axf r t' proof (prove)
goal:
No subgoals!