src/HOL/IMP/Denotation.thy
author nipkow
Sun, 30 Mar 1997 13:40:38 +0200
changeset 2847 6226b83ce2d8
parent 1696 e84bff5c519b
child 4897 be11be0b6ea1
permissions -rw-r--r--
Replaced (s,t) : id by s=t.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
     1
(*  Title:      HOL/IMP/Denotation.thy
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1374
diff changeset
     3
    Author:     Heiko Loetzbeyer & Robert Sandner, TUM
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     4
    Copyright   1994 TUM
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     5
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
     6
Denotational semantics of commands
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     7
*)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     8
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
     9
Denotation = Natural + 
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    10
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    11
types com_den = "(state*state)set"
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    12
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    13
constdefs
1374
5e407f2a3323 removed quotes from consts and syntax sections
clasohm
parents: 1151
diff changeset
    14
  Gamma :: [bexp,com_den] => (com_den => com_den)
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    15
           "Gamma b cd == (%phi.{(s,t). (s,t) : (phi O cd) & b(s)} Un 
2847
6226b83ce2d8 Replaced (s,t) : id by s=t.
nipkow
parents: 1696
diff changeset
    16
                                 {(s,t). s=t & ~b(s)})"
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    17
    
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    18
consts
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    19
  C     :: com => com_den
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    20
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    21
primrec C com
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    22
  C_skip    "C(SKIP) = id"
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    23
  C_assign  "C(x := a) = {(s,t). t = s[a(s)/x]}"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    24
  C_comp    "C(c0 ; c1) = C(c1) O C(c0)"
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    25
  C_if      "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    26
                                       {(s,t). (s,t) : C(c2) & ~ b(s)}"
1481
03f096efa26d Modified datatype com.
nipkow
parents: 1476
diff changeset
    27
  C_while   "C(WHILE b DO c) = lfp (Gamma b (C c))"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    28
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    29
end
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    30
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    31