src/HOL/Isar_examples/ExprCompiler.thy

tuned antiquotations;

(*  Title:      HOL/Isar_examples/ExprCompiler.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Correctness of a simple expression/stack-machine compiler.
*)

theory ExprCompiler = Main:;

title
  "Correctness of a simple expression/stack-machine compiler --- an Isabelle/Isar demonstration"
  "Markus Wenzel";


section "Basics";

text {|
  First we define a type abbreviation for binary operations over some
  type @{type "'val"} of values.
|};

types
  'val binop = "'val => 'val => 'val";


section "Machine";

text {|
  Next we model a simple stack machine, with three instructions.
|};

datatype ('adr, 'val) instr =
  Const 'val |
  Load 'adr |
  Apply "'val binop";

text {|
  Execution of a list of stack machine instructions is
  straight-forward.
|};

consts
  exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";

primrec
  "exec [] stack env = stack"
  "exec (instr # instrs) stack env =
    (case instr of
      Const c => exec instrs (c # stack) env
    | Load x => exec instrs (env x # stack) env
    | Apply f => exec instrs (f (hd stack) (hd (tl stack)) # (tl (tl stack))) env)";

constdefs
  execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
  "execute instrs env == hd (exec instrs [] env)";


section "Expressions";

text {|
  We introduce a simple language of expressions: variables ---
  constants --- binary operations.
|};

datatype ('adr, 'val) expr =
  Variable 'adr |
  Constant 'val |
  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";

text {|
  Evaluation of expressions does not do any unexpected things.
|};

consts
  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";

primrec
  "eval (Variable x) env = env x"
  "eval (Constant c) env = c"
  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";


section "Compiler";

text {|
  So we are ready to define the compilation function of expressions to
  lists of stack machine instructions.
|};

consts
  comp :: "('adr, 'val) expr => (('adr, 'val) instr) list";

primrec
  "comp (Variable x) = [Load x]"
  "comp (Constant c) = [Const c]"
  "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";


text {|
  The main result of this developement is the correctness theorem for
  @{term "comp"}.  We first establish some lemmas.
|};

ML "reset HOL_quantifiers";

lemma exec_append:
  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "??P xs");
proof (induct ??P xs type: list);
  show "??P []"; by simp;

  fix x xs;
  assume "??P xs";
  show "??P (x # xs)" (is "??Q x");
  proof (induct ??Q x type: instr);
    fix val; show "??Q (Const val)"; by brute_force;
    next;
    fix adr; show "??Q (Load adr)"; by brute_force;
    next;
    fix fun; show "??Q (Apply fun)"; by brute_force;
  qed;
qed;


lemma exec_comp:
  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "??P e");
proof (induct ??P e type: expr);

  fix adr; show "??P (Variable adr)"; by brute_force;
  next;
  fix val; show "??P (Constant val)"; by brute_force;
  next;
  fix fun e1 e2; assume "??P e1" "??P e2"; show "??P (Binop fun e1 e2)";
    by (brute_force simp add: exec_append);
qed;


text "Main theorem ahead.";

theorem correctness: "execute (comp e) env = eval e env";
  by (simp add: execute_def exec_comp);


end;