--- a/src/HOL/Isar_examples/BasicLogic.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Fri Oct 15 16:44:37 1999 +0200
@@ -54,7 +54,7 @@
text {*
Isar provides several ways to fine-tune the reasoning, avoiding
- irrelevant detail. Several abbreviated language elements are
+ excessive detail. Several abbreviated language elements are
available, enabling the writer to express proofs in a more concise
way, even without referring to any automated proof tools yet.
@@ -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 usual in Isabelle, proof by assumption
- involves full higher-order unification.}. Thus we may skip the
- rather vacuous body of the above proof as well.
+ trivial operation, as proof by assumption involves full higher-order
+ unification.}. Thus we may skip the rather vacuous body of the above
+ proof as well.
*};
lemma "A --> A";
@@ -91,7 +91,7 @@
by rule;
text {*
- Proof by a single rule may be abbreviated as a double dot.
+ Proof by a single rule may be abbreviated as double-dot.
*};
lemma "A --> A"; ..;
@@ -103,7 +103,7 @@
*};
text {*
- Let us also reconsider $K$. It's statement is composed of iterated
+ Let us also reconsider $K$. Its statement is composed of iterated
connectives. Basic decomposition is by a single rule at a time,
which is why our first version above was by nesting two proofs.
@@ -135,10 +135,10 @@
\isacommand{proof}~($\idt{intro}$~\name{impI}~\name{allI}) to strip
implications and universal quantifiers.
- Such well-tuned iterated decomposition of certain structure is the
- prime application of $\idt{intro}$ and $\idt{elim}$. In general,
- terminal steps that solve a goal completely are typically performed
- by actual automated proof methods (such as
+ Such well-tuned iterated decomposition of certain structures is the
+ prime application of $\idt{intro}$ and $\idt{elim}$. In contrast,
+ terminal steps that solve a goal completely are usually performed by
+ actual automated proof methods (such as
\isacommand{by}~$\idt{blast}$).
*};
@@ -206,8 +206,9 @@
qed;
text {*
- Subsequently, only the outermost decomposition step is left backward,
- all the rest is forward.
+ In the subsequent version we flatten the structure of the main body
+ by doing forward reasoning all the time. Only the outermost
+ decomposition step is left as backward.
*};
lemma "A & B --> B & A";
@@ -247,9 +248,9 @@
decomposition, and bottom-up forward composition. In practice, there
is no single best way to arrange some pieces of formal reasoning, of
course. Depending on the actual applications, the intended audience
- etc., certain aspects such as rules~/ methods vs.\ facts have to be
- emphasized in an appropriate way. This requires the proof writer to
- develop good taste, and some practice, of course.
+ etc., rules (and methods) on the one hand vs.\ facts on the other
+ hand have to be emphasized in an appropriate way. This requires the
+ proof writer to develop good taste, and some practice, of course.
*};
text {*
@@ -321,8 +322,8 @@
case.
\medskip In our example the situation is even simpler, since the two
- ``cases'' actually coincide. Consequently the proof may be rephrased
- as follows.
+ cases actually coincide. Consequently the proof may be rephrased as
+ follows.
*};
lemma "P | P --> P";
--- a/src/HOL/Isar_examples/Cantor.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Fri Oct 15 16:44:37 1999 +0200
@@ -14,16 +14,17 @@
elements. It has become a favorite basic example in pure
higher-order logic since it is so easily expressed: \[\all{f::\alpha
\To \alpha \To \idt{bool}} \ex{S::\alpha \To \idt{bool}}
- \all{x::\alpha}. f \ap x \not= S\]
+ \all{x::\alpha} f \ap x \not= S\]
Viewing types as sets, $\alpha \To \idt{bool}$ represents the
powerset of $\alpha$. This version of the theorem states that for
every function from $\alpha$ to its powerset, some subset is outside
its range. The Isabelle/Isar proofs below uses HOL's set theory,
- with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.
+ with the type $\alpha \ap \idt{set}$ and the operator
+ $\idt{range}::(\alpha \To \beta) \To \beta \ap \idt{set}$.
\bigskip We first consider a slightly awkward version of the proof,
- with the reasoning expressed quite naively.
+ with the innermost reasoning expressed quite naively.
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -58,11 +59,11 @@
change the order of assumptions introduced in the two cases of rule
\name{equalityCE}, streamlining the flow of intermediate facts and
avoiding explicit naming.\footnote{In general, neither the order of
- assumptions as introduced \isacommand{assume}, nor the order of goals
- as solved by \isacommand{show} matters. The basic logical structure
- has to be left intact, though. In particular, assumptions
- ``belonging'' to some goal have to be introduced \emph{before} its
- corresponding \isacommand{show}.}
+ assumptions as introduced by \isacommand{assume}, nor the order of
+ goals as solved by \isacommand{show} is of any significance. The
+ basic logical structure has to be left intact, though. In
+ particular, assumptions ``belonging'' to some goal have to be
+ introduced \emph{before} its corresponding \isacommand{show}.}
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -91,10 +92,10 @@
text {*
How much creativity is required? As it happens, Isabelle can prove
- this theorem automatically. The default context of the classical
- proof tools 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 best-first search. Depth-first search
+ 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 best-first search. Depth-first search
would diverge, but best-first search successfully navigates through
the large search space.
*};
@@ -106,8 +107,8 @@
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 system-level representations of Isabelle proofs
- back into Isar documents. Writing proof documents really is a
- creative process, after all.
+ back into Isar documents. Writing intelligible proof documents
+ really is a creative process, after all.
*};
end;
--- a/src/HOL/Isar_examples/ExprCompiler.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/ExprCompiler.thy Fri Oct 15 16:44:37 1999 +0200
@@ -10,9 +10,9 @@
theory ExprCompiler = Main:;
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.
+ This is a (rather trivial) example of program verification. We model
+ a compiler for translating expressions to stack machine instructions,
+ and prove its correctness wrt.\ some evaluation semantics.
*};
@@ -21,7 +21,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
- embedding''.
+ embedding'' here.
*};
types
@@ -42,8 +42,8 @@
Binop "'val binop" "('adr, 'val) expr" "('adr, 'val) expr";
text {*
- Evaluation (wrt.\ an environment) is defined by primitive recursion
- over the structure of expressions.
+ Evaluation (wrt.\ some environment of variable assignments) is
+ defined by primitive recursion over the structure of expressions.
*};
consts
--- a/src/HOL/Isar_examples/Group.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/Group.thy Fri Oct 15 16:44:37 1999 +0200
@@ -7,12 +7,13 @@
theory Group = Main:;
-subsection {* Groups *};
+subsection {* Groups and calculational reasoning *};
text {*
- We define an axiomatic type class of general groups over signature
- $({\times} :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha,
- \idt{inv} :: \alpha \To \alpha)$.
+ We define an axiomatic type class of groups over signature $({\times}
+ :: \alpha \To \alpha \To \alpha, \idt{one} :: \alpha, \idt{inv} ::
+ \alpha \To \alpha)$. Note that the parent class $\idt{times}$ is
+ provided by the basic HOL theory.
*};
consts
@@ -27,9 +28,7 @@
text {*
The group axioms only state the properties of left unit and inverse,
- the right versions are derivable as follows. The calculational proof
- style below closely follows typical presentations given in any basic
- course on algebra.
+ the right versions may be derived as follows.
*};
theorem group_right_inverse: "x * inv x = (one::'a::group)";
@@ -55,7 +54,7 @@
text {*
With \name{group-right-inverse} already at our disposal,
- \name{group-right-unit} is now obtained much easier as follows.
+ \name{group-right-unit} is now obtained much easier.
*};
theorem group_right_unit: "x * one = (x::'a::group)";
@@ -72,18 +71,27 @@
qed;
text {*
- \bigskip There are only two Isar language elements for calculational
- proofs: \isakeyword{also} for initial or intermediate calculational
- steps, and \isakeyword{finally} for building the 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.
+ \medskip The calculational proof style above follows typical
+ 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 low-level
+ logical parts of equational reasoning are left implicit.
- Note that ``$\dots$'' is just a special term binding that happens to
- be bound automatically to the argument of the last fact established
- by assume or any local goal. 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 happens to
+ be bound automatically to the argument\footnote{The argument of a
+ curried infix expression happens to be its right-hand 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.
+
+ There are only two separate Isar language elements for calculational
+ proofs: ``\isakeyword{also}'' for initial or intermediate
+ calculational steps, and ``\isakeyword{finally}'' for exhibiting the
+ 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.
*};
theorem "x * one = (x::'a::group)";
@@ -112,16 +120,26 @@
note calculation = trans [OF calculation this]
-- {* final calculational step: compose with transitivity rule ... *};
from calculation
- -- {* ... and pick up final result *};
+ -- {* ... and pick up the final result *};
show ?thesis; .;
qed;
+text {*
+ Note that this scheme of calculations is not restricted to plain
+ transitivity. Rules like anti-symmetry, 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 higher-order unification.
+*};
+
subsection {* Groups as monoids *};
text {*
- Monoids are usually defined like this.
+ Monoids over signature $({\times} :: \alpha \To \alpha \To \alpha,
+ \idt{one} :: \alpha)$ are defined like this.
*};
axclass monoid < times
@@ -144,4 +162,13 @@
rule group_left_unit,
rule group_right_unit);
+text {*
+ The \isacommand{instance} command actually is a version of
+ \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
+ type signature extension behind the scenes.
+*};
+
end;
--- a/src/HOL/Isar_examples/KnasterTarski.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Fri Oct 15 16:44:37 1999 +0200
@@ -13,10 +13,9 @@
subsection {* Prose version *};
text {*
- According to the book ``Introduction to Lattices and Order''
- \cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint
- theorem is as follows.\footnote{We have dualized the argument, and
- tuned the notation a little bit.}
+ According to the textbook \cite[pages 93--94]{davey-priestley}, the
+ Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
+ dualized the argument, and tuned the notation a little bit.}
\medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a
complete lattice and $f \colon L \to L$ an order-preserving map.
@@ -51,10 +50,10 @@
proof -;
{{;
fix x;
- assume mem: "x : ?H";
+ assume H: "x : ?H";
hence "?a <= x"; by (rule Inter_lower);
with mono; have "f ?a <= f x"; ..;
- also; from mem; have "... <= x"; ..;
+ also; from H; have "... <= x"; ..;
finally; have "f ?a <= x"; .;
}};
hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
@@ -77,7 +76,7 @@
changed to achieve structured top-down 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.
+ features of the Isar language, we are certainly more at ease here.
*};
theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a";
@@ -91,10 +90,10 @@
show ge: "f ?a <= ?a";
proof (rule Inter_greatest);
fix x;
- assume mem: "x : ?H";
+ assume H: "x : ?H";
hence "?a <= x"; by (rule Inter_lower);
with mono; have "f ?a <= f x"; ..;
- also; from mem; have "... <= x"; ..;
+ also; from H; have "... <= x"; ..;
finally; show "f ?a <= x"; .;
qed;
show "?a <= f ?a";
--- a/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/MultisetOrder.thy Fri Oct 15 16:44:37 1999 +0200
@@ -29,7 +29,8 @@
M0 + {#a#} = M0' + {#a'#} & N = M0' + K & ?r K a'"; by simp;
thus "?case1 | ?case2";
proof (elim exE conjE);
- fix a' M0' K; assume N: "N = M0' + K" and r: "?r K a'";
+ fix a' M0' K;
+ assume N: "N = M0' + K" and r: "?r K a'";
assume "M0 + {#a#} = M0' + {#a'#}";
hence "M0 = M0' & a = a' |
(EX K'. M0 = K' + {#a'#} & M0' = K' + {#a#})";
@@ -66,7 +67,8 @@
and acc_hyp: "ALL M. (M, M0) : ?R --> M + {#a#} : ?W";
have "M0 + {#a#} : ?W";
proof (rule accI [of "M0 + {#a#}"]);
- fix N; assume "(N, M0 + {#a#}) : ?R";
+ fix N;
+ assume "(N, M0 + {#a#}) : ?R";
hence "((EX M. (M, M0) : ?R & N = M + {#a#}) |
(EX K. (ALL b. elem K b --> (b, a) : r) & N = M0 + K))";
by (rule less_add);
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy Fri Oct 15 16:44:37 1999 +0200
@@ -54,7 +54,7 @@
qed;
-subsection {* Basic properties of below *};
+subsection {* Basic properties of ``below'' *};
constdefs
below :: "nat => nat set"
@@ -77,7 +77,7 @@
lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
-subsection {* Basic properties of evnodd *};
+subsection {* Basic properties of ``evnodd'' *};
constdefs
evnodd :: "(nat * nat) set => nat => (nat * nat) set"
@@ -223,7 +223,7 @@
thus "?thesis b";
proof (elim exE);
have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
- also; fix i j; assume e: "?e a b = {(i, j)}";
+ also; fix i j; assume "?e a b = {(i, j)}";
also; have "... Un ?e t b = insert (i, j) (?e t b)"; by simp;
also; have "card ... = Suc (card (?e t b))";
proof (rule card_insert_disjoint);
@@ -292,7 +292,7 @@
also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
also; from t''; have "card ... = card (?e ?t'' 0)";
by (rule tiling_domino_01 [RS sym]);
- finally; show False; ..;
+ finally; have "... < ..."; .; thus False; ..;
qed;
qed;
--- a/src/HOL/Isar_examples/Peirce.thy Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Fri Oct 15 16:44:37 1999 +0200
@@ -13,11 +13,10 @@
certainly involve some form of classical contradiction.
The first proof is again a well-balanced combination of plain
- backward and forward reasoning. The actual classical reasoning step
- is where the negated goal is introduced as additional assumption.
- This eventually leads to a contradiction.\footnote{The rule involved
- here is negation elimination; it holds in intuitionistic logic as
- well.}
+ backward and forward reasoning. The actual classical step is where
+ the negated goal may be introduced as additional assumption. This
+ eventually leads to a contradiction.\footnote{The rule involved there
+ is negation elimination; it holds in intuitionistic logic as well.}
*};
theorem "((A --> B) --> A) --> A";
@@ -36,12 +35,13 @@
qed;
text {*
- The subsequent version rearranges the reasoning by means of ``weak
- assumptions'' (as introduced by \isacommand{presume}). Before
+ In the subsequent version the reasoning is rearranged by means of
+ ``weak assumptions'' (as introduced by \isacommand{presume}). Before
assuming the negated goal $\neg A$, its intended consequence $A \impl
B$ is put into place in order to solve the main problem.
Nevertheless, we do not get anything for free, but have to establish
- $A \impl B$ later on. The overall effect is that of a \emph{cut}.
+ $A \impl B$ later on. The overall effect is that of a logical
+ \emph{cut}.
Technically speaking, whenever some goal is solved by
\isacommand{show} in the context of weak assumptions then the latter
@@ -58,11 +58,11 @@
presume "A --> B";
with aba; show A; ..;
next;
- assume not_a: "~ A";
+ assume "~ A";
show "A --> B";
proof;
assume A;
- with not_a; show B; ..;
+ thus B; by contradiction;
qed;
qed;
qed;
@@ -70,9 +70,9 @@
text {*
Note that the goals stemming from weak assumptions may be even left
until qed time, where they get eventually solved ``by assumption'' as
- well. In that case there is really no big difference between the two
- kinds of assumptions, apart from the order of reducing the individual
- parts of the proof configuration.
+ well. In that case there is really no fundamental difference between
+ the two kinds of assumptions, apart from the order of reducing the
+ individual parts of the proof configuration.
Nevertheless, the ``strong'' mode of plain assumptions is quite
important in practice to achieve robustness of proof document
--- a/src/HOL/Isar_examples/document/root.tex Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/document/root.tex Fri Oct 15 16:44:37 1999 +0200
@@ -10,10 +10,10 @@
\maketitle
\begin{abstract}
- Isar offers a high-level proof (and theory) language interface to Isabelle.
- We give various examples of Isabelle/Isar proof developments, ranging from
- simple demonstrations of certain language features to more advanced
- applications.
+ Isar offers a high-level proof (and theory) language for Isabelle.
+ We give various examples of Isabelle/Isar proof developments,
+ ranging from simple demonstrations of certain language features to
+ more advanced applications.
\end{abstract}
\tableofcontents
--- a/src/HOL/Isar_examples/document/style.tex Fri Oct 15 16:43:05 1999 +0200
+++ b/src/HOL/Isar_examples/document/style.tex Fri Oct 15 16:44:37 1999 +0200
@@ -9,7 +9,7 @@
\newcommand{\name}[1]{\textsl{#1}}
\newcommand{\idt}[1]{{\mathord{\mathit{#1}}}}
-\newcommand{\var}[1]{{?\!#1}}
+\newcommand{\var}[1]{{?\!\idt{#1}}}
\DeclareMathSymbol{\dshsym}{\mathalpha}{letters}{"2D}
\newcommand{\dsh}{\dshsym}