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