author | nipkow |
Tue, 05 Jan 1999 17:27:59 +0100 | |
changeset 6059 | aa00e235ea27 |
parent 5183 | 89f162de39cf |
child 8029 | 05446a898852 |
permissions | -rw-r--r-- |
1476 | 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 | 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 | 6 |
Semantics of arithmetic and boolean expressions |
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 |
|
5183 | 10 |
Com = Datatype + |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
11 |
|
1696 | 12 |
types |
13 |
val |
|
14 |
loc |
|
15 |
state = "loc => val" |
|
16 |
aexp = "state => val" |
|
17 |
bexp = state => bool |
|
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
18 |
|
1696 | 19 |
arities loc,val :: 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 | 22 |
com = SKIP |
1481 | 23 |
| ":=" loc aexp (infixl 60) |
24 |
| Semi com com ("_; _" [60, 60] 10) |
|
25 |
| Cond bexp com com ("IF _ THEN _ ELSE _" 60) |
|
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 |