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