theory Corres_UL_C

lemma ccorres_Un:
  assumes pt: "ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c"
  and     pn: "ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c"
  shows "ccorres_underlying sr \<Gamma> r xf arrel axf P (PT \<union> PN) hs a c" using pt pn apply - apply (rule ccorresI) apply (erule UnE) apply (erule (5) ccorresE) apply simp apply (erule (5) ccorresE) apply simp apply (erule UnE) apply (erule (5) ccorresE) apply (erule bexI [rotated], clarsimp) apply (erule (5) ccorresE) apply (erule bexI [rotated], clarsimp) done

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

goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> r xf arrel axf P (PT \<union> PN) hs a c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P (PT \<union> PN) hs a c proof (prove)
goal (2 subgoals):
 1. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck\<rbrakk> \<Longrightarrow> False
 2. \<And>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<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. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck; s' \<in> PT\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck; s' \<in> PN\<rbrakk> \<Longrightarrow> False
 3. \<And>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<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 t' ra t. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck; s' \<in> PT; z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> False
 2. \<And>s s' n z. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck; s' \<in> PN\<rbrakk> \<Longrightarrow> False
 3. \<And>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<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>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck; s' \<in> PN\<rbrakk> \<Longrightarrow> False
 2. \<And>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<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 t' ra t. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; (s, s') \<in> sr; P s; \<not> snd (a s); \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, z); isAbr z \<or> isFault z \<or> z = Stuck; s' \<in> PN; z = Normal t'; (ra, t) \<in> fst (a s); (t, t') \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'; n \<le> length hs\<rbrakk> \<Longrightarrow> False
 2. \<And>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<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>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; s' \<in> PT \<union> PN; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s)\<rbrakk> \<Longrightarrow> \<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>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); s' \<in> PT\<rbrakk> \<Longrightarrow> \<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>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); s' \<in> PN\<rbrakk> \<Longrightarrow> \<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>n t' s s' t'a ra t. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); s' \<in> PT; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'a; n \<le> length hs\<rbrakk> \<Longrightarrow> \<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>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); s' \<in> PN\<rbrakk> \<Longrightarrow> \<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>n t' s s'. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; ccorres_underlying sr \<Gamma> r xf arrel axf P PN hs a c; (s, s') \<in> sr; P s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); s' \<in> PN\<rbrakk> \<Longrightarrow> \<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>n t' s s' t'a ra t. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf P PT hs a c; (s, s') \<in> sr; P s; \<Gamma>\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, Normal t'); \<not> snd (a s); s' \<in> PN; Normal t' = Normal t'a; (ra, t) \<in> fst (a s); (t, t'a) \<in> sr; unif_rrel (n = length hs) r xf arrel axf ra t'a; n \<le> length hs\<rbrakk> \<Longrightarrow> \<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!