src/HOL/Isar_examples/BasicLogic.thy
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 18193 54419506df9e
child 23373 ead82c82da9e
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
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
haftmann@16417
    10
theory BasicLogic imports Main begin
wenzelm@6444
    11
wenzelm@7761
    12
wenzelm@10007
    13
subsection {* Pure backward reasoning *}
wenzelm@7740
    14
wenzelm@7820
    15
text {*
wenzelm@18193
    16
  In order to get a first idea of how Isabelle/Isar proof documents
wenzelm@18193
    17
  may look like, we consider the propositions @{text I}, @{text K},
wenzelm@18193
    18
  and @{text S}.  The following (rather explicit) proofs should
wenzelm@18193
    19
  require little extra 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@18193
    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@18193
    56
  Isar provides several ways to fine-tune the reasoning, avoiding
wenzelm@18193
    57
  excessive detail.  Several abbreviated language elements are
wenzelm@18193
    58
  available, enabling the writer to express proofs in a more concise
wenzelm@18193
    59
  way, even without referring to any automated proof tools yet.
wenzelm@7761
    60
wenzelm@18193
    61
  First of all, proof by assumption may be abbreviated as a single
wenzelm@18193
    62
  dot.
wenzelm@10007
    63
*}
wenzelm@7820
    64
wenzelm@10007
    65
lemma "A --> A"
wenzelm@10007
    66
proof
wenzelm@10007
    67
  assume A
wenzelm@10007
    68
  show A .
wenzelm@10007
    69
qed
wenzelm@7820
    70
wenzelm@7820
    71
text {*
wenzelm@18193
    72
  In fact, concluding any (sub-)proof already involves solving any
wenzelm@18193
    73
  remaining goals by assumption\footnote{This is not a completely
wenzelm@18193
    74
  trivial operation, as proof by assumption may involve full
wenzelm@18193
    75
  higher-order unification.}.  Thus we may skip the rather vacuous
wenzelm@18193
    76
  body of the above proof as well.
wenzelm@10007
    77
*}
wenzelm@7820
    78
wenzelm@10007
    79
lemma "A --> A"
wenzelm@10007
    80
proof
wenzelm@10007
    81
qed
wenzelm@7820
    82
wenzelm@7820
    83
text {*
wenzelm@18193
    84
  Note that the \isacommand{proof} command refers to the @{text rule}
wenzelm@18193
    85
  method (without arguments) by default.  Thus it implicitly applies a
wenzelm@18193
    86
  single rule, as determined from the syntactic form of the statements
wenzelm@18193
    87
  involved.  The \isacommand{by} command abbreviates any proof with
wenzelm@18193
    88
  empty body, so the proof may be further pruned.
wenzelm@10007
    89
*}
wenzelm@7820
    90
wenzelm@10007
    91
lemma "A --> A"
wenzelm@10007
    92
  by rule
wenzelm@7820
    93
wenzelm@7820
    94
text {*
wenzelm@18193
    95
  Proof by a single rule may be abbreviated as double-dot.
wenzelm@10007
    96
*}
wenzelm@7820
    97
wenzelm@10007
    98
lemma "A --> A" ..
wenzelm@7820
    99
wenzelm@7820
   100
text {*
wenzelm@18193
   101
  Thus we have arrived at an adequate representation of the proof of a
wenzelm@18193
   102
  tautology that holds by a single standard rule.\footnote{Apparently,
wenzelm@18193
   103
  the rule here is implication introduction.}
wenzelm@10007
   104
*}
wenzelm@7820
   105
wenzelm@7820
   106
