author | wenzelm |
Wed, 14 Jun 2000 17:59:53 +0200 | |
changeset 9066 | b1e874e38dab |
parent 8304 | e132d147374b |
child 9659 | b9cf6801f3da |
permissions | -rw-r--r-- |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Isar_examples/ExprCompiler.thy |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
3 |
Author: Markus Wenzel, TU Muenchen |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
4 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
5 |
Correctness of a simple expression/stack-machine compiler. |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
6 |
*) |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
7 |
|
7748 | 8 |
header {* Correctness of a simple expression compiler *}; |
9 |
||
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
10 |
theory ExprCompiler = Main:; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
11 |
|
7869 | 12 |
text {* |
7874 | 13 |
This is a (rather trivial) example of program verification. We model |
14 |
a compiler for translating expressions to stack machine instructions, |
|
15 |
and prove its correctness wrt.\ some evaluation semantics. |
|
7869 | 16 |
*}; |
17 |
||
18 |
||
19 |
subsection {* Binary operations *}; |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
20 |
|
6744 | 21 |
text {* |
7869 | 22 |
Binary operations are just functions over some type of values. This |
7982 | 23 |
is both for abstract syntax and semantics, i.e.\ we use a ``shallow |
7874 | 24 |
embedding'' here. |
6744 | 25 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
26 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
27 |
types |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
28 |
'val binop = "'val => 'val => 'val"; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
29 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
30 |
|
7869 | 31 |
subsection {* Expressions *}; |
32 |
||
33 |
text {* |
|
34 |
The language of expressions is defined as an inductive type, |
|
35 |
consisting of variables, constants, and binary operations on |
|
36 |
expressions. |
|
37 |
*}; |
|
38 |
||
39 |
datatype ('adr, 'val) expr = |
|
40 |
Variable 'adr | |
|
41 |
Constant 'val | |
|
42 |
Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"; |
|
43 |
||
44 |
text {* |
|
7874 | 45 |
Evaluation (wrt.\ some environment of variable assignments) is |
46 |
defined by primitive recursion over the structure of expressions. |
|
7869 | 47 |
*}; |
48 |
||
49 |
consts |
|
50 |
eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"; |
|
51 |
||
52 |
primrec |
|
53 |
"eval (Variable x) env = env x" |
|
54 |
"eval (Constant c) env = c" |
|
55 |
"eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"; |
|
56 |
||
57 |
||
7748 | 58 |
subsection {* Machine *}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
59 |
|
6744 | 60 |
text {* |
6792 | 61 |
Next we model a simple stack machine, with three instructions. |
6744 | 62 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
63 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
64 |
datatype ('adr, 'val) instr = |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
65 |
Const 'val | |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
66 |
Load 'adr | |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
67 |
Apply "'val binop"; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
68 |
|
6744 | 69 |
text {* |
7869 | 70 |
Execution of a list of stack machine instructions is easily defined |
71 |
as follows. |
|
6744 | 72 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
73 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
74 |
consts |
7761 | 75 |
exec :: "(('adr, 'val) instr) list |
76 |
=> 'val list => ('adr => 'val) => 'val list"; |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
77 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
78 |
primrec |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
79 |
"exec [] stack env = stack" |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
80 |
"exec (instr # instrs) stack env = |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
81 |
(case instr of |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
82 |
Const c => exec instrs (c # stack) env |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
83 |
| Load x => exec instrs (env x # stack) env |
7761 | 84 |
| Apply f => exec instrs (f (hd stack) (hd (tl stack)) |
85 |
# (tl (tl stack))) env)"; |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
86 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
87 |
constdefs |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
88 |
execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val" |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
89 |
"execute instrs env == hd (exec instrs [] env)"; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
90 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
91 |
|
7748 | 92 |
subsection {* Compiler *}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
93 |
|
6744 | 94 |
text {* |
7869 | 95 |
We are ready to define the compilation function of expressions to |
6792 | 96 |
lists of stack machine instructions. |
6744 | 97 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
98 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
99 |
consts |
8031
826c6222cca2
renamed comp to compile (avoids clash with Relation.comp);
wenzelm
parents:
7982
diff
changeset
|
100 |
compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
101 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
102 |
primrec |
8031
826c6222cca2
renamed comp to compile (avoids clash with Relation.comp);
wenzelm
parents:
7982
diff
changeset
|
103 |
"compile (Variable x) = [Load x]" |
826c6222cca2
renamed comp to compile (avoids clash with Relation.comp);
wenzelm
parents:
7982
diff
changeset
|
104 |
"compile (Constant c) = [Const c]" |
826c6222cca2
renamed comp to compile (avoids clash with Relation.comp);
wenzelm
parents:
7982
diff
changeset
|
105 |
"compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
106 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
107 |
|
6744 | 108 |
text {* |
8051 | 109 |
The main result of this development is the correctness theorem for |
110 |
$\idt{compile}$. We first establish a lemma about $\idt{exec}$ and |
|
111 |
list append. |
|
6744 | 112 |
*}; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
113 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
114 |
lemma exec_append: |
7748 | 115 |
"ALL stack. exec (xs @ ys) stack env = |
116 |
exec ys (exec xs stack env) env" (is "?P xs"); |
|
8304 | 117 |
proof (induct ?P xs type: list); |
7480 | 118 |
show "?P []"; by simp; |
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
119 |
|
8051 | 120 |
fix x xs; assume "?P xs"; |
7480 | 121 |
show "?P (x # xs)" (is "?Q x"); |
8304 | 122 |
proof (induct ?Q x type: instr); |
8052 | 123 |
show "!!val. ?Q (Const val)"; by (simp!); |
124 |
show "!!adr. ?Q (Load adr)"; by (simp!); |
|
125 |
show "!!fun. ?Q (Apply fun)"; by (simp!); |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
126 |
qed; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
127 |
qed; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
128 |
|
8051 | 129 |
theorem correctness: "execute (compile e) env = eval e env"; |
130 |
proof -; |
|
131 |
have "ALL stack. exec (compile e) stack env = |
|
7748 | 132 |
eval e env # stack" (is "?P e"); |
8304 | 133 |
proof (induct ?P e type: expr); |
8052 | 134 |
show "!!adr. ?P (Variable adr)"; by simp; |
135 |
show "!!val. ?P (Constant val)"; by simp; |
|
136 |
show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))"; |
|
137 |
by (simp add: exec_append); |
|
8051 | 138 |
qed; |
139 |
thus ?thesis; by (simp add: execute_def); |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
140 |
qed; |
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
141 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
142 |
|
8051 | 143 |
text {* |
144 |
\bigskip In the proofs above, the \name{simp} method does quite a lot |
|
145 |
of work behind the scenes (mostly ``functional program execution''). |
|
146 |
Subsequently, the same reasoning is elaborated in detail --- at most |
|
147 |
one recursive function definition is used at a time. Thus we get a |
|
148 |
better idea of what is actually going on. |
|
149 |
*}; |
|
150 |
||
151 |
lemma exec_append: |
|
8052 | 152 |
"ALL stack. exec (xs @ ys) stack env |
8051 | 153 |
= exec ys (exec xs stack env) env" (is "?P xs"); |
154 |
proof (induct ?P xs); |
|
155 |
show "?P []" (is "ALL s. ?Q s"); |
|
156 |
proof; |
|
157 |
fix s; have "exec ([] @ ys) s env = exec ys s env"; by simp; |
|
158 |
also; have "... = exec ys (exec [] s env) env"; by simp; |
|
159 |
finally; show "?Q s"; .; |
|
160 |
qed; |
|
161 |
fix x xs; assume hyp: "?P xs"; |
|
162 |
show "?P (x # xs)"; |
|
163 |
proof (induct x); |
|
8052 | 164 |
fix val; |
8051 | 165 |
show "?P (Const val # xs)" (is "ALL s. ?Q s"); |
166 |
proof; |
|
167 |
fix s; |
|
8052 | 168 |
have "exec ((Const val # xs) @ ys) s env = |
169 |
exec (Const val # xs @ ys) s env"; |
|
170 |
by simp; |
|
8051 | 171 |
also; have "... = exec (xs @ ys) (val # s) env"; by simp; |
172 |
also; from hyp; have "... = exec ys (exec xs (val # s) env) env"; ..; |
|
8052 | 173 |
also; have "... = exec ys (exec (Const val # xs) s env) env"; |
174 |
by simp; |
|
8051 | 175 |
finally; show "?Q s"; .; |
176 |
qed; |
|
177 |
next; |
|
178 |
fix adr; from hyp; show "?P (Load adr # xs)"; by simp -- {* same as above *}; |
|
179 |
next; |
|
8052 | 180 |
fix fun; |
8051 | 181 |
show "?P (Apply fun # xs)" (is "ALL s. ?Q s"); |
182 |
proof; |
|
183 |
fix s; |
|
8052 | 184 |
have "exec ((Apply fun # xs) @ ys) s env = |
185 |
exec (Apply fun # xs @ ys) s env"; |
|
8051 | 186 |
by simp; |
8052 | 187 |
also; have "... = |
188 |
exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"; |
|
189 |
by simp; |
|
190 |
also; from hyp; have "... = |
|
191 |
exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"; ..; |
|
8051 | 192 |
also; have "... = exec ys (exec (Apply fun # xs) s env) env"; by simp; |
193 |
finally; show "?Q s"; .; |
|
194 |
qed; |
|
195 |
qed; |
|
196 |
qed; |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
197 |
|
8031
826c6222cca2
renamed comp to compile (avoids clash with Relation.comp);
wenzelm
parents:
7982
diff
changeset
|
198 |
theorem correctness: "execute (compile e) env = eval e env"; |
8051 | 199 |
proof -; |
8052 | 200 |
have exec_compile: |
8051 | 201 |
"ALL stack. exec (compile e) stack env = eval e env # stack" (is "?P e"); |
202 |
proof (induct e); |
|
203 |
fix adr; show "?P (Variable adr)" (is "ALL s. ?Q s"); |
|
204 |
proof; |
|
205 |
fix s; |
|
8052 | 206 |
have "exec (compile (Variable adr)) s env = exec [Load adr] s env"; |
207 |
by simp; |
|
8051 | 208 |
also; have "... = env adr # s"; by simp; |
209 |
also; have "env adr = eval (Variable adr) env"; by simp; |
|
210 |
finally; show "?Q s"; .; |
|
211 |
qed; |
|
212 |
next; |
|
213 |
fix val; show "?P (Constant val)"; by simp -- {* same as above *}; |
|
214 |
next; |
|
215 |
fix fun e1 e2; assume hyp1: "?P e1" and hyp2: "?P e2"; |
|
216 |
show "?P (Binop fun e1 e2)" (is "ALL s. ?Q s"); |
|
217 |
proof; |
|
8052 | 218 |
fix s; have "exec (compile (Binop fun e1 e2)) s env |
8051 | 219 |
= exec (compile e2 @ compile e1 @ [Apply fun]) s env"; by simp; |
8052 | 220 |
also; have "... = |
221 |
exec [Apply fun] (exec (compile e1) (exec (compile e2) s env) env) env"; |
|
222 |
by (simp only: exec_append); |
|
8051 | 223 |
also; from hyp2; have "exec (compile e2) s env = eval e2 env # s"; ..; |
224 |
also; from hyp1; have "exec (compile e1) ... env = eval e1 env # ..."; ..; |
|
8052 | 225 |
also; have "exec [Apply fun] ... env = |
226 |
fun (hd ...) (hd (tl ...)) # (tl (tl ...))"; by simp; |
|
8051 | 227 |
also; have "... = fun (eval e1 env) (eval e2 env) # s"; by simp; |
8052 | 228 |
also; have "fun (eval e1 env) (eval e2 env) = eval (Binop fun e1 e2) env"; |
8051 | 229 |
by simp; |
230 |
finally; show "?Q s"; .; |
|
231 |
qed; |
|
232 |
qed; |
|
233 |
||
8052 | 234 |
have "execute (compile e) env = hd (exec (compile e) [] env)"; |
8051 | 235 |
by (simp add: execute_def); |
236 |
also; from exec_compile; have "exec (compile e) [] env = [eval e env]"; ..; |
|
237 |
also; have "hd ... = eval e env"; by simp; |
|
238 |
finally; show ?thesis; .; |
|
239 |
qed; |
|
6444
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
240 |
|
2ebe9e630cab
Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
wenzelm
parents:
diff
changeset
|
241 |
end; |