src/HOL/Isar_Examples/Expr_Compiler.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 46582 dcc312f22ee8
child 55640 abc140f21caa
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     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 exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list"
    63 where
    64   "exec [] stack env = stack"
    65 | "exec (instr # instrs) stack env =
    66     (case instr of
    67       Const c => exec instrs (c # stack) env
    68     | Load x => exec instrs (env x # stack) env
    69     | Apply f => exec instrs (f (hd stack) (hd (tl stack))
    70                    # (tl (tl stack))) env)"
    71 
    72 definition execute :: "(('adr, 'val) instr) list => ('adr => 'val) => '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 => (('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 show ?case by simp
   118   next
   119     case Constant show ?case by simp
   120   next
   121     case Binop then show ?case by (simp add: exec_append)
   122   qed
   123   then show ?thesis by (simp add: execute_def)
   124 qed
   125 
   126 
   127 text {* \bigskip In the proofs above, the @{text simp} method does
   128   quite a lot of work behind the scenes (mostly ``functional program
   129   execution'').  Subsequently, the same reasoning is elaborated in
   130   detail --- at most one recursive function definition is used at a
   131   time.  Thus we get a better idea of what is actually going on. *}
   132 
   133 lemma exec_append':
   134   "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
   135 proof (induct xs arbitrary: stack)
   136   case (Nil s)
   137   have "exec ([] @ ys) s env = exec ys s env" by simp
   138   also have "... = exec ys (exec [] s env) env" by simp
   139   finally show ?case .
   140 next
   141   case (Cons x xs s)
   142   show ?case
   143   proof (induct x)
   144     case (Const val)
   145     have "exec ((Const val # xs) @ ys) s env = exec (Const val # xs @ ys) s env"
   146       by simp
   147     also have "... = exec (xs @ ys) (val # s) env" by simp
   148     also from Cons have "... = exec ys (exec xs (val # s) env) env" .
   149     also have "... = exec ys (exec (Const val # xs) s env) env" by simp
   150     finally show ?case .
   151   next
   152     case (Load adr)
   153     from Cons show ?case by simp -- {* same as above *}
   154   next
   155     case (Apply fn)
   156     have "exec ((Apply fn # xs) @ ys) s env =
   157         exec (Apply fn # xs @ ys) s env" by simp
   158     also have "... =
   159         exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env" by simp
   160     also from Cons have "... =
   161         exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
   162     also have "... = exec ys (exec (Apply fn # xs) s env) env" by simp
   163     finally show ?case .
   164   qed
   165 qed
   166 
   167 theorem correctness': "execute (compile e) env = eval e env"
   168 proof -
   169   have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
   170   proof (induct e)
   171     case (Variable adr s)
   172     have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
   173       by simp
   174     also have "... = env adr # s" by simp
   175     also have "env adr = eval (Variable adr) env" by simp
   176     finally show ?case .
   177   next
   178     case (Constant val s)
   179     show ?case by simp -- {* same as above *}
   180   next
   181     case (Binop fn e1 e2 s)
   182     have "exec (compile (Binop fn e1 e2)) s env =
   183         exec (compile e2 @ compile e1 @ [Apply fn]) s env" by simp
   184     also have "... = exec [Apply fn]
   185         (exec (compile e1) (exec (compile e2) s env) env) env"
   186       by (simp only: exec_append)
   187     also have "exec (compile e2) s env = eval e2 env # s" by fact
   188     also have "exec (compile e1) ... env = eval e1 env # ..." by fact
   189     also have "exec [Apply fn] ... env =
   190         fn (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
   191     also have "... = fn (eval e1 env) (eval e2 env) # s" by simp
   192     also have "fn (eval e1 env) (eval e2 env) =
   193         eval (Binop fn e1 e2) env"
   194       by simp
   195     finally show ?case .
   196   qed
   197 
   198   have "execute (compile e) env = hd (exec (compile e) [] env)"
   199     by (simp add: execute_def)
   200   also from exec_compile have "exec (compile e) [] env = [eval e env]" .
   201   also have "hd ... = eval e env" by simp
   202   finally show ?thesis .
   203 qed
   204 
   205 end