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
