src/HOL/IMP/Com.thy
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338 de0f4a63baa5
parent 9241 f961c1fdff50
child 12431 07ec657249e5
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
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
oheimb@9241
    12
types
nipkow@1696
    13
      loc
oheimb@9241
    14
      val   = nat (* or anything else, nat used in examples *)
oheimb@9241
    15
      state = loc => val
oheimb@9241
    16
      aexp  = state => val
nipkow@1696
    17
      bexp  = state => bool
clasohm@924
    18
wenzelm@12338
    19
arities loc :: type
clasohm@924
    20
clasohm@924
    21
datatype
nipkow@1696
    22
  com = SKIP
oheimb@9241
    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