src/HOL/Isar_examples/ExprCompiler.thy

--- a/src/HOL/Isar_examples/ExprCompiler.thy	Tue Oct 05 21:20:28 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Wed Oct 06 00:31:40 1999 +0200
@@ -5,23 +5,22 @@
 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.
@@ -53,7 +52,7 @@
   "execute instrs env == hd (exec instrs [] env)";
 
 
-section {* Expressions *};
+subsection {* Expressions *};
 
 text {*
  We introduce a simple language of expressions: variables ---
@@ -78,7 +77,7 @@
   "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
@@ -95,12 +94,13 @@
 
 
 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;
 
@@ -117,7 +117,8 @@
 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;
@@ -133,5 +134,4 @@
 theorem correctness: "execute (comp e) env = eval e env";
   by (simp add: execute_def exec_comp);
 
-
 end;