src/HOL/Isar_Examples/Expr_Compiler.thy
author blanchet
Tue Sep 09 20:51:36 2014 +0200 (2014-09-09)
changeset 58260 c96e511bfb79
parent 58249 180f1b3508ed
child 58310 91ea607a34d8
permissions -rw-r--r--
ported Isar_Examples to new datatypes
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@55640
    25
type_synonym 'val binop = "'val \<Rightarrow> 'val \<Rightarrow> '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
blanchet@58260
    34
datatype_new (dead 'adr, dead '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@55640
    42
primrec eval :: "('adr, 'val) expr \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> '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
blanchet@58260
    54
datatype_new (dead 'adr, dead '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@55640
    62
primrec exec :: "(('adr, 'val) instr) list \<Rightarrow> 'val list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> '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@55640
    67
      Const c \<Rightarrow> exec instrs (c # stack) env
wenzelm@55640
    68
    | Load x \<Rightarrow> exec instrs (env x # stack) env
wenzelm@55640
    69
    | Apply f \<Rightarrow> exec instrs (f (hd stack) (hd (tl stack))
wenzelm@10007
    70
                   # (tl (tl stack))) env)"
wenzelm@6444
    71
wenzelm@55640
    72
definition execute :: "(('adr, 'val) instr) list \<Rightarrow> ('adr \<Rightarrow> 'val) \<Rightarrow> '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@55640
    81
primrec compile :: "('adr, 'val) expr \<Rightarrow> (('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@55640
   117
    case Variable
wenzelm@55640
   118
    show ?case by simp
wenzelm@18153
   119
  next
wenzelm@55640
   120
    case Constant
wenzelm@55640
   121
    show ?case by simp
wenzelm@18153
   122
  next
wenzelm@55640
   123
    case Binop
wenzelm@55640
   124
    then show ?case by (simp add: exec_append)
wenzelm@10007
   125
  qed
wenzelm@23373
   126
  then show ?thesis by (simp add: execute_def)
wenzelm@10007
   127
qed
wenzelm@6444
   128
wenzelm@6444
   129
wenzelm@37671
   130
text {* \bigskip In the proofs above, the @{text simp} method does
wenzelm@37671
   131
  quite a lot of work behind the scenes (mostly ``functional program
wenzelm@37671
   132
  execution'').  Subsequently, the same reasoning is elaborated in
wenzelm@37671
   133
  detail --- at most one recursive function definition is used at a
wenzelm@37671
   134
  time.  Thus we get a better idea of what is actually going on. *}
wenzelm@8051
   135
wenzelm@13524
   136
lemma exec_append':
wenzelm@18153
   137
  "exec (xs @ ys) stack env = exec ys (exec xs stack env) env"
wenzelm@20503
   138
proof (induct xs arbitrary: stack)
wenzelm@18153
   139
  case (Nil s)
wenzelm@55640
   140
  have "exec ([] @ ys) s env = exec ys s env"
wenzelm@55640
   141
    by simp
wenzelm@55640
   142
  also have "\<dots> = exec ys (exec [] s env) env"
wenzelm@55640
   143
    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@55640
   152
    also have "\<dots> = exec (xs @ ys) (val # s) env"
wenzelm@55640
   153
      by simp
wenzelm@55640
   154
    also from Cons have "\<dots> = exec ys (exec xs (val # s) env) env" .
wenzelm@55640
   155
    also have "\<dots> = exec ys (exec (Const val # xs) s env) env"
wenzelm@55640
   156
      by simp
wenzelm@18153
   157
    finally show ?case .
wenzelm@10007
   158
  next
wenzelm@18153
   159
    case (Load adr)
wenzelm@55640
   160
    from Cons show ?case
wenzelm@55640
   161
      by simp -- {* same as above *}
wenzelm@18153
   162
  next
krauss@20523
   163
    case (Apply fn)
krauss@20523
   164
    have "exec ((Apply fn # xs) @ ys) s env =
krauss@20523
   165
        exec (Apply fn # xs @ ys) s env" by simp
wenzelm@55640
   166
    also have "\<dots> =
wenzelm@55640
   167
        exec (xs @ ys) (fn (hd s) (hd (tl s)) # (tl (tl s))) env"
wenzelm@55640
   168
      by simp
wenzelm@55640
   169
    also from Cons have "\<dots> =
krauss@20523
   170
        exec ys (exec xs (fn (hd s) (hd (tl s)) # tl (tl s)) env) env" .
wenzelm@55640
   171
    also have "\<dots> = exec ys (exec (Apply fn # xs) s env) env"
wenzelm@55640
   172
      by simp
wenzelm@18153
   173
    finally show ?case .
wenzelm@10007
   174
  qed
wenzelm@10007
   175
qed
wenzelm@6444
   176
wenzelm@13537
   177
theorem correctness': "execute (compile e) env = eval e env"
wenzelm@10007
   178
proof -
wenzelm@18193
   179
  have exec_compile: "\<And>stack. exec (compile e) stack env = eval e env # stack"
wenzelm@10007
   180
  proof (induct e)
wenzelm@18153
   181
    case (Variable adr s)
wenzelm@18153
   182
    have "exec (compile (Variable adr)) s env = exec [Load adr] s env"
wenzelm@18153
   183
      by simp
wenzelm@55640
   184
    also have "\<dots> = env adr # s"
wenzelm@55640
   185
      by simp
wenzelm@55640
   186
    also have "env adr = eval (Variable adr) env"
wenzelm@55640
   187
      by simp
wenzelm@18153
   188
    finally show ?case .
wenzelm@10007
   189
  next
wenzelm@18153
   190
    case (Constant val s)
wenzelm@18153
   191
    show ?case by simp -- {* same as above *}
wenzelm@10007
   192
  next
krauss@20523
   193
    case (Binop fn e1 e2 s)
krauss@20523
   194
    have "exec (compile (Binop fn e1 e2)) s env =
wenzelm@55640
   195
        exec (compile e2 @ compile e1 @ [Apply fn]) s env"
wenzelm@55640
   196
      by simp
wenzelm@55640
   197
    also have "\<dots> = exec [Apply fn]
wenzelm@18153
   198
        (exec (compile e1) (exec (compile e2) s env) env) env"
wenzelm@18153
   199
      by (simp only: exec_append)
wenzelm@55640
   200
    also have "exec (compile e2) s env = eval e2 env # s"
wenzelm@55640
   201
      by fact
wenzelm@55640
   202
    also have "exec (compile e1) \<dots> env = eval e1 env # \<dots>"
wenzelm@55640
   203
      by fact
wenzelm@55640
   204
    also have "exec [Apply fn] \<dots> env =
wenzelm@55640
   205
        fn (hd \<dots>) (hd (tl \<dots>)) # (tl (tl \<dots>))"
wenzelm@55640
   206
      by simp
wenzelm@55640
   207
    also have "\<dots> = fn (eval e1 env) (eval e2 env) # s"
wenzelm@55640
   208
      by simp
krauss@20523
   209
    also have "fn (eval e1 env) (eval e2 env) =
krauss@20523
   210
        eval (Binop fn e1 e2) env"
wenzelm@18153
   211
      by simp
wenzelm@18153
   212
    finally show ?case .
wenzelm@10007
   213
  qed
wenzelm@8051
   214
wenzelm@10007
   215
  have "execute (compile e) env = hd (exec (compile e) [] env)"
wenzelm@10007
   216
    by (simp add: execute_def)
wenzelm@37671
   217
  also from exec_compile have "exec (compile e) [] env = [eval e env]" .
wenzelm@55640
   218
  also have "hd \<dots> = eval e env"
wenzelm@55640
   219
    by simp
wenzelm@10007
   220
  finally show ?thesis .
wenzelm@10007
   221
qed
wenzelm@6444
   222
wenzelm@10007
   223
end