(* Authors: Heiko Loetzbeyer, Robert Sandner, Tobias Nipkow *)
section "Denotational Semantics of Commands"
theory Denotational imports Big_Step begin
type_synonym com_den = "(state \ state) set"
definition W :: "(state \ bool) \ com_den \ (com_den \ com_den)" where
"W db dc = (\dw. {(s,t). if db s then (s,t) \ dc O dw else s=t})"
fun D :: "com \ com_den" where
"D SKIP = Id" |
"D (x ::= a) = {(s,t). t = s(x := aval a s)}" |
"D (c1;;c2) = D(c1) O D(c2)" |
"D (IF b THEN c1 ELSE c2)
= {(s,t). if bval b s then (s,t) \<in> D c1 else (s,t) \<in> D c2}" |
"D (WHILE b DO c) = lfp (W (bval b) (D c))"
lemma W_mono: "mono (W b r)"
by (unfold W_def mono_def) auto
lemma D_While_If:
"D(WHILE b DO c) = D(IF b THEN c;;WHILE b DO c ELSE SKIP)"
proof-
let ?w = "WHILE b DO c" let ?f = "W (bval b) (D c)"
have "D ?w = lfp ?f" by simp
also have "\ = ?f (lfp ?f)" by(rule lfp_unfold [OF W_mono])
also have "\ = D(IF b THEN c;;?w ELSE SKIP)" by (simp add: W_def)
finally show ?thesis .
qed
text\<open>Equivalence of denotational and big-step semantics:\<close>
lemma D_if_big_step: "(c,s) \ t \ (s,t) \ D(c)"
proof (induction rule: big_step_induct)
case WhileFalse
with D_While_If show ?case by auto
next
case WhileTrue
show ?case unfolding D_While_If using WhileTrue by auto
qed auto
abbreviation Big_step :: "com \ com_den" where
"Big_step c \ {(s,t). (c,s) \ t}"
lemma Big_step_if_D: "(s,t) \ D(c) \ (s,t) \ Big_step c"
proof (induction c arbitrary: s t)
case Seq thus ?case by fastforce
next
case (While b c)
let ?B = "Big_step (WHILE b DO c)" let ?f = "W (bval b) (D c)"
have "?f ?B \ ?B" using While.IH by (auto simp: W_def)
from lfp_lowerbound[where ?f = "?f", OF this] While.prems
show ?case by auto
qed (auto split: if_splits)
theorem denotational_is_big_step:
"(s,t) \ D(c) = ((c,s) \ t)"
by (metis D_if_big_step Big_step_if_D[simplified])
corollary equiv_c_iff_equal_D: "(c1 \ c2) \ D c1 = D c2"
by(simp add: denotational_is_big_step[symmetric] set_eq_iff)
subsection "Continuity"
definition chain :: "(nat \ 'a set) \ bool" where
"chain S = (\i. S i \ S(Suc i))"
lemma chain_total: "chain S \ S i \ S j \ S j \ S i"
by (metis chain_def le_cases lift_Suc_mono_le)
definition cont :: "('a set \ 'b set) \ bool" where
"cont f = (\S. chain S \ f(UN n. S n) = (UN n. f(S n)))"
lemma mono_if_cont: fixes f :: "'a set \ 'b set"
assumes "cont f" shows "mono f"
proof
fix a b :: "'a set" assume "a \ b"
let ?S = "\n::nat. if n=0 then a else b"
have "chain ?S" using \<open>a \<subseteq> b\<close> by(auto simp: chain_def)
hence "f(UN n. ?S n) = (UN n. f(?S n))"
using assms by (simp add: cont_def del: if_image_distrib)
moreover have "(UN n. ?S n) = b" using \<open>a \<subseteq> b\<close> by (auto split: if_splits)
moreover have "(UN n. f(?S n)) = f a \ f b" by (auto split: if_splits)
ultimately show "f a \ f b" by (metis Un_upper1)
qed
lemma chain_iterates: fixes f :: "'a set \ 'a set"
assumes "mono f" shows "chain(\n. (f^^n) {})"
proof-
have "(f ^^ n) {} \ (f ^^ Suc n) {}" for n
proof (induction n)
case 0 show ?case by simp
next
case (Suc n) thus ?case using assms by (auto simp: mono_def)
qed
thus ?thesis by(auto simp: chain_def assms)
qed
theorem lfp_if_cont:
assumes "cont f" shows "lfp f = (UN n. (f^^n) {})" (is "_ = ?U")
proof
from assms mono_if_cont
have mono: "(f ^^ n) {} \ (f ^^ Suc n) {}" for n
using funpow_decreasing [of n "Suc n"] by auto
show "lfp f \ ?U"
proof (rule lfp_lowerbound)
have "f ?U = (UN n. (f^^Suc n){})"
using chain_iterates[OF mono_if_cont[OF assms]] assms
by(simp add: cont_def)
also have "\ = (f^^0){} \ \" by simp
also have "\ = ?U"
using mono by auto (metis funpow_simps_right(2) funpow_swap1 o_apply)
finally show "f ?U \ ?U" by simp
qed
next
have "(f^^n){} \ p" if "f p \ p" for n p
proof -
show ?thesis
proof(induction n)
case 0 show ?case by simp
next
case Suc
from monoD[OF mono_if_cont[OF assms] Suc] \<open>f p \<subseteq> p\<close>
show ?case by simp
qed
qed
thus "?U \ lfp f" by(auto simp: lfp_def)
qed
lemma cont_W: "cont(W b r)"
by(auto simp: cont_def W_def)
subsection\<open>The denotational semantics is deterministic\<close>
lemma single_valued_UN_chain:
assumes "chain S" "(\n. single_valued (S n))"
shows "single_valued(UN n. S n)"
proof(auto simp: single_valued_def)
fix m n x y z assume "(x, y) \ S m" "(x, z) \ S n"
with chain_total[OF assms(1), of m n] assms(2)
show "y = z" by (auto simp: single_valued_def)
qed
lemma single_valued_lfp: fixes f :: "com_den \ com_den"
assumes "cont f" "\r. single_valued r \ single_valued (f r)"
shows "single_valued(lfp f)"
unfolding lfp_if_cont[OF assms(1)]
proof(rule single_valued_UN_chain[OF chain_iterates[OF mono_if_cont[OF assms(1)]]])
fix n show "single_valued ((f ^^ n) {})"
by(induction n)(auto simp: assms(2))
qed
lemma single_valued_D: "single_valued (D c)"
proof(induction c)
case Seq thus ?case by(simp add: single_valued_relcomp)
next
case (While b c)
let ?f = "W (bval b) (D c)"
have "single_valued (lfp ?f)"
proof(rule single_valued_lfp[OF cont_W])
show "\r. single_valued r \ single_valued (?f r)"
using While.IH by(force simp: single_valued_def W_def)
qed
thus ?case by simp
qed (auto simp add: single_valued_def)
end
¤ Dauer der Verarbeitung: 0.14 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.
|
