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