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