theory Ctac

lemma ceqv_xpres_Catch:
  assumes cxc: "ceqv_xpres \<Gamma> xf v True c c_pres_norm c_pres_abr c_abnormal c'"
  assumes cxd: "ceqv_xpres \<Gamma> xf v c_pres_abr d d_pres_norm d_pres_abr d_abnormal d'"
  notes cxs = cxc cxd
  \<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 "ceqv_xpres \<Gamma> xf v True (Catch c d) pres_norm pres_abr abnormal (Catch c' d')" proof (cases c_pres_abr) case True note cxs' = cxs[simplified True] note ceqvs = cxs'[THEN ceqv_xpres_ceqvD] note xpres = cxs'[THEN ceqv_xpres_xpresD] note rew' = rew[simplified True] show ?thesis apply (rule ceqv_xpresI[OF Catch_ceqv[OF ceqvs xpres(1)]]) apply (rule xpres_strong_catch[OF xpres rew']) done next case False have 1: "d_pres_norm = d_abnormal \<and> \<not> d_pres_abr \<and> d' = d" using cxd by (simp add: False ceqv_xpres_def) have 3: "abnormal = (d_abnormal \<and> c_abnormal) \<and> pres_norm = abnormal \<and> \<not> pres_abr" using 1 rew by (auto simp add: False xpres_eq_If_def if_bool_simps) show ?thesis apply (simp add: 1 3) apply (rule ceqv_xpresI[OF Catch_ceqv_weak[OF cxc[THEN ceqv_xpres_ceqvD]]]) apply (clarsimp simp: xpres_strong_def cong: conj_cong) apply (erule exec_Normal_elim_cases
         ; erule Normal_resultE
         ; erule (1) cxs[THEN ceqv_xpres_abnormalD, THEN xpres_abnormalD])+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
goal (2 subgoals):
 1. c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)
 2. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
this:
c_pres_abr

goal (2 subgoals):
 1. c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)
 2. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
this:
ceqv_xpres \<Gamma> xf v True c c_pres_norm True c_abnormal c'
ceqv_xpres \<Gamma> xf v True d d_pres_norm d_pres_abr d_abnormal d'

goal (2 subgoals):
 1. c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)
 2. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
this:
ceqv \<Gamma> xf v ?s ?t c c'
ceqv \<Gamma> xf v ?s ?t d d'

goal (2 subgoals):
 1. c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)
 2. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
this:
xpres_strong \<Gamma> xf v c c_pres_norm True c_abnormal
xpres_strong \<Gamma> xf v d d_pres_norm d_pres_abr d_abnormal

goal (2 subgoals):
 1. c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)
 2. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
this:
xpres_eq_If c_abnormal d_abnormal False abnormal
xpres_eq_If c_pres_norm True 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 True d_pres_abr False pres_abr

goal (2 subgoals):
 1. c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)
 2. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal proof (prove)
goal:
No subgoals! proof (state)
this:
ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)

goal (1 subgoal):
 1. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
goal (1 subgoal):
 1. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (state)
this:
\<not> c_pres_abr

goal (1 subgoal):
 1. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (prove)
goal (1 subgoal):
 1. d_pres_norm = d_abnormal \<and> \<not> d_pres_abr \<and> d' = d proof (prove)
using this:
ceqv_xpres \<Gamma> xf v c_pres_abr d d_pres_norm d_pres_abr d_abnormal d'

goal (1 subgoal):
 1. d_pres_norm = d_abnormal \<and> \<not> d_pres_abr \<and> d' = d proof (state)
this:
d_pres_norm = d_abnormal \<and> \<not> d_pres_abr \<and> d' = d

goal (1 subgoal):
 1. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (prove)
goal (1 subgoal):
 1. abnormal = (d_abnormal \<and> c_abnormal) \<and> pres_norm = abnormal \<and> \<not> pres_abr proof (prove)
using this:
d_pres_norm = d_abnormal \<and> \<not> d_pres_abr \<and> d' = d
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

goal (1 subgoal):
 1. abnormal = (d_abnormal \<and> c_abnormal) \<and> pres_norm = abnormal \<and> \<not> pres_abr proof (state)
this:
abnormal = (d_abnormal \<and> c_abnormal) \<and> pres_norm = abnormal \<and> \<not> pres_abr

goal (1 subgoal):
 1. \<not> c_pres_abr \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END) proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) (d_abnormal \<and> c_abnormal) False (d_abnormal \<and> c_abnormal) (TRY
  c'
CATCH d
END) proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (TRY
  c
CATCH d
END) (d_abnormal \<and> c_abnormal) False (d_abnormal \<and> c_abnormal) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>\<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> Normal t; d_abnormal; c_abnormal\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
ceqv_xpres \<Gamma> xf v True (TRY
  c
CATCH d
END) pres_norm pres_abr abnormal (TRY
  c'
CATCH d'
END)

goal:
No subgoals!