diff -r c1262feb61c7 -r 3edd5f813f01 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,230 +0,0 @@
-(*  Title:      HOL/Isar_examples/ExprCompiler.thy
-    ID:         $Id$
-    Author:     Markus Wenzel, TU Muenchen
-
-Correctness of a simple expression/stack-machine compiler.
-*)
-
-header {* Correctness of a simple expression compiler *}
-
-theory ExprCompiler 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