Quelle  Denotation.thy   Sprache: Isabelle

(*  Title:      ZF/IMP/Denotation.thy
    Author:     Heiko Loetzbeyer and Robert Sandner, TU München
*)

section ‹Denotational semantics of expressions and commands›

theory Denotation imports Com begin

subsection ‹Definitions›

consts
  A     :: "i \ i \ i"
  B     :: "i \ i \ i"
  C     :: "i \ i"

definition
  Gamma :: "[i,i,i] \ i"  (‹Γ›) where
  "\(b,cden) \
    (λphi. {io ∈ (phi O cden). B(b,fst(io))=1} ∪
           {io ∈ id(loc->nat). B(b,fst(io))=0})"

primrec
  "A(N(n), sigma) = n"
  "A(X(x), sigma) = sigma`x"
  "A(Op1(f,a), sigma) = f`A(a,sigma)"
  "A(Op2(f,a0,a1), sigma) = f`"

primrec
  "B(true, sigma) = 1"
  "B(false, sigma) = 0"
  "B(ROp(f,a0,a1), sigma) = f`"
  "B(noti(b), sigma) = not(B(b,sigma))"
  "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
  "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"

primrec
  "C(\) = id(loc->nat)"
  "C(x \ a) =
    {io ∈ (loc->nat) × (loc->nat). snd(io) = fst(io)(x := A(a,fst(io)))}"
  "C(c0\ c1) = C(c1) O C(c0)"
  "C(\ b \ c0 \ c1) =
    {io ∈ C(c0). B(b,fst(io)) = 1} ∪ {io ∈ C(c1). B(b,fst(io)) = 0}"
  "C(\ b \ c) = lfp((loc->nat) \ (loc->nat), \(b,C(c)))"


subsection ‹Misc lemmas›

lemma A_type [TC]: "\a \ aexp; sigma \ loc->nat\ \ A(a,sigma) \ nat"
  by (erule aexp.induct) simp_all

lemma B_type [TC]: "\b \ bexp; sigma \ loc->nat\ \ B(b,sigma) \ bool"
by (erule bexp.induct, simp_all)

lemma C_subset: "c \ com \ C(c) \ (loc->nat) \ (loc->nat)"
  apply (erule com.induct)
      apply simp_all
      apply (blast dest: lfp_subset [THEN subsetD])+
  done

lemma C_type_D [dest]:
    "\\x,y\ \ C(c); c \ com\ \ x \ loc->nat \ y \ loc->nat"
  by (blast dest: C_subset [THEN subsetD])

lemma C_type_fst [dest]: "\x \ C(c); c \ com\ \ fst(x) \ loc->nat"
  by (auto dest!: C_subset [THEN subsetD])

lemma Gamma_bnd_mono:
  "cden \ (loc->nat) \ (loc->nat)
    ==> bnd_mono ((loc->nat) × (loc->nat), Γ(b,cden))"
  by (unfold bnd_mono_def Gamma_def) blast

end