src/HOL/IMP/Com.thy
author nipkow
Wed Nov 24 12:12:36 1999 +0100 (1999-11-24)
changeset 8029 05446a898852
parent 5183 89f162de39cf
child 9241 f961c1fdff50
permissions -rw-r--r--
Basis now Main.
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
nipkow@8029
    10
Com = Main +
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