src/HOL/Isar_examples/BasicLogic.thy
author wenzelm
Wed Nov 16 19:34:19 2005 +0100 (2005-11-16)
changeset 18193 54419506df9e
parent 16417 9bc16273c2d4
child 23373 ead82c82da9e
permissions -rw-r--r--
tuned document;
     1 (*  Title:      HOL/Isar_examples/BasicLogic.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Basic propositional and quantifier reasoning.
     6 *)
     7 
     8 header {* Basic logical reasoning *}
     9 
    10 theory BasicLogic imports Main begin
    11 
    12 
    13 subsection {* Pure backward reasoning *}
    14 
    15 text {*
    16   In order to get a first idea of how Isabelle/Isar proof documents
    17   may look like, we consider the propositions @{text I}, @{text K},
    18   and @{text S}.  The following (rather explicit) proofs should
    19   require little extra explanations.
    20 *}
    21 
    22 lemma I: "A --> A"
    23 proof
    24   assume A
    25   show A by assumption
    26 qed
    27 
    28 lemma K: "A --> B --> A"
    29 proof
    30   assume A
    31   show "B --> A"
    32   proof
    33     show A by assumption
    34   qed
    35 qed
    36 
    37 lemma S: "(A --> B --> C) --> (A --> B) --> A --> C"
    38 proof
    39   assume "A --> B --> C"
    40   show "(A --> B) --> A --> C"
    41   proof
    42     assume "A --> B"
    43     show "A --> C"
    44     proof
    45       assume A
    46       show C
    47       proof (rule mp)
    48         show "B --> C" by (rule mp)
    49         show B by (rule mp)
    50       qed
    51     qed
    52   qed
    53 qed
    54 
    55 text {*
    56   Isar provides several ways to fine-tune the reasoning, avoiding
    57   excessive detail.  Several abbreviated language elements are
    58   available, enabling the writer to express proofs in a more concise
    59   way, even without referring to any automated proof tools yet.
    60 
    61   First of all, proof by assumption may be abbreviated as a single
    62   dot.
    63 *}
    64 
    65 lemma "A --> A"
    66 proof
    67   assume A
    68   show A .
    69 qed
    70 
    71 text {*
    72   In fact, concluding any (sub-)proof already involves solving any
    73   remaining goals by assumption\footnote{This is not a completely
    74   trivial operation, as proof by assumption may involve full
    75   higher-order unification.}.  Thus we may skip the rather vacuous
    76   body of the above proof as well.
    77 *}
    78 
    79 lemma "A --> A"
    80 proof
    81 qed
    82 
    83 text {*
    84   Note that the \isacommand{proof} command refers to the @{text rule}
    85   method (without arguments) by default.  Thus it implicitly applies a
    86   single rule, as determined from the syntactic form of the statements
    87   involved.  The \isacommand{by} command abbreviates any proof with
    88   empty body, so the proof may be further pruned.
    89 *}
    90 
    91 lemma "A --> A"
    92   by rule
    93 
    94 text {*
    95   Proof by a single rule may be abbreviated as double-dot.
    96 *}
    97 
    98 lemma "A --> A" ..
    99 
   100 text {*
   101   Thus we have arrived at an adequate representation of the proof of a
   102   tautology that holds by a single standard rule.\footnote{Apparently,
   103   the rule here is implication introduction.}
   104 *}
   105 
   106 text {*
   107   Let us also reconsider @{text K}.  Its statement is composed of
   108   iterated connectives.  Basic decomposition is by a single rule at a
   109   time, which is why our first version above was by nesting two
   110   proofs.
   111 
   112   The @{text intro} proof method repeatedly decomposes a goal's
   113   conclusion.\footnote{The dual method is @{text elim}, acting on a
   114   goal's premises.}
   115 *}
   116 
   117 lemma "A --> B --> A"
   118 proof (intro impI)
   119   assume A
   120   show A .
   121 qed
   122 
   123 text {*
   124   Again, the body may be collapsed.
   125 *}
   126 
   127 lemma "A --> B --> A"
   128   by (intro impI)
   129 
   130 text {*
   131   Just like @{text rule}, the @{text intro} and @{text elim} proof
   132   methods pick standard structural rules, in case no explicit
   133   arguments are given.  While implicit rules are usually just fine for
   134   single rule application, this may go too far with iteration.  Thus
   135   in practice, @{text intro} and @{text elim} would be typically
   136   restricted to certain structures by giving a few rules only, e.g.\
   137   \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
   138   and universal quantifiers.
   139 
   140   Such well-tuned iterated decomposition of certain structures is the
   141   prime application of @{text intro} and @{text elim}.  In contrast,
   142   terminal steps that solve a goal completely are usually performed by
   143   actual automated proof methods (such as \isacommand{by}~@{text
   144   blast}.
   145 *}
   146 
   147 
   148 subsection {* Variations of backward vs.\ forward reasoning *}
   149 
   150 text {*
   151   Certainly, any proof may be performed in backward-style only.  On
   152   the other hand, small steps of reasoning are often more naturally
   153   expressed in forward-style.  Isar supports both backward and forward
   154   reasoning as a first-class concept.  In order to demonstrate the
   155   difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
   156 
   157   The first version is purely backward.
   158 *}
   159 
   160 lemma "A & B --> B & A"
   161 proof
   162   assume "A & B"
   163   show "B & A"
   164   proof
   165     show B by (rule conjunct2)
   166     show A by (rule conjunct1)
   167   qed
   168 qed
   169 
   170 text {*
   171   Above, the @{text "conjunct_1/2"} projection rules had to be named
   172   explicitly, since the goals @{text B} and @{text A} did not provide
   173   any structural clue.  This may be avoided using \isacommand{from} to
   174   focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the
   175   current facts, enabling the use of double-dot proofs.  Note that
   176   \isacommand{from} already does forward-chaining, involving the
   177   \name{conjE} rule here.
   178 *}
   179 
   180 lemma "A & B --> B & A"
   181 proof
   182   assume "A & B"
   183   show "B & A"
   184   proof
   185     from prems show B ..
   186     from prems show A ..
   187   qed
   188 qed
   189 
   190 text {*
   191   In the next version, we move the forward step one level upwards.
   192   Forward-chaining from the most recent facts is indicated by the
   193   \isacommand{then} command.  Thus the proof of @{text "B \<and> A"} from
   194   @{text "A \<and> B"} actually becomes an elimination, rather than an
   195   introduction.  The resulting proof structure directly corresponds to
   196   that of the @{text conjE} rule, including the repeated goal
   197   proposition that is abbreviated as @{text ?thesis} below.
   198 *}
   199 
   200 lemma "A & B --> B & A"
   201 proof
   202   assume "A & B"
   203   then show "B & A"
   204   proof                    -- {* rule @{text conjE} of @{text "A \<and> B"} *}
   205     assume A B
   206     show ?thesis ..       -- {* rule @{text conjI} of @{text "B \<and> A"} *}
   207   qed
   208 qed
   209 
   210 text {*
   211   In the subsequent version we flatten the structure of the main body
   212   by doing forward reasoning all the time.  Only the outermost
   213   decomposition step is left as backward.
   214 *}
   215 
   216 lemma "A & B --> B & A"
   217 proof
   218   assume ab: "A & B"
   219   from ab have a: A ..
   220   from ab have b: B ..
   221   from b a show "B & A" ..
   222 qed
   223 
   224 text {*
   225   We can still push forward-reasoning a bit further, even at the risk
   226   of getting ridiculous.  Note that we force the initial proof step to
   227   do nothing here, by referring to the ``-'' proof method.
   228 *}
   229 
   230 lemma "A & B --> B & A"
   231 proof -
   232   {
   233     assume ab: "A & B"
   234     from ab have a: A ..
   235     from ab have b: B ..
   236     from b a have "B & A" ..
   237   }
   238   thus ?thesis ..         -- {* rule \name{impI} *}
   239 qed
   240 
   241 text {*
   242   \medskip With these examples we have shifted through a whole range
   243   from purely backward to purely forward reasoning.  Apparently, in
   244   the extreme ends we get slightly ill-structured proofs, which also
   245   require much explicit naming of either rules (backward) or local
   246   facts (forward).
   247 
   248   The general lesson learned here is that good proof style would
   249   achieve just the \emph{right} balance of top-down backward
   250   decomposition, and bottom-up forward composition.  In general, there
   251   is no single best way to arrange some pieces of formal reasoning, of
   252   course.  Depending on the actual applications, the intended audience
   253   etc., rules (and methods) on the one hand vs.\ facts on the other
   254   hand have to be emphasized in an appropriate way.  This requires the
   255   proof writer to develop good taste, and some practice, of course.
   256 *}
   257 
   258 text {*
   259   For our example the most appropriate way of reasoning is probably
   260   the middle one, with conjunction introduction done after
   261   elimination.  This reads even more concisely using
   262   \isacommand{thus}, which abbreviates
   263   \isacommand{then}~\isacommand{show}.\footnote{In the same vein,
   264   \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}
   265 *}
   266 
   267 lemma "A & B --> B & A"
   268 proof
   269   assume "A & B"
   270   thus "B & A"
   271   proof
   272     assume A B
   273     show ?thesis ..
   274   qed
   275 qed
   276 
   277 
   278 
   279 subsection {* A few examples from ``Introduction to Isabelle'' *}
   280 
   281 text {*
   282   We rephrase some of the basic reasoning examples of
   283   \cite{isabelle-intro}, using HOL rather than FOL.
   284 *}
   285 
   286 subsubsection {* A propositional proof *}
   287 
   288 text {*
   289   We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof below
   290   involves forward-chaining from @{text "P \<or> P"}, followed by an
   291   explicit case-analysis on the two \emph{identical} cases.
   292 *}
   293 
   294 lemma "P | P --> P"
   295 proof
   296   assume "P | P"
   297   thus P
   298   proof                    -- {*
   299     rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
   300   *}
   301     assume P show P .
   302   next
   303     assume P show P .
   304   qed
   305 qed
   306 
   307 text {*
   308   Case splits are \emph{not} hardwired into the Isar language as a
   309   special feature.  The \isacommand{next} command used to separate the
   310   cases above is just a short form of managing block structure.
   311 
   312   \medskip In general, applying proof methods may split up a goal into
   313   separate ``cases'', i.e.\ new subgoals with individual local
   314   assumptions.  The corresponding proof text typically mimics this by
   315   establishing results in appropriate contexts, separated by blocks.
   316 
   317   In order to avoid too much explicit parentheses, the Isar system
   318   implicitly opens an additional block for any new goal, the
   319   \isacommand{next} statement then closes one block level, opening a
   320   new one.  The resulting behavior is what one would expect from
   321   separating cases, only that it is more flexible.  E.g.\ an induction
   322   base case (which does not introduce local assumptions) would
   323   \emph{not} require \isacommand{next} to separate the subsequent step
   324   case.
   325 
   326   \medskip In our example the situation is even simpler, since the two
   327   cases actually coincide.  Consequently the proof may be rephrased as
   328   follows.
   329 *}
   330 
   331 lemma "P | P --> P"
   332 proof
   333   assume "P | P"
   334   thus P
   335   proof
   336     assume P
   337     show P .
   338     show P .
   339   qed
   340 qed
   341 
   342 text {*
   343   Again, the rather vacuous body of the proof may be collapsed.  Thus
   344   the case analysis degenerates into two assumption steps, which are
   345   implicitly performed when concluding the single rule step of the
   346   double-dot proof as follows.
   347 *}
   348 
   349 lemma "P | P --> P"
   350 proof
   351   assume "P | P"
   352   thus P ..
   353 qed
   354 
   355 
   356 subsubsection {* A quantifier proof *}
   357 
   358 text {*
   359   To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
   360   x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any @{text a}
   361   with @{text "P (f a)"} may be taken as a witness for the second
   362   existential statement.
   363 
   364   The first proof is rather verbose, exhibiting quite a lot of
   365   (redundant) detail.  It gives explicit rules, even with some
   366   instantiation.  Furthermore, we encounter two new language elements:
   367   the \isacommand{fix} command augments the context by some new
   368   ``arbitrary, but fixed'' element; the \isacommand{is} annotation
   369   binds term abbreviations by higher-order pattern matching.
   370 *}
   371 
   372 lemma "(EX x. P (f x)) --> (EX y. P y)"
   373 proof
   374   assume "EX x. P (f x)"
   375   thus "EX y. P y"
   376   proof (rule exE)             -- {*
   377     rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
   378   *}
   379     fix a
   380     assume "P (f a)" (is "P ?witness")
   381     show ?thesis by (rule exI [of P ?witness])
   382   qed
   383 qed
   384 
   385 text {*
   386   While explicit rule instantiation may occasionally improve
   387   readability of certain aspects of reasoning, it is usually quite
   388   redundant.  Above, the basic proof outline gives already enough
   389   structural clues for the system to infer both the rules and their
   390   instances (by higher-order unification).  Thus we may as well prune
   391   the text as follows.
   392 *}
   393 
   394 lemma "(EX x. P (f x)) --> (EX y. P y)"
   395 proof
   396   assume "EX x. P (f x)"
   397   thus "EX y. P y"
   398   proof
   399     fix a
   400     assume "P (f a)"
   401     show ?thesis ..
   402   qed
   403 qed
   404 
   405 text {*
   406   Explicit @{text \<exists>}-elimination as seen above can become quite
   407   cumbersome in practice.  The derived Isar language element
   408   ``\isakeyword{obtain}'' provides a more handsome way to do
   409   generalized existence reasoning.
   410 *}
   411 
   412 lemma "(EX x. P (f x)) --> (EX y. P y)"
   413 proof
   414   assume "EX x. P (f x)"
   415   then obtain a where "P (f a)" ..
   416   thus "EX y. P y" ..
   417 qed
   418 
   419 text {*
   420   Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
   421   \isakeyword{assume} together with a soundness proof of the
   422   elimination involved.  Thus it behaves similar to any other forward
   423   proof element.  Also note that due to the nature of general
   424   existence reasoning involved here, any result exported from the
   425   context of an \isakeyword{obtain} statement may \emph{not} refer to
   426   the parameters introduced there.
   427 *}
   428 
   429 
   430 
   431 subsubsection {* Deriving rules in Isabelle *}
   432 
   433 text {*
   434   We derive the conjunction elimination rule from the corresponding
   435   projections.  The proof is quite straight-forward, since
   436   Isabelle/Isar supports non-atomic goals and assumptions fully
   437   transparently.
   438 *}
   439 
   440 theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
   441 proof -
   442   assume "A & B"
   443   assume r: "A ==> B ==> C"
   444   show C
   445   proof (rule r)
   446     show A by (rule conjunct1)
   447     show B by (rule conjunct2)
   448   qed
   449 qed
   450 
   451 text {*
   452   Note that classic Isabelle handles higher rules in a slightly
   453   different way.  The tactic script as given in \cite{isabelle-intro}
   454   for the same example of \name{conjE} depends on the primitive
   455   \texttt{goal} command to decompose the rule into premises and
   456   conclusion.  The actual result would then emerge by discharging of
   457   the context at \texttt{qed} time.
   458 *}
   459 
   460 end