kings-crown/FVELER_Isabelle huggingface dataset:
theory SIMPL_Lemmas

lemma Cond_false:
  "\<Gamma> \<turnstile>\<^bsub>/F\<^esub> P f Q, A \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/F\<^esub> (P \<inter> - b) Cond b t f Q, A" apply (rule hoare_complete) apply (drule hoare_sound) apply (clarsimp simp: HoarePartialDef.cvalid_def HoarePartialDef.valid_def) apply (erule exec_Normal_elim_cases) apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P f Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> (P \<inter> - b) Cond b t f Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P f Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> (P \<inter> - b) Cond b t f Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>,{}\<Turnstile>\<^bsub>/F\<^esub> P f Q,A \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/F\<^esub> (P \<inter> - b) Cond b t f Q,A proof (prove)
goal (1 subgoal):
 1. \<And>ta x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>f,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; \<Gamma>\<turnstile> \<langle>Cond b t f,Normal x\<rangle> \<Rightarrow> ta; x \<in> P; x \<notin> b; ta \<notin> Fault ` F; ta \<notin> Abrupt ` A\<rbrakk> \<Longrightarrow> ta \<in> Normal ` Q proof (prove)
goal (2 subgoals):
 1. \<And>ta x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>f,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; x \<in> P; x \<notin> b; ta \<notin> Fault ` F; ta \<notin> Abrupt ` A; x \<in> b; \<Gamma>\<turnstile> \<langle>t,Normal x\<rangle> \<Rightarrow> ta\<rbrakk> \<Longrightarrow> ta \<in> Normal ` Q
 2. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>f,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; x \<in> P; x \<notin> b; t \<notin> Fault ` F; t \<notin> Abrupt ` A; x \<notin> b; \<Gamma>\<turnstile> \<langle>f,Normal x\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>f,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<notin> Fault ` F \<longrightarrow> t \<in> Normal ` Q \<or> t \<in> Abrupt ` A; x \<in> P; x \<notin> b; t \<notin> Fault ` F; t \<notin> Abrupt ` A; x \<notin> b; \<Gamma>\<turnstile> \<langle>f,Normal x\<rangle> \<Rightarrow> t\<rbrakk> \<Longrightarrow> t \<in> Normal ` Q proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma update_desc_def_ext:
  "update_desc x y = (\<lambda>d. \<lparr>field_access = field_access d \<circ> x, field_update = \<lambda>bs v. y (field_update d bs (x v)) v\<rparr>)" apply (rule ext) apply (simp add: update_desc_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. update_desc x y = (\<lambda>d. \<lparr>field_access = field_access d \<circ> x, field_update = \<lambda>bs v. y (field_update d bs (x v)) v\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>d. update_desc x y d = \<lparr>field_access = field_access d \<circ> x, field_update = \<lambda>bs v. y (field_update d bs (x v)) v\<rparr> proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma adjust_ti_adjust_ti:
  "adjust_ti (adjust_ti t xf xfu) xf' xfu' = adjust_ti t (xf \<circ> xf') (\<lambda>c a. xfu' (xfu c (xf' a)) a)" unfolding adjust_ti_def by (simp add: map_td_map comp_def update_desc_def_ext)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. adjust_ti (adjust_ti t xf xfu) xf' xfu' = adjust_ti t (xf \<circ> xf') (\<lambda>c a. xfu' (xfu c (xf' a)) a) proof (prove)
goal (1 subgoal):
 1. map_td (\<lambda>n algn. update_desc xf' xfu') (map_td (\<lambda>n algn. update_desc xf xfu) t) = map_td (\<lambda>n algn. update_desc (xf \<circ> xf') (\<lambda>c a. xfu' (xfu c (xf' a)) a)) t
theory SIMPL_Lemmas

lemma fg_cons_comp:
  assumes fg: "fg_cons xf xfu"
  and     fg': "fg_cons xf' xfu'"
  shows "fg_cons (xf \<circ> xf') (\<lambda>c a. xfu' (xfu c (xf' a)) a)" using fg fg' unfolding fg_cons_def by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fg_cons (xf \<circ> xf') (\<lambda>c a. xfu' (xfu c (xf' a)) a) proof (prove)
using this:
fg_cons xf xfu
fg_cons xf' xfu'

goal (1 subgoal):
 1. fg_cons (xf \<circ> xf') (\<lambda>c a. xfu' (xfu c (xf' a)) a) proof (prove)
using this:
(\<forall>bs v. xf (xfu bs v) = bs) \<and> (\<forall>bs bs' v. xfu bs (xfu bs' v) = xfu bs v) \<and> (\<forall>v. xfu (xf v) v = v)
(\<forall>bs v. xf' (xfu' bs v) = bs) \<and> (\<forall>bs bs' v. xfu' bs (xfu' bs' v) = xfu' bs v) \<and> (\<forall>v. xfu' (xf' v) v = v)

goal (1 subgoal):
 1. (\<forall>bs v. (xf \<circ> xf') (xfu' (xfu bs (xf' v)) v) = bs) \<and> (\<forall>bs bs' v. xfu' (xfu bs (xf' (xfu' (xfu bs' (xf' v)) v))) (xfu' (xfu bs' (xf' v)) v) = xfu' (xfu bs (xf' v)) v) \<and> (\<forall>v. xfu' (xfu ((xf \<circ> xf') v) (xf' v)) v = v)
theory SIMPL_Lemmas

lemma hoarep_Int:
  fixes P' :: "'a set" and P :: "'a set"
  assumes s1: "\<Gamma> \<turnstile> P c Q"
  and     s2: "\<Gamma> \<turnstile> P' c Q'"
  shows   "\<Gamma> \<turnstile> (P \<inter> P') c (Q \<inter> Q')" using s1 s2 apply - apply (rule hoare_complete) apply (drule hoare_sound)+ apply (clarsimp simp add: cvalid_def HoarePartialDef.valid_def) apply (drule spec, drule spec, drule (1) mp) apply (drule spec, drule spec, drule (1) mp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> (P \<inter> P') c (Q \<inter> Q') proof (prove)
using this:
\<Gamma>\<turnstile> P c Q
\<Gamma>\<turnstile> P' c Q'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> (P \<inter> P') c (Q \<inter> Q') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> P c Q; \<Gamma>\<turnstile> P' c Q'\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (P \<inter> P') c (Q \<inter> Q') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> P c Q; \<Gamma>\<turnstile> P' c Q'\<rbrakk> \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> (P \<inter> P') c (Q \<inter> Q'),{} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>,{}\<Turnstile>\<^bsub>/{}\<^esub> P c Q,{}; \<Gamma>,{}\<Turnstile>\<^bsub>/{}\<^esub> P' c Q',{}\<rbrakk> \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> (P \<inter> P') c (Q \<inter> Q'),{} proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q; \<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P' \<longrightarrow> t \<in> Normal ` Q'; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; x \<in> P; x \<in> P'\<rbrakk> \<Longrightarrow> t \<in> Normal ` (Q \<inter> Q') proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<forall>s t. \<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> t \<longrightarrow> s \<in> Normal ` P' \<longrightarrow> t \<in> Normal ` Q'; \<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; x \<in> P; x \<in> P'; Normal x \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q\<rbrakk> \<Longrightarrow> t \<in> Normal ` (Q \<inter> Q') proof (prove)
goal (1 subgoal):
 1. \<And>t x. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal x\<rangle> \<Rightarrow> t; x \<in> P; x \<in> P'; Normal x \<in> Normal ` P \<longrightarrow> t \<in> Normal ` Q; Normal x \<in> Normal ` P' \<longrightarrow> t \<in> Normal ` Q'\<rbrakk> \<Longrightarrow> t \<in> Normal ` (Q \<inter> Q') proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma Normal_resultE:
  "\<lbrakk> \<Gamma> \<turnstile> \<langle>c, s\<rangle> \<Rightarrow> Normal t'; \<And>t. \<lbrakk> \<Gamma> \<turnstile> \<langle>c, Normal t\<rangle> \<Rightarrow> Normal t'; s = Normal t\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" apply (frule Normal_result) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Normal t'; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> Normal t'; s = Normal t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Normal t'; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> Normal t'; s = Normal t\<rbrakk> \<Longrightarrow> P; \<exists>t. s = Normal t\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma Abrupt_resultE [consumes 1, case_names normal abrupt]:
  "\<lbrakk>\<Gamma> \<turnstile> \<langle>c, s\<rangle> \<Rightarrow> Abrupt t';
    \<And>t. \<lbrakk>\<Gamma> \<turnstile> \<langle>c, Normal t\<rangle> \<Rightarrow> Abrupt t'; s = Normal t\<rbrakk> \<Longrightarrow> P;
    \<And>t. \<lbrakk>\<Gamma> \<turnstile> \<langle>c, Abrupt t\<rangle> \<Rightarrow> Abrupt t'; s = Abrupt t\<rbrakk> \<Longrightarrow> P\<rbrakk>
   \<Longrightarrow> P" apply (frule Abrupt_result) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t'; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> Abrupt t'; s = Normal t\<rbrakk> \<Longrightarrow> P; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Abrupt t\<rangle> \<Rightarrow> Abrupt t'; s = Abrupt t\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,s\<rangle> \<Rightarrow> Abrupt t'; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> Abrupt t'; s = Normal t\<rbrakk> \<Longrightarrow> P; \<And>t. \<lbrakk>\<Gamma>\<turnstile> \<langle>c,Abrupt t\<rangle> \<Rightarrow> Abrupt t'; s = Abrupt t\<rbrakk> \<Longrightarrow> P; (\<exists>t. s = Normal t) \<or> s = Abrupt t'\<rbrakk> \<Longrightarrow> P
theory SIMPL_Lemmas

lemma Fault_result:
  assumes ex: "\<Gamma> \<turnstile> \<langle>a, s\<rangle> \<Rightarrow> t"
  and      t: "t = Fault f"
  shows    "s = Fault f \<or> (\<exists>s'. s = Normal s')" using ex t by induct auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s = Fault f \<or> (\<exists>s'. s = Normal s') proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> t
t = Fault f

goal (1 subgoal):
 1. s = Fault f \<or> (\<exists>s'. s = Normal s')
theory SIMPL_Lemmas

lemma Fault_resultE:
  assumes ex: "\<Gamma> \<turnstile> \<langle>a, s\<rangle> \<Rightarrow> Fault f"
  and     r1: "\<lbrakk> \<Gamma> \<turnstile> \<langle>a, Fault f\<rangle> \<Rightarrow> Fault f; s = Fault f \<rbrakk> \<Longrightarrow> P"
  and     r2: "\<And>s'. \<lbrakk> \<Gamma> \<turnstile> \<langle>a, Normal s'\<rangle> \<Rightarrow> Fault f; s = Normal s'\<rbrakk> \<Longrightarrow> P"
  shows   P using ex apply - apply (frule Fault_result [OF _ refl]) apply (erule disjE) apply (rule r1, simp_all) apply (erule exE) apply (rule r2, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f

goal (1 subgoal):
 1. P proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f; s = Fault f \<or> (\<exists>s'. s = Normal s')\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f; s = Fault f\<rbrakk> \<Longrightarrow> P
 2. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f; \<exists>s'. s = Normal s'\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f; \<exists>s'. s = Normal s'\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Fault f; s = Normal s'\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma Stuck_result:
  assumes ex: "\<Gamma> \<turnstile> \<langle>a, s\<rangle> \<Rightarrow> t"
  and      t: "t = Stuck"
  shows    "s = Stuck \<or> (\<exists>s'. s = Normal s')" using ex t by induct auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s = Stuck \<or> (\<exists>s'. s = Normal s') proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> t
t = Stuck

goal (1 subgoal):
 1. s = Stuck \<or> (\<exists>s'. s = Normal s')
theory SIMPL_Lemmas

lemma Stuck_resultE:
  assumes ex: "\<Gamma> \<turnstile> \<langle>a, s\<rangle> \<Rightarrow> Stuck"
  and     r1: "\<lbrakk> \<Gamma> \<turnstile> \<langle>a, Stuck\<rangle> \<Rightarrow> Stuck; s = Stuck \<rbrakk> \<Longrightarrow> P"
  and     r2: "\<And>s'. \<lbrakk> \<Gamma> \<turnstile> \<langle>a, Normal s'\<rangle> \<Rightarrow> Stuck; s = Normal s'\<rbrakk> \<Longrightarrow> P"
  shows   P using ex apply - apply (frule Stuck_result [OF _ refl]) apply (erule disjE) apply (rule r1, simp_all) apply (erule exE) apply (rule r2, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
\<Gamma>\<turnstile> \<langle>a,s\<rangle> \<Rightarrow> Stuck

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

lemma ceqvI:
  assumes rl: "xf s = v \<Longrightarrow> (\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> s') = (\<Gamma> \<turnstile> \<langle>b, Normal s\<rangle> \<Rightarrow> s')"
  shows   "ceqv \<Gamma> xf v s s' a b" using rl unfolding ceqv_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf v s s' a b proof (prove)
using this:
xf s = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. ceqv \<Gamma> xf v s s' a b proof (prove)
using this:
xf s = v \<Longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. xf s = v \<longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'
theory SIMPL_Lemmas

lemma ceqvD1:
  assumes lhs: "\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> s'"
  and     xf:  "xf s = v"
  and     ceq: "ceqv \<Gamma> xf v s s' a b"
  shows   "\<Gamma> \<turnstile> \<langle>b, Normal s\<rangle> \<Rightarrow> s'" using ceq xf lhs unfolding ceqv_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' proof (prove)
using this:
ceqv \<Gamma> xf v s s' a b
xf s = v
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' proof (prove)
using this:
xf s = v \<longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'
xf s = v
\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'
theory SIMPL_Lemmas

lemma ceqvD2:
  assumes lhs: "\<Gamma> \<turnstile> \<langle>b, Normal s\<rangle> \<Rightarrow> s'"
  and     xf:  "xf s = v"
  and     ceq: "ceqv \<Gamma> xf v s s' a b"
  shows   "\<Gamma> \<turnstile> \<langle>a, Normal s\<rangle> \<Rightarrow> s'" using ceq xf lhs unfolding ceqv_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' proof (prove)
using this:
ceqv \<Gamma> xf v s s' a b
xf s = v
\<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'

goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' proof (prove)
using this:
xf s = v \<longrightarrow> \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'
xf s = v
\<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s'

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

lemma ceqv_sym [sym]:
  "ceqv \<Gamma> xf' rv' t t' c c' \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c' c" unfolding ceqv_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf' rv' t t' c c' \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c' c proof (prove)
goal (1 subgoal):
 1. xf' t = rv' \<longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>c',Normal t\<rangle> \<Rightarrow> t' \<Longrightarrow> xf' t = rv' \<longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> t'
theory SIMPL_Lemmas

lemma exec_eq_is_valid_eq:
  fixes P :: "'a set"
  assumes eq: "\<And>t t'. (\<Gamma> \<turnstile> \<langle>a, Normal t\<rangle> \<Rightarrow> t') = (\<Gamma> \<turnstile> \<langle>a', Normal t\<rangle> \<Rightarrow> t')"
  shows     vl: "hoarep \<Gamma> {} F P a Q A = hoarep \<Gamma> {} F P a' Q A" apply rule apply (erule exec_eq_is_valid_eq0 [OF eq]) apply (erule exec_eq_is_valid_eq0 [OF eq [symmetric]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A = \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A proof (prove)
goal (2 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A
 2. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a' Q,A \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/F\<^esub> P a Q,A proof (prove)
goal:
No subgoals!
theory SIMPL_Lemmas

lemma Int_eq_symmetric:
  "A \<inter> {s. x s = y s} = A \<inter> {s. y s = x s}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<inter> {s. x s = y s} = A \<inter> {s. y s = x s}
theory SIMPL_Lemmas

lemma ceqv_refl:
  "ceqv \<Gamma> xf' rv' t t' c c" unfolding ceqv_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> xf' rv' t t' c c proof (prove)
goal (1 subgoal):
 1. xf' t = rv' \<longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> t'
theory SIMPL_Lemmas

lemma ceqv_trans:
  "\<lbrakk> ceqv \<Gamma> xf' rv' t t' c c'; ceqv \<Gamma> xf' rv' t t' c' c'' \<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c c''" unfolding ceqv_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ceqv \<Gamma> xf' rv' t t' c c'; ceqv \<Gamma> xf' rv' t t' c' c''\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xf' rv' t t' c c'' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>xf' t = rv' \<longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>c',Normal t\<rangle> \<Rightarrow> t'; xf' t = rv' \<longrightarrow> \<Gamma>\<turnstile> \<langle>c',Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>c'',Normal t\<rangle> \<Rightarrow> t'\<rbrakk> \<Longrightarrow> xf' t = rv' \<longrightarrow> \<Gamma>\<turnstile> \<langle>c,Normal t\<rangle> \<Rightarrow> t' = \<Gamma>\<turnstile> \<langle>c'',Normal t\<rangle> \<Rightarrow> t'
theory SIMPL_Lemmas

lemma semantic_equiv_sym:
  "semantic_equiv \<Gamma> s s' a b = semantic_equiv \<Gamma> s s' b a" unfolding semantic_equiv_def by (auto intro: ceqv_sym)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv \<Gamma> s s' a b = semantic_equiv \<Gamma> s s' b a proof (prove)
goal (1 subgoal):
 1. ceqv \<Gamma> (\<lambda>_. ()) () s s' a b = ceqv \<Gamma> (\<lambda>_. ()) () s s' b a
theory SIMPL_Lemmas

lemma semantic_equivI:
  "(\<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s') \<Longrightarrow> semantic_equiv \<Gamma> s s' a b" unfolding semantic_equiv_def by (auto intro: ceqvI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' \<Longrightarrow> semantic_equiv \<Gamma> s s' a b proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> \<langle>a,Normal s\<rangle> \<Rightarrow> s' = \<Gamma>\<turnstile> \<langle>b,Normal s\<rangle> \<Rightarrow> s' \<Longrightarrow> ceqv \<Gamma> (\<lambda>_. ()) () s s' a b
theory SIMPL_Lemmas

lemma Guard_Seq_semantic_equiv:
  "semantic_equiv \<Gamma> s s' (Guard F S c ;; d) (Guard F S (c ;; d))" by (auto elim!: exec_Normal_elim_cases intro: semantic_equivI exec.intros)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. semantic_equiv \<Gamma> s s' (Guard F S c;;
d) (Guard F S (c;;
d))