src/HOL/Isar_examples/ExprCompiler.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10007 64bf7da1994a
child 11809 c9ffdd63dd93
permissions -rw-r--r--
improved theory reference in comment
     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 = Main:
    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   "ALL stack. exec (xs @ ys) stack env =
   116     exec ys (exec xs stack env) env" (is "?P xs")
   117 proof (induct ?P xs type: list)
   118   show "?P []" by simp
   119 
   120   fix x xs assume "?P xs"
   121   show "?P (x # xs)" (is "?Q x")
   122   proof (induct ?Q x type: instr)
   123     show "!!val. ?Q (Const val)" by (simp!)
   124     show "!!adr. ?Q (Load adr)" by (simp!)
   125     show "!!fun. ?Q (Apply fun)" by (simp!)
   126   qed
   127 qed
   128 
   129 theorem correctness: "execute (compile e) env = eval e env"
   130 proof -
   131   have "ALL stack. exec (compile e) stack env =
   132     eval e env # stack" (is "?P e")
   133   proof (induct ?P e type: expr)
   134     show "!!adr. ?P (Variable adr)" by simp
   135     show "!!val. ?P (Constant val)" by simp
   136     show "!!fun e1 e2. (?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2))"
   137       by (simp add: exec_append)
   138   qed
   139   thus ?thesis by (simp add: execute_def)
   140 qed
   141 
   142 
   143 text {*
   144  \bigskip In the proofs above, the \name{simp} method does quite a lot
   145  of work behind the scenes (mostly ``functional program execution'').
   146  Subsequently, the same reasoning is elaborated in detail --- at most
   147  one recursive function definition is used at a time.  Thus we get a
   148  better idea of what is actually going on.
   149 *}
   150 
   151 lemma exec_append:
   152   "ALL stack. exec (xs @ ys) stack env
   153     = exec ys (exec xs stack env) env" (is "?P xs")
   154 proof (induct ?P xs)
   155   show "?P []" (is "ALL s. ?Q s")
   156   proof
   157     fix s have "exec ([] @ ys) s env = exec ys s env" by simp
   158     also have "... = exec ys (exec [] s env) env" by simp
   159     finally show "?Q s" .
   160   qed
   161   fix x xs assume hyp: "?P xs"
   162   show "?P (x # xs)"
   163   proof (induct x)
   164     fix val
   165     show "?P (Const val # xs)" (is "ALL s. ?Q s")
   166     proof
   167       fix s
   168       have "exec ((Const val # xs) @ ys) s env =
   169           exec (Const val # xs @ ys) s env"
   170         by simp
   171       also have "... = exec (xs @ ys) (val # s) env" by simp
   172       also from hyp
   173         have "... = exec ys (exec xs (val # s) env) env" ..
   174       also have "... = exec ys (exec (Const val # xs) s env) env"
   175         by simp
   176       finally show "?Q s" .
   177     qed
   178   next
   179     fix adr from hyp show "?P (Load adr # xs)" by simp -- {* same as above *}
   180   next
   181     fix fun
   182     show "?P (Apply fun # xs)" (is "ALL s. ?Q s")
   183     proof
   184       fix s
   185       have "exec ((Apply fun # xs) @ ys) s env =
   186           exec (Apply fun # xs @ ys) s env"
   187         by simp
   188       also have "... =
   189           exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"
   190         by simp
   191       also from hyp have "... =
   192         exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"
   193         ..
   194       also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp
   195       finally show "?Q s" .
   196     qed
   197   qed
   198 qed
   199 
   200 theorem correctness: "execute (compile e) env = eval e env"
   201 proof -
   202   have exec_compile:
   203     "ALL stack. exec (compile e) stack env = eval e env # stack"
   204     (is "?P e")
   205   proof (induct e)
   206     fix adr show "?P (Variable adr)" (is "ALL s. ?Q s")
   207     proof
   208       fix s
   209       have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
   210         by simp
   211       also have "... = env adr # s" by simp
   212       also have "env adr = eval (Variable adr) env" by simp
   213       finally show "?Q s" .
   214     qed
   215   next
   216     fix val show "?P (Constant val)" by simp -- {* same as above *}
   217   next
   218     fix fun e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"
   219     show "?P (Binop fun e1 e2)" (is "ALL s. ?Q s")
   220     proof
   221       fix s have "exec (compile (Binop fun e1 e2)) s env
   222         = exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp
   223       also have "... = exec [Apply fun]
   224           (exec (compile e1) (exec (compile e2) s env) env) env"
   225         by (simp only: exec_append)
   226       also from hyp2
   227         have "exec (compile e2) s env = eval e2 env # s" ..
   228       also from hyp1
   229         have "exec (compile e1) ... env = eval e1 env # ..." ..
   230       also have "exec [Apply fun] ... env =
   231         fun (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
   232       also have "... = fun (eval e1 env) (eval e2 env) # s" by simp
   233       also have "fun (eval e1 env) (eval e2 env) =
   234           eval (Binop fun e1 e2) env"
   235         by simp
   236       finally show "?Q s" .
   237     qed
   238   qed
   239 
   240   have "execute (compile e) env = hd (exec (compile e) [] env)"
   241     by (simp add: execute_def)
   242   also from exec_compile
   243     have "exec (compile e) [] env = [eval e env]" ..
   244   also have "hd ... = eval e env" by simp
   245   finally show ?thesis .
   246 qed
   247 
   248 end