theory Corres_UL_C

lemma ccorres_context_cong_helper':
  assumes c: "ccorres_underlying sr \<Gamma> r xf ar axf P Q hs a c"
  assumes "\<And>s. P s = P' s"
  \<comment> \<open>Don't use membership equality when rewriting Q, as the LHS can be simplified into something
     that is unable to unify with the RHS.
  assumes "\<And>s s'. \<lbrakk> (s,s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> s' \<in> Q = (s' \<in> Q')"\<close>
  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s \<rbrakk> \<Longrightarrow> Q = Q'"
  assumes "hs = hs'"
  assumes "\<And>s s'. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk> \<Longrightarrow> a s = a' s"
  assumes "\<And>s s' s''. \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q' \<rbrakk>  \<Longrightarrow> semantic_equiv \<Gamma> s' s'' c c'"
  assumes "\<And>s s' t'.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
             xf t' = xf' t'"
  assumes "\<And>x s t s' t'.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s);
               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (size hs', Normal t') \<rbrakk> \<Longrightarrow>
             r x (xf' t') = r' x (xf' t')"
  assumes "\<And>s s' t' n.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; n \<noteq> size hs'; \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
             axf t' = axf' t'"
  assumes "\<And>x s t s' t' n.
             \<lbrakk> (s, s') \<in> sr; P' s; s' \<in> Q'; (t, t') \<in> sr; (x, t) \<in> fst (a' s); n \<noteq> size hs';
               \<Gamma> \<turnstile>\<^sub>h \<langle>c' # hs', s'\<rangle> \<Rightarrow> (n, Normal t') \<rbrakk> \<Longrightarrow>
             ar x (axf' t') = ar' x (axf' t')"
  shows   "ccorres_underlying sr \<Gamma> r' xf' ar' axf' P' Q' hs' a' c'" using c apply - apply (rule ccorresI') apply (erule (1) ccorresE) apply (force simp: assms) apply (force simp: assms) apply (force simp: assms) apply (clarsimp simp: assms) apply (erule exec_handlers_semantic_equivD2) apply (force simp: assms) apply (fastforce simp: unif_rrel_def assms) done

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

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