# HG changeset patch
# User wenzelm
# Date 941307648 7200
# Node ID d534b897ce398cd9eace7f008033e366fb51453d
# Parent 5120a2a15d06b90359aa9a1c0cf1f07e2d7891de
improved presentation;
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/BasicLogic.thy
 a/src/HOL/Isar_examples/BasicLogic.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Sat Oct 30 20:20:48 1999 +0200
@@ 5,7 +5,7 @@
Basic propositional and quantifier reasoning.
*)
header {* Basic reasoning *};
+header {* Basic logical reasoning *};
theory BasicLogic = Main:;
@@ 70,9 +70,9 @@
text {*
In fact, concluding any (sub)proof already involves solving any
remaining goals by assumption\footnote{This is not a completely
 trivial operation, as proof by assumption involves full higherorder
 unification.}. Thus we may skip the rather vacuous body of the above
 proof as well.
+ trivial operation, as proof by assumption may involve full
+ higherorder unification.}. Thus we may skip the rather vacuous body
+ of the above proof as well.
*};
lemma "A > A";
@@ 99,7 +99,7 @@
text {*
Thus we have arrived at an adequate representation of the proof of a
tautology that holds by a single standard rule.\footnote{Apparently,
 the rule is implication introduction.}
+ the rule here is implication introduction.}
*};
text {*
@@ 129,7 +129,7 @@
Just like $\idt{rule}$, the $\idt{intro}$ and $\idt{elim}$ proof
methods pick standard structural rules, in case no explicit arguments
are given. While implicit rules are usually just fine for single
 rule application, this may go too far in iteration. Thus in
+ rule application, this may go too far with iteration. Thus in
practice, $\idt{intro}$ and $\idt{elim}$ would be typically
restricted to certain structures by giving a few rules only, e.g.\
\isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip
@@ 168,11 +168,12 @@
text {*
Above, the $\idt{conjunct}_{1/2}$ projection rules had to be named
 explicitly, since the goals did not provide any structural clue.
 This may be avoided using \isacommand{from} to focus on $\idt{prems}$
 (i.e.\ the $A \conj B$ assumption) as the current facts, enabling the
 use of doubledot proofs. Note that \isacommand{from} already
 does forwardchaining, involving the \name{conjE} rule.
+ explicitly, since the goals $B$ and $A$ did not provide any
+ structural clue. This may be avoided using \isacommand{from} to
+ focus on $\idt{prems}$ (i.e.\ the $A \conj B$ assumption) as the
+ current facts, enabling the use of doubledot proofs. Note that
+ \isacommand{from} already does forwardchaining, involving the
+ \name{conjE} rule here.
*};
lemma "A & B > B & A";
@@ 222,7 +223,7 @@
text {*
We can still push forward reasoning a bit further, even at the risk
of getting ridiculous. Note that we force the initial proof step to
 do nothing, by referring to the ``'' proof method.
+ do nothing here, by referring to the ``'' proof method.
*};
lemma "A & B > B & A";
@@ 245,7 +246,7 @@
The general lesson learned here is that good proof style would
achieve just the \emph{right} balance of topdown backward
 decomposition, and bottomup forward composition. In practice, there
+ decomposition, and bottomup forward composition. In general, there
is no single best way to arrange some pieces of formal reasoning, of
course. Depending on the actual applications, the intended audience
etc., rules (and methods) on the one hand vs.\ facts on the other
@@ 278,7 +279,7 @@
text {*
We rephrase some of the basic reasoning examples of
 \cite{isabelleintro} (using HOL rather than FOL).
+ \cite{isabelleintro}, using HOL rather than FOL.
*};
subsubsection {* A propositional proof *};
@@ 315,8 +316,8 @@
In order to avoid too much explicit parentheses, the Isar system
implicitly opens an additional block for any new goal, the
\isacommand{next} statement then closes one block level, opening a
 new one. The resulting behavior is what one might expect from
 separating cases, only that it is more flexible. E.g. an induction
+ new one. The resulting behavior is what one would expect from
+ separating cases, only that it is more flexible. E.g.\ an induction
base case (which does not introduce local assumptions) would
\emph{not} require \isacommand{next} to separate the subsequent step
case.
@@ 381,8 +382,8 @@
qed;
text {*
 While explicit rule instantiation may occasionally help to improve
 the readability of certain aspects of reasoning, it is usually quite
+ While explicit rule instantiation may occasionally improve
+ readability of certain aspects of reasoning, it is usually quite
redundant. Above, the basic proof outline gives already enough
structural clues for the system to infer both the rules and their
instances (by higherorder unification). Thus we may as well prune
@@ 404,17 +405,18 @@
subsubsection {* Deriving rules in Isabelle *};
text {*
 We derive the conjunction elimination rule from the projections. The
 proof is quite straightforward, since Isabelle/Isar supports
 nonatomic goals and assumptions fully transparently.
+ We derive the conjunction elimination rule from the corresponding
+ projections. The proof is quite straightforward, since
+ Isabelle/Isar supports nonatomic goals and assumptions fully
+ transparently.
*};
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
proof ;
assume "A & B";
 assume ab_c: "A ==> B ==> C";
+ assume r: "A ==> B ==> C";
show C;
 proof (rule ab_c);
+ proof (rule r);
show A; by (rule conjunct1);
show B; by (rule conjunct2);
qed;
@@ 425,7 +427,7 @@
different way. The tactic script as given in \cite{isabelleintro}
for the same example of \name{conjE} depends on the primitive
\texttt{goal} command to decompose the rule into premises and
 conclusion. The proper result would then emerge by discharging of
+ conclusion. The actual result would then emerge by discharging of
the context at \texttt{qed} time.
*};
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/Cantor.thy
 a/src/HOL/Isar_examples/Cantor.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Sat Oct 30 20:20:48 1999 +0200
@@ 30,7 +30,7 @@
with the innermost reasoning expressed quite naively.
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
+theorem "EX S. S ~: range (f :: 'a => 'a set)";
proof;
let ?S = "{x. x ~: f x}";
show "?S ~: range f";
@@ 69,7 +69,7 @@
introduced \emph{before} its corresponding \isacommand{show}.}
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
+theorem "EX S. S ~: range (f :: 'a => 'a set)";
proof;
let ?S = "{x. x ~: f x}";
show "?S ~: range f";
@@ 95,22 +95,22 @@
text {*
How much creativity is required? As it happens, Isabelle can prove
 this theorem automatically. The default context of the Isabelle's
 classical prover contains rules for most of the constructs of HOL's
 set theory. We must augment it with \name{equalityCE} to break up
 set equalities, and then apply bestfirst search. Depthfirst search
 would diverge, but bestfirst search successfully navigates through
 the large search space.
+ this theorem automatically. The context of Isabelle's classical
+ prover contains rules for most of the constructs of HOL's set theory.
+ We must augment it with \name{equalityCE} to break up set equalities,
+ and then apply bestfirst search. Depthfirst search would diverge,
+ but bestfirst search successfully navigates through the large search
+ space.
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
+theorem "EX S. S ~: range (f :: 'a => 'a set)";
by (best elim: equalityCE);
text {*
While this establishes the same theorem internally, we do not get any
idea of how the proof actually works. There is currently no way to
transform internal systemlevel representations of Isabelle proofs
 back into Isar documents. Writing intelligible proof documents
+ back into Isar text. Writing intelligible proof documents
really is a creative process, after all.
*};
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/ExprCompiler.thy
 a/src/HOL/Isar_examples/ExprCompiler.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Sat Oct 30 20:20:48 1999 +0200
@@ 20,7 +20,7 @@
text {*
Binary operations are just functions over some type of values. This
 is both for syntax and semantics, i.e.\ we use a ``shallow
+ is both for abstract syntax and semantics, i.e.\ we use a ``shallow
embedding'' here.
*};
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/Group.thy
 a/src/HOL/Isar_examples/Group.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Sat Oct 30 20:20:48 1999 +0200
@@ 53,8 +53,9 @@
qed;
text {*
 With \name{grouprightinverse} already at our disposal,
 \name{grouprightunit} is now obtained much easier.
+ With \name{grouprightinverse} already available,
+ \name{grouprightunit}\label{thm:grouprightunit} is now
+ established much easier.
*};
theorem group_right_unit: "x * one = (x::'a::group)";
@@ 75,14 +76,14 @@
presentations given in any introductory course on algebra. The basic
technique is to form a transitive chain of equations, which in turn
are established by simplifying with appropriate rules. The lowlevel
 logical parts of equational reasoning are left implicit.
+ logical details of equational reasoning are left implicit.
 Note that ``$\dots$'' is just a special term variable that happens to
 be bound automatically to the argument\footnote{The argument of a
 curried infix expression happens to be its righthand side.} of the
 last fact achieved by any local assumption or proven statement. In
 contrast to $\var{thesis}$, the ``$\dots$'' variable is bound
 \emph{after} the proof is finished.
+ Note that ``$\dots$'' is just a special term variable that is bound
+ automatically to the argument\footnote{The argument of a curried
+ infix expression happens to be its righthand side.} of the last fact
+ achieved by any local assumption or proven statement. In contrast to
+ $\var{thesis}$, the ``$\dots$'' variable is bound \emph{after} the
+ proof is finished, though.
There are only two separate Isar language elements for calculational
proofs: ``\isakeyword{also}'' for initial or intermediate
@@ 90,8 +91,8 @@
result of a calculation. These constructs are not hardwired into
Isabelle/Isar, but defined on top of the basic Isar/VM interpreter.
Expanding the \isakeyword{also} and \isakeyword{finally} derived
 language elements, calculations may be simulated as demonstrated
 below.
+ language elements, calculations may be simulated by hand as
+ demonstrated below.
*};
theorem "x * one = (x::'a::group)";
@@ 128,10 +129,10 @@
text {*
Note that this scheme of calculations is not restricted to plain
transitivity. Rules like antisymmetry, or even forward and backward
 substitution work as well. For the actual \isacommand{also} and
 \isacommand{finally} commands, Isabelle/Isar maintains separate
 context information of ``transitivity'' rules. Rule selection takes
 place automatically by higherorder unification.
+ substitution work as well. For the actual implementation of
+ \isacommand{also} and \isacommand{finally}, Isabelle/Isar maintains
+ separate context information of ``transitivity'' rules. Rule
+ selection takes place automatically by higherorder unification.
*};
@@ 150,10 +151,11 @@
text {*
Groups are \emph{not} yet monoids directly from the definition. For
monoids, \name{rightunit} had to be included as an axiom, but for
 groups both \name{rightunit} and \name{rightinverse} are
 derivable from the other axioms. With \name{grouprightunit}
 derived as a theorem of group theory (see above), we may still
 instantiate $\idt{group} \subset \idt{monoid}$ properly as follows.
+ groups both \name{rightunit} and \name{rightinverse} are derivable
+ from the other axioms. With \name{grouprightunit} derived as a
+ theorem of group theory (see page~\pageref{thm:grouprightunit}), we
+ may still instantiate $\idt{group} \subset \idt{monoid}$ properly as
+ follows.
*};
instance group < monoid;
@@ 167,7 +169,7 @@
\isacommand{theorem}, setting up a goal that reflects the intended
class relation (or type constructor arity). Thus any Isar proof
language element may be involved to establish this statement. When
 concluding the proof, the result is transformed into the original
