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