# Theory Sem_Equiv

```section "Constant Folding"

theory Sem_Equiv
imports Big_Step
begin

subsection "Semantic Equivalence up to a Condition"

type_synonym assn = "state ⇒ bool"

definition
equiv_up_to :: "assn ⇒ com ⇒ com ⇒ bool" ("_ ⊨ _ ∼ _" [50,0,10] 50)
where
"(P ⊨ c ∼ c') = (∀s s'. P s ⟶ (c,s) ⇒ s' ⟷ (c',s) ⇒ s')"

definition
bequiv_up_to :: "assn ⇒ bexp ⇒ bexp ⇒ bool" ("_ ⊨ _ <∼> _" [50,0,10] 50)
where
"(P ⊨ b <∼> b') = (∀s. P s ⟶ bval b s = bval b' s)"

lemma equiv_up_to_True:
"((λ_. True) ⊨ c ∼ c') = (c ∼ c')"
by (simp add: equiv_def equiv_up_to_def)

lemma equiv_up_to_weaken:
"P ⊨ c ∼ c' ⟹ (⋀s. P' s ⟹ P s) ⟹ P' ⊨ c ∼ c'"
by (simp add: equiv_up_to_def)

lemma equiv_up_toI:
"(⋀s s'. P s ⟹ (c, s) ⇒ s' = (c', s) ⇒ s') ⟹ P ⊨ c ∼ c'"
by (unfold equiv_up_to_def) blast

lemma equiv_up_toD1:
"P ⊨ c ∼ c' ⟹ (c, s) ⇒ s' ⟹ P s ⟹ (c', s) ⇒ s'"
by (unfold equiv_up_to_def) blast

lemma equiv_up_toD2:
"P ⊨ c ∼ c' ⟹ (c', s) ⇒ s' ⟹ P s ⟹ (c, s) ⇒ s'"
by (unfold equiv_up_to_def) blast

lemma equiv_up_to_refl [simp, intro!]:
"P ⊨ c ∼ c"
by (auto simp: equiv_up_to_def)

lemma equiv_up_to_sym:
"(P ⊨ c ∼ c') = (P ⊨ c' ∼ c)"
by (auto simp: equiv_up_to_def)

lemma equiv_up_to_trans:
"P ⊨ c ∼ c' ⟹ P ⊨ c' ∼ c'' ⟹ P ⊨ c ∼ c''"
by (auto simp: equiv_up_to_def)

lemma bequiv_up_to_refl [simp, intro!]:
"P ⊨ b <∼> b"
by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_sym:
"(P ⊨ b <∼> b') = (P ⊨ b' <∼> b)"
by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_trans:
"P ⊨ b <∼> b' ⟹ P ⊨ b' <∼> b'' ⟹ P ⊨ b <∼> b''"
by (auto simp: bequiv_up_to_def)

lemma bequiv_up_to_subst:
"P ⊨ b <∼> b' ⟹ P s ⟹ bval b s = bval b' s"
by (simp add: bequiv_up_to_def)

lemma equiv_up_to_seq:
"P ⊨ c ∼ c' ⟹ Q ⊨ d ∼ d' ⟹
(⋀s s'. (c,s) ⇒ s' ⟹ P s ⟹ Q s') ⟹
P ⊨ (c;; d) ∼ (c';; d')"
by (clarsimp simp: equiv_up_to_def) blast

lemma equiv_up_to_while_lemma_weak:
shows "(d,s) ⇒ s' ⟹
P ⊨ b <∼> b' ⟹
P ⊨ c ∼ c' ⟹
(⋀s s'. (c, s) ⇒ s' ⟹ P s ⟹ bval b s ⟹ P s') ⟹
P s ⟹
d = WHILE b DO c ⟹
(WHILE b' DO c', s) ⇒ s'"
proof (induction rule: big_step_induct)
case (WhileTrue b s1 c s2 s3)
hence IH: "P s2 ⟹ (WHILE b' DO c', s2) ⇒ s3" by auto
from WhileTrue.prems
have "P ⊨ b <∼> b'" by simp
with ‹bval b s1› ‹P s1›
have "bval b' s1" by (simp add: bequiv_up_to_def)
moreover
from WhileTrue.prems
have "P ⊨ c ∼ c'" by simp
with ‹bval b s1› ‹P s1› ‹(c, s1) ⇒ s2›
have "(c', s1) ⇒ s2" by (simp add: equiv_up_to_def)
moreover
from WhileTrue.prems
have "⋀s s'. (c,s) ⇒ s' ⟹ P s ⟹ bval b s ⟹ P s'" by simp
with ‹P s1› ‹bval b s1› ‹(c, s1) ⇒ s2›
have "P s2" by simp
hence "(WHILE b' DO c', s2) ⇒ s3" by (rule IH)
ultimately
show ?case by blast
next
case WhileFalse
thus ?case by (auto simp: bequiv_up_to_def)
qed (fastforce simp: equiv_up_to_def bequiv_up_to_def)+

lemma equiv_up_to_while_weak:
assumes b: "P ⊨ b <∼> b'"
assumes c: "P ⊨ c ∼ c'"
assumes I: "⋀s s'. (c, s) ⇒ s' ⟹ P s ⟹ bval b s ⟹ P s'"
shows "P ⊨ WHILE b DO c ∼ WHILE b' DO c'"
proof -
from b have b': "P ⊨ b' <∼> b" by (simp add: bequiv_up_to_sym)

from c b have c': "P ⊨ c' ∼ c" by (simp add: equiv_up_to_sym)

from I
have I': "⋀s s'. (c', s) ⇒ s' ⟹ P s ⟹ bval b' s ⟹ P s'"
by (auto dest!: equiv_up_toD1 [OF c'] simp: bequiv_up_to_subst [OF b'])

note equiv_up_to_while_lemma_weak [OF _ b c]
equiv_up_to_while_lemma_weak [OF _ b' c']
thus ?thesis using I I' by (auto intro!: equiv_up_toI)
qed

lemma equiv_up_to_if_weak:
"P ⊨ b <∼> b' ⟹ P ⊨ c ∼ c' ⟹ P ⊨ d ∼ d' ⟹
P ⊨ IF b THEN c ELSE d ∼ IF b' THEN c' ELSE d'"
by (auto simp: bequiv_up_to_def equiv_up_to_def)

lemma equiv_up_to_if_True [intro!]:
"(⋀s. P s ⟹ bval b s) ⟹ P ⊨ IF b THEN c1 ELSE c2 ∼ c1"
by (auto simp: equiv_up_to_def)

lemma equiv_up_to_if_False [intro!]:
"(⋀s. P s ⟹ ¬ bval b s) ⟹ P ⊨ IF b THEN c1 ELSE c2 ∼ c2"
by (auto simp: equiv_up_to_def)

lemma equiv_up_to_while_False [intro!]:
"(⋀s. P s ⟹ ¬ bval b s) ⟹ P ⊨ WHILE b DO c ∼ SKIP"
by (auto simp: equiv_up_to_def)

lemma while_never: "(c, s) ⇒ u ⟹ c ≠ WHILE (Bc True) DO c'"
by (induct rule: big_step_induct) auto

lemma equiv_up_to_while_True [intro!,simp]:
"P ⊨ WHILE Bc True DO c ∼ WHILE Bc True DO SKIP"
unfolding equiv_up_to_def
by (blast dest: while_never)

end
```