kings-crown/FVELER_Isabelle huggingface dataset:
theory Ctac

lemma Basic_ceqv:
  assumes rl: "rewrite_xf xf t v f f'"
  shows   "ceqv \<Gamma> xf v t t' (Basic f) (Basic f')" apply - apply (rule ceqvI) apply (drule rewrite_xfD [OF rl]) apply rule apply (erule exec_Normal_elim_cases) apply simp apply rule apply (erule exec_Normal_elim_cases) apply simp apply (erule subst) apply (rule exec.Basic) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Basic f) (Basic f') proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Basic f) (Basic f') proof (prove)
goal (1 subgoal):
 1. xf t = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. f t = f' t \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f t = f' t; \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>f t = f' t; \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f t = f' t; t' = Normal (f t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t'
 2. \<lbrakk>f t = f' t; \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>f t = f' t; t' = Normal (f' t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> Normal (f' t)
 2. \<lbrakk>f t = f' t; \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f t = f' t; \<Gamma>\<turnstile> \<langle>Basic f',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f t = f' t; t' = Normal (f' t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f t = f' t; t' = Normal (f' t)\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> Normal (f' t) proof (prove)
goal (1 subgoal):
 1. t' = Normal (f' t) \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Basic f,Normal t\<rangle> \<Rightarrow> Normal (f t) proof (prove)
goal:
No subgoals!
theory Ctac

lemma xpres_ceqv:
  assumes xp: "xpres_strong \<Gamma> xf v a pres_norm pres_abr abnormal"
  and    ceq: "\<And>t t'. ceqv \<Gamma> xf v t t' a a'"
  shows  "xpres_strong \<Gamma> xf v a' pres_norm pres_abr False" apply (rule xpres_strongI) apply (drule (1) ceqvD2[OF _ _ ceq], erule (2) xpres_execs[OF xp])+ by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v a' pres_norm pres_abr False proof (prove)
goal (4 subgoals):
 1. \<And>s t. \<lbrakk>pres_norm; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Normal t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v
 2. \<And>s t. \<lbrakk>pres_abr; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Abrupt t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v
 3. \<And>s t. \<lbrakk>False; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False
 4. False \<Longrightarrow> pres_norm proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>False; \<Gamma>\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False
 2. False \<Longrightarrow> pres_norm
theory Ctac

lemma call_ceqv':
  assumes ieq: "\<And>t. rewrite_xf xf t v i i'"
  and    ceqv: "\<And>t t' s'. ceqv \<Gamma> xf v (r t s') t' (c t s') (c' t s')" (* For record field updates *)
  and     xf:  "\<And>t t'. xf (r t t') = xf t"
  shows   "ceqv \<Gamma> xf v t t' (call i f r c) (call i' f r c')" by (rule call_ceqv [OF ieq ceqv], simp add: xf)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (call i f r c) (call i' f r c')
theory Ctac

lemma Catch_ceqv_weak_imp:
  assumes "\<And>s t. ceqv \<Gamma> xf v s t c c'"
  assumes "xf s = v"
  assumes "\<Gamma> \<turnstile> \<langle>Catch c d, Normal s\<rangle> \<Rightarrow> t"
  shows "\<Gamma> \<turnstile> \<langle>Catch c' d, Normal s\<rangle> \<Rightarrow> t" using assms apply (clarsimp simp: ceqv_def) apply (erule exec_Normal_elim_cases; simp; erule (1) exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>TRY
  c'
CATCH d
END,Normal s\<rangle> \<Rightarrow> t proof (prove)
using this:
ceqv \<Gamma> xf v ?s ?t c c'
xf s = v
\<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> t

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>TRY
  c'
CATCH d
END,Normal s\<rangle> \<Rightarrow> t proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>sa t. xf sa = xf s \<longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal sa\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>c',Normal sa\<rangle> \<Rightarrow> t; \<Gamma>\<turnstile> \<langle>TRY
  c
CATCH d
END,Normal s\<rangle> \<Rightarrow> t; v = xf s\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>TRY
  c'
CATCH d
END,Normal s\<rangle> \<Rightarrow> t proof (prove)
goal:
No subgoals!
theory Ctac

lemma Catch_ceqv_weak:
  assumes c: "\<And>s t. ceqv \<Gamma> xf v s t c c'"
  notes s = ceqv_sym[OF c]
  notes cs = c s
  shows "ceqv \<Gamma> xf v t t' (Catch c d) (Catch c' d)" by (intro ceqvI iffI; erule (1) cs[THEN Catch_ceqv_weak_imp])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (TRY
  c
CATCH d
END) (TRY
  c'
CATCH d
END)
theory Ctac

lemma Collect_mem_eqv:
  "rewrite_xf xf t v Q Q' \<Longrightarrow> xf t = v \<longrightarrow> (t \<in> Collect Q) = (t \<in> Collect Q')" apply (rule impI) apply (drule (1) rewrite_xfD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rewrite_xf xf t v Q Q' \<Longrightarrow> xf t = v \<longrightarrow> (t \<in> Collect Q) = (t \<in> Collect Q') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>rewrite_xf xf t v Q Q'; xf t = v\<rbrakk> \<Longrightarrow> (t \<in> Collect Q) = (t \<in> Collect Q') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf t = v; Q t = Q' t\<rbrakk> \<Longrightarrow> (t \<in> Collect Q) = (t \<in> Collect Q') proof (prove)
