src/HOL/IMP/Com.thy
author oheimb
Tue, 04 Jul 2000 10:54:46 +0200
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 12338 de0f4a63baa5
permissions -rw-r--r--
disambiguated := ; added Examples (factorial)
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
8029
05446a898852 Basis now Main.
nipkow
parents: 5183
diff changeset
    10
Com = Main +
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    11
9241
f961c1fdff50 disambiguated := ; added Examples (factorial)
oheimb
parents: 8029
diff changeset
    12
types
1696
e84bff5c519b A completely new version of IMP.
nipkow
parents: 1481
diff changeset
    13
      loc
9241
f961c1fdff50 disambiguated := ; added Examples (factorial)
oheimb
parents: 8029
diff changeset
    14
      val   = nat (* or anything else, nat used in examples *)
f961c1fdff50 disambiguated := ; added Examples (factorial)
oheimb
parents: 8029
diff changeset
    15
      state = loc => val
f961c1fdff50 disambiguated := ; added Examples (factorial)
oheimb
parents: 8029
diff changeset
    16
      aexp  = state => val
1696
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
9241
f961c1fdff50 disambiguated := ; added Examples (factorial)
oheimb
parents: 8029
diff changeset
    19
arities loc :: 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
9241
f961c1fdff50 disambiguated := ; added Examples (factorial)
oheimb
parents: 8029
diff changeset
    23
      | ":=="  loc aexp         (infixl  60)
1481
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