src/HOL/Isar_examples/ExprCompiler.thy
author wenzelm
Tue Aug 27 11:03:05 2002 +0200 (2002-08-27)
changeset 13524 604d0f3622d6
parent 11809 c9ffdd63dd93
child 13537 f506eb568121
permissions -rw-r--r--
*** empty log message ***
wenzelm@6444
     1
(*  Title:      HOL/Isar_examples/ExprCompiler.thy
wenzelm@6444
     2
    ID:         $Id$
wenzelm@6444
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6444
     4
wenzelm@6444
     5
Correctness of a simple expression/stack-machine compiler.
wenzelm@6444
     6
*)
wenzelm@6444
     7
wenzelm@10007
     8
header {* Correctness of a simple expression compiler *}
wenzelm@7748
     9
wenzelm@10007
    10
theory ExprCompiler = Main:
wenzelm@6444
    11
wenzelm@7869
    12
text {*
wenzelm@7874
    13
 This is a (rather trivial) example of program verification.  We model
wenzelm@7874
    14
 a compiler for translating expressions to stack machine instructions,
wenzelm@7874
    15
 and prove its correctness wrt.\ some evaluation semantics.
wenzelm@10007
    16
*}
wenzelm@7869
    17
wenzelm@7869
    18
wenzelm@10007
    19
subsection {* Binary operations *}
wenzelm@6444
    20
wenzelm@6744
    21
text {*
wenzelm@7869
    22
 Binary operations are just functions over some type of values.  This
wenzelm@7982
    23
 is both for abstract syntax and semantics, i.e.\ we use a ``shallow
wenzelm@7874
    24
 embedding'' here.
wenzelm@10007
    25
*}
wenzelm@6444
    26
wenzelm@6444
    27
types
wenzelm@10007
    28
  'val binop = "'val => 'val => 'val"
wenzelm@6444
    29
wenzelm@6444
    30
wenzelm@10007
    31
subsection {* Expressions *}
wenzelm@7869
    32
wenzelm@7869
    33
text {*
wenzelm@7869
    34
 The language of expressions is defined as an inductive type,
wenzelm@7869
    35
 consisting of variables, constants, and binary operations on
wenzelm@7869
    36
 expressions.
wenzelm@10007
    37
*}
wenzelm@7869
    38
wenzelm@7869
    39
datatype ('adr, 'val) expr =
wenzelm@7869
    40
  Variable 'adr |
wenzelm@7869
    41
  Constant 'val |
wenzelm@10007
    42
  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr"
wenzelm@7869
    43
wenzelm@7869
    44
text {*
wenzelm@7874
    45
 Evaluation (wrt.\ some environment of variable assignments) is
wenzelm@7874
    46
 defined by primitive recursion over the structure of expressions.
wenzelm@10007
    47
*}
wenzelm@7869
    48
wenzelm@7869
    49
consts
wenzelm@10007
    50
  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val"
wenzelm@7869
    51
wenzelm@7869
    52
primrec
wenzelm@7869
    53
  "eval (Variable x) env = env x"
wenzelm@7869
    54
  "eval (Constant c) env = c"
wenzelm@10007
    55
  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)"
wenzelm@7869
    56
wenzelm@7869
    57
wenzelm@10007
    58
subsection {* Machine *}
wenzelm@6444
    59
wenzelm@6744
    60
text {*
wenzelm@6792
    61
 Next we model a simple stack machine, with three instructions.
wenzelm@10007
    62
*}
wenzelm@6444
    63
wenzelm@6444
    64
datatype ('adr, 'val) instr =
wenzelm@6444
    65
  Const 'val |
wenzelm@6444
    66
  Load 'adr |
wenzelm@10007
    67
  Apply "'val binop"
wenzelm@6444
    68
wenzelm@6744
    69
text {*
wenzelm@7869
    70
 Execution of a list of stack machine instructions is easily defined
wenzelm@7869
    71
 as follows.
wenzelm@10007
    72
*}
wenzelm@6444
    73
wenzelm@6444
    74
consts
wenzelm@7761
    75
  exec :: "(('adr, 'val) instr) list
wenzelm@10007
    76
    => 'val list => ('adr => 'val) => 'val list"
wenzelm@6444
    77
wenzelm@6444
    78
primrec
wenzelm@6444
    79
  "exec [] stack env = stack"
wenzelm@6444
    80
  "exec (instr # instrs) stack env =
