theory XPres

lemma xpres_strong_cond:
  assumes xpc: "xpres_strong \<Gamma> xf v c c_pres_norm c_pres_abr c_abnormal"
  assumes xpd: "xpres_strong \<Gamma> xf v d d_pres_norm d_pres_abr d_abnormal"
  notes xps = xpc xpd
  \<comment> \<open>pres_norm \<longleftrightarrow> abnormal \<or> c_pres_norm \<and> d_pres_norm \<or> c_abnormal \<and> d_pres_norm \<or> c_pres_norm \<and> d_abnormal\<close>
  \<comment> \<open>pres_abr \<longleftrightarrow> c_pres_abr \<and> d_pres_abr\<close>
  \<comment> \<open>abnormal \<longleftrightarrow> c_abnormal \<and> d_abnormal\<close>
  assumes rew: "xpres_eq_If c_abnormal d_abnormal False abnormal"
               "xpres_eq_If c_pres_norm d_pres_norm False cd_pres_norm"
               "xpres_eq_If c_abnormal d_pres_norm False ca_pres_norm"
               "xpres_eq_If c_pres_norm d_abnormal False da_pres_norm"
               "xpres_eq_If ca_pres_norm True da_pres_norm cda_pres_norm"
               "xpres_eq_If cd_pres_norm True cda_pres_norm pres_norm'"
               "xpres_eq_If abnormal True pres_norm' pres_norm"
               "xpres_eq_If c_pres_abr d_pres_abr False pres_abr"
  shows "xpres_strong \<Gamma> xf v (Cond x c d) pres_norm pres_abr abnormal" unfolding rew[simplified xpres_eq_If_def if_bool_simps] apply (rule xpres_strongI; simp?; erule exec_Normal_elim_cases; elim disjE conjE) apply (all \<open>(drule (1) xps[THEN xpres_exec_abnormal], simp)?\<close>) apply (all \<open>(erule (2) xpres_execs[OF xpc] xpres_execs[OF xpd])\<close>) done

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