src/ZF/IMP/Denotation.thy
author wenzelm
Sat Mar 13 16:44:12 2010 +0100 (2010-03-13)
changeset 35762 af3ff2ba4c54
parent 21404 eb85850d3eb7
child 40945 b8703f63bfb2
permissions -rw-r--r--
removed old CVS Ids;
tuned headers;
     1 (*  Title:      ZF/IMP/Denotation.thy
     2     Author:     Heiko Loetzbeyer and Robert Sandner, TU München
     3 *)
     4 
     5 header {* Denotational semantics of expressions and commands *}
     6 
     7 theory Denotation imports Com begin
     8 
     9 subsection {* Definitions *}
    10 
    11 consts
    12   A     :: "i => i => i"
    13   B     :: "i => i => i"
    14   C     :: "i => i"
    15 
    16 definition
    17   Gamma :: "[i,i,i] => i"  ("\<Gamma>") where
    18   "\<Gamma>(b,cden) ==
    19     (\<lambda>phi. {io \<in> (phi O cden). B(b,fst(io))=1} \<union>
    20            {io \<in> id(loc->nat). B(b,fst(io))=0})"
    21 
    22 primrec
    23   "A(N(n), sigma) = n"
    24   "A(X(x), sigma) = sigma`x"
    25   "A(Op1(f,a), sigma) = f`A(a,sigma)"
    26   "A(Op2(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
    27 
    28 primrec
    29   "B(true, sigma) = 1"
    30   "B(false, sigma) = 0"
    31   "B(ROp(f,a0,a1), sigma) = f`<A(a0,sigma),A(a1,sigma)>"
    32   "B(noti(b), sigma) = not(B(b,sigma))"
    33   "B(b0 andi b1, sigma) = B(b0,sigma) and B(b1,sigma)"
    34   "B(b0 ori b1, sigma) = B(b0,sigma) or B(b1,sigma)"
    35 
    36 primrec
    37   "C(\<SKIP>) = id(loc->nat)"
    38   "C(x \<ASSN> a) =
    39     {io \<in> (loc->nat) \<times> (loc->nat). snd(io) = fst(io)(x := A(a,fst(io)))}"
    40   "C(c0\<SEQ> c1) = C(c1) O C(c0)"
    41   "C(\<IF> b \<THEN> c0 \<ELSE> c1) =
    42     {io \<in> C(c0). B(b,fst(io)) = 1} \<union> {io \<in> C(c1). B(b,fst(io)) = 0}"
    43   "C(\<WHILE> b \<DO> c) = lfp((loc->nat) \<times> (loc->nat), \<Gamma>(b,C(c)))"
    44 
    45 
    46 subsection {* Misc lemmas *}
    47 
    48 lemma A_type [TC]: "[|a \<in> aexp; sigma \<in> loc->nat|] ==> A(a,sigma) \<in> nat"
    49   by (erule aexp.induct) simp_all
    50 
    51 lemma B_type [TC]: "[|b \<in> bexp; sigma \<in> loc->nat|] ==> B(b,sigma) \<in> bool"
    52 by (erule bexp.induct, simp_all)
    53 
    54 lemma C_subset: "c \<in> com ==> C(c) \<subseteq> (loc->nat) \<times> (loc->nat)"
    55   apply (erule com.induct)
    56       apply simp_all
    57       apply (blast dest: lfp_subset [THEN subsetD])+
    58   done
    59 
    60 lemma C_type_D [dest]:
    61     "[| <x,y> \<in> C(c); c \<in> com |] ==> x \<in> loc->nat & y \<in> loc->nat"
    62   by (blast dest: C_subset [THEN subsetD])
    63 
    64 lemma C_type_fst [dest]: "[| x \<in> C(c); c \<in> com |] ==> fst(x) \<in> loc->nat"
    65   by (auto dest!: C_subset [THEN subsetD])
    66 
    67 lemma Gamma_bnd_mono:
    68   "cden \<subseteq> (loc->nat) \<times> (loc->nat)
    69     ==> bnd_mono ((loc->nat) \<times> (loc->nat), \<Gamma>(b,cden))"
    70   by (unfold bnd_mono_def Gamma_def) blast
    71 
    72 end