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