--- a/src/HOL/Isar_examples/BasicLogic.thy Mon Jun 22 22:51:08 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,447 +0,0 @@
-(* Title: HOL/Isar_examples/BasicLogic.thy
- ID: $Id$
- Author: Markus Wenzel, TU Muenchen
-
-Basic propositional and quantifier reasoning.
-*)
-
-header {* Basic logical reasoning *}
-
-theory BasicLogic imports Main begin
-
-
-subsection {* Pure backward reasoning *}
-
-text {*
- In order to get a first idea of how Isabelle/Isar proof documents
- may look like, we consider the propositions @{text I}, @{text K},
- and @{text S}. The following (rather explicit) proofs should
- require little extra explanations.
-*}
-
-lemma I: "A --> A"
-proof
- assume A
- show A by fact
-qed
-
-lemma K: "A --> B --> A"
-proof
- assume A
- show "B --> A"
- proof
- show A by fact
- qed
-qed
-
-lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
-proof
- assume "A --> B --> C"
- show "(A --> B) --> A --> C"
- proof
- assume "A --> B"
- show "A --> C"
- proof
- assume A
- show C
- proof (rule mp)
- show "B --> C" by (rule mp) fact+
- show B by (rule mp) fact+
- qed
- qed
- qed
-qed
-
-text {*
- Isar provides several ways to fine-tune the reasoning, avoiding
- 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.
-
- First of all, proof by assumption may be abbreviated as a single
- dot.
-*}
-
-lemma "A --> A"
-proof
- assume A
- show A by fact+
-qed
-
-text {*
- In fact, concluding any (sub-)proof already involves solving any
- remaining goals by assumption\footnote{This is not a completely
- trivial operation, as proof by assumption may involve full
- higher-order unification.}. 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 @{text 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 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{Apparently,
- the rule here is implication introduction.}
-*}
-
-text {*
- Let us also reconsider @{text 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.
-
- The @{text intro} proof method repeatedly decomposes a goal's
- conclusion.\footnote{The dual method is @{text elim}, acting on a
- goal's premises.}
-*}
-
-lemma "A --> B --> A"
-proof (intro impI)
- assume A
- show A by fact
-qed
-
-text {*
- Again, the body may be collapsed.
-*}
-
-lemma "A --> B --> A"
- by (intro impI)
-
-text {*
- Just like @{text rule}, the @{text intro} and @{text 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 with iteration. Thus
- in practice, @{text intro} and @{text elim} would be typically
- restricted to certain structures by giving a few rules only, e.g.\
- \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
- and universal quantifiers.
-
- Such well-tuned iterated decomposition of certain structures is the
- prime application of @{text intro} and @{text elim}. In contrast,
- terminal steps that solve a goal completely are usually performed by
- actual automated proof methods (such as \isacommand{by}~@{text
- 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 @{text "A \<and> B \<longrightarrow> B \<and> A"}.
-
- The first version is purely backward.
-*}
-
-lemma "A & B --> B & A"
-proof
- assume "A & B"
- show "B & A"
- proof
- show B by (rule conjunct2) fact
- show A by (rule conjunct1) fact
- qed
-qed
-
-text {*
- Above, the @{text "conjunct_1/2"} projection rules had to be named
- explicitly, since the goals @{text B} and @{text A} did not provide
- any structural clue. This may be avoided using \isacommand{from} to
- focus on the @{text "A \<and> B"} assumption as the current facts,
- enabling the use of double-dot proofs. Note that \isacommand{from}
- already does forward-chaining, involving the \name{conjE} rule here.
-*}
-
-lemma "A & B --> B & A"
-proof
- assume "A & B"
- show "B & A"
- proof
- from `A & B` show B ..
- from `A & B` show A ..
- 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 @{text "B \<and> A"} from
- @{text "A \<and> B"} actually becomes an elimination, rather than an
- introduction. The resulting proof structure directly corresponds to
- that of the @{text conjE} rule, including the repeated goal
- proposition that is abbreviated as @{text ?thesis} below.
-*}
-
-lemma "A & B --> B & A"
-proof
- assume "A & B"
- then show "B & A"
- proof -- {* rule @{text conjE} of @{text "A \<and> B"} *}
- assume B A
- then show ?thesis .. -- {* rule @{text conjI} of @{text "B \<and> A"} *}
- qed
-qed
-
-text {*
- 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"
-proof
- assume "A & B"
- from `A & B` have A ..
- from `A & B` have B ..
- from `B` `A` show "B & A" ..
-qed
-
-text {*
- We can still push forward-reasoning a bit further, even at the risk
- of getting ridiculous. Note that we force the initial proof step to
- do nothing here, by referring to the ``-'' proof method.
-*}
-
-lemma "A & B --> B & A"
-proof -
- {
- assume "A & B"
- from `A & B` have A ..
- from `A & B` have B ..
- from `B` `A` have "B & A" ..
- }
- then show ?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 general, there
- is no single best way to arrange some pieces of formal reasoning, of
- course. Depending on the actual applications, the intended audience
- 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 {*
- For our example the most appropriate way of reasoning is probably
- the middle one, with conjunction introduction done after
- elimination.
-*}
-
-lemma "A & B --> B & A"
-proof
- assume "A & B"
- then show "B & A"
- proof
- assume B A
- then 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}, using HOL rather than FOL.
-*}
-
-subsubsection {* A propositional proof *}
-
-text {*
- We consider the proposition @{text "P \<or> P \<longrightarrow> P"}. The proof below
- involves forward-chaining from @{text "P \<or> P"}, followed by an
- explicit case-analysis on the two \emph{identical} cases.
-*}
-
-lemma "P | P --> P"
-proof
- assume "P | P"
- then show P
- proof -- {*
- rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
- *}
- assume P show P by fact
- next
- assume P show P by fact
- qed
-qed
-
-text {*
- Case splits are \emph{not} hardwired into the Isar language as a
- special feature. The \isacommand{next} command used to separate the
- cases above is just a short form of managing block structure.
-
- \medskip In general, applying proof methods may split up a goal into
- separate ``cases'', i.e.\ new subgoals with individual local
- assumptions. The corresponding proof text typically mimics this by
- establishing results in appropriate contexts, separated by blocks.
-
- 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 would expect from
- separating cases, only that it is more flexible. E.g.\ an induction
- base case (which does not introduce local assumptions) would
- \emph{not} require \isacommand{next} to separate the subsequent step
- case.
-
- \medskip In our example the situation is even simpler, since the two
- cases actually coincide. Consequently the proof may be rephrased as
- follows.
-*}
-
-lemma "P | P --> P"
-proof
- assume "P | P"
- then show P
- proof
- assume P
- show P by fact
- show P by fact
- qed
-qed
-
-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 as follows.
-*}
-
-lemma "P | P --> P"
-proof
- assume "P | P"
- then show P ..
-qed
-
-
-subsubsection {* A quantifier proof *}
-
-text {*
- To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
- x)) \<longrightarrow> (\<exists>y. P y)"}. Informally, this holds because any @{text a}
- with @{text "P (f a)"} may be taken as a witness for the second
- existential statement.
-
- The first proof is rather verbose, exhibiting quite a lot of
- (redundant) detail. It gives explicit rules, even with some
- instantiation. Furthermore, we encounter two new language elements:
- the \isacommand{fix} command augments the context by some new
- ``arbitrary, but fixed'' element; the \isacommand{is} annotation
- binds term abbreviations by higher-order pattern matching.
-*}
-
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
- assume "EX x. P (f x)"
- then show "EX y. P y"
- proof (rule exE) -- {*
- rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
- *}
- fix a
- assume "P (f a)" (is "P ?witness")
- then show ?thesis by (rule exI [of P ?witness])
- qed
-qed
-
-text {*
- While explicit rule instantiation may occasionally improve
- 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
- the text as follows.
-*}
-
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
- assume "EX x. P (f x)"
- then show "EX y. P y"
- proof
- fix a
- assume "P (f a)"
- then show ?thesis ..
- qed
-qed
-
-text {*
- Explicit @{text \<exists>}-elimination as seen above can become quite
- cumbersome in practice. The derived Isar language element
- ``\isakeyword{obtain}'' provides a more handsome way to do
- generalized existence reasoning.
-*}
-
-lemma "(EX x. P (f x)) --> (EX y. P y)"
-proof
- assume "EX x. P (f x)"
- then obtain a where "P (f a)" ..
- then show "EX y. P y" ..
-qed
-
-text {*
- Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
- \isakeyword{assume} together with a soundness proof of the
- elimination involved. Thus it behaves similar to any other forward
- proof element. Also note that due to the nature of general
- existence reasoning involved here, any result exported from the
- context of an \isakeyword{obtain} statement may \emph{not} refer to
- the parameters introduced there.
-*}
-
-
-
-subsubsection {* Deriving rules in Isabelle *}
-
-text {*
- We derive the conjunction elimination rule from the corresponding
- projections. The proof is quite straight-forward, since
- Isabelle/Isar supports non-atomic goals and assumptions fully
- transparently.
-*}
-
-theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
-proof -
- assume "A & B"
- assume r: "A ==> B ==> C"
- show C
- proof (rule r)
- show A by (rule conjunct1) fact
- show B by (rule conjunct2) fact
- qed
-qed
-
-end