author | clasohm |
Fri, 24 Mar 1995 12:30:35 +0100 | |
changeset 972 | e61b058d58d2 |
parent 965 | 24eef3860714 |
child 977 | 5d57287e5e1e |
permissions | -rw-r--r-- |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
1 |
(* Title: HOL/IMP/Com.thy |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
3 |
Author: Heiko Loetzbeyer & Robert Sandner, TUM |
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 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
6 |
Arithmetic expressions, Boolean expressions, Commands |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
7 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
8 |
And their Operational semantics |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
9 |
*) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
10 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
11 |
Com = Arith + |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
12 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
13 |
(** Arithmetic expressions **) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
14 |
types loc |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
15 |
state = "loc => nat" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
16 |
n2n = "nat => nat" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
17 |
n2n2n = "nat => nat => nat" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
18 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
19 |
arities loc :: term |
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 |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
22 |
aexp = N (nat) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
23 |
| X (loc) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
24 |
| Op1 (n2n, aexp) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
25 |
| Op2 (n2n2n, aexp, aexp) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
26 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
27 |
(** Evaluation of arithmetic expressions **) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
28 |
consts evala :: "(aexp*state*nat)set" |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
29 |
"@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50) |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
30 |
translations |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
31 |
"<ae,sig> -a-> n" == "(ae,sig,n) : evala" |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
32 |
inductive "evala" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
33 |
intrs |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
34 |
N "<N(n),s> -a-> n" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
35 |
X "<X(x),s> -a-> s(x)" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
36 |
Op1 "<e,s> -a-> n ==> <Op1 f e,s> -a-> f(n)" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
37 |
Op2 "[| <e0,s> -a-> n0; <e1,s> -a-> n1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
38 |
\ ==> <Op2 f e0 e1,s> -a-> f n0 n1" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
39 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
40 |
types n2n2b = "[nat,nat] => bool" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
41 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
42 |
(** Boolean expressions **) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
43 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
44 |
datatype |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
45 |
bexp = true |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
46 |
| false |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
47 |
| ROp (n2n2b, aexp, aexp) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
48 |
| noti (bexp) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
49 |
| andi (bexp,bexp) (infixl 60) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
50 |
| ori (bexp,bexp) (infixl 60) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
51 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
52 |
(** Evaluation of boolean expressions **) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
53 |
consts evalb :: "(bexp*state*bool)set" |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
54 |
"@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50) |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
55 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
56 |
translations |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
57 |
"<be,sig> -b-> b" == "(be,sig,b) : evalb" |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
58 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
59 |
inductive "evalb" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
60 |
intrs (*avoid clash with ML constructors true, false*) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
61 |
tru "<true,s> -b-> True" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
62 |
fls "<false,s> -b-> False" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
63 |
ROp "[| <a0,s> -a-> n0; <a1,s> -a-> n1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
64 |
\ ==> <ROp f a0 a1,s> -b-> f n0 n1" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
65 |
noti "<b,s> -b-> w ==> <noti(b),s> -b-> (~w)" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
66 |
andi "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
67 |
\ ==> <b0 andi b1,s> -b-> (w0 & w1)" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
68 |
ori "[| <b0,s> -b-> w0; <b1,s> -b-> w1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
69 |
\ ==> <b0 ori b1,s> -b-> (w0 | w1)" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
70 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
71 |
(** Commands **) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
72 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
73 |
datatype |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
74 |
com = skip |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
75 |
| ":=" (loc,aexp) (infixl 60) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
76 |
| semic (com,com) ("_; _" [60, 60] 10) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
77 |
| whileC (bexp,com) ("while _ do _" 60) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
78 |
| ifC (bexp, com, com) ("ifc _ then _ else _" 60) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
79 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
80 |
(** Execution of commands **) |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
81 |
consts evalc :: "(com*state*state)set" |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
82 |
"@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50) |
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
83 |
"assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95) |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
84 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
85 |
translations |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
965
diff
changeset
|
86 |
"<ce,sig> -c-> s" == "(ce,sig,s) : evalc" |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
87 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
88 |
rules |
965 | 89 |
assign_def "s[m/x] == (%y. if y=x then m else s y)" |
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
90 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
91 |
inductive "evalc" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
92 |
intrs |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
93 |
skip "<skip,s> -c-> s" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
94 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
95 |
assign "<a,s> -a-> m ==> <x := a,s> -c-> s[m/x]" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
96 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
97 |
semi "[| <c0,s> -c-> s2; <c1,s2> -c-> s1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
98 |
\ ==> <c0 ; c1, s> -c-> s1" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
99 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
100 |
ifcTrue "[| <b,s> -b-> True; <c0,s> -c-> s1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
101 |
\ ==> <ifc b then c0 else c1, s> -c-> s1" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
102 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
103 |
ifcFalse "[| <b,s> -b-> False; <c1,s> -c-> s1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
104 |
\ ==> <ifc b then c0 else c1, s> -c-> s1" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
105 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
106 |
whileFalse "<b, s> -b-> False ==> <while b do c,s> -c-> s" |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
107 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
108 |
whileTrue "[| <b,s> -b-> True; <c,s> -c-> s2; \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
109 |
\ <while b do c, s2> -c-> s1 |] \ |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
110 |
\ ==> <while b do c, s> -c-> s1 " |
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
111 |
|
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
112 |
end |