src/HOL/Isar_Examples/Expr_Compiler.thy
author nipkow
Mon Jan 30 21:49:41 2012 +0100 (2012-01-30)
changeset 46372 6fa9cdb8b850
parent 41818 6d4c3ee8219d
child 46582 dcc312f22ee8
permissions -rw-r--r--
added "'a rel"
     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 => 'val => '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 => ('adr => 'val) => '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
    63   exec :: "(('adr, 'val) instr) list
    64     => 'val list => ('adr => 'val) => 'val list"
    65 where
    66   "exec [] stack env = stack"
    67 | "exec (instr # instrs) stack env =
    68     (case instr of
    69       Const c => exec instrs (c # stack) env
    70     | Load x => exec instrs (env x # stack) env
    71     | Apply f => exec instrs (f (hd stack) (hd (tl stack))
    72                    # (tl (tl stack))) env)"
    73 
    74 definition
    75   execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
    76   where "execute instrs env = hd (exec instrs [] env)"
    77 
    78 
    79 subsection {* Compiler *}
    80 
    81 text {* We are ready to define the compilation function of expressions
    82   to lists of stack machine instructions. *}
    83 
    84 primrec
    85   compile :: "('adr, 'val) expr => (('adr, 'val) instr) list"
    86 where
    87   "compile (Variable x) = [Load x]"
    88 | "compile (Constant c) = [Const c]"
    89 | "compile (Binop f e1 e2) = compile e2 @ compile e1 @ [Apply f]"
    90 
    91 
    92 text {* The main result of this development is the correctness theorem
    93   for @{text compile}.  We first establish a lemma about @{text exec}
    94   and list append. *}
    95 
    96 lemma exec_append:
    97   "exec (xs @ ys) stack env =
    98     exec ys (exec xs stack env) env"
    99 proof (induct xs arbitrary: stack)
   100   case Nil
   101   show ?case by simp
   102 next
   103   case (Cons x xs)
   104   show ?case
   105   proof (induct x)
   106     case Const
   107     from Cons show ?case by simp
   108   next
   109     case Load
   110     from Cons show ?case by simp
   111   next
   112     case Apply
   113     from Cons show ?case by simp
   114   qed
   115 qed
   116 
   117 theorem correctness: "execute (compile e) env = eval e env"
   118 proof -
   119   have "\<And>stack. exec (compile e) stack env = eval e env # stack"
   120   proof (induct e)
   121     case Variable show ?case by simp
   122   next
   123     case Constant show ?case by simp
   124   next
   125     case Binop then show ?case by (simp add: exec_append)
   126   qed
   127   then show ?thesis by (simp add: execute_def)
   128 qed
   129 
   130 
   131 text {* \bigskip In the proofs above, the @{text simp} method does
   132   quite a lot of work behind the scenes (mostly ``functional program
   133   execution'').  Subsequently, the same reasoning is elaborated in
   134   detail --- at most one recursive function definition is used at a
   135   time.  Thus we get a better idea of what is actually going on. *}
   136 
   137 lemma exec_append':
   138   "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
   139 proof (induct xs arbitrary: stack)
   140   case (Nil s)
   141   have "exec ([] @ ys) s env = exec ys s env" by simp
   142   also have "... = exec ys (exec [] s env) env" by simp
   143   finally show ?case .
   144 next
   145   case (Cons x xs s)
   146   show ?case
   147   proof (induct x)
   148     case (Const val)
   149     have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
   150       by simp
   151     also have "... = exec (xs @ ys) (val # s) env" by simp
   152     also from Cons have "... = exec ys (exec xs (val # s) env) env" .
   153     also have "... = exec ys (exec (Const val # xs) s env) env" by simp
   154     finally show ?case .
   155   next
   156     case (Load adr)
   157     from Cons show ?case by simp -- {* same as above *}
   158   next
   159     case (Apply fn)
   160     have "exec ((Apply fn # xs) @ ys) s env =
   161         exec (Apply fn # xs @ ys) s env" by simp
   162     also have "... =
   163         exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
   164     also from Cons have "... =
   165         exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
   166     also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
   167     finally show ?case .
   168   qed
   169 qed
   170 
   171 theorem correctness': "execute (compile e) env = eval e env"
   172 proof -
   173   have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
   174   proof (induct e)
   175     case (Variable adr s)
   176     have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
   177       by simp
   178     also have "... = env adr # s" by simp
   179     also have "env adr = eval (Variable adr) env" by simp
   180     finally show ?case .
   181   next
   182     case (Constant val s)
   183     show ?case by simp -- {* same as above *}
   184   next
   185     case (Binop fn e1 e2 s)
   186     have "exec (compile (Binop fn e1 e2)) s env =
   187         exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
   188     also have "... = exec [Apply fn]
   189         (exec (compile e1) (exec (compile e2) s env) env) env"
   190       by (simp only: exec_append)
   191     also have "exec (compile e2) s env = eval e2 env # s" by fact
   192     also have "exec (compile e1) ... env = eval e1 env # ..." by fact
   193     also have "exec [Apply fn] ... env =
   194         fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
   195     also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
   196     also have "fn (eval e1 env) (eval e2 env) =
   197         eval (Binop fn e1 e2) env"
   198       by simp
   199     finally show ?case .
   200   qed
   201 
   202   have "execute (compile e) env = hd (exec (compile e) [] env)"
   203     by (simp add: execute_def)
   204   also from exec_compile have "exec (compile e) [] env = [eval e env]" .
   205   also have "hd ... = eval e env" by simp
   206   finally show ?thesis .
   207 qed
   208 
   209 end