# Theory Denotation

Up to index of Isabelle/ZF/IMP

theory Denotation
imports Com
begin

    (*  Title:      ZF/IMP/Denotation.thy
        ID:         $Id: Denotation.thy,v 1.12 2005/06/17 14:15:11 haftmann Exp $
        Author:     Heiko Loetzbeyer and Robert Sandner, TU München
    *)

    header {* 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"

    constdefs
      Gamma :: "[i,i,i] => i"    ("Γ")
      "Γ(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`<A(a0,sigma),A(a1,sigma)>"

    primrec
      "B(true, sigma) = 1"
      "B(false, sigma) = 0"
      "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
      "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(\<SKIP>) = id(loc->nat)"
      "C(x \<ASSN> a) =
        {io ∈ (loc->nat) × (loc->nat). snd(io) = fst(io)(x := A(a,fst(io)))}"
      "C(c0\<SEQ> c1) = C(c1) O C(c0)"
      "C(\<IF> b \<THEN> c0 \<ELSE> c1) =
        {io ∈ C(c0). B(b,fst(io)) = 1} ∪ {io ∈ C(c1). B(b,fst(io)) = 0}"
      "C(\<WHILE> b \<DO> 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

### Definitions

### Misc lemmas

lemma A_type:

      [| a ∈ aexp; sigma ∈ loc -> nat |] ==> A(a, sigma) ∈ nat

lemma B_type:

      [| b ∈ bexp; sigma ∈ loc -> nat |] ==> B(b, sigma) ∈ bool

lemma C_subset:

      c ∈ com ==> C(c) ⊆ (loc -> nat) × (loc -> nat)

lemma C_type_D:

      [| ⟨x, y⟩ ∈ C(c); c ∈ com |] ==> x ∈ loc -> nat ∧ y ∈ loc -> nat

lemma C_type_fst:

      [| x ∈ C(c); c ∈ com |] ==> fst(x) ∈ loc -> nat

lemma Gamma_bnd_mono:

      cden ⊆ (loc -> nat) × (loc -> nat)
      ==> bnd_mono((loc -> nat) × (loc -> nat), Γ(b, cden))