src/HOL/Isar_Examples/Expr_Compiler.thy
changeset 33026 8f35633c4922
parent 31758 3edd5f813f01
child 35416 d8d7d1b785af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Isar_Examples/Expr_Compiler.thy	Tue Oct 20 19:37:09 2009 +0200
     1.3 @@ -0,0 +1,231 @@
     1.4 +(*  Title:      HOL/Isar_Examples/Expr_Compiler.thy
     1.5 +    Author:     Markus Wenzel, TU Muenchen
     1.6 +
     1.7 +Correctness of a simple expression/stack-machine compiler.
     1.8 +*)
     1.9 +
    1.10 +header {* Correctness of a simple expression compiler *}
    1.11 +
    1.12 +theory Expr_Compiler
    1.13 +imports Main
    1.14 +begin
    1.15 +
    1.16 +text {*
    1.17 + This is a (rather trivial) example of program verification.  We model
    1.18 + a compiler for translating expressions to stack machine instructions,
    1.19 + and prove its correctness wrt.\ some evaluation semantics.
    1.20 +*}
    1.21 +
    1.22 +
    1.23 +subsection {* Binary operations *}
    1.24 +
    1.25 +text {*
    1.26 + Binary operations are just functions over some type of values.  This
    1.27 + is both for abstract syntax and semantics, i.e.\ we use a ``shallow
    1.28 + embedding'' here.
    1.29 +*}
    1.30 +
    1.31 +types
    1.32 +  'val binop = "'val => 'val => 'val"
    1.33 +
    1.34 +
    1.35 +subsection {* Expressions *}
    1.36 +
    1.37 +text {*
    1.38 + The language of expressions is defined as an inductive type,
    1.39 + consisting of variables, constants, and binary operations on
    1.40 + expressions.
    1.41 +*}
    1.42 +
    1.43 +datatype ('adr, 'val) expr =
    1.44 +  Variable 'adr |
    1.45 +  Constant 'val |
    1.46 +  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
    1.47 +
    1.48 +text {*
    1.49 + Evaluation (wrt.\ some environment of variable assignments) is
    1.50 + defined by primitive recursion over the structure of expressions.
    1.51 +*}
    1.52 +
    1.53 +consts
    1.54 +  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
    1.55 +
    1.56 +primrec
    1.57 +  "eval (Variable x) env = env x"
    1.58 +  "eval (Constant c) env = c"
    1.59 +  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
    1.60 +
    1.61 +
    1.62 +subsection {* Machine *}
    1.63 +
    1.64 +text {*
    1.65 + Next we model a simple stack machine, with three instructions.
    1.66 +*}
    1.67 +
    1.68 +datatype ('adr, 'val) instr =
    1.69 +  Const 'val |
    1.70 +  Load 'adr |
    1.71 +  Apply "'val binop"
    1.72 +
    1.73 +text {*
    1.74 + Execution of a list of stack machine instructions is easily defined
    1.75 + as follows.
    1.76 +*}
    1.77 +
    1.78 +consts
    1.79 +  exec :: "(('adr, 'val) instr) list
    1.80 +    => 'val list => ('adr => 'val) => 'val list"
    1.81 +
    1.82 +primrec
    1.83 +  "exec [] stack env = stack"
    1.84 +  "exec (instr # instrs) stack env =
    1.85 +    (case instr of
    1.86 +      Const c => exec instrs (c # stack) env
    1.87 +    | Load x => exec instrs (env x # stack) env
    1.88 +    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
    1.89 +                   # (tl (tl stack))) env)"
    1.90 +
    1.91 +constdefs
    1.92 +  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
    1.93 +  "execute instrs env == hd (exec instrs [] env)"
    1.94 +
    1.95 +
    1.96 +subsection {* Compiler *}
    1.97 +
    1.98 +text {*
    1.99 + We are ready to define the compilation function of expressions to
   1.100 + lists of stack machine instructions.
   1.101 +*}
   1.102 +
   1.103 +consts
   1.104 +  compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
   1.105 +
   1.106 +primrec
   1.107 +  "compile (Variable x) = [Load x]"
   1.108 +  "compile (Constant c) = [Const c]"
   1.109 +  "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
   1.110 +
   1.111 +
   1.112 +text {*
   1.113 + The main result of this development is the correctness theorem for
   1.114 + $\idt{compile}$.  We first establish a lemma about $\idt{exec}$ and
   1.115 + list append.
   1.116 +*}
   1.117 +
   1.118 +lemma exec_append:
   1.119 +  "exec (xs @ ys) stack env =
   1.120 +    exec ys (exec xs stack env) env"
   1.121 +proof (induct xs arbitrary: stack)
   1.122 +  case Nil
   1.123 +  show ?case by simp
   1.124 +next
   1.125 +  case (Cons x xs)
   1.126 +  show ?case
   1.127 +  proof (induct x)
   1.128 +    case Const
   1.129 +    from Cons show ?case by simp
   1.130 +  next
   1.131 +    case Load
   1.132 +    from Cons show ?case by simp
   1.133 +  next
   1.134 +    case Apply
   1.135 +    from Cons show ?case by simp
   1.136 +  qed
   1.137 +qed
   1.138 +
   1.139 +theorem correctness: "execute (compile e) env = eval e env"
   1.140 +proof -
   1.141 +  have "\<And>stack. exec (compile e) stack env = eval e env # stack"
   1.142 +  proof (induct e)
   1.143 +    case Variable show ?case by simp
   1.144 +  next
   1.145 +    case Constant show ?case by simp
   1.146 +  next
   1.147 +    case Binop then show ?case by (simp add: exec_append)
   1.148 +  qed
   1.149 +  then show ?thesis by (simp add: execute_def)
   1.150 +qed
   1.151 +
   1.152 +
   1.153 +text {*
   1.154 + \bigskip In the proofs above, the \name{simp} method does quite a lot
   1.155 + of work behind the scenes (mostly ``functional program execution'').
   1.156 + Subsequently, the same reasoning is elaborated in detail --- at most
   1.157 + one recursive function definition is used at a time.  Thus we get a
   1.158 + better idea of what is actually going on.
   1.159 +*}
   1.160 +
   1.161 +lemma exec_append':
   1.162 +  "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
   1.163 +proof (induct xs arbitrary: stack)
   1.164 +  case (Nil s)
   1.165 +  have "exec ([] @ ys) s env = exec ys s env" by simp
   1.166 +  also have "... = exec ys (exec [] s env) env" by simp
   1.167 +  finally show ?case .
   1.168 +next
   1.169 +  case (Cons x xs s)
   1.170 +  show ?case
   1.171 +  proof (induct x)
   1.172 +    case (Const val)
   1.173 +    have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
   1.174 +      by simp
   1.175 +    also have "... = exec (xs @ ys) (val # s) env" by simp
   1.176 +    also from Cons have "... = exec ys (exec xs (val # s) env) env" .
   1.177 +    also have "... = exec ys (exec (Const val # xs) s env) env" by simp
   1.178 +    finally show ?case .
   1.179 +  next
   1.180 +    case (Load adr)
   1.181 +    from Cons show ?case by simp -- {* same as above *}
   1.182 +  next
   1.183 +    case (Apply fn)
   1.184 +    have "exec ((Apply fn # xs) @ ys) s env =
   1.185 +        exec (Apply fn # xs @ ys) s env" by simp
   1.186 +    also have "... =
   1.187 +        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
   1.188 +    also from Cons have "... =
   1.189 +        exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
   1.190 +    also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
   1.191 +    finally show ?case .
   1.192 +  qed
   1.193 +qed
   1.194 +
   1.195 +theorem correctness': "execute (compile e) env = eval e env"
   1.196 +proof -
   1.197 +  have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
   1.198 +  proof (induct e)
   1.199 +    case (Variable adr s)
   1.200 +    have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
   1.201 +      by simp
   1.202 +    also have "... = env adr # s" by simp
   1.203 +    also have "env adr = eval (Variable adr) env" by simp
   1.204 +    finally show ?case .
   1.205 +  next
   1.206 +    case (Constant val s)
   1.207 +    show ?case by simp -- {* same as above *}
   1.208 +  next
   1.209 +    case (Binop fn e1 e2 s)
   1.210 +    have "exec (compile (Binop fn e1 e2)) s env =
   1.211 +        exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
   1.212 +    also have "... = exec [Apply fn]
   1.213 +        (exec (compile e1) (exec (compile e2) s env) env) env"
   1.214 +      by (simp only: exec_append)
   1.215 +    also have "exec (compile e2) s env = eval e2 env # s" by fact
   1.216 +    also have "exec (compile e1) ... env = eval e1 env # ..." by fact
   1.217 +    also have "exec [Apply fn] ... env =
   1.218 +        fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
   1.219 +    also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
   1.220 +    also have "fn (eval e1 env) (eval e2 env) =
   1.221 +        eval (Binop fn e1 e2) env"
   1.222 +      by simp
   1.223 +    finally show ?case .
   1.224 +  qed
   1.225 +
   1.226 +  have "execute (compile e) env = hd (exec (compile e) [] env)"
   1.227 +    by (simp add: execute_def)
   1.228 +  also from exec_compile
   1.229 +    have "exec (compile e) [] env = [eval e env]" .
   1.230 +  also have "hd ... = eval e env" by simp
   1.231 +  finally show ?thesis .
   1.232 +qed
   1.233 +
   1.234 +end