src/HOL/Isar_examples/ExprCompiler.thy
author wenzelm
Sat Sep 04 21:13:01 1999 +0200 (1999-09-04)
changeset 7480 0a0e0dbe1269
parent 7253 a494a78fea39
child 7565 bfa85f429629
permissions -rw-r--r--
replaced ?? by ?;
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@6444
     8
theory ExprCompiler = Main:;
wenzelm@6444
     9
wenzelm@6746
    10
title {* Correctness of a simple expression/stack-machine compiler *};
wenzelm@6444
    11
wenzelm@6444
    12
wenzelm@6746
    13
section {* Basics *};
wenzelm@6444
    14
wenzelm@6744
    15
text {*
wenzelm@6792
    16
 First we define a type abbreviation for binary operations over some
wenzelm@6792
    17
 type @{type "'val"} of values.
wenzelm@6744
    18
*};
wenzelm@6444
    19
wenzelm@6444
    20
types
wenzelm@6444
    21
  'val binop = "'val => 'val => 'val";
wenzelm@6444
    22
wenzelm@6444
    23
wenzelm@6746
    24
section {* Machine *};
wenzelm@6444
    25
wenzelm@6744
    26
text {*
wenzelm@6792
    27
 Next we model a simple stack machine, with three instructions.
wenzelm@6744
    28
*};
wenzelm@6444
    29
wenzelm@6444
    30
datatype ('adr, 'val) instr =
wenzelm@6444
    31
  Const 'val |
wenzelm@6444
    32
  Load 'adr |
wenzelm@6444
    33
  Apply "'val binop";
wenzelm@6444
    34
wenzelm@6744
    35
text {*
wenzelm@6792
    36
 Execution of a list of stack machine instructions is
wenzelm@6792
    37
 straight-forward.
wenzelm@6744
    38
*};
wenzelm@6444
    39
wenzelm@6444
    40
consts
wenzelm@6444
    41
  exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";
wenzelm@6444
    42
wenzelm@6444
    43
primrec
wenzelm@6444
    44
  "exec [] stack env = stack"
wenzelm@6444
    45
  "exec (instr # instrs) stack env =
wenzelm@6444
    46
    (case instr of
wenzelm@6444
    47
      Const c => exec instrs (c # stack) env
wenzelm@6444
    48
    | Load x => exec instrs (env x # stack) env
wenzelm@6444
    49
    | Apply f => exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)";
wenzelm@6444
    50
wenzelm@6444
    51
constdefs
wenzelm@6444
    52
  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
wenzelm@6444
    53
  "execute instrs env == hd (exec instrs [] env)";
wenzelm@6444
    54
wenzelm@6444
    55
wenzelm@6746
    56
section {* Expressions *};
wenzelm@6444
    57
wenzelm@6744
    58
text {*
wenzelm@6792
    59
 We introduce a simple language of expressions: variables ---
wenzelm@6792
    60
 constants --- binary operations.
wenzelm@6744
    61
*};
wenzelm@6444
    62
wenzelm@6444
    63
datatype ('adr, 'val) expr =
wenzelm@6444
    64
  Variable 'adr |
wenzelm@6444
    65
  Constant 'val |
wenzelm@6444
    66
  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
wenzelm@6444
    67
wenzelm@6744
    68
text {*
wenzelm@6792
    69
 Evaluation of expressions does not do any unexpected things.
wenzelm@6744
    70
*};
wenzelm@6444
    71
wenzelm@6444
    72
consts
wenzelm@6444
    73
  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
wenzelm@6444
    74
wenzelm@6444
    75
primrec
wenzelm@6444
    76
  "eval (Variable x) env = env x"
wenzelm@6444
    77
  "eval (Constant c) env = c"
wenzelm@6444
    78
  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
wenzelm@6444
    79
wenzelm@6444
    80
wenzelm@6746
    81
section {* Compiler *};
wenzelm@6444
    82
wenzelm@6744
    83
text {*
wenzelm@6792
    84
 So we are ready to define the compilation function of expressions to
wenzelm@6792
    85
 lists of stack machine instructions.
wenzelm@6744
    86
*};
wenzelm@6444
    87
wenzelm@6444
    88
consts
wenzelm@6444
    89
  comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";
wenzelm@6444
    90
wenzelm@6444
    91
primrec
wenzelm@6444
    92
  "comp (Variable x) = [Load x]"
wenzelm@6444
    93
  "comp (Constant c) = [Const c]"
wenzelm@6444
    94
  "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
wenzelm@6444
    95
wenzelm@6444
    96
wenzelm@6744
    97
text {*
wenzelm@6792
    98
 The main result of this development is the correctness theorem for
wenzelm@6792
    99
 @{term "comp"}.  We first establish some lemmas.
wenzelm@6744
   100
*};
wenzelm@6444
   101
wenzelm@6444
   102
lemma exec_append:
wenzelm@7480
   103
  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs");
wenzelm@7480
   104
proof (induct ?P xs type: list);
wenzelm@7480
   105
  show "?P []"; by simp;
wenzelm@6444
   106
wenzelm@6444
   107
  fix x xs;
wenzelm@7480
   108
  assume "?P xs";
wenzelm@7480
   109
  show "?P (x # xs)" (is "?Q x");
wenzelm@7480
   110
  proof (induct ?Q x type: instr);
wenzelm@7480
   111
    fix val; show "?Q (Const val)"; by force;
wenzelm@6938
   112
  next;
wenzelm@7480
   113
    fix adr; show "?Q (Load adr)"; by force;
wenzelm@6938
   114
  next;
wenzelm@7480
   115
    fix fun; show "?Q (Apply fun)"; by force;
wenzelm@6444
   116
  qed;
wenzelm@6444
   117
qed;
wenzelm@6444
   118
wenzelm@6444
   119
lemma exec_comp:
wenzelm@7480
   120
  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
wenzelm@7480
   121
proof (induct ?P e type: expr);
wenzelm@7480
   122
  fix adr; show "?P (Variable adr)"; by force;
wenzelm@6938
   123
next;
wenzelm@7480
   124
  fix val; show "?P (Constant val)"; by force;
wenzelm@6938
   125
next;
wenzelm@7480
   126
  fix fun e1 e2; assume "?P e1" "?P e2"; show "?P (Binop fun e1 e2)";
wenzelm@7253
   127
    by (force simp add: exec_append);
wenzelm@6444
   128
qed;
wenzelm@6444
   129
wenzelm@6444
   130
wenzelm@6746
   131
text {* Main theorem ahead. *};
wenzelm@6444
   132
wenzelm@6444
   133
theorem correctness: "execute (comp e) env = eval e env";
wenzelm@6444
   134
  by (simp add: execute_def exec_comp);
wenzelm@6444
   135
wenzelm@6444
   136
wenzelm@6444
   137
end;