src/HOL/IMP/Com.thy
author oheimb
Tue Jul 04 10:54:46 2000 +0200 (2000-07-04)
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 12338 de0f4a63baa5
permissions -rw-r--r--
disambiguated := ; added Examples (factorial)
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
oheimb@9241
    19
arities loc :: term
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