wenzelm@6444
    81
    (case instr of
wenzelm@6444
    82
      Const c => exec instrs (c # stack) env
wenzelm@6444
    83
    | Load x => exec instrs (env x # stack) env
wenzelm@7761
    84
    | Apply f => exec instrs (f (hd stack) (hd (tl stack))
wenzelm@10007
    85
                   # (tl (tl stack))) env)"
wenzelm@6444
    86
wenzelm@6444
    87
constdefs
wenzelm@6444
    88
  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
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@7748
   115
  "ALL stack. exec (xs @ ys) stack env =
wenzelm@10007
   116
    exec ys (exec xs stack env) env" (is "?P xs")
wenzelm@11809
   117
proof (induct xs)
wenzelm@10007
   118
  show "?P []" by simp
wenzelm@11809
   119
next
wenzelm@11809
   120
  fix x xs assume hyp: "?P xs"
wenzelm@11809
   121
  show "?P (x # xs)"
wenzelm@11809
   122
  proof (induct x)
wenzelm@11809
   123
    from hyp show "!!val. ?P (Const val # xs)" by simp
wenzelm@11809
   124
    from hyp show "!!adr. ?P (Load adr # xs)" by simp
wenzelm@11809
   125
    from hyp show "!!fun. ?P (Apply fun # xs)" by simp
wenzelm@10007
   126
  qed
wenzelm@10007
   127
qed
wenzelm@6444
   128
wenzelm@10007
   129
theorem correctness: "execute (compile e) env = eval e env"
wenzelm@10007
   130
proof -
wenzelm@8051
   131
  have "ALL stack. exec (compile e) stack env =
wenzelm@10007
   132
    eval e env # stack" (is "?P e")
wenzelm@11809
   133
  proof (induct e)
wenzelm@10007
   134
    show "!!adr. ?P (Variable adr)" by simp
wenzelm@10007
   135
    show "!!val. ?P (Constant val)" by simp
wenzelm@11809
   136
    show "!!fun e1 e2. ?P e1 ==> ?P e2 ==> ?P (Binop fun e1 e2)"
wenzelm@10007
   137
      by (simp add: exec_append)
wenzelm@10007
   138
  qed
wenzelm@10007
   139
  thus ?thesis by (simp add: execute_def)
wenzelm@10007
   140
qed
wenzelm@6444
   141
wenzelm@6444
   142
wenzelm@8051
   143
text {*
wenzelm@8051
   144
 \bigskip In the proofs above, the \name{simp} method does quite a lot
wenzelm@8051
   145
 of work behind the scenes (mostly ``functional program execution'').
wenzelm@8051
   146
 Subsequently, the same reasoning is elaborated in detail --- at most
wenzelm@8051
   147
 one recursive function definition is used at a time.  Thus we get a
wenzelm@8051
   148
 better idea of what is actually going on.
wenzelm@10007
   149
*}
wenzelm@8051
   150
wenzelm@13524
   151
lemma exec_append':
wenzelm@8052
   152
  "ALL stack. exec (xs @ ys) stack env
wenzelm@10007
   153
    = exec ys (exec xs stack env) env" (is "?P xs")
wenzelm@11809
   154
proof (induct xs)
wenzelm@10007
   155
  show "?P []" (is "ALL s. ?Q s")
wenzelm@10007
   156
  proof
wenzelm@10007
   157
    fix s have "exec ([] @ ys) s env = exec ys s env" by simp
wenzelm@10007
   158
    also have "... = exec ys (exec [] s env) env" by simp
wenzelm@10007
   159
    finally show "?Q s" .
wenzelm@10007
   160
  qed
wenzelm@10007
   161
  fix x xs assume hyp: "?P xs"
wenzelm@10007
   162
  show "?P (x # xs)"
wenzelm@10007
   163
  proof (induct x)
wenzelm@10007
   164
    fix val
wenzelm@10007
   165
    show "?P (Const val # xs)" (is "ALL s. ?Q s")
wenzelm@10007
   166
    proof
wenzelm@10007
   167
      fix s
wenzelm@8052
   168
      have "exec ((Const val # xs) @ ys) s env =
wenzelm@10007
   169
          exec (Const val # xs @ ys) s env"
wenzelm@10007
   170
        by simp
wenzelm@10007
   171
      also have "... = exec (xs @ ys) (val # s) env" by simp
wenzelm@10007
   172
      also from hyp
wenzelm@10007
   173
        have "... = exec ys (exec xs (val # s) env) env" ..
wenzelm@10007
   174
      also have "... = exec ys (exec (Const val # xs) s env) env"
wenzelm@10007
   175
        by simp
wenzelm@10007
   176
      finally show "?Q s" .
wenzelm@10007
   177
    qed
wenzelm@10007
   178
  next
wenzelm@10007
   179
    fix adr from hyp show "?P (Load adr # xs)" by simp -- {* same as above *}
wenzelm@10007
   180
  next
wenzelm@10007
   181
    fix fun
wenzelm@10007
   182
    show "?P (Apply fun # xs)" (is "ALL s. ?Q s")
wenzelm@10007
   183
    proof
wenzelm@10007
   184
      fix s
wenzelm@8052
   185
      have "exec ((Apply fun # xs) @ ys) s env =
wenzelm@10007
   186
          exec (Apply fun # xs @ ys) s env"
wenzelm@10007
   187
        by simp
wenzelm@10007
   188
      also have "... =
wenzelm@10007
   189
          exec (xs @ ys) (fun (hd s) (hd (tl s)) # (tl (tl s))) env"
wenzelm@10007
   190
        by simp
wenzelm@10007
   191
      also from hyp have "... =
wenzelm@10007
   192
        exec ys (exec xs (fun (hd s) (hd (tl s)) # tl (tl s)) env) env"
wenzelm@10007
   193
        ..
wenzelm@10007
   194
      also have "... = exec ys (exec (Apply fun # xs) s env) env" by simp
wenzelm@10007
   195
      finally show "?Q s" .
wenzelm@10007
   196
    qed
wenzelm@10007
   197
  qed
wenzelm@10007
   198
qed
wenzelm@6444
   199
wenzelm@10007
   200
theorem correctness: "execute (compile e) env = eval e env"
wenzelm@10007
   201
proof -
wenzelm@8052
   202
  have exec_compile:
wenzelm@9659
   203
    "ALL stack. exec (compile e) stack env = eval e env # stack"
wenzelm@10007
   204
    (is "?P e")
wenzelm@10007
   205
  proof (induct e)
wenzelm@10007
   206
    fix adr show "?P (Variable adr)" (is "ALL s. ?Q s")
wenzelm@10007
   207
    proof
wenzelm@10007
   208
      fix s
wenzelm@10007
   209
      have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
wenzelm@10007
   210
        by simp
wenzelm@10007
   211
      also have "... = env adr # s" by simp
wenzelm@10007
   212
      also have "env adr = eval (Variable adr) env" by simp
wenzelm@10007
   213
      finally show "?Q s" .
wenzelm@10007
   214
    qed
wenzelm@10007
   215
  next
wenzelm@10007
   216
    fix val show "?P (Constant val)" by simp -- {* same as above *}
wenzelm@10007
   217
  next
wenzelm@10007
   218
    fix fun e1 e2 assume hyp1: "?P e1" and hyp2: "?P e2"
wenzelm@10007
   219
    show "?P (Binop fun e1 e2)" (is "ALL s. ?Q s")
wenzelm@10007
   220
    proof
wenzelm@10007
   221
      fix s have "exec (compile (Binop fun e1 e2)) s env
wenzelm@10007
   222
        = exec (compile e2 @ compile e1 @ [Apply fun]) s env" by simp
wenzelm@10007
   223
      also have "... = exec [Apply fun]
wenzelm@10007
   224
          (exec (compile e1) (exec (compile e2) s env) env) env"
wenzelm@10007
   225
        by (simp only: exec_append)
wenzelm@10007
   226
      also from hyp2
wenzelm@10007
   227
        have "exec (compile e2) s env = eval e2 env # s" ..
wenzelm@10007
   228
      also from hyp1
wenzelm@10007
   229
        have "exec (compile e1) ... env = eval e1 env # ..." ..
wenzelm@10007
   230
      also have "exec [Apply fun] ... env =
wenzelm@10007
   231
        fun (hd ...) (hd (tl ...)) # (tl (tl ...))" by simp
wenzelm@10007
   232
      also have "... = fun (eval e1 env) (eval e2 env) # s" by simp
wenzelm@10007
   233
      also have "fun (eval e1 env) (eval e2 env) =
wenzelm@10007
   234
          eval (Binop fun e1 e2) env"
wenzelm@10007
   235
        by simp
wenzelm@10007
   236
      finally show "?Q s" .
wenzelm@10007
   237
    qed
wenzelm@10007
   238
  qed
wenzelm@8051
   239
wenzelm@10007
   240
  have "execute (compile e) env = hd (exec (compile e) [] env)"
wenzelm@10007
   241
    by (simp add: execute_def)
wenzelm@10007
   242
  also from exec_compile
wenzelm@10007
   243
    have "exec (compile e) [] env = [eval e env]" ..
wenzelm@10007
   244
  also have "hd ... = eval e env" by simp
wenzelm@10007
   245
  finally show ?thesis .
wenzelm@10007
   246
qed
wenzelm@6444
   247
wenzelm@10007
   248
end