--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/Expr_Compiler.thy Mon Jun 22 23:48:24 2009 +0200
@@ -0,0 +1,231 @@
+(* Title: HOL/Isar_examples/Expr_Compiler.thy
+ Author: Markus Wenzel, TU Muenchen
+
+Correctness of a simple expression/stack-machine compiler.
+*)
+
+header {* Correctness of a simple expression compiler *}
+
+theory Expr_Compiler
+imports Main
+begin
+
+text {*
+ This is a (rather trivial) example of program verification. We model
+ a compiler for translating expressions to stack machine instructions,
+ and prove its correctness wrt.\ some evaluation semantics.
+*}
+
+
+subsection {* Binary operations *}
+
+text {*
+ Binary operations are just functions over some type of values. This
+ is both for abstract syntax and semantics, i.e.\ we use a ``shallow
+ embedding'' here.
+*}
+
+types
+ 'val binop = "'val => 'val => 'val"
+
+
+subsection {* Expressions *}
+
+text {*
+ The language of expressions is defined as an inductive type,
+ consisting of variables, constants, and binary operations on
+ expressions.
+*}
+
+datatype ('adr, 'val) expr =
+ Variable 'adr |
+ Constant 'val |
+ Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
+
+text {*
+ Evaluation (wrt.\ some environment of variable assignments) is
+ defined by primitive recursion over the structure of expressions.
+*}
+
+consts
+ eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
+
+primrec
+ "eval (Variable x) env = env x"
+ "eval (Constant c) env = c"
+ "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
+
+
+subsection {* Machine *}
+
+text {*
+ Next we model a simple stack machine, with three instructions.
+*}
+
+datatype ('adr, 'val) instr =
+ Const 'val |
+ Load 'adr |
+ Apply "'val binop"
+
+text {*
+ Execution of a list of stack machine instructions is easily defined
+ as follows.
+*}
+
+consts
+ exec :: "(('adr, 'val) instr) list
+ => 'val list => ('adr => 'val) => 'val list"
+
+primrec
+ "exec [] stack env = stack"
+ "exec (instr # instrs) stack env =
+ (case instr of
+ Const c => exec instrs (c # stack) env
+ | Load x => exec instrs (env x # stack) env
+ | Apply f => exec instrs (f (hd stack) (hd (tl stack))
+ # (tl (tl stack))) env)"
+
+constdefs
+ execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
+ "execute instrs env == hd (exec instrs [] env)"
+
+
+subsection {* Compiler *}
+
+text {*
+ We are ready to define the compilation function of expressions to
+ lists of stack machine instructions.
+*}
+
+consts
+ compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
+
+primrec
+ "compile (Variable x) = [Load x]"
+ "compile (Constant c) = [Const c]"
+ "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
+
+
+text {*
+ The main result of this development is the correctness theorem for
+ $\idt{compile}$. We first establish a lemma about $\idt{exec}$ and
+ list append.
+*}
+
+lemma exec_append:
+ "exec (xs @ ys) stack env =
+ exec ys (exec xs stack env) env"
+proof (induct xs arbitrary: stack)
+ case Nil
+ show ?case by simp
+next
+ case (Cons x xs)
+ show ?case
+ proof (induct x)
+ case Const
+ from Cons show ?case by simp
+ next
+ case Load
+ from Cons show ?case by simp
+ next
+ case Apply
+ from Cons show ?case by simp
+ qed
+qed
+
+theorem correctness: "execute (compile e) env = eval e env"
+proof -
+ have "\<And>stack. exec (compile e) stack env = eval e env # stack"
+ proof (induct e)
+ case Variable show ?case by simp
+ next
+ case Constant show ?case by simp
+ next
+ case Binop then show ?case by (simp add: exec_append)
+ qed
+ then show ?thesis by (simp add: execute_def)
+qed
+
+
+text {*
+ \bigskip In the proofs above, the \name{simp} method does quite a lot
+ of work behind the scenes (mostly ``functional program execution'').
+ Subsequently, the same reasoning is elaborated in detail --- at most
+ one recursive function definition is used at a time. Thus we get a
+ better idea of what is actually going on.
+*}
+
+lemma exec_append':
+ "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
+proof (induct xs arbitrary: stack)
+ case (Nil s)
+ have "exec ([] @ ys) s env = exec ys s env" by simp
+ also have "... = exec ys (exec [] s env) env" by simp
+ finally show ?case .
+next
+ case (Cons x xs s)
+ show ?case
+ proof (induct x)
+ case (Const val)
+ have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
+ by simp
+ also have "... = exec (xs @ ys) (val # s) env" by simp
+ also from Cons have "... = exec ys (exec xs (val # s) env) env" .
+ also have "... = exec ys (exec (Const val # xs) s env) env" by simp
+ finally show ?case .
+ next
+ case (Load adr)
+ from Cons show ?case by simp -- {* same as above *}
+ next
+ case (Apply fn)
+ have "exec ((Apply fn # xs) @ ys) s env =
+ exec (Apply fn # xs @ ys) s env" by simp
+ also have "... =
+ exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
+ also from Cons have "... =
+ exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
+ also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
+ finally show ?case .
+ qed
+qed
+
+theorem correctness': "execute (compile e) env = eval e env"
+proof -
+ have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
+ proof (induct e)
+ case (Variable adr s)
+ have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
+ by simp
+ also have "... = env adr # s" by simp
+ also have "env adr = eval (Variable adr) env" by simp
+ finally show ?case .
+ next
+ case (Constant val s)
+ show ?case by simp -- {* same as above *}
+ next
+ case (Binop fn e1 e2 s)
+ have "exec (compile (Binop fn e1 e2)) s env =
+ exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
+ also have "... = exec [Apply fn]
+ (exec (compile e1) (exec (compile e2) s env) env) env"
+ by (simp only: exec_append)
+ also have "exec (compile e2) s env = eval e2 env # s" by fact
+ also have "exec (compile e1) ... env = eval e1 env # ..." by fact
+ also have "exec [Apply fn] ... env =
+ fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
+ also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
+ also have "fn (eval e1 env) (eval e2 env) =
+ eval (Binop fn e1 e2) env"
+ by simp
+ finally show ?case .
+ qed
+
+ have "execute (compile e) env = hd (exec (compile e) [] env)"
+ by (simp add: execute_def)
+ also from exec_compile
+ have "exec (compile e) [] env = [eval e env]" .
+ also have "hd ... = eval e env" by simp
+ finally show ?thesis .
+qed
+
+end