author wenzelm Sat, 09 Oct 1999 23:20:49 +0200 changeset 7820 cad7cc30fa40 parent 7819 6dd018b6cf3f child 7821 a8717f53036c
more explanations;
--- 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";