theory Corres_UL_C

lemma ccorres_cond_both:
  assumes abs: "\<forall>s s'. (s, s') \<in> sr \<and> R s \<longrightarrow> P s = (s' \<in> P')"
  and     c1: "ccorres_underlying sr \<Gamma> r xf arrel axf Pt Rt hs a c"
  and     c2: "ccorres_underlying sr \<Gamma> r xf arrel axf Pf Rf hs a c'"
  shows   "ccorres_underlying sr \<Gamma> r xf arrel axf (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) ((Rt \<inter> P') \<union> (Rf \<inter> - P')) hs a (Cond P' c c')" apply (rule ccorresI') apply (erule UnE) apply (drule exec_handlers_semantic_equivD1 [where b = c]) apply (rule semantic_equivI) apply (fastforce elim: exec_Normal_elim_cases intro: exec.CondTrue) apply (fastforce simp: abs elim: ccorresE [OF c1] elim!: bexI [rotated]) apply (drule exec_handlers_semantic_equivD2 [where b = c']) apply (rule semantic_equivI) apply (fastforce elim: exec_Normal_elim_cases intro: exec.CondFalse) apply (fastforce simp: abs elim: ccorresE [OF c2] elim!: bexI [rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) (Rt \<inter> P' \<union> Rf \<inter> - P') hs a (Cond P' c c') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; s' \<in> Rt \<inter> P' \<union> Rf \<inter> - P'; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # 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 (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rt \<inter> P'\<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')
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - P'\<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 s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rt \<inter> P'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a (Cond P' c c') c
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - P'\<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 s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rt \<inter> P'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond P' c c',Normal s'\<rangle> \<Rightarrow> s'a = \<Gamma>\<turnstile> \<langle>c,Normal s'\<rangle> \<Rightarrow> s'a
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 3. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - P'\<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>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rt \<inter> P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z)\<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')
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - P'\<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. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond P' c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - P'\<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 s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rf \<inter> - P'\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a c' (Cond P' c c')
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rf \<inter> - P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<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 s'a. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rf \<inter> - P'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> s'a = \<Gamma>\<turnstile> \<langle>Cond P' c c',Normal s'\<rangle> \<Rightarrow> s'a
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rf \<inter> - P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<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. \<lbrakk>(s, s') \<in> sr; (R and (\<lambda>s. P s \<longrightarrow> Pt s) and (\<lambda>s. \<not> P s \<longrightarrow> Pf s)) s; \<not> snd (a s); s' \<in> Rf \<inter> - P'; \<Gamma>\<turnstile>\<^sub>h \<langle>c' # hs,s'\<rangle> \<Rightarrow> (n, z)\<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!