theory Ctac

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

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

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

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

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

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

goal (1 subgoal):
 1. \<not> c_pres_norm \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (c;;
d) pres_norm pres_abr abnormal (c';;
d') 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_norm 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_norm \<Longrightarrow> ceqv_xpres \<Gamma> xf v True (c;;
d) pres_norm pres_abr abnormal (c';;
d') proof (prove)
goal (1 subgoal):
 1. \<not> c_abnormal proof (prove)
using this:
ceqv_xpres \<Gamma> xf v True c c_pres_norm c_pres_abr c_abnormal c'

goal (1 subgoal):
 1. \<not> c_abnormal proof (state)
this:
\<not> c_abnormal

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

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

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

goal:
No subgoals!