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