src/HOL/Isar_examples/ExprCompiler.thy

     Author:     Markus Wenzel, TU Muenchen
 
 Correctness of a simple expression/stack-machine compiler.
 *)
 
+header {* Correctness of a simple expression compiler *};
+
 theory ExprCompiler = Main:;
 
-chapter {* Correctness of a simple expression/stack-machine compiler *};
-
-
-section {* Basics *};
+subsection {* Basics *};
 
 text {*
  First we define a type abbreviation for binary operations over some
- type @{type "'val"} of values.
+ type of values.
 *};
 
 types
   'val binop = "'val => 'val => 'val";
 
 
-section {* Machine *};
+subsection {* Machine *};
 
 text {*
  Next we model a simple stack machine, with three instructions.
 *};
 

 constdefs
   execute :: "(('adr, 'val) instr) list => ('adr => 'val) => 'val"
   "execute instrs env == hd (exec instrs [] env)";
 
 
-section {* Expressions *};
+subsection {* Expressions *};
 
 text {*
  We introduce a simple language of expressions: variables ---
  constants --- binary operations.
 *};

   "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 *};
+subsection {* Compiler *};
 
 text {*
  So we are ready to define the compilation function of expressions to
  lists of stack machine instructions.
 *};

   "comp (Constant c) = [Const c]"
   "comp (Binop f e1 e2) = comp e2 @ comp e1 @ [Apply f]";
 
 
 text {*
- The main result of this development is the correctness theorem for
- @{term "comp"}.  We first establish some lemmas.
+  The main result of this development is the correctness theorem for
+  $\idt{comp}$.  We first establish some lemmas about $\idt{exec}$.
 *};
 
 lemma exec_append:
-  "ALL stack. exec (xs @ ys) stack env = exec ys (exec xs stack env) env" (is "?P xs");
+  "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";

     fix fun; show "?Q (Apply fun)"; by (simp!);
   qed;
 qed;
 
 lemma exec_comp:
-  "ALL stack. exec (comp e) stack env = eval e env # stack" (is "?P e");
+  "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 (simp!);
 next;
   fix val; show "?P (Constant val)"; by (simp!);
 next;

 text {* Main theorem ahead. *};
 
 theorem correctness: "execute (comp e) env = eval e env";
   by (simp add: execute_def exec_comp);
 
-
 end;