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