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