theory Corres_UL_C

lemma stronger_ccorres_guard_imp:
  assumes x: "ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g"
  assumes y: "\<And>s s'. \<lbrakk> A s; s' \<in> A'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> Q s"
  assumes z: "\<And>s s'. \<lbrakk> A s; s' \<in> A'; (s, s') \<in> sr \<rbrakk> \<Longrightarrow> s' \<in> Q'"
  shows      "ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g" using x apply - apply (rule ccorresI') apply (erule (1) ccorresE) apply (erule (2) y) apply (erule (2) z) apply assumption apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
using this:
ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf A A' hs f g proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf Q Q' hs f g; (s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f 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 s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> Q s
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> s' \<in> Q'
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<not> snd (f s)
 4. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 5. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); ?x3 s s' n z = Normal t'; (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (?n3 s s' n z = length hs) r xf arrel axf ra t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f 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>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> s' \<in> Q'
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<not> snd (f s)
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 4. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); ?x3 s s' n z = Normal t'; (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (?n3 s s' n z = length hs) r xf arrel axf ra t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f 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>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<not> snd (f s)
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 3. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); ?x3 s s' n z = Normal t'; (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (?n3 s s' n z = length hs) r xf arrel axf ra t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f 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>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (?n3 s s' n z, ?x3 s s' n z)
 2. \<And>s s' n z t' ra t. \<lbrakk>(s, s') \<in> sr; A s; s' \<in> A'; \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (f s); ?x3 s s' n z = Normal t'; (ra, t) \<in> fst (f s); (t, t') \<in> sr; unif_rrel (?n3 s s' n z = length hs) r xf arrel axf ra t'; ?n3 s s' n z \<le> length hs\<rbrakk> \<Longrightarrow> \<exists>t'. z = Normal t' \<and> (\<exists>(ra, t)\<in>fst (f s). (t, t') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra t') proof (prove)
goal:
No subgoals!