theory XPres

lemma xpres_strong_catch:
  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>abnormal \<longleftrightarrow> c_abnormal \<and> d_abnormal\<close>
  \<comment> \<open>pres_norm \<longleftrightarrow> abnormal \<or> c_pres_norm \<and> c_pres_abr \<and> d_pres_norm\<close>
  \<comment> \<open>pres_abr \<longleftrightarrow> c_pres_abr \<and> c_pres_abr\<close>
  assumes rew: "xpres_eq_If c_abnormal d_abnormal False abnormal"
               "xpres_eq_If c_pres_norm c_pres_abr False c_pres_norm_abr"
               "xpres_eq_If c_pres_norm_abr d_pres_norm False cd_pres_norm"
               "xpres_eq_If abnormal True cd_pres_norm pres_norm"
               "xpres_eq_If c_pres_abr d_pres_abr False pres_abr"
  shows "xpres_strong \<Gamma> xf v (Catch 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; simp?; (elim disjE conjE)?) apply (all \<open>(drule (1) xps[THEN xpres_exec_abnormal], simp)?\<close>) apply (all \<open>drule (2) xpres_execs[OF xpc], assumption?\<close>) apply (all \<open>drule (2) xpres_execs[OF xpd], assumption\<close>) done

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