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