Quelle Denotational.thy Sprache: Isabelle

(* 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

quality97%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.