goal:
No subgoals!
theory Ctac

lemma UNIV_mem_eqv:
  "xf t = v \<longrightarrow> (t \<in> UNIV) = (t \<in> UNIV)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xf t = v \<longrightarrow> (t \<in> UNIV) = (t \<in> UNIV)
theory Ctac

lemma empty_mem_eqv:
  "xf t = v \<longrightarrow> (t \<in> {}) = (t \<in> {})" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xf t = v \<longrightarrow> (t \<in> {}) = (t \<in> {})
theory Ctac

lemma Cond_empty_ceqv: (* Crops up occasionally *)
  assumes ca: "ceqv \<Gamma> xf v t t' b b'"
  shows   "ceqv \<Gamma> xf v t t' (Cond {} a b) b'" using ca apply - apply (rule ceqvI) apply (auto elim!: exec_Normal_elim_cases dest: ceqvD1 ceqvD2 intro: exec.intros) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Cond {} a b) b' proof (prove)
using this:
ceqv \<Gamma> xf v t t' b b'

goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' (Cond {} a b) b' proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v t t' b b' \<Longrightarrow> ceqv \<Gamma> xf v t t' (Cond {} a b) b' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv \<Gamma> xf v t t' b b'; xf t = v\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> \<langle>Cond {} a b,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>b',Normal t\<rangle> \<Rightarrow> t' proof (prove)
goal:
No subgoals!
theory Ctac

