src/HOL/Isar_examples/ExprCompiler.thy

 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";
+title {* Correctness of a simple expression/stack-machine compiler *};
 
 
-section "Basics";
+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";
+section {* 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";
+section {* 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";
+section {* Compiler *};
 
 text {*
   So we are ready to define the compilation function of expressions to
   lists of stack machine instructions.
 *};

 text {*
   The main result of this developement is the correctness theorem for
   @{term "comp"}.  We first establish some lemmas.
 *};
 
-
 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;
 

     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;

   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.";
+text {* Main theorem ahead. *};
 
 theorem correctness: "execute (comp e) env = eval e env";
   by (simp add: execute_def exec_comp);