theory Corres_UL_C

lemma ccorres_semantic_equiv0:
  assumes rl: "\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' 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' hs m c'" using c rl apply - apply (rule ccorresI') apply (erule (4) ccorresE) apply (erule exec_handlers_semantic_equivD2) apply assumption apply (clarsimp elim!: bexI [rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c' proof (prove)
using this:
ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c
?s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> ?s ?s' c c'

goal (1 subgoal):
 1. ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' hs m c; \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'\<rbrakk> \<Longrightarrow> ccorres_underlying srel \<Gamma> rrel xf arrel axf G G' 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; \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; (s, s') \<in> srel; G s; s' \<in> G'; \<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 (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; (s, s') \<in> srel; G s; s' \<in> G'; \<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> (?n5 s s' n z, ?x5 s s' n z)
 2. \<And>s s' n z t' r t. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; (s, s') \<in> srel; G s; s' \<in> G'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (m s); ?x5 s s' n z = Normal t'; (r, t) \<in> fst (m s); (t, t') \<in> srel; unif_rrel (?n5 s s' n z = length hs) rrel xf arrel axf r t'; ?n5 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 s'a. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; (s, s') \<in> srel; G s; s' \<in> G'; \<not> snd (m s)\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a c c'
 2. \<And>s s' n z t' r t. \<lbrakk>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; (s, s') \<in> srel; G s; s' \<in> G'; \<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>\<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv \<Gamma> s s' c c'; (s, s') \<in> srel; G s; s' \<in> G'; \<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:
No subgoals!