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