theory Corres_UL_C

lemma ccorres_cond_weak:
  assumes 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 (Pt and Pf) ((Rt \<inter> b) \<union> (Rf \<inter> -b)) hs a (Cond b  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 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 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 (Pt and Pf) (Rt \<inter> b \<union> Rf \<inter> - b) hs a (Cond b c c') proof (prove)
goal (1 subgoal):
 1. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (Pt and Pf) s; s' \<in> Rt \<inter> b \<union> Rf \<inter> - b; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b 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; (Pt and Pf) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rt \<inter> b\<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; (Pt and Pf) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - b\<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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rt \<inter> b\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a (Cond b c c') c
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rt \<inter> b; \<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; (Pt and Pf) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - b\<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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rt \<inter> b\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond b 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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rt \<inter> b; \<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; (Pt and Pf) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - b\<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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rt \<inter> b; \<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; (Pt and Pf) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - b\<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; (Pt and Pf) s; \<Gamma>\<turnstile>\<^sub>h \<langle>Cond b c c' # hs,s'\<rangle> \<Rightarrow> (n, z); \<not> snd (a s); s' \<in> Rf \<inter> - b\<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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rf \<inter> - b\<rbrakk> \<Longrightarrow> semantic_equiv \<Gamma> s' s'a c' (Cond b c c')
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rf \<inter> - b; \<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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rf \<inter> - b\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal s'\<rangle> \<Rightarrow> s'a = \<Gamma>\<turnstile> \<langle>Cond b c c',Normal s'\<rangle> \<Rightarrow> s'a
 2. \<And>s s' n z. \<lbrakk>(s, s') \<in> sr; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rf \<inter> - b; \<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; (Pt and Pf) s; \<not> snd (a s); s' \<in> Rf \<inter> - b; \<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!