lemma ceqv_xpresI:
  assumes "\<And>s t. ceqv \<Gamma> xf v s t c c'"
  assumes "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal"
  shows "ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'" using assms by (simp add: ceqv_xpres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c' proof (prove)
using this:
ceqv \<Gamma> xf v ?s ?t c c'
xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'
theory Ctac

lemma ceqv_xpres_ceqvD:
  assumes "ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'"
  shows "ceqv \<Gamma> xf v s t c c'" using assms by (simp add: ceqv_xpres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v s t c c' proof (prove)
using this:
ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'

goal (1 subgoal):
 1. ceqv \<Gamma> xf v s t c c'
theory Ctac

lemma ceqv_xpres_xpresD:
  assumes "ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'"
  shows "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal" using assms by (simp add: ceqv_xpres_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal proof (prove)
using this:
ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'

goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal
theory Ctac

lemma ceqv_xpres_abnormalD:
  assumes "ceqv_xpres \<Gamma> xf v pres_cont c pres_norm pres_abr abnormal c'"
  shows "xpres_abnormal \<Gamma> c abnormal" using assms by (auto simp: ceqv_xpres_def xpres_strong_def xpres_abnormal_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_abnormal \<Gamma> c abnormal proof (prove)
using this:
ceqv_xpres \<Gamma> xf v pres_cont c pres_norm pres_abr abnormal c'

goal (1 subgoal):
 1. xpres_abnormal \<Gamma> c abnormal
theory Ctac

lemma ceqv_xpres_abnormal_iff:
  "ceqv_xpres \<Gamma> xf v False c abnormal False abnormal c \<longleftrightarrow> xpres_abnormal \<Gamma> c abnormal" by (auto simp: ceqv_xpres_def xpres_strong_def xpres_abnormal_def ceqv_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v False c abnormal False abnormal c = xpres_abnormal \<Gamma> c abnormal
theory Ctac

lemma ceqv_xpres_xfdc:
  "ceqv_xpres \<Gamma> xfdc v pres c pres pres False c" by (auto simp: ceqv_xpres_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xfdc v pres c pres pres False c
theory Ctac

lemma ceqv_xpres_call_restore_argsI:
  "\<forall> s. f s = g s \<Longrightarrow> ceqv_xpres_call_restore_args i f g" by (simp add: ceqv_xpres_call_restore_args_def fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. f s = g s \<Longrightarrow> ceqv_xpres_call_restore_args i f g
theory Ctac

lemma ceqv_xpres_Cond:
  assumes rws: "ceqv_xpres_rewrite_set xf v S S'"
  assumes cxs: "ceqv_xpres \<Gamma> xf v True c c_pres_norm c_pres_abr c_abnormal c'"
               "ceqv_xpres \<Gamma> xf v True d d_pres_norm d_pres_abr d_abnormal d'"
  \<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 ifs: "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 "ceqv_xpres \<Gamma> xf v True (Cond S c d) pres_norm pres_abr abnormal (Cond S' c' d')" apply (rule ceqv_xpresI[OF Cond_ceqv[OF _ cxs[THEN ceqv_xpres_ceqvD]]
                                  xpres_strong_cond[OF cxs[THEN ceqv_xpres_xpresD] ifs]]) using rws by (simp add: ceqv_xpres_rewrite_set_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (Cond S c d) pres_norm pres_abr abnormal (Cond S' c' d') proof (prove)
goal (1 subgoal):
 1. \<And>s t ta. xf ta = v \<longrightarrow> (ta \<in> S) = (ta \<in> S') proof (prove)
using this:
ceqv_xpres_rewrite_set xf v S S'

goal (1 subgoal):
 1. \<And>s t ta. xf ta = v \<longrightarrow> (ta \<in> S) = (ta \<in> S')
theory Ctac

lemma ceqv_xpres_Guard:
  assumes "ceqv_xpres_rewrite_set xf v S S'"
  assumes "ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'"
  shows "ceqv_xpres \<Gamma> xf v True (Guard g S c) pres_norm pres_abr abnormal (Guard g S' c')" using assms apply (clarsimp simp: ceqv_xpres_def xpres_strong_guard) apply (rule Guard_ceqv) apply (simp add: ceqv_xpres_rewrite_set_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (Guard g S c) pres_norm pres_abr abnormal (Guard g S' c') proof (prove)
using this:
ceqv_xpres_rewrite_set xf v S S'
ceqv_xpres \<Gamma> xf v True c pres_norm pres_abr abnormal c'

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (Guard g S c) pres_norm pres_abr abnormal (Guard g S' c') proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s t (Guard g S c) (Guard g S' c') proof (prove)
goal (2 subgoals):
 1. \<And>s t ta. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> xf ta = v \<longrightarrow> (ta \<in> S) = (ta \<in> S')
 2. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s t c c' proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>ceqv_xpres_rewrite_set xf v S S'; \<forall>s t. ceqv \<Gamma> xf v s t c c'; xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s t c c' proof (prove)
goal:
No subgoals!
theory Ctac

lemma ceqv_xpres_Basic:
  assumes "ceqv_xpres_rewrite_basic xf v f f'"
  assumes "ceqv_xpres_basic_preserves (Basic f) xf v \<top> f' pres"
  shows "ceqv_xpres \<Gamma> xf v True (Basic f) pres pres_abr False (Basic f')" using assms apply (simp add: ceqv_xpres_def ceqv_xpres_rewrite_basic_def ceqv_xpres_basic_preserves_def) apply (intro allI impI conjI) apply (rule Basic_ceqv) apply (simp add: rewrite_xf_def) apply (rule xpres_strong_basic', simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (Basic f) pres pres_abr False (Basic f') proof (prove)
using this:
ceqv_xpres_rewrite_basic xf v f f'
ceqv_xpres_basic_preserves (Basic f) xf v (\<lambda>_. True) f' pres

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (Basic f) pres pres_abr False (Basic f') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. xf s = v \<longrightarrow> f s = f' s; pres \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f' s) = v)\<rbrakk> \<Longrightarrow> (\<forall>s t. ceqv \<Gamma> xf v s t (Basic f) (Basic f')) \<and> xpres_strong \<Gamma> xf v (Basic f) pres pres_abr False proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s. xf s = v \<longrightarrow> f s = f' s; pres \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f' s) = v)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf v s t (Basic f) (Basic f')
 2. \<lbrakk>\<forall>s. xf s = v \<longrightarrow> f s = f' s; pres \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f' s) = v)\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (Basic f) pres pres_abr False proof (prove)
goal (2 subgoals):
 1. \<And>s t. \<lbrakk>\<forall>s. xf s = v \<longrightarrow> f s = f' s; pres \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f' s) = v)\<rbrakk> \<Longrightarrow> rewrite_xf xf s v f f'
 2. \<lbrakk>\<forall>s. xf s = v \<longrightarrow> f s = f' s; pres \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f' s) = v)\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (Basic f) pres pres_abr False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. xf s = v \<longrightarrow> f s = f' s; pres \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (f' s) = v)\<rbrakk> \<Longrightarrow> xpres_strong \<Gamma> xf v (Basic f) pres pres_abr False proof (prove)
goal:
No subgoals!
theory Ctac

lemma ceqv_xpres_call_ceqv_xpres:
  assumes "ceqv_xpres_call \<Gamma> xf v f glob i ret pres_norm pres_abr abnormal i' ret'"
  shows "ceqv_xpres \<Gamma> xf v True (call i f glob ret) pres_norm pres_abr abnormal (call i' f glob ret')" using assms by (simp add: ceqv_xpres_call_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (call i f glob ret) pres_norm pres_abr abnormal (call i' f glob ret') proof (prove)
using this:
ceqv_xpres_call \<Gamma> xf v f glob i ret pres_norm pres_abr abnormal i' ret'

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (call i f glob ret) pres_norm pres_abr abnormal (call i' f glob ret')
theory Ctac

lemma ceqv_xpres_Skip:
  "ceqv_xpres \<Gamma> xf v True Skip True True False Skip" by (simp add: ceqv_xpres_def Skip_ceqv xpres_skip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True SKIP True True False SKIP
theory Ctac

lemma exec_Basic_Seq:
  "\<Gamma> \<turnstile> \<langle>Basic f ;; c, Normal s\<rangle> \<Rightarrow> s'
     = \<Gamma> \<turnstile> \<langle>c, Normal (f s)\<rangle> \<Rightarrow> s'" by (auto elim: exec_elim_cases intro: exec.Basic exec.Seq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Basic f;;
c,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>c,Normal (f s)\<rangle> \<Rightarrow> s'
theory Ctac

lemma exec_Basic_Seq_Basic:
  "\<Gamma>\<turnstile> \<langle>Basic f;; Basic g, x\<rangle> \<Rightarrow> y = \<Gamma>\<turnstile> \<langle>Basic (g \<circ> f), x\<rangle> \<Rightarrow> y" by (auto simp: o_def elim: exec_elim_cases intro: exec.Basic exec.Seq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>Basic f;;
Basic g,x\<rangle> \<Rightarrow> y = \<Gamma>\<turnstile> \<langle>Basic (g \<circ> f),x\<rangle> \<Rightarrow> y
theory Ctac

lemma ceqv_xpres_creturn:
  assumes "abnormal \<longrightarrow> pres_norm"
  assumes "ceqv_xpres_rewrite_basic xf v qf qf'"
  assumes "\<And>f. ceqv_xpres_basic_preserves (creturn exu xfu qf, 1) xf v \<top> (xfu f) pres'"
  assumes "\<And>f. ceqv_xpres_basic_preserves (creturn exu xfu qf, 2) xf v \<top> (exu f) pres''"
  assumes "xpres_eq_If pres' pres'' False pres"
  shows "ceqv_xpres \<Gamma> xf v True (creturn exu xfu qf) pres_norm pres abnormal (creturn exu xfu qf')" using assms apply (simp add: ceqv_xpres_defs ceqv_xpres_rewrite_basic_def
                   ceqv_xpres_basic_preserves_def creturn_def
                   xpres_eq_If_def if_bool_simps) apply (auto elim!: exec_elim_cases simp: exec_Basic_Seq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (creturn exu xfu qf) pres_norm pres abnormal (creturn exu xfu qf') proof (prove)
using this:
abnormal \<longrightarrow> pres_norm
ceqv_xpres_rewrite_basic xf v qf qf'
ceqv_xpres_basic_preserves (creturn exu xfu qf, 1::'g) xf v (\<lambda>_. True) (xfu ?f) pres'
ceqv_xpres_basic_preserves (creturn exu xfu qf, 2::'j) xf v (\<lambda>_. True) (exu ?f) pres''
xpres_eq_If pres' pres'' False pres

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (creturn exu xfu qf) pres_norm pres abnormal (creturn exu xfu qf') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>abnormal \<longrightarrow> pres_norm; \<forall>s. xf s = v \<longrightarrow> qf s = qf' s; \<And>f. pres' \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (xfu f s) = v); \<And>f. pres'' \<longrightarrow> (\<forall>s. xf s = v \<longrightarrow> xf (exu f s) = v); pres = (pres' \<and> pres'')\<rbrakk> \<Longrightarrow> (\<forall>s. xf s = v \<longrightarrow> (\<forall>t. \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. qf s) s);;
(Basic (exu (\<lambda>_. Return));;
THROW),Normal s\<rangle> \<Rightarrow> t = \<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. qf' s) s);;
(Basic (exu (\<lambda>_. Return));;
THROW),Normal s\<rangle> \<Rightarrow> t)) \<and> (\<forall>s t. (\<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. qf s) s);;
(Basic (exu (\<lambda>_. Return));;
THROW),Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>Basic (\<lambda>s. xfu (\<lambda>_. qf s) s);;
(Basic (exu (\<lambda>_. Return));;
THROW),Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres' \<and> pres'' \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) proof (prove)
goal:
No subgoals!
theory Ctac

lemma ceqv_xpres_Throw:
  "ceqv_xpres \<Gamma> xf v True Throw True True abnormal Throw" by (simp add: ceqv_xpres_def Throw_ceqv xpres_strong_throw')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True THROW True True abnormal THROW
theory Ctac

lemma ceqv_xpres_creturn_void:
  assumes "abnormal \<longrightarrow> pres_norm"
  assumes "\<And>f. ceqv_xpres_basic_preserves (creturn_void exu) xf v \<top> (exu f) pres"
  shows "ceqv_xpres \<Gamma> xf v True (creturn_void exu) pres_norm pres abnormal (creturn_void exu)" using assms by (auto simp: ceqv_xpres_defs creturn_void_def ceqv_xpres_basic_preserves_def
                      elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (creturn_void exu) pres_norm pres abnormal (creturn_void exu) proof (prove)
using this:
abnormal \<longrightarrow> pres_norm
ceqv_xpres_basic_preserves (creturn_void exu) xf v (\<lambda>_. True) (exu ?f) pres

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (creturn_void exu) pres_norm pres abnormal (creturn_void exu)
theory Ctac

lemma ceqv_xpres_cbreak:
  assumes "abnormal \<longrightarrow> pres_norm"
  assumes "\<And>f. ceqv_xpres_basic_preserves (cbreak exu) xf v \<top> (exu f) pres"
  shows "ceqv_xpres \<Gamma> xf v True (cbreak exu) pres_norm pres abnormal (cbreak exu)" using assms by (auto simp: ceqv_xpres_defs cbreak_def ceqv_xpres_basic_preserves_def
                      elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (cbreak exu) pres_norm pres abnormal (cbreak exu) proof (prove)
using this:
abnormal \<longrightarrow> pres_norm
ceqv_xpres_basic_preserves (cbreak exu) xf v (\<lambda>_. True) (exu ?f) pres

goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (cbreak exu) pres_norm pres abnormal (cbreak exu)
theory Ctac

lemma ceqv_xpres_ccatchbrk:
  "ceqv_xpres \<Gamma> xf v True (ccatchbrk exv) True True False (ccatchbrk exv)" by (auto simp: ceqv_xpres_defs ccatchbrk_def ceqv_xpres_basic_preserves_def
          elim!: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv_xpres \<Gamma> xf v True (ccatchbrk exv) True True False (ccatchbrk exv)