theory Corres_UL_C

lemma ccorres_abstract:
  assumes ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and       cc: "\<And>rv'. ccorres_underlying sr \<Gamma> r xf arrel axf G (G' rv') hs a (d' rv')"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf G {s. s \<in> G' (xf' s)} hs a d" apply (rule ccorresI') apply (erule (1) ccorresE [OF cc]) apply simp apply assumption apply (erule ceqvhD1 [OF _ refl ceqv]) apply (clarsimp elim!: bexI [rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf G {s. s \<in> G' (xf' s)} hs a d proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # 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 (4 subgoals):
 1. \<And>s s' n z. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> s' \<in> G' (?rv'3 s s' n z)
 2. \<And>s s' n z. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 3. \<And>s s' n z. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d' (?rv'3 s s' n z) # hs,s'\<rangle> \<Rightarrow> (?n2 s s' n z, ?x2 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); ?x2 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n2 s s' n z = length hs) r xf arrel axf ra t'; ?n2 s s' n z \<le> length hs\<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. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<not> snd (a s)
 2. \<And>s s' n z. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d' (xf' s') # hs,s'\<rangle> \<Rightarrow> (?n2 s s' n z, ?x2 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); ?x2 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n2 s s' n z = length hs) r xf arrel axf ra t'; ?n2 s s' n z \<le> length hs\<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. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>d' (xf' s') # hs,s'\<rangle> \<Rightarrow> (?n2 s s' n z, ?x2 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); ?x2 s s' n z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (?n2 s s' n z = length hs) r xf arrel axf ra t'; ?n2 s s' n z \<le> length hs\<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 t' ra t. \<lbrakk>G s; s' \<in> {s. s \<in> G' (xf' s)}; \<Gamma>\<turnstile>\<^sub>h \<langle>d # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs\<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!