--- 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}.}
*};
--- 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.
*};
--- 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;
--- 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:
--- 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}
--- 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"