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