src/HOL/IMP/Com.thy
author berghofe
Fri, 24 Jul 1998 13:03:20 +0200
changeset 5183 89f162de39cf
parent 1696 e84bff5c519b
child 8029 05446a898852
permissions -rw-r--r--
Adapted to new datatype package.
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/Com.thy
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
     3
    Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, 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
Semantics of arithmetic and boolean expressions
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
     7
Syntax of commands
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     8
*)
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     9
5183
89f162de39cf Adapted to new datatype package.
berghofe
parents: 1696
diff changeset
    10
Com = Datatype +
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    11
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    12
types 
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    13
      val
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    14
      loc
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    15
      state = "loc => val"
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    16
      aexp  = "state => val"
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    17
      bexp  = state => bool
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    18
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    19
arities loc,val :: term
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
datatype
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    22
  com = SKIP
1481
03f096efa26d Modified datatype com.
nipkow
parents: 1476
diff changeset
    23
      | ":="  loc aexp         (infixl  60)
03f096efa26d Modified datatype com.
nipkow
parents: 1476
diff changeset
    24
      | Semi  com com          ("_; _"  [60, 60] 10)
03f096efa26d Modified datatype com.
nipkow
parents: 1476
diff changeset
    25
      | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
03f096efa26d Modified datatype com.
nipkow
parents: 1476
diff changeset
    26
      | While bexp com         ("WHILE _ DO _"  60)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    27
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    28
end