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' \
(\<And>s s'. (c,s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> Q s') \<Longrightarrow>
P \<Turnstile> (c;; d) \<sim> (c';; d')"
by (clarsimp simp: equiv_up_to_def) blast
lemma equiv_up_to_while_lemma_weak:
shows "(d,s) \ s' \
P \<Turnstile> b <\<sim>> b' \<Longrightarrow>
P \<Turnstile> c \<sim> c' \<Longrightarrow>
(\<And>s s'. (c, s) \<Rightarrow> s' \<Longrightarrow> P s \<Longrightarrow> bval b s \<Longrightarrow> P s') \<Longrightarrow>
P s \<Longrightarrow>
d = WHILE b DO c \<Longrightarrow>
(WHILE b' DO c', s) \<Rightarrow> 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 \<open>bval b s1\<close> \<open>P s1\<close>
have "bval b' s1" by (simp add: bequiv_up_to_def)
moreover
from WhileTrue.prems
have "P \ c \ c'" by simp
with \<open>bval b s1\<close> \<open>P s1\<close> \<open>(c, s1) \<Rightarrow> s2\<close>
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 \<open>P s1\<close> \<open>bval b s1\<close> \<open>(c, s1) \<Rightarrow> s2\<close>
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 \<Turnstile> IF b THEN c ELSE d \<sim> 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
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