+ concluding the proof, the result is transformed into the intended
type signature extension behind the scenes.
*};
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/KnasterTarski.thy
 a/src/HOL/Isar_examples/KnasterTarski.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Sat Oct 30 20:20:48 1999 +0200
@@ 37,7 +37,8 @@
The Isar proof below closely follows the original presentation.
Virtually all of the prose narration has been rephrased in terms of
formal Isar language elements. Just as many textbookstyle proofs,
 there is a strong bias towards forward reasoning.
+ there is a strong bias towards forward proof, and several bends
+ in the course of reasoning.
*};
theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
@@ 72,11 +73,11 @@
explicit block structure and weak assumptions. Thus we have mimicked
the particular way of reasoning of the original text.
 In the subsequent version of the proof the order of reasoning is
 changed to achieve structured topdown decomposition of the problem
 at the outer level, while the small inner steps of reasoning or done
 in a forward manner. Note that this requires only the most basic
 features of the Isar language, we are certainly more at ease here.
+ In the subsequent version the order of reasoning is changed to
+ achieve structured topdown decomposition of the problem at the outer
+ level, while only the inner steps of reasoning are done in a forward
+ manner. We are certainly more at ease here, requiring only the most
+ basic features of the Isar language.
*};
theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a";
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/MultisetOrder.thy
 a/src/HOL/Isar_examples/MultisetOrder.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Sat Oct 30 20:20:48 1999 +0200
