--- a/src/HOL/Isar_examples/BasicLogic.thy Wed Oct 13 19:44:33 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Thu Oct 14 01:07:24 1999 +0200
@@ -69,8 +69,10 @@
text {*
In fact, concluding any (sub-)proof already involves solving any
- remaining goals by assumption. Thus we may skip the rather vacuous
- body of the above proof as well.
+ 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.
*};
lemma "A --> A";
@@ -96,8 +98,8 @@
text {*
Thus we have arrived at an adequate representation of the proof of a
- tautology that holds by a single standard rule.\footnote{Here the
- rule is implication introduction.}
+ tautology that holds by a single standard rule.\footnote{Apparently,
+ the rule is implication introduction.}
*};
text {*
@@ -130,13 +132,13 @@
rule application, this may go too far in iteration. Thus in
practice, $\idt{intro}$ and $\idt{elim}$ would be typically
restricted to certain structures by giving a few rules only, e.g.\
- $(\idt{intro}~\name{impI}~\name{allI})$ to strip implications and
- universal quantifiers.
+ \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}$~/ $\idt{elim}$. In general,
+ 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 (e.g.\
+ by actual automated proof methods (such as
\isacommand{by}~$\idt{blast}$).
*};
@@ -309,7 +311,7 @@
assumptions. The corresponding proof text typically mimics this by
establishing results in appropriate contexts, separated by blocks.
- In order to avoid too much explicit bracketing, the Isar system
+ 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
@@ -336,9 +338,9 @@
text {*
Again, the rather vacuous body of the proof may be collapsed. Thus
- the case analysis degenerates into two assumption steps, which
- are implicitly performed when concluding the single rule step of the
- double-dot proof below.
+ the case analysis degenerates into two assumption steps, which are
+ implicitly performed when concluding the single rule step of the
+ double-dot proof as follows.
*};
lemma "P | P --> P";
@@ -379,7 +381,7 @@
text {*
While explicit rule instantiation may occasionally help to improve
- the readability of certain aspects of reasoning it is usually quite
+ the 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 higher-order unification). Thus we may as well prune
@@ -402,12 +404,8 @@
text {*
We derive the conjunction elimination rule from the projections. The
- proof below follows is quite straight-forward, since Isabelle/Isar
- supports non-atomic goals and assumptions fully transparently. Note
- that this is in contrast to classic Isabelle: the corresponding
- tactic script given in \cite{isabelle-intro} depends on the primitive
- goal command to decompose the rule into premises and conclusion, with
- the result emerging by discharging the context again later.
+ proof is quite straight-forward, since Isabelle/Isar supports
+ non-atomic goals and assumptions fully transparently.
*};
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
@@ -421,4 +419,13 @@
qed;
qed;
+text {*
+ Note that classic Isabelle handles higher rules in a slightly
+ different way. The tactic script as given in \cite{isabelle-intro}
+ 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
+ the context at \texttt{qed} time.
+*};
+
end;
--- a/src/HOL/Isar_examples/Cantor.thy Wed Oct 13 19:44:33 1999 +0200
+++ b/src/HOL/Isar_examples/Cantor.thy Thu Oct 14 01:07:24 1999 +0200
@@ -19,12 +19,11 @@
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 use HOL's set theory, with
- the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.
+ its range. The Isabelle/Isar proofs below uses HOL's set theory,
+ with the type $\alpha \ap \idt{set}$ and the operator $\idt{range}$.
- \bigskip We first consider a rather verbose version of the proof,
- with the reasoning expressed quite naively. We only make use of the
- pure core of the Isar proof language.
+ \bigskip We first consider a slightly awkward version of the proof,
+ with the reasoning expressed quite naively.
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -33,21 +32,21 @@
show "?S ~: range f";
proof;
assume "?S : range f";
- then; show False;
+ thus False;
proof;
fix y;
assume "?S = f y";
- then; show ?thesis;
+ thus ?thesis;
proof (rule equalityCE);
- assume y_in_S: "y : ?S";
- assume y_in_fy: "y : f y";
- from y_in_S; have y_notin_fy: "y ~: f y"; ..;
- from y_notin_fy y_in_fy; show ?thesis; by contradiction;
+ assume in_S: "y : ?S";
+ assume in_fy: "y : f y";
+ from in_S; have notin_fy: "y ~: f y"; ..;
+ from notin_fy in_fy; show ?thesis; by contradiction;
next;
- assume y_notin_S: "y ~: ?S";
- assume y_notin_fy: "y ~: f y";
- from y_notin_S; have y_in_fy: "y : f y"; ..;
- from y_notin_fy y_in_fy; show ?thesis; by contradiction;
+ assume notin_S: "y ~: ?S";
+ assume notin_fy: "y ~: f y";
+ from notin_S; have in_fy: "y : f y"; ..;
+ from notin_fy in_fy; show ?thesis; by contradiction;
qed;
qed;
qed;
@@ -55,8 +54,15 @@
text {*
The following version of the proof essentially does the same
- reasoning, only that it is expressed more neatly, with some derived
- Isar language elements involved.
+ reasoning, only that it is expressed more neatly. In particular, we
+ 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}.}
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -85,11 +91,12 @@
text {*
How much creativity is required? As it happens, Isabelle can prove
- this theorem automatically. The default classical set 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.
+ 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
+ would diverge, but best-first search successfully navigates through
+ the large search space.
*};
theorem "EX S. S ~: range(f :: 'a => 'a set)";
@@ -100,7 +107,7 @@
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.
+ creative process, after all.
*};
end;
--- a/src/HOL/Isar_examples/KnasterTarski.thy Wed Oct 13 19:44:33 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Thu Oct 14 01:07:24 1999 +0200
@@ -15,7 +15,7 @@
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 their argument, and
+ 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
--- a/src/HOL/Isar_examples/Peirce.thy Wed Oct 13 19:44:33 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy Thu Oct 14 01:07:24 1999 +0200
@@ -3,10 +3,23 @@
Author: Markus Wenzel, TU Muenchen
*)
-header {* Examples of classical proof: Peirce's Law *};
+header {* Peirce's Law *};
theory Peirce = Main:;
+text {*
+ We consider Peirce's Law: $((A \impl B) \impl A) \impl A$. This is
+ an inherently non-intuitionistic statement, so its proof will
+ 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.}
+*};
+
theorem "((A --> B) --> A) --> A";
proof;
assume aba: "(A --> B) --> A";
@@ -22,6 +35,21 @@
qed;
qed;
+text {*
+ The subsequent version rearranges the reasoning 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}.
+
+ Technically speaking, whenever some goal is solved by
+ \isacommand{show} in the context of weak assumptions then the latter
+ give rise to new subgoals, which may be established separately. In
+ contrast, strong assumptions (as introduced by \isacommand{assume})
+ are solved immediately.
+*};
+
theorem "((A --> B) --> A) --> A";
proof;
assume aba: "(A --> B) --> A";
@@ -39,4 +67,23 @@
qed;
qed;
+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.
+
+ 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.
+*};
+
end;