theory XPres

lemma xpres_strong_seq:
  assumes xpa: "xpres_strong \<Gamma> xf v c c_pres_norm c_pres_abr c_abnormal"
  assumes xpb: "xpres_strong \<Gamma> xf v d d_pres_norm d_pres_abr d_abnormal"
  notes xps = xpa xpb
  \<comment> \<open>abnormal \<longleftrightarrow> c_abnormal \<or> d_abnormal\<close>
  \<comment> \<open>pres_norm \<longleftrightarrow> c_pres_norm \<and> d_pres_norm \<or> abnormal\<close>
  \<comment> \<open>pres_abr \<longleftrightarrow> c_pres_abr \<and> c_pres_norm \<and> d_pres_abr \<or> c_abnormal \<and> c_pres_abr\<close>
  assumes ifs: "xpres_eq_If c_abnormal True d_abnormal abnormal"
               "xpres_eq_If c_pres_norm d_pres_norm False cd_pres_norm"
               "xpres_eq_If cd_pres_norm True abnormal pres_norm"
               "xpres_eq_If c_pres_norm d_pres_abr False c_norm_d_pres_abr"
               "xpres_eq_If c_pres_abr c_norm_d_pres_abr False cd_pres_abr"
               "xpres_eq_If c_abnormal c_pres_abr False c_abnormal_pres_abr"
               "xpres_eq_If cd_pres_abr True c_abnormal_pres_abr pres_abr"
  shows "xpres_strong \<Gamma> xf v (c ;; d) pres_norm pres_abr abnormal" unfolding ifs[simplified xpres_eq_If_def if_bool_simps] apply (rule xpres_strongI
         ; simp?
         ; erule exec_Normal_elim_cases
         ; erule Normal_resultE Abrupt_resultE
         ; simp
         ; elim disjE conjE exec_elim_cases) apply (all \<open>(drule (1) xps[THEN xpres_exec_abnormal], simp)?\<close>) apply (all \<open>(drule (2) xpres_execs[OF xpa])\<close>, simp_all) apply (all \<open>(erule (2) xpres_execs[OF xpb])\<close>) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (c;;
d) pres_norm pres_abr abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (c;;
d) (c_pres_norm \<and> d_pres_norm \<or> c_abnormal \<or> d_abnormal) (c_pres_abr \<and> c_pres_norm \<and> d_pres_abr \<or> c_abnormal \<and> c_pres_abr) (c_abnormal \<or> d_abnormal) proof (prove)
goal (9 subgoals):
 1. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; c_pres_norm; d_pres_norm\<rbrakk> \<Longrightarrow> xf t = v
 2. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; c_abnormal\<rbrakk> \<Longrightarrow> xf t = v
 3. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; d_abnormal\<rbrakk> \<Longrightarrow> xf t = v
 4. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Abrupt t; s' = Normal ta; c_pres_abr; c_pres_norm; d_pres_abr\<rbrakk> \<Longrightarrow> xf t = v
 5. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Abrupt t; s' = Normal ta; c_abnormal; c_pres_abr\<rbrakk> \<Longrightarrow> xf t = v
 6. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt ta; s' = Abrupt ta; c_pres_abr; c_pres_norm; d_pres_abr; Abrupt t = Abrupt ta\<rbrakk> \<Longrightarrow> xf t = v
 7. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt ta; s' = Abrupt ta; c_abnormal; c_pres_abr; Abrupt t = Abrupt ta\<rbrakk> \<Longrightarrow> xf t = v
 8. \<And>s t s' ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; c_abnormal\<rbrakk> \<Longrightarrow> False
 9. \<And>s t s' ta. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; d_abnormal\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; c_pres_norm; d_pres_norm\<rbrakk> \<Longrightarrow> xf t = v
 2. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Abrupt t; s' = Normal ta; c_pres_abr; c_pres_norm; d_pres_abr\<rbrakk> \<Longrightarrow> xf t = v
 3. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt ta; s' = Abrupt ta; c_pres_abr; c_pres_norm; d_pres_abr; Abrupt t = Abrupt ta\<rbrakk> \<Longrightarrow> xf t = v
 4. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt ta; s' = Abrupt ta; c_abnormal; c_pres_abr; Abrupt t = Abrupt ta\<rbrakk> \<Longrightarrow> xf t = v proof (prove)
goal (2 subgoals):
 1. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Normal t; s' = Normal ta; d_pres_norm; xf ta = v\<rbrakk> \<Longrightarrow> xf t = v
 2. \<And>s t s' ta. \<lbrakk>xf s = v; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal ta; \<Gamma>\<turnstile> \<langle>d,Normal ta\<rangle> \<Rightarrow> Abrupt t; s' = Normal ta; c_pres_abr; d_pres_abr; xf ta = v\<rbrakk> \<Longrightarrow> xf t = v proof (prove)
goal:
No subgoals!