src/HOL/Isar_examples/ExprCompiler.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7874 180364256231
child 8031 826c6222cca2
permissions -rw-r--r--
improved presentation;
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@7748
     8
header {* Correctness of a simple expression compiler *};
wenzelm@7748
     9
wenzelm@6444
    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@7869
    16
*};
wenzelm@7869
    17
wenzelm@7869
    18
wenzelm@7869
    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@6744
    25
*};
wenzelm@6444
    26
wenzelm@6444
    27
types
wenzelm@6444
    28
  'val binop = "'val => 'val => 'val";
wenzelm@6444
    29
wenzelm@6444
    30
wenzelm@7869
    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@7869
    37
*};
wenzelm@7869
    38
wenzelm@7869
    39
datatype ('adr, 'val) expr =
wenzelm@7869
    40
  Variable 'adr |
wenzelm@7869
    41
  Constant 'val |
wenzelm@7869
    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@7869
    47
*};
wenzelm@7869
    48
wenzelm@7869
    49
consts
wenzelm@7869
    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@7869
    55
  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
wenzelm@7869
    56
wenzelm@7869
    57
wenzelm@7748
    58
subsection {* Machine *};
wenzelm@6444
    59
wenzelm@6744
    60
text {*
wenzelm@6792
    61
 Next we model a simple stack machine, with three instructions.
wenzelm@6744
    62
*};
wenzelm@6444
    63
wenzelm@6444
    64
datatype ('adr, 'val) instr =
wenzelm@6444
    65
  Const 'val |
wenzelm@6444
    66
  Load 'adr |
wenzelm@6444
    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@6744
    72
*};
wenzelm@6444
    73
wenzelm@6444
    74
consts
wenzelm@7761
    75
  exec :: "(('adr, 'val) instr) list
wenzelm@7761
    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@7761
    85
                   # (tl (tl stack))) env)";
wenzelm@6444
    86
wenzelm@6444
    87
constdefs
wenzelm@6444
    88
  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
wenzelm@6444
    89
  "execute instrs env == hd (exec instrs [] env)";
wenzelm@6444
    90
wenzelm@6444
    91
wenzelm@7748
    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@6744
    97
*};
wenzelm@6444
    98
wenzelm@6444
    99
consts
wenzelm@6444
   100
  comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";
wenzelm@6444
   101
wenzelm@6444
   102
primrec
wenzelm@6444
   103
  "comp (Variable x) = [Load x]"
wenzelm@6444
   104
  "comp (Constant c) = [Const c]"
wenzelm@6444
   105
  "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
wenzelm@6444
   106
wenzelm@6444
   107
wenzelm@6744
   108
text {*
wenzelm@7748
   109
  The main result of this development is the correctness theorem for
wenzelm@7748
   110
  $\idt{comp}$.  We first establish some lemmas about $\idt{exec}$.
wenzelm@6744
   111
*};
wenzelm@6444
   112
wenzelm@6444
   113
lemma exec_append:
wenzelm@7748
   114
  "ALL stack. exec (xs @ ys) stack env =
wenzelm@7748
   115
    exec ys (exec xs stack env) env" (is "?P xs");
wenzelm@7480
   116
proof (induct ?P xs type: list);
wenzelm@7480
   117
  show "?P []"; by simp;
wenzelm@6444
   118
wenzelm@6444
   119
  fix x xs;
wenzelm@7480
   120
  assume "?P xs";
wenzelm@7480
   121
  show "?P (x # xs)" (is "?Q x");
wenzelm@7480
   122
  proof (induct ?Q x type: instr);
wenzelm@7565
   123
    fix val; show "?Q (Const val)"; by (simp!);
wenzelm@6938
   124
  next;
wenzelm@7565
   125
    fix adr; show "?Q (Load adr)"; by (simp!);
wenzelm@6938
   126
  next;
wenzelm@7565
   127
    fix fun; show "?Q (Apply fun)"; by (simp!);
wenzelm@6444
   128
  qed;
wenzelm@6444
   129
qed;
wenzelm@6444
   130
wenzelm@6444
   131
lemma exec_comp:
wenzelm@7748
   132
  "ALL stack. exec (comp e) stack env =
wenzelm@7748
   133
    eval e env # stack" (is "?P e");
wenzelm@7480
   134
proof (induct ?P e type: expr);
wenzelm@7565
   135
  fix adr; show "?P (Variable adr)"; by (simp!);
wenzelm@6938
   136
next;
wenzelm@7565
   137
  fix val; show "?P (Constant val)"; by (simp!);
wenzelm@6938
   138
next;
wenzelm@7480
   139
  fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
wenzelm@7565
   140
    by (simp! add: exec_append);
wenzelm@6444
   141
qed;
wenzelm@6444
   142
wenzelm@6444
   143
wenzelm@6746
   144
text {* Main theorem ahead. *};
wenzelm@6444
   145
wenzelm@6444
   146
theorem correctness: "execute (comp e) env = eval e env";
wenzelm@6444
   147
  by (simp add: execute_def exec_comp);
wenzelm@6444
   148
wenzelm@6444
   149
end;