src/HOL/Isar_examples/ExprCompiler.thy

 
 
 section {* Basics *};
 
 text {*
-  First we define a type abbreviation for binary operations over some
-  type @{type "'val"} of values.
+ 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.
+ 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.
+ Execution of a list of stack machine instructions is
+ straight-forward.
 *};
 
 consts
   exec :: "(('adr, 'val) instr) list => 'val list => ('adr => 'val) => 'val list";
 

 
 
 section {* Expressions *};
 
 text {*
-  We introduce a simple language of expressions: variables ---
-  constants --- binary operations.
+ 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.
+ Evaluation of expressions does not do any unexpected things.
 *};
 
 consts
   eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
 

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

   "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.
+ The main result of this development 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);