--- a/src/HOL/Isar_examples/BasicLogic.thy Sat Oct 09 23:20:02 1999 +0200
+++ b/src/HOL/Isar_examples/BasicLogic.thy Sat Oct 09 23:20:49 1999 +0200
@@ -10,15 +10,19 @@
theory BasicLogic = Main:;
-subsection {* Some trivialities *};
+subsection {* Pure backward reasoning *};
-text {* Just a few toy examples to get an idea of how Isabelle/Isar
- proof documents may look like. *};
+text {*
+ In order to get a first idea of how Isabelle/Isar proof documents may
+ look like, we consider the propositions $I$, $K$, and $S$. The
+ following (rather explicit) proofs should require little extra
+ explanations.
+*};
lemma I: "A --> A";
proof;
assume A;
- show A; .;
+ show A; by assumption;
qed;
lemma K: "A --> B --> A";
@@ -26,25 +30,10 @@
assume A;
show "B --> A";
proof;
- show A; .;
+ show A; by assumption;
qed;
qed;
-lemma K': "A --> B --> A";
-proof;
- assume A;
- thus "B --> A"; ..;
-qed;
-
-lemma K'': "A --> B --> A";
-proof intro;
- assume A;
- show A; .;
-qed;
-
-lemma K''': "A --> B --> A";
- by intro;
-
lemma S: "(A --> B --> C) --> (A --> B) --> A --> C";
proof;
assume "A --> B --> C";
@@ -63,8 +52,107 @@
qed;
qed;
+text {*
+ Isar provides several ways to fine-tune the reasoning, avoiding
+ irrelevant 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.
-subsection {* Variations of backward vs.\ forward reasoning \dots *};
+ First of all, proof by assumption may be abbreviated as a single dot.
+*};
+
+lemma "A --> A";
+proof;
+ assume A;
+ show A; .;
+qed;
+
+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.
+*};
+
+lemma "A --> A";
+proof;
+qed;
+
+text {*
+ Note that the \isacommand{proof} command refers to the $\idt{rule}$
+ method (without arguments) by default. Thus it implicitly applies a
+ single rule, as determined from the syntactic form of the statements
+ involved. The \isacommand{by} command abbreviates any proof with
+ empty body, so the proof may be further pruned.
+*};
+
+lemma "A --> A";
+ by rule;
+
+text {*
+ Proof by a single rule may be abbreviated as a double dot.
+*};
+
+lemma "A --> A"; ..;
+
+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.}
+*};
+
+text {*
+ Let us also reconsider $K$. It's 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.
+
+ The $\idt{intro}$ proof method repeatedly decomposes a goal's
+ conclusion.\footnote{The dual method is $\idt{elim}$, acting on a
+ goal's premises.}
+*};
+
+lemma "A --> B --> A";
+proof intro;
+ assume A;
+ show A; .;
+qed;
+
+text {*
+ Again, the body may be collapsed.
+*};
+
+lemma "A --> B --> A";
+ by intro;
+
+text {*
+ 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
+ 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.
+
+ Such well-tuned iterated decomposition of certain structure is the
+ prime application of $\idt{intro}$~/ $\idt{elim}$. In general,
+ terminal steps that solve a goal completely are typically performed
+ by actual automated proof methods (e.g.\
+ \isacommand{by}~$\idt{blast}$).
+*};
+
+
+subsection {* Variations of backward vs.\ forward reasoning *};
+
+text {*
+ Certainly, any proof may be performed in backward-style only. On the
+ other hand, small steps of reasoning are often more naturally
+ expressed in forward-style. Isar supports both backward and forward
+ reasoning as a first-class concept. In order to demonstrate the
+ difference, we consider several proofs of $A \conj B \impl B \conj
+ A$.
+
+ The first version is purely backward.
+*};
lemma "A & B --> B & A";
proof;
@@ -76,15 +164,14 @@
qed;
qed;
-lemma "A & B --> B & A";
-proof;
- assume "A & B";
- then; show "B & A";
- proof;
- assume A B;
- show ?thesis; ..;
- qed;
-qed;
+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 double-dot proofs. Note that \isacommand{from} already
+ involves forward-chaining.
+*};
lemma "A & B --> B & A";
proof;
@@ -96,6 +183,31 @@
qed;
qed;
+text {*
+ In the next version, we move the forward step one level upwards.
+ Forward-chaining from the most recent facts is indicated by the
+ \isacommand{then} command. Thus the proof of $B \conj A$ from $A
+ \conj B$ actually becomes an elimination, rather than an
+ introduction. The resulting proof structure directly corresponds to
+ that of the $\name{conjE}$ rule, including the repeated goal
+ proposition that is abbreviated as $\var{thesis}$ below.
+*};
+
+lemma "A & B --> B & A";
+proof;
+ assume "A & B";
+ then; show "B & A";
+ proof -- {* rule \name{conjE} of $A \conj B$ *};
+ assume A B;
+ show ?thesis; .. -- {* rule \name{conjI} of $B \conj A$ *};
+ qed;
+qed;
+
+text {*
+ Subsequently, only the outermost decomposition step is left backward,
+ all the rest is forward.
+*};
+
lemma "A & B --> B & A";
proof;
assume ab: "A & B";
@@ -104,9 +216,68 @@
from b a; show "B & A"; ..;
qed;
+text {*
+ We can still push forward reasoning a bit further, even at the danger
+ of getting ridiculous. Note that we force the initial proof step to
+ do nothing, by referring to the ``-'' proof method.
+*};
+
+lemma "A & B --> B & A";
+proof -;
+ {{;
+ assume ab: "A & B";
+ from ab; have a: A; ..;
+ from ab; have b: B; ..;
+ from b a; have "B & A"; ..;
+ }};
+ thus ?thesis; .. -- {* rule \name{impI} *};
+qed;
+
+text {*
+ \medskip With these examples we have shifted through a whole range
+ from purely backward to purely forward reasoning. Apparently, in the
+ extreme ends we get slightly ill-structured proofs, which also
+ require much explicit naming of either rules (backward) or local
+ facts (forward).
+
+ The general lesson learned here is that good proof style would
+ achieve just the \emph{right} balance of top-down backward
+ 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
+ emphasised in an appropriate way. This requires the proof writer to
+ develop good taste, and some practice, of course.
+*};
+
+text {*
+ For our example the most appropriate way of reasoning is probably the
+ middle one, with conjunction introduction done after elimination.
+ This reads even more concisely using \isacommand{thus}, which
+ abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same
+ vein, \isacommand{hence} abbreviates
+ \isacommand{then}~\isacommand{have}.}
+*};
+
+lemma "A & B --> B & A";
+proof;
+ assume "A & B";
+ thus "B & A";
+ proof;
+ assume A B;
+ show ?thesis; ..;
+ qed;
+qed;
+
+
subsection {* A few examples from ``Introduction to Isabelle'' *};
+text {*
+ We rephrase some of the basic reasoning examples of
+ \cite{isabelle-intro}.
+*};
+
subsubsection {* Propositional proof *};
lemma "P | P --> P";