text {*
wenzelm@18193
   107
  Let us also reconsider @{text K}.  Its statement is composed of
wenzelm@18193
   108
  iterated connectives.  Basic decomposition is by a single rule at a
wenzelm@18193
   109
  time, which is why our first version above was by nesting two
wenzelm@18193
   110
  proofs.
wenzelm@7820
   111
wenzelm@18193
   112
  The @{text intro} proof method repeatedly decomposes a goal's
wenzelm@18193
   113
  conclusion.\footnote{The dual method is @{text elim}, acting on a
wenzelm@18193
   114
  goal's premises.}
wenzelm@10007
   115
*}
wenzelm@7820
   116
wenzelm@10007
   117
lemma "A --> B --> A"
wenzelm@12387
   118
proof (intro impI)
wenzelm@10007
   119
  assume A
wenzelm@10007
   120
  show A .
wenzelm@10007
   121
qed
wenzelm@7820
   122
wenzelm@7820
   123
text {*
wenzelm@18193
   124
  Again, the body may be collapsed.
wenzelm@10007
   125
*}
wenzelm@7820
   126
wenzelm@10007
   127
lemma "A --> B --> A"
wenzelm@12387
   128
  by (intro impI)
wenzelm@7820
   129
wenzelm@7820
   130
text {*
wenzelm@18193
   131
  Just like @{text rule}, the @{text intro} and @{text elim} proof
wenzelm@18193
   132
  methods pick standard structural rules, in case no explicit
wenzelm@18193
   133
  arguments are given.  While implicit rules are usually just fine for
wenzelm@18193
   134
  single rule application, this may go too far with iteration.  Thus
wenzelm@18193
   135
  in practice, @{text intro} and @{text elim} would be typically
wenzelm@18193
   136
  restricted to certain structures by giving a few rules only, e.g.\
wenzelm@18193
   137
  \isacommand{proof}~@{text "(intro impI allI)"} to strip implications
wenzelm@18193
   138
  and universal quantifiers.
wenzelm@7820
   139
wenzelm@18193
   140
  Such well-tuned iterated decomposition of certain structures is the
wenzelm@18193
   141
  prime application of @{text intro} and @{text elim}.  In contrast,
wenzelm@18193
   142
  terminal steps that solve a goal completely are usually performed by
wenzelm@18193
   143
  actual automated proof methods (such as \isacommand{by}~@{text
wenzelm@18193
   144
  blast}.
wenzelm@10007
   145
*}
wenzelm@7820
   146
wenzelm@7820
   147
wenzelm@10007
   148
subsection {* Variations of backward vs.\ forward reasoning *}
wenzelm@7820
   149
wenzelm@7820
   150
text {*
wenzelm@18193
   151
  Certainly, any proof may be performed in backward-style only.  On
wenzelm@18193
   152
  the other hand, small steps of reasoning are often more naturally
wenzelm@18193
   153
  expressed in forward-style.  Isar supports both backward and forward
wenzelm@18193
   154
  reasoning as a first-class concept.  In order to demonstrate the
wenzelm@18193
   155
  difference, we consider several proofs of @{text "A \<and> B \<longrightarrow> B \<and> A"}.
wenzelm@7820
   156
wenzelm@18193
   157
  The first version is purely backward.
wenzelm@10007
   158
*}
wenzelm@7001
   159
wenzelm@10007
   160
lemma "A & B --> B & A"
wenzelm@10007
   161
proof
wenzelm@10007
   162
  assume "A & B"
wenzelm@10007
   163
  show "B & A"
wenzelm@10007
   164
  proof
wenzelm@10007
   165
    show B by (rule conjunct2)
wenzelm@10007
   166
    show A by (rule conjunct1)
wenzelm@10007
   167
  qed
wenzelm@10007
   168
qed
wenzelm@6444
   169
wenzelm@7820
   170
text {*
wenzelm@18193
   171
  Above, the @{text "conjunct_1/2"} projection rules had to be named
wenzelm@18193
   172
  explicitly, since the goals @{text B} and @{text A} did not provide
wenzelm@18193
   173
  any structural clue.  This may be avoided using \isacommand{from} to
wenzelm@18193
   174
  focus on @{text prems} (i.e.\ the @{text "A \<and> B"} assumption) as the
wenzelm@18193
   175
  current facts, enabling the use of double-dot proofs.  Note that
wenzelm@18193
   176
  \isacommand{from} already does forward-chaining, involving the
wenzelm@18193
   177
  \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@10007
   185
    from prems show B ..
wenzelm@10007
   186
    from prems 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@10007
   205
    assume A B
wenzelm@18193
   206
    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@10007
   218
  assume ab: "A & B"
wenzelm@10007
   219
  from ab have a: A ..
wenzelm@10007
   220
  from ab have b: B ..
wenzelm@10007
   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@10007
   233
    assume ab: "A & B"
wenzelm@10007
   234
    from ab have a: A ..
wenzelm@10007
   235
    from ab have b: B ..
wenzelm@10007
   236
    from b a have "B & A" ..
wenzelm@10007
   237
  }
wenzelm@10007
   238
  thus ?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@18193
   261
  elimination.  This reads even more concisely using
wenzelm@18193
   262
  \isacommand{thus}, which abbreviates
wenzelm@18193
   263
  \isacommand{then}~\isacommand{show}.\footnote{In the same vein,
wenzelm@18193
   264
  \isacommand{hence} abbreviates \isacommand{then}~\isacommand{have}.}
wenzelm@10007
   265
*}
wenzelm@7820
   266
wenzelm@10007
   267
lemma "A & B --> B & A"
wenzelm@10007
   268
proof
wenzelm@10007
   269
  assume "A & B"
wenzelm@10007
   270
  thus "B & A"
wenzelm@10007
   271
  proof
wenzelm@10007
   272
    assume A B
wenzelm@10007
   273
    show ?thesis ..
wenzelm@10007
   274
  qed
wenzelm@10007
   275
qed
wenzelm@7820
   276
wenzelm@7820
   277
wenzelm@6444
   278
wenzelm@10007
   279
subsection {* A few examples from ``Introduction to Isabelle'' *}
wenzelm@7001
   280
wenzelm@7820
   281
text {*
wenzelm@18193
   282
  We rephrase some of the basic reasoning examples of
wenzelm@18193
   283
  \cite{isabelle-intro}, using HOL rather than FOL.
wenzelm@10007
   284
*}
wenzelm@7820
   285
wenzelm@10007
   286
subsubsection {* A propositional proof *}
wenzelm@7833
   287
wenzelm@7833
   288
text {*
wenzelm@18193
   289
  We consider the proposition @{text "P \<or> P \<longrightarrow> P"}.  The proof below
wenzelm@18193
   290
  involves forward-chaining from @{text "P \<or> P"}, followed by an
wenzelm@18193
   291
  explicit case-analysis on the two \emph{identical} cases.
wenzelm@10007
   292
*}
wenzelm@6444
   293
wenzelm@10007
   294
lemma "P | P --> P"
wenzelm@10007
   295
proof
wenzelm@10007
   296
  assume "P | P"
wenzelm@10007
   297
  thus P
wenzelm@7833
   298
  proof                    -- {*
wenzelm@18193
   299
    rule @{text disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
wenzelm@10007
   300
  *}
wenzelm@10007
   301
    assume P show P .
wenzelm@10007
   302
  next
wenzelm@10007
   303
    assume P show P .
wenzelm@10007
   304
  qed
wenzelm@10007
   305
qed
wenzelm@7833
   306
wenzelm@7833
   307
text {*
wenzelm@18193
   308
  Case splits are \emph{not} hardwired into the Isar language as a
wenzelm@18193
   309
  special feature.  The \isacommand{next} command used to separate the
wenzelm@18193
   310
  cases above is just a short form of managing block structure.
wenzelm@7833
   311
wenzelm@18193
   312
  \medskip In general, applying proof methods may split up a goal into
wenzelm@18193
   313
  separate ``cases'', i.e.\ new subgoals with individual local
wenzelm@18193
   314
  assumptions.  The corresponding proof text typically mimics this by
wenzelm@18193
   315
  establishing results in appropriate contexts, separated by blocks.
wenzelm@7833
   316
wenzelm@18193
   317
  In order to avoid too much explicit parentheses, the Isar system
wenzelm@18193
   318
  implicitly opens an additional block for any new goal, the
wenzelm@18193
   319
  \isacommand{next} statement then closes one block level, opening a
wenzelm@18193
   320
  new one.  The resulting behavior is what one would expect from
wenzelm@18193
   321
  separating cases, only that it is more flexible.  E.g.\ an induction
wenzelm@18193
   322
  base case (which does not introduce local assumptions) would
wenzelm@18193
   323
  \emph{not} require \isacommand{next} to separate the subsequent step
wenzelm@18193
   324
  case.
wenzelm@7833
   325
wenzelm@18193
   326
  \medskip In our example the situation is even simpler, since the two
wenzelm@18193
   327
  cases actually coincide.  Consequently the proof may be rephrased as
wenzelm@18193
   328
  follows.
wenzelm@10007
   329
*}
wenzelm@7833
   330
wenzelm@10007
   331
lemma "P | P --> P"
wenzelm@10007
   332
proof
wenzelm@10007
   333
  assume "P | P"
wenzelm@10007
   334
  thus P
wenzelm@10007
   335
  proof
wenzelm@10007
   336
    assume P
wenzelm@10007
   337
    show P .
wenzelm@10007
   338
    show P .
wenzelm@10007
   339
  qed
wenzelm@10007
   340
qed
wenzelm@6444
   341
wenzelm@7833
   342
text {*
wenzelm@18193
   343
  Again, the rather vacuous body of the proof may be collapsed.  Thus
wenzelm@18193
   344
  the case analysis degenerates into two assumption steps, which are
wenzelm@18193
   345
  implicitly performed when concluding the single rule step of the
wenzelm@18193
   346
  double-dot proof as follows.
wenzelm@10007
   347
*}
wenzelm@7833
   348
wenzelm@10007
   349
lemma "P | P --> P"
wenzelm@10007
   350
proof
wenzelm@10007
   351
  assume "P | P"
wenzelm@10007
   352
  thus P ..
wenzelm@10007
   353
qed
wenzelm@6444
   354
wenzelm@6444
   355
wenzelm@10007
   356
subsubsection {* A quantifier proof *}
wenzelm@7833
   357
wenzelm@7833
   358
text {*
wenzelm@18193
   359
  To illustrate quantifier reasoning, let us prove @{text "(\<exists>x. P (f
wenzelm@18193
   360
  x)) \<longrightarrow> (\<exists>y. P y)"}.  Informally, this holds because any @{text a}
wenzelm@18193
   361
  with @{text "P (f a)"} may be taken as a witness for the second
wenzelm@18193
   362
  existential statement.
wenzelm@6444
   363
wenzelm@18193
   364
  The first proof is rather verbose, exhibiting quite a lot of
wenzelm@18193
   365
  (redundant) detail.  It gives explicit rules, even with some
wenzelm@18193
   366
  instantiation.  Furthermore, we encounter two new language elements:
wenzelm@18193
   367
  the \isacommand{fix} command augments the context by some new
wenzelm@18193
   368
  ``arbitrary, but fixed'' element; the \isacommand{is} annotation
wenzelm@18193
   369
  binds term abbreviations by higher-order pattern matching.
wenzelm@10007
   370
*}
wenzelm@7833
   371
wenzelm@10636
   372
lemma "(EX x. P (f x)) --> (EX y. P y)"
wenzelm@10007
   373
proof
wenzelm@10007
   374
  assume "EX x. P (f x)"
wenzelm@10636
   375
  thus "EX y. P y"
wenzelm@7833
   376
  proof (rule exE)             -- {*
wenzelm@7833
   377
    rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
wenzelm@10007
   378
  *}
wenzelm@10007
   379
    fix a
wenzelm@10007
   380
    assume "P (f a)" (is "P ?witness")
wenzelm@10007
   381
    show ?thesis by (rule exI [of P ?witness])
wenzelm@10007
   382
  qed
wenzelm@10007
   383
qed
wenzelm@6444
   384
wenzelm@7833
   385
text {*
wenzelm@18193
   386
  While explicit rule instantiation may occasionally improve
wenzelm@18193
   387
  readability of certain aspects of reasoning, it is usually quite
wenzelm@18193
   388
  redundant.  Above, the basic proof outline gives already enough
wenzelm@18193
   389
  structural clues for the system to infer both the rules and their
wenzelm@18193
   390
  instances (by higher-order unification).  Thus we may as well prune
wenzelm@18193
   391
  the text as follows.
wenzelm@10007
   392
*}
wenzelm@7833
   393
wenzelm@10636
   394
lemma "(EX x. P (f x)) --> (EX y. P y)"
wenzelm@10007
   395
proof
wenzelm@10007
   396
  assume "EX x. P (f x)"
wenzelm@10636
   397
  thus "EX y. P y"
wenzelm@10007
   398
  proof
wenzelm@10007
   399
    fix a
wenzelm@10007
   400
    assume "P (f a)"
wenzelm@10007
   401
    show ?thesis ..
wenzelm@10007
   402
  qed
wenzelm@10007
   403
qed
wenzelm@6444
   404
wenzelm@9477
   405
text {*
wenzelm@18193
   406
  Explicit @{text \<exists>}-elimination as seen above can become quite
wenzelm@18193
   407
  cumbersome in practice.  The derived Isar language element
wenzelm@18193
   408
  ``\isakeyword{obtain}'' provides a more handsome way to do
wenzelm@18193
   409
  generalized existence reasoning.
wenzelm@10007
   410
*}
wenzelm@9477
   411
wenzelm@10636
   412
lemma "(EX x. P (f x)) --> (EX y. P y)"
wenzelm@10007
   413
proof
wenzelm@10007
   414
  assume "EX x. P (f x)"
wenzelm@10636
   415
  then obtain a where "P (f a)" ..
wenzelm@10636
   416
  thus "EX y. P y" ..
wenzelm@10007
   417
qed
wenzelm@9477
   418
wenzelm@9477
   419
text {*
wenzelm@18193
   420
  Technically, \isakeyword{obtain} is similar to \isakeyword{fix} and
wenzelm@18193
   421
  \isakeyword{assume} together with a soundness proof of the
wenzelm@18193
   422
  elimination involved.  Thus it behaves similar to any other forward
wenzelm@18193
   423
  proof element.  Also note that due to the nature of general
wenzelm@18193
   424
  existence reasoning involved here, any result exported from the
wenzelm@18193
   425
  context of an \isakeyword{obtain} statement may \emph{not} refer to
wenzelm@18193
   426
  the parameters introduced there.
wenzelm@10007
   427
*}
wenzelm@9477
   428
wenzelm@9477
   429
wenzelm@6444
   430
wenzelm@10007
   431
subsubsection {* Deriving rules in Isabelle *}
wenzelm@7001
   432
wenzelm@7833
   433
text {*
wenzelm@18193
   434
  We derive the conjunction elimination rule from the corresponding
wenzelm@18193
   435
  projections.  The proof is quite straight-forward, since
wenzelm@18193
   436
  Isabelle/Isar supports non-atomic goals and assumptions fully
wenzelm@18193
   437
  transparently.
wenzelm@10007
   438
*}
wenzelm@7001
   439
wenzelm@10007
   440
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C"
wenzelm@10007
   441
proof -
wenzelm@10007
   442
  assume "A & B"
wenzelm@10007
   443
  assume r: "A ==> B ==> C"
wenzelm@10007
   444
  show C
wenzelm@10007
   445
  proof (rule r)
wenzelm@10007
   446
    show A by (rule conjunct1)
wenzelm@10007
   447
    show B by (rule conjunct2)
wenzelm@10007
   448
  qed
wenzelm@10007
   449
qed
wenzelm@7001
   450
wenzelm@7860
   451
text {*
wenzelm@18193
   452
  Note that classic Isabelle handles higher rules in a slightly
wenzelm@18193
   453
  different way.  The tactic script as given in \cite{isabelle-intro}
wenzelm@18193
   454
  for the same example of \name{conjE} depends on the primitive
wenzelm@18193
   455
  \texttt{goal} command to decompose the rule into premises and
wenzelm@18193
   456
  conclusion.  The actual result would then emerge by discharging of
wenzelm@18193
   457
  the context at \texttt{qed} time.
wenzelm@10007
   458
*}
wenzelm@7860
   459
wenzelm@10007
   460
end