src/HOL/Isar_examples/BasicLogic.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 18193 54419506df9e child 23373 ead82c82da9e permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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