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