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