kings-crown/FVELER_Isabelle huggingface dataset:
theory XPres

lemma xpres_strong_basic':
  assumes rl: "\<And>s. pres_norm \<Longrightarrow> xf s = v \<Longrightarrow> xf (f s) = v"
  shows "xpres_strong \<Gamma> xf v (Basic f) pres_norm pres_abr False" by (rule xpres_strongI; simp?; erule exec_Normal_elim_cases; clarsimp simp: rl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic f) pres_norm pres_abr False
theory XPres

lemma xpres_basic_False:
  "xpres_strong \<Gamma> xf v (Basic f) False True False" by (rule xpres_strong_basic, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic f) False True False
theory XPres

lemma xpres_exec_Normal:
  assumes "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal"
  assumes pres_norm
  assumes "\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t"
  assumes "xf s = v"
  shows "xf t = v" using assms unfolding xpres_strong_def apply - by (drule (1) mp | erule allE conjE trivial)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xf t = v proof (prove)
using this:
xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal
pres_norm
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t
xf s = v

goal (1 subgoal):
 1. xf t = v proof (prove)
using this:
(\<forall>s t. (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (abnormal \<longrightarrow> pres_norm)
pres_norm
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t
xf s = v

goal (1 subgoal):
 1. xf t = v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>s t. (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (abnormal \<longrightarrow> pres_norm); pres_norm; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v
theory XPres

lemma xpres_exec_Abrupt:
  assumes xp: "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal"
  assumes pa: pres_abr
  assumes ex: "\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Abrupt t"
  assumes xf: "xf s = v"
  shows   "xf t = v" using assms unfolding xpres_strong_def apply - by (drule (1) mp | erule allE conjE trivial)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xf t = v proof (prove)
using this:
xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal
pres_abr
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t
xf s = v

goal (1 subgoal):
 1. xf t = v proof (prove)
using this:
(\<forall>s t. (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (abnormal \<longrightarrow> pres_norm)
pres_abr
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t
xf s = v

goal (1 subgoal):
 1. xf t = v proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>s t. (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (abnormal \<longrightarrow> pres_norm); pres_abr; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v
theory XPres

lemma xpres_exec_abnormal:
  assumes "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal"
  assumes abnormal
  assumes "\<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t"
  shows "False" using assms unfolding xpres_strong_def apply - by (drule (1) mp | erule allE conjE notE)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. False proof (prove)
using this:
xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal
abnormal
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t

goal (1 subgoal):
 1. False proof (prove)
using this:
(\<forall>s t. (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (abnormal \<longrightarrow> pres_norm)
abnormal
\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t

goal (1 subgoal):
 1. False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<forall>s t. (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t \<longrightarrow> \<not> abnormal \<and> (pres_norm \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (\<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Abrupt t \<longrightarrow> pres_abr \<longrightarrow> xf s = v \<longrightarrow> xf t = v)) \<and> (abnormal \<longrightarrow> pres_norm); abnormal; \<Gamma>\<turnstile> \<langle>c,Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False
theory XPres

lemma xpres_seq:
  assumes xpa: "xpres \<Gamma> xf v a"
  assumes xpb: "xpres \<Gamma> xf v b"
  shows "xpres \<Gamma> xf v (a ;; b)" by (rule xpres_strong_seq[OF xpa xpb] xpres_eq_If_rules)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v (a;;
b)
theory XPres

lemma xpres_strong_while:
  assumes xp: "xpres_strong \<Gamma> xf v x pres_norm pres_abr abnormal"
  assumes pa: "xpres_eq_If pres_norm pres_abr False pres_abr'"
  shows   "xpres_strong \<Gamma> xf v (While b x) pres_norm pres_abr' False" unfolding pa[simplified xpres_eq_If_def if_bool_simps] apply (rule xpres_strongI) apply (erule xpres_strong_while0[OF _ xp refl]; simp)+ by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (While b x) pres_norm pres_abr' False proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (While b x) pres_norm (pres_norm \<and> pres_abr) False proof (prove)
goal (4 subgoals):
 1. \<And>s t. \<lbrakk>pres_norm; \<Gamma>\<turnstile> \<langle>While b x,Normal s\<rangle> \<Rightarrow> Normal t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v
 2. \<And>s t. \<lbrakk>pres_norm \<and> pres_abr; \<Gamma>\<turnstile> \<langle>While b x,Normal s\<rangle> \<Rightarrow> Abrupt t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v
 3. \<And>s t. \<lbrakk>False; \<Gamma>\<turnstile> \<langle>While b x,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>While b x,Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False
 2. False \<Longrightarrow> pres_norm
theory XPres

lemma xpres_strong_xpres_abnormalI:
  assumes abn: "xpres_strong \<Gamma> xf v c' pres_norm pres_abr' abnormal"
  assumes "\<And>s t. \<lbrakk>pres_norm; \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v"
  assumes "\<And>s t. \<lbrakk>pres_abr; \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Abrupt t; xf s = v\<rbrakk> \<Longrightarrow> xf t = v"
  assumes "\<And>s t. \<lbrakk>abnormal; \<Gamma> \<turnstile> \<langle>c, Normal s\<rangle> \<Rightarrow> Normal t\<rbrakk> \<Longrightarrow> False"
  shows "xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal" by (rule xpres_strongI[OF _ _ _ xpres_strong_abnormalD[OF abn]]; erule assms trivial; assumption)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v c pres_norm pres_abr abnormal
theory XPres

lemma xpres_catch:
  assumes "xpres \<Gamma> xf v b"
  assumes "xpres \<Gamma> xf v c"
  shows "xpres \<Gamma> xf v (Catch b c)" by (rule xpres_strong_catch[OF assms] xpres_eq_If_rules)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v (TRY
  b
CATCH c
END)
theory XPres

lemma xpres_cond:
  assumes "xpres \<Gamma> xf v a"
  assumes "xpres \<Gamma> xf v b"
  shows "xpres \<Gamma> xf v (Cond x a b)" by (rule xpres_strong_cond[OF assms] xpres_eq_If_rules)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v (Cond x a b)
theory XPres

lemma xpres_strong_throw':
  shows   "xpres_strong \<Gamma> xf v Throw True True abnormal" by (rule xpres_strongI; simp?; erule exec_Normal_elim_cases; simp)

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

lemma xpres_strong_creturn':
  assumes xfu: "\<And>s f. pres_abr \<Longrightarrow> xf (xfu f s) = xf s"
  and xfg: "\<And>s f. pres_abr \<Longrightarrow> xf (exnu f s) = xf s"
  shows   "xpres_strong \<Gamma> xf v (creturn exnu xfu v') True pres_abr abnormal" unfolding creturn_def by (rule xpres_strongI; clarsimp elim!: exec_Normal_elim_cases simp: xfu xfg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (creturn exnu xfu v') True pres_abr abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic (\<lambda>s. xfu (\<lambda>_. v' s) s);;
(Basic (exnu (\<lambda>_. Return));;
THROW)) True pres_abr abnormal
theory XPres

lemma xpres_strong_creturn_void':
  assumes xfg: "\<And>s f. pres_abr \<Longrightarrow> xf (exnu f s) = xf s"
  shows   "xpres_strong \<Gamma> xf v (creturn_void exnu) True pres_abr abnormal" unfolding creturn_void_def by (rule xpres_strongI; clarsimp elim!: exec_Normal_elim_cases simp: xfg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (creturn_void exnu) True pres_abr abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic (exnu (\<lambda>_. Return));;
THROW) True pres_abr abnormal
theory XPres

lemma xpres_strong_cbreak':
  assumes xfg: "\<And>s f. pres_abr \<Longrightarrow> xf (exnu f s) = xf s"
  shows   "xpres_strong \<Gamma> xf v (cbreak exnu) True pres_abr abnormal" unfolding cbreak_def by (rule xpres_strongI; clarsimp elim!: exec_Normal_elim_cases simp add: xfg)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (cbreak exnu) True pres_abr abnormal proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (Basic (exnu (\<lambda>_. Break));;
THROW) True pres_abr abnormal
theory XPres

lemma xpres_catchbrk_C:
  shows   "xpres \<Gamma> xf v (ccatchbrk exnu)" unfolding ccatchbrk_def by (rule xpresI; fastforce elim!: exec_Normal_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v (ccatchbrk exnu) proof (prove)
goal (1 subgoal):
 1. xpres \<Gamma> xf v (IF \<acute>exnu = Break THEN
  SKIP
ELSE
  THROW
FI)
theory XPres

lemma xpres_strong_lvar_nondet_init:
  assumes xfg: "\<And>s f. pres_norm \<Longrightarrow> xf (st f s) = xf s"
  shows   "xpres_strong \<Gamma> xf v (lvar_nondet_init gt st) pres_norm True False" by (auto intro!: xpres_strongI elim!: exec_Normal_elim_cases simp: xfg lvar_nondet_init_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xpres_strong \<Gamma> xf v (lvar_nondet_init gt st) pres_norm True False
theory Ctac

lemma match_ccorres:
  "ccorres_underlying sr G r xf' arrel axf P P' hs a c
      \<Longrightarrow> ccorres_underlying sr G r xf' arrel axf P P' hs a c" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf' arrel axf P P' hs a c \<Longrightarrow> ccorres_underlying sr G r xf' arrel axf P P' hs a c
theory Ctac

lemma match_ccorres_record:
  fixes xfru :: "('a \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b" and xf' :: "cstate \<Rightarrow> 'b" and xfr :: "'b \<Rightarrow> 'a"
  shows "ccorres_underlying sr G r (xfr \<circ> xf') arrel axf P P' hs a (c xfru)
          \<Longrightarrow> ccorres_underlying sr G r (xfr \<circ> xf') arrel axf P P' hs a (c xfru)" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r (xfr \<circ> xf') arrel axf P P' hs a (c xfru) \<Longrightarrow> ccorres_underlying sr G r (xfr \<circ> xf') arrel axf P P' hs a (c xfru)
theory Ctac

lemma match_ccorres_Seq:
  "ccorres_underlying sr G r xf arrel axf P P' hs a (c ;; d)
   \<Longrightarrow> ccorres_underlying sr G r xf arrel axf P P' hs a (c ;; d)" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf arrel axf P P' hs a (c;;
d) \<Longrightarrow> ccorres_underlying sr G r xf arrel axf P P' hs a (c;;
d)
theory Ctac

lemma match_ccorres_call_Seq:
  "ccorres_underlying sr G r xf arrel axf P P' hs a (call i f g c ;; d)
      \<Longrightarrow> ccorres_underlying sr G r xf arrel axf P P' hs a (call i f g c ;; d)" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr G r xf arrel axf P P' hs a (call i f g c;;
d) \<Longrightarrow> ccorres_underlying sr G r xf arrel axf P P' hs a (call i f g c;;
d)
theory Ctac

lemma ccorres_lift_rhs_remove_lvar_init:
  assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a d"
  assumes gg: "\<And>x f s. globals (i_upd f s) = globals s"
  assumes upd_acc: "\<And>s. i_upd (\<lambda>_. i_acc s) s = s"
  assumes arb: "\<And>s v. s \<in> G' \<Longrightarrow> i_upd (\<lambda>_. v) s \<in> G'"
  shows   "ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a (lvar_nondet_init i_acc i_upd ;; d)" apply (unfold lvar_nondet_init_def) apply (rule ccorres_guard_imp) apply (rule ccorres_lift_rhs_Spec_stateful [OF cc ceqv_refl gg]) apply (rule upd_acc) apply assumption apply (simp add: arb) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a (lvar_nondet_init i_acc i_upd;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a (Spec {(s, t). \<exists>v. t = i_upd (\<lambda>_. v) s};;
d) proof (prove)
goal (3 subgoals):
 1. ccorres_underlying rf_sr \<Gamma> r xf ar arf ?Q ?Q' hs a (Spec {(s, t). \<exists>v. t = i_upd (\<lambda>_. v) s};;
d)
 2. \<And>s. G s \<Longrightarrow> ?Q s
 3. \<And>s. s \<in> G' \<Longrightarrow> s \<in> ?Q' proof (prove)
goal (3 subgoals):
 1. \<And>s. i_upd (\<lambda>a. ?accessor4 s) s = s
 2. \<And>s. G s \<Longrightarrow> G s
 3. \<And>s. s \<in> G' \<Longrightarrow> s \<in> {s. \<forall>v. i_upd (\<lambda>a. v) s \<in> G'} proof (prove)
goal (2 subgoals):
 1. \<And>s. G s \<Longrightarrow> G s
 2. \<And>s. s \<in> G' \<Longrightarrow> s \<in> {s. \<forall>v. i_upd (\<lambda>a. v) s \<in> G'} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> G' \<Longrightarrow> s \<in> {s. \<forall>v. i_upd (\<lambda>a. v) s \<in> G'} proof (prove)
goal:
No subgoals!
theory Ctac

lemma ccorres_lift_rhs_remove_lvar_init_unknown_guard:
  assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf ar arf G G' hs a d"
  assumes gg: "\<And>x f s. globals (i_upd f s) = globals s"
  assumes upd_acc: "\<And>s. i_upd (\<lambda>_. i_acc s) s = s"
  shows   "ccorres_underlying rf_sr \<Gamma> r xf ar arf G {s. \<forall>v. i_upd (\<lambda>_. v) s \<in> G'} hs a (lvar_nondet_init i_acc i_upd ;; d)" unfolding lvar_nondet_init_def by (rule ccorres_lift_rhs_Spec_stateful [OF cc ceqv_refl gg], rule upd_acc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf ar arf G {s. \<forall>v. i_upd (\<lambda>_. v) s \<in> G'} hs a (lvar_nondet_init i_acc i_upd;;
d) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf ar arf G {s. \<forall>v. i_upd (\<lambda>_. v) s \<in> G'} hs a (Spec {(s, t). \<exists>v. t = i_upd (\<lambda>_. v) s};;
d)
theory Ctac

lemma ccorres_special_Int_cong:
  "(\<And>s. P s = P' s) \<Longrightarrow> ccorres r xf G (G' \<inter> {s. P s}) hs a c = ccorres r xf G (G' \<inter> {s. P' s}) hs a c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. P s = P' s) \<Longrightarrow> ccorres r xf G (G' \<inter> {s. P s}) hs a c = ccorres r xf G (G' \<inter> {s. P' s}) hs a c
theory Ctac

lemma ccorres_special_trim_Int:
  "ccorres r xf G G' hs a c \<Longrightarrow> ccorres r xf G (G' \<inter> P') hs a c" apply (erule ccorres_guard_imp) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf G G' hs a c \<Longrightarrow> ccorres r xf G (G' \<inter> P') hs a c proof (prove)
goal (2 subgoals):
 1. \<And>s. G s \<Longrightarrow> G s
 2. \<And>s. s \<in> G' \<inter> P' \<Longrightarrow> s \<in> G' proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> G' \<inter> P' \<Longrightarrow> s \<in> G' proof (prove)
goal:
No subgoals!
theory Ctac

lemma semantic_equiv_def2:
  fixes s :: "'b" and s' :: "('b, 'c) xstate"
  shows "semantic_equiv G s s' a a' \<equiv> ((G \<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s') = (G \<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'))" unfolding semantic_equiv_def ceqv_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv G s s' a a' \<equiv> G\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = G\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. () = () \<longrightarrow> G\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = G\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s' \<equiv> G\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = G\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'
theory Ctac

lemma semantic_equiv_While_cong:
  assumes se: "\<And>s s'. semantic_equiv Gamma s s' b b'"
  shows   "semantic_equiv Gamma s s' (While G b) (While G b')" using se apply - apply (rule semantic_equivI) apply (rule exec_While_cong) apply (simp add: semantic_equiv_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (While G b) (While G b') proof (prove)
using this:
semantic_equiv Gamma ?s1 ?s'1 b b'

goal (1 subgoal):
 1. semantic_equiv Gamma s s' (While G b) (While G b') proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. semantic_equiv Gamma s s' b b') \<Longrightarrow> semantic_equiv Gamma s s' (While G b) (While G b') proof (prove)
goal (1 subgoal):
 1. (\<And>s s'. semantic_equiv Gamma s s' b b') \<Longrightarrow> Gamma\<turnstile> \<langle>While G b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>While G b',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. (\<And>s s'. semantic_equiv Gamma s s' b b') \<Longrightarrow> Gamma\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Ctac

lemma semantic_equiv_Seq_cong:
  assumes sea: "\<And>s'. semantic_equiv Gamma s s' a a'"
  and     seb: "\<And>s. semantic_equiv Gamma s s' b b'"
  shows   "semantic_equiv Gamma s s' (a ;; b) (a' ;; b')" using sea seb apply (simp add: semantic_equiv_def2) apply (rule exec_Seq_cong) apply assumption apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
b) (a';;
b') proof (prove)
using this:
semantic_equiv Gamma s ?s'1 a a'
semantic_equiv Gamma ?s1 s' b b'

goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
b) (a';;
b') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s'. Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; \<And>s. Gamma\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>a;;
b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a';;
b',Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal (2 subgoals):
 1. \<And>s''. \<lbrakk>\<And>s'. Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; \<And>s. Gamma\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s\<rangle> \<Rightarrow> s'\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s''
 2. \<And>s''. \<lbrakk>\<And>s'. Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; \<And>s. Gamma\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s\<rangle> \<Rightarrow> s'; Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Normal s''\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal (1 subgoal):
 1. \<And>s''. \<lbrakk>\<And>s'. Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'; \<And>s. Gamma\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s\<rangle> \<Rightarrow> s'; Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> Normal s''\<rbrakk> \<Longrightarrow> Gamma\<turnstile> \<langle>b,Normal s''\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>b',Normal s''\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Ctac

lemma semantic_equiv_Seq_Skip:
  assumes se: "semantic_equiv Gamma s s' a a'"
  shows   "semantic_equiv Gamma s s' (a ;; SKIP) a'" using se unfolding semantic_equiv_def2 by (simp add: exec_Seq_Skip_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
SKIP) a' proof (prove)
using this:
semantic_equiv Gamma s s' a a'

goal (1 subgoal):
 1. semantic_equiv Gamma s s' (a;;
SKIP) a' proof (prove)
using this:
Gamma\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. Gamma\<turnstile> \<langle>a;;
SKIP,Normal s\<rangle> \<Rightarrow> s' = Gamma\<turnstile> \<langle>a',Normal s\<rangle> \<Rightarrow> s'
theory Ctac

lemma semantic_equiv_Guard_cong:
  assumes se: "semantic_equiv Gamma s s' a a'"
  shows   "semantic_equiv Gamma s s' (Guard F G a) (Guard F G a')" using se by (simp add: semantic_equiv_def2 exec_Guard)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (Guard F G a) (Guard F G a') proof (prove)
using this:
semantic_equiv Gamma s s' a a'

goal (1 subgoal):
 1. semantic_equiv Gamma s s' (Guard F G a) (Guard F G a')
theory Ctac

lemma semantic_equiv_Guard_UNIV:
  assumes se: "semantic_equiv Gamma s s' a a'"
  shows   "semantic_equiv Gamma s s' (Guard F UNIV a) a'" using se by (simp add: semantic_equiv_def2 exec_Guard_UNIV_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (Guard F UNIV a) a' proof (prove)
using this:
semantic_equiv Gamma s s' a a'

goal (1 subgoal):
 1. semantic_equiv Gamma s s' (Guard F UNIV a) a'
theory Ctac

lemma semantic_equiv_Guard_True:
  assumes se: "semantic_equiv Gamma s s' a a'"
  shows   "semantic_equiv Gamma s s' (Guard F \<lbrace>True\<rbrace> a) a'" using se by (simp add: semantic_equiv_def2 exec_Guard_UNIV_simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv Gamma s s' (Guard F \<lbrace>True\<rbrace> a) a' proof (prove)
using this:
semantic_equiv Gamma s s' a a'

goal (1 subgoal):
 1. semantic_equiv Gamma s s' (Guard F \<lbrace>True\<rbrace> a) a'