# HG changeset patch
# User wenzelm
# Date 939909759 -7200
# Node ID c007f801cd598daa4bdc559c2d37af295db2a008
# Parent  0cb6508f190c9605ef6c9696b73995aa6231428e
improved presentation;

diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/Cantor.thy
--- a/src/HOL/Isar_examples/Cantor.thy	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy	Thu Oct 14 16:02:39 1999 +0200
@@ -5,7 +5,7 @@
 
 header {* Cantor's Theorem *};
 
-theory Cantor = Main:;verbatim {* \footnote{This is an Isar version of
+theory Cantor = Main:;text_raw {* \footnote{This is an Isar version of
  the final example of the Isabelle/HOL manual \cite{isabelle-HOL}.}
 *};
 
diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/ExprCompiler.thy
--- a/src/HOL/Isar_examples/ExprCompiler.thy	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy	Thu Oct 14 16:02:39 1999 +0200
@@ -9,17 +9,52 @@
 
 theory ExprCompiler = Main:;
 
-subsection {* Basics *};
+text {*
+ This is a (quite trivial) example of program verification.  We model
+ a compiler translating expressions to stack machine instructions, and
+ prove its correctness wrt.\ evaluation semantics.
+*};
+
+
+subsection {* Binary operations *};
 
 text {*
- First we define a type abbreviation for binary operations over some
- type of values.
+ Binary operations are just functions over some type of values.  This
+ is both for syntax and semantics, i.e.\ we use a ``shallow
+ embedding''.
 *};
 
 types
   'val binop = "'val => 'val => 'val";
 
 
+subsection {* Expressions *};
+
+text {*
+ The language of expressions is defined as an inductive type,
+ consisting of variables, constants, and binary operations on
+ expressions.
+*};
+
+datatype ('adr, 'val) expr =
+  Variable 'adr |
+  Constant 'val |
+  Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
+
+text {*
+ Evaluation (wrt.\ an environment) is defined by primitive recursion
+ over the structure of expressions.
+*};
+
+consts
+  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
+
+primrec
+  "eval (Variable x) env = env x"
+  "eval (Constant c) env = c"
+  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
+
+
 subsection {* Machine *};
 
 text {*
@@ -32,8 +67,8 @@
   Apply "'val binop";
 
 text {*
- Execution of a list of stack machine instructions is
- straight-forward.
+ Execution of a list of stack machine instructions is easily defined
+ as follows.
 *};
 
 consts
@@ -54,35 +89,10 @@
   "execute instrs env == hd (exec instrs [] env)";
 
 
-subsection {* Expressions *};
-
-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 {*
- Evaluation of expressions does not do any unexpected things.
-*};
-
-consts
-  eval :: "('adr, 'val) expr => ('adr => 'val) => 'val";
-
-primrec
-  "eval (Variable x) env = env x"
-  "eval (Constant c) env = c"
-  "eval (Binop f e1 e2) env = f (eval e1 env) (eval e2 env)";
-
-
 subsection {* Compiler *};
 
 text {*
- So we are ready to define the compilation function of expressions to
+ We are ready to define the compilation function of expressions to
  lists of stack machine instructions.
 *};
 
diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Thu Oct 14 16:02:39 1999 +0200
@@ -77,13 +77,13 @@
  Nevertheless, the ``strong'' mode of plain assumptions is quite
  important in practice to achieve robustness of proof document
  interpretation.  By forcing both the conclusion \emph{and} the
- assumptions to unify with any pending goal to be solved, goal
- selection becomes quite deterministic.  For example, typical
- ``case-analysis'' rules give rise to several goals that only differ
- in there local contexts.  With strong assumptions these may be still
- solved in any order in a predictable way, while weak ones would
- quickly lead to great confusion, eventually demanding even some
- backtracking.
+ assumptions to unify with the pending goal to be solved, goal
+ selection becomes quite deterministic.  For example, decomposition
+ with ``case-analysis'' type rules usually give rise to several goals
+ that only differ in there local contexts.  With strong assumptions
+ these may be still solved in any order in a predictable way, while
+ weak ones would quickly lead to great confusion, eventually demanding
+ even some backtracking.
 *};
 
 end;
diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/Summation.thy
--- a/src/HOL/Isar_examples/Summation.thy	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy	Thu Oct 14 16:02:39 1999 +0200
@@ -30,7 +30,7 @@
 
 subsection {* Summation laws *};
 
-verbatim {* \begin{comment} *};
+text_raw {* \begin{comment} *};
 
 (* FIXME binary arithmetic does not yet work here *)
 
@@ -46,7 +46,7 @@
 
 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
 
-verbatim {* \end{comment} *};
+text_raw {* \end{comment} *};
 
 
 theorem sum_of_naturals:
diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/document/root.tex
--- a/src/HOL/Isar_examples/document/root.tex	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/document/root.tex	Thu Oct 14 16:02:39 1999 +0200
@@ -17,6 +17,8 @@
 \end{abstract}
 
 \tableofcontents
+
+\parindent 0pt \parskip 0.5ex
 \input{session}
 
 \nocite{isabelle-isar-ref,Wenzel:1999:TPHOL}
diff -r 0cb6508f190c -r c007f801cd59 src/HOL/Isar_examples/document/style.tex
--- a/src/HOL/Isar_examples/document/style.tex	Thu Oct 14 15:14:14 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex	Thu Oct 14 16:02:39 1999 +0200
@@ -5,7 +5,6 @@
 \usepackage{comment,proof,isabelle,pdfsetup}
 
 \renewcommand{\isamarkupheader}[1]{\section{#1}}
-\parindent 0pt \parskip 0.5ex
 
 \newcommand{\name}[1]{\textsl{#1}}
 
@@ -24,7 +23,6 @@
 \newcommand{\conj}{\land}
 \newcommand{\disj}{\lor}
 
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "root"