# HG changeset patch # User wenzelm # Date 939504049 -7200 # Node ID cad7cc30fa408f37618c5df3486e1487045128fb # Parent 6dd018b6cf3fa9e81d90a3d062e3b35a649c405f more explanations; diff -r 6dd018b6cf3f -r cad7cc30fa40 src/HOL/Isar_examples/BasicLogic.thy --- 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";