@@ 10,7 +10,7 @@
theory MultisetOrder = Multiset:;
text_raw {*
 \footnote{Original tactic script by Tobias Nipkow (see also
+ \footnote{Original tactic script by Tobias Nipkow (see
\url{http://isabelle.in.tum.de/library/HOL/Induct/Multiset.html}),
based on a penandpaper proof due to Wilfried Buchholz.}
*};
@@ 22,8 +22,8 @@
(EX K. (ALL b. elem K b > (b, a) : r) & N = M0 + K)"
(concl is "?case1 (mult1 r)  ?case2");
proof (unfold mult1_def);
 let ?r = "%K a. ALL b. elem K b > (b, a) : r";
 let ?R = "%N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
+ let ?r = "\K a. ALL b. elem K b > (b, a) : r";
+ let ?R = "\N M. EX a M0 K. M = M0 + {#a#} & N = M0 + K & ?r K a";
let ?case1 = "?case1 {(N, M). ?R N M}";
assume "(N, M0 + {#a#}) : {(N, M). ?R N M}";
@@ 61,7 +61,6 @@
proof;
let ?R = "mult1 r";
let ?W = "acc ?R";

{{;
fix M M0 a;
assume M0: "M0 : ?W"
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/Peirce.thy
 a/src/HOL/Isar_examples/Peirce.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Sat Oct 30 20:20:48 1999 +0200
@@ 75,15 +75,15 @@
individual parts of the proof configuration.
Nevertheless, the ``strong'' mode of plain assumptions is quite
 important in practice to achieve robustness of proof document
+ important in practice to achieve robustness of proof text
interpretation. By forcing both the conclusion \emph{and} the
assumptions to unify with the pending goal to be solved, goal
selection becomes quite deterministic. For example, decomposition
 with ``caseanalysis'' 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.
+ with rules of the ``caseanalysis'' type usually gives 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 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/Summation.thy
 a/src/HOL/Isar_examples/Summation.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/Summation.thy Sat Oct 30 20:20:48 1999 +0200
@@ 16,7 +16,7 @@
text {*
Subsequently, we prove some summation laws of natural numbers
 (including odds, squares and cubes). These examples demonstrate how
+ (including odds, squares, and cubes). These examples demonstrate how
plain natural deduction (including induction) may be combined with
calculational proof.
*};
@@ 26,25 +26,25 @@
text {*
The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To
 \idt{nat} \To \idt{nat}$ formalizes summation from $0$ up to $k$
 (excluding the bound).
+ \idt{nat} \To \idt{nat}$ formalizes summation of natural numbers
+ indexed from $0$ up to $k$ (excluding the bound):
\[
\sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k
\]
*};
consts
 sum :: "[nat => nat, nat] => nat";
+ sum :: "[nat => nat, nat] => nat";
primrec
"sum f 0 = 0"
"sum f (Suc n) = f n + sum f n";
syntax
 "_SUM" :: "idt => nat => nat => nat"
+ "_SUM" :: "[idt, nat, nat] => nat"
("SUM _ < _. _" [0, 0, 10] 10);
translations
 "SUM i < k. b" == "sum (%i. b) k";
+ "SUM i < k. b" == "sum (\i. b) k";
subsection {* Summation laws *};
@@ 69,8 +69,8 @@
text {*
The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
 1)/2$. In order to avoid formal reasoning about division, we just
 show $2 \times \Sigma_{i < n} i = n \times (n + 1)$.
+ 1)/2$. Avoiding formal reasoning about division we prove this
+ equation multiplied by $2$.
*};
theorem sum_of_naturals:
@@ 90,23 +90,22 @@
The above proof is a typical instance of mathematical induction. The
main statement is viewed as some $\var{P} \ap n$ that is split by the
induction method into base case $\var{P} \ap 0$, and step case
 $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for any $n$.
+ $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
The step case is established by a short calculation in forward
manner. Starting from the lefthand side $\var{S} \ap (n + 1)$ of
 the thesis, the final result is achieved by basic transformations
 involving arithmetic reasoning (using the Simplifier). The main
 point is where the induction hypothesis $\var{S} \ap n = n \times (n
 + 1)$ is introduced in order to replace a certain subterm. So the
+ the thesis, the final result is achieved by transformations involving
+ basic arithmetic reasoning (using the Simplifier). The main point is
+ where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
+ introduced in order to replace a certain subterm. So the
``transitivity'' rule involved here is actual \emph{substitution}.
Also note how the occurrence of ``\dots'' in the subsequent step
 documents the position where the righthand side of the hypotheses
+ documents the position where the righthand side of the hypothesis
got filled in.
\medskip A further notable point here is integration of calculations
 with plain natural deduction. This works works quite well in Isar
 for two reasons.

+ with plain natural deduction. This works so well in Isar for two
+ reasons.
\begin{enumerate}
\item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
@@ 116,19 +115,18 @@
\item There are two \emph{separate} primitives for building natural
deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
 Thus it is possible to start reasoning with new ``arbitrary, but
 fixed'' elements before bringing in the actual assumptions.
 Occasionally, natural deduction is formalized with basic context
 elements of the form $x:A$; this would rule out mixing with
 calculations as done here.
+ Thus it is possible to start reasoning with some new ``arbitrary, but
+ fixed'' elements before bringing in the actual assumption. In
+ contrast, natural deduction is occasionally formalized with basic
+ context elements of the form $x:A$ instead.
\end{enumerate}
*};
text {*
 \medskip We derive further summation laws for odds, squares, cubes as
 follows. The basic technique of induction plus calculation is the
 same.
+ \medskip We derive further summation laws for odds, squares, and
+ cubes as follows. The basic technique of induction plus calculation
+ is the same as before.
*};
theorem sum_of_odds:
@@ 175,20 +173,20 @@
text {*
Comparing these examples with the tactic script version
\url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
 an important difference how of induction vs.\ simplification is
+ an important difference of how induction vs.\ simplification is
applied. While \cite[\S10]{isabelleref} advises for these examples
that ``induction should not be applied until the goal is in the
simplest form'' this would be a very bad idea in our setting.
Simplification normalizes all arithmetic expressions involved,
 producing huge intermediate goals. Applying induction afterwards,
 the Isar document would then have to reflect the emerging
 configuration by appropriate the subproofs. This would result in
 badly structured, lowlevel technical reasoning, without any good
 idea of the actual point.
+ producing huge intermediate goals. With applying induction
+ afterwards, the Isar proof text would have to reflect the emerging
+ configuration by appropriate subproofs. This would result in badly
+ structured, lowlevel technical reasoning, without any good idea of
+ the actual point.
\medskip As a general rule of good proof style, automatic methods
 such as $\idt{simp}$ or $\idt{auto}$ should normally never used as
+ such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
initial proof methods, but only as terminal ones, solving certain
goals completely.
*};
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/W_correct.thy
 a/src/HOL/Isar_examples/W_correct.thy Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy Sat Oct 30 20:20:48 1999 +0200
@@ 39,7 +39,7 @@
AppI: "[ a  e1 :: t2 > t1; a  e2 :: t2 ]
==> a  App e1 e2 :: t1";
text {* Type assigment is close wrt.\ substitution. *};
+text {* Type assigment is closed wrt.\ substitution. *};
lemma has_type_subst_closed: "a  e :: t ==> $s a  e :: $s t";
proof ;
@@ 79,10 +79,10 @@
primrec
"W (Var i) a n =
 (if i < length a then Ok(id_subst, a ! i, n) else Fail)"
+ (if i < length a then Ok (id_subst, a ! i, n) else Fail)"
"W (Abs e) a n =
((s, t, m) := W e (TVar n # a) (Suc n);
 Ok(s, (s n) > t, m))"
+ Ok (s, (s n) > t, m))"
"W (App e1 e2) a n =
((s1, t1, m1) := W e1 a n;
(s2, t2, m2) := W e2 ($s1 a) m1;
@@ 92,9 +92,13 @@
subsection {* Correctness theorem *};
+text_raw {* \begin{comment} *};
+
(* FIXME proper split att/mod *)
ML_setup {* Addsplits [split_bind]; *};
+text_raw {* \end{comment} *};
+
theorem W_correct: "W e a n = Ok (s, t, m) ==> $ s a  e :: t";
proof ;
assume W_ok: "W e a n = Ok (s, t, m)";
diff r 5120a2a15d06 r d534b897ce39 src/HOL/Isar_examples/document/style.tex
 a/src/HOL/Isar_examples/document/style.tex Sat Oct 30 20:13:16 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex Sat Oct 30 20:20:48 1999 +0200
@@ 2,7 +2,7 @@
%% $Id$
\documentclass[11pt,a4paper]{article}
\usepackage{comment,proof,isabelle,pdfsetup}
+\usepackage{comment,proof,isabelle,isabellesym,pdfsetup}
\renewcommand{\isamarkupheader}[1]{\section{#1}}