src/HOL/Isar_examples/ExprCompiler.thy

   "Markus Wenzel";
 
 
 section "Basics";
 
-text {|
+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 {|
+text {*
   Next we model a simple stack machine, with three instructions.
-|};
+*};
 
 datatype ('adr, 'val) instr =
   Const 'val |
   Load 'adr |
   Apply "'val binop";
 
-text {|
+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

   "execute instrs env == hd (exec instrs [] env)";
 
 
 section "Expressions";
 
-text {|
+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 {|
+text {*
   Evaluation of expressions does not do any unexpected things.
-|};
+*};
 
 consts
   eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
 
 primrec

   "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
 
 
 section "Compiler";
 
-text {|
+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 {|
+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);