Quelle  Denotational.thy

(* 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) ∈ D c1 else (s,t) ∈ 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‹Equivalence of denotational and big-step semantics:›

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 ‹a ⊆ b› 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 ‹a ⊆ b› 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] ‹f p ⊆ p›
      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‹The denotational semantics is deterministic›

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