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