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