src/HOL/Isar_examples/BasicLogic.thy
author wenzelm
Fri Oct 15 16:44:37 1999 +0200 (1999-10-15)
changeset 7874 180364256231
parent 7860 7819547df4d8
child 7982 d534b897ce39
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@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@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@7860
    72
 remaining goals by assumption\footnote{This is not a completely
wenzelm@7874
    73
 trivial operation, as proof by assumption involves full higher-order
wenzelm@7874
    74
 unification.}.  Thus we may skip the rather vacuous body of the above
wenzelm@7874
    75
 proof as well.
wenzelm@7820
    76
*};
wenzelm@7820
    77
wenzelm@7820
    78
lemma "A --> A";
wenzelm@7820
    79
proof;
wenzelm@7820
    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@7820
    88
*};
wenzelm@7820
    89
wenzelm@7820
    90
lemma "A --> A";
wenzelm@7820
    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@7820
    95
*};
wenzelm@7820
    96
wenzelm@7820
    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@7860
   102
 the rule is implication introduction.}
wenzelm@7820
   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@7820
   113
*};
wenzelm@7820
   114
wenzelm@7820
   115
lemma "A --> B --> A";
wenzelm@7820
   116
proof intro;
wenzelm@7820
   117
  assume A;
wenzelm@7820
   118
  show A; .;
wenzelm@7820
   119
qed;
wenzelm@7820
   120
wenzelm@7820
   121
text {*
wenzelm@7820
   122
 Again, the body may be collapsed.
wenzelm@7820
   123
*};
wenzelm@7820
   124
wenzelm@7820
   125
lemma "A --> B --> A";
wenzelm@7820
   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@7820
   132
 rule application, this may go too far in 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@7820
   143
*};
wenzelm@7820
   144
wenzelm@7820
   145
wenzelm@7820
   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@7820
   157
*};
wenzelm@7001
   158
wenzelm@6444
   159
lemma "A & B --> B & A";
wenzelm@6444
   160
proof;
wenzelm@6444
   161
  assume "A & B";
wenzelm@6444
   162
  show "B & A";
wenzelm@6444
   163
  proof;
wenzelm@6444
   164
    show B; by (rule conjunct2);
wenzelm@6444
   165
    show A; by (rule conjunct1);
wenzelm@6444
   166
  qed;
wenzelm@6444
   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@7820
   171
 explicitly, since the goals did not provide any structural clue.
wenzelm@7820
   172
 This may be avoided using \isacommand{from} to focus on $\idt{prems}$
wenzelm@7820
   173
 (i.e.\ the $A \conj B$ assumption) as the current facts, enabling the
wenzelm@7820
   174
 use of double-dot proofs.  Note that \isacommand{from} already
wenzelm@7833
   175
 does forward-chaining, involving the \name{conjE} rule.
wenzelm@7820
   176
*};
wenzelm@6444
   177
wenzelm@6444
   178
lemma "A & B --> B & A";
wenzelm@6444
   179
proof;
wenzelm@7604
   180
  assume "A & B";
wenzelm@7604
   181
  show "B & A";
wenzelm@7604
   182
  proof;
wenzelm@7604
   183
    from prems; show B; ..;
wenzelm@7604
   184
    from prems; show A; ..;
wenzelm@7604
   185
  qed;
wenzelm@7604
   186
qed;
wenzelm@7604
   187
wenzelm@7820
   188
text {*
wenzelm@7820
   189
 In the next version, we move the forward step one level upwards.
wenzelm@7820
   190
 Forward-chaining from the most recent facts is indicated by the
wenzelm@7820
   191
 \isacommand{then} command.  Thus the proof of $B \conj A$ from $A
wenzelm@7820
   192
 \conj B$ actually becomes an elimination, rather than an
wenzelm@7820
   193
 introduction.  The resulting proof structure directly corresponds to
wenzelm@7820
   194
 that of the $\name{conjE}$ rule, including the repeated goal
wenzelm@7820
   195
 proposition that is abbreviated as $\var{thesis}$ below.
wenzelm@7820
   196
*};
wenzelm@7820
   197
wenzelm@7820
   198
lemma "A & B --> B & A";
wenzelm@7820
   199
proof;
wenzelm@7820
   200
  assume "A & B";
wenzelm@7820
   201
  then; show "B & A";
wenzelm@7820
   202
  proof                    -- {* rule \name{conjE} of $A \conj B$ *};
wenzelm@7820
   203
    assume A B;
wenzelm@7820
   204
    show ?thesis; ..       -- {* rule \name{conjI} of $B \conj A$ *};
wenzelm@7820
   205
  qed;
wenzelm@7820
   206
qed;
wenzelm@7820
   207
wenzelm@7820
   208
text {*
wenzelm@7874
   209
 In the subsequent version we flatten the structure of the main body
wenzelm@7874
   210
 by doing forward reasoning all the time.  Only the outermost
wenzelm@7874
   211
 decomposition step is left as backward.
wenzelm@7820
   212
*};
wenzelm@7820
   213
wenzelm@7604
   214
lemma "A & B --> B & A";
wenzelm@7604
   215
proof;
wenzelm@6892
   216
  assume ab: "A & B";
wenzelm@6892
   217
  from ab; have a: A; ..;
wenzelm@6892
   218
  from ab; have b: B; ..;
wenzelm@6892
   219
  from b a; show "B & A"; ..;
wenzelm@6444
   220
qed;
wenzelm@6444
   221
wenzelm@7820
   222
text {*
wenzelm@7833
   223
 We can still push forward reasoning a bit further, even at the risk
wenzelm@7820
   224
 of getting ridiculous.  Note that we force the initial proof step to
wenzelm@7820
   225
 do nothing, by referring to the ``-'' proof method.
wenzelm@7820
   226
*};
wenzelm@7820
   227
wenzelm@7820
   228
lemma "A & B --> B & A";
wenzelm@7820
   229
proof -;
wenzelm@7820
   230
  {{;
wenzelm@7820
   231
    assume ab: "A & B";
wenzelm@7820
   232
    from ab; have a: A; ..;
wenzelm@7820
   233
    from ab; have b: B; ..;
wenzelm@7820
   234
    from b a; have "B & A"; ..;
wenzelm@7820
   235
  }};
wenzelm@7820
   236
  thus ?thesis; ..         -- {* rule \name{impI} *};
wenzelm@7820
   237
qed;
wenzelm@7820
   238
wenzelm@7820
   239
text {*
wenzelm@7820
   240
 \medskip With these examples we have shifted through a whole range
wenzelm@7820
   241
 from purely backward to purely forward reasoning.  Apparently, in the
wenzelm@7820
   242
 extreme ends we get slightly ill-structured proofs, which also
wenzelm@7820
   243
 require much explicit naming of either rules (backward) or local
wenzelm@7820
   244
 facts (forward).
wenzelm@7820
   245
wenzelm@7820
   246
 The general lesson learned here is that good proof style would
wenzelm@7820
   247
 achieve just the \emph{right} balance of top-down backward
wenzelm@7820
   248
 decomposition, and bottom-up forward composition.  In practice, there
wenzelm@7820
   249
 is no single best way to arrange some pieces of formal reasoning, of
wenzelm@7820
   250
 course.  Depending on the actual applications, the intended audience
wenzelm@7874
   251
 etc., rules (and methods) on the one hand vs.\ facts on the other
wenzelm@7874
   252
 hand have to be emphasized in an appropriate way.  This requires the
wenzelm@7874
   253
 proof writer to develop good taste, and some practice, of course.
wenzelm@7820
   254
*};
wenzelm@7820
   255
wenzelm@7820
   256
text {*
wenzelm@7820
   257
 For our example the most appropriate way of reasoning is probably the
wenzelm@7820
   258
 middle one, with conjunction introduction done after elimination.
wenzelm@7820
   259
 This reads even more concisely using \isacommand{thus}, which
wenzelm@7820
   260
 abbreviates \isacommand{then}~\isacommand{show}.\footnote{In the same
wenzelm@7820
   261
 vein, \isacommand{hence} abbreviates
wenzelm@7820
   262
 \isacommand{then}~\isacommand{have}.}
wenzelm@7820
   263
*};
wenzelm@7820
   264
wenzelm@7820
   265
lemma "A & B --> B & A";
wenzelm@7820
   266
proof;
wenzelm@7820
   267
  assume "A & B";
wenzelm@7820
   268
  thus "B & A";
wenzelm@7820
   269
  proof;
wenzelm@7820
   270
    assume A B;
wenzelm@7820
   271
    show ?thesis; ..;
wenzelm@7820
   272
  qed;
wenzelm@7820
   273
qed;
wenzelm@7820
   274
wenzelm@7820
   275
wenzelm@6444
   276
wenzelm@7740
   277
subsection {* A few examples from ``Introduction to Isabelle'' *};
wenzelm@7001
   278
wenzelm@7820
   279
text {*
wenzelm@7820
   280
 We rephrase some of the basic reasoning examples of
wenzelm@7833
   281
 \cite{isabelle-intro} (using HOL rather than FOL).
wenzelm@7820
   282
*};
wenzelm@7820
   283
wenzelm@7833
   284
subsubsection {* A propositional proof *};
wenzelm@7833
   285
wenzelm@7833
   286
text {*
wenzelm@7833
   287
 We consider the proposition $P \disj P \impl P$.  The proof below
wenzelm@7833
   288
 involves forward-chaining from $P \disj P$, followed by an explicit
wenzelm@7833
   289
 case-analysis on the two \emph{identical} cases.
wenzelm@7833
   290
*};
wenzelm@6444
   291
wenzelm@6444
   292
lemma "P | P --> P";
wenzelm@6444
   293
proof;
wenzelm@6444
   294
  assume "P | P";
wenzelm@7833
   295
  thus P;
wenzelm@7833
   296
  proof                    -- {*
wenzelm@7833
   297
    rule \name{disjE}: \smash{$\infer{C}{A \disj B & \infer*{C}{[A]} & \infer*{C}{[B]}}$}
wenzelm@7833
   298
  *};
wenzelm@7833
   299
    assume P; show P; .;
wenzelm@7833
   300
  next;
wenzelm@7833
   301
    assume P; show P; .;
wenzelm@7833
   302
  qed;
wenzelm@7833
   303
qed;
wenzelm@7833
   304
wenzelm@7833
   305
text {*
wenzelm@7833
   306
 Case splits are \emph{not} hardwired into the Isar language as a
wenzelm@7833
   307
 special feature.  The \isacommand{next} command used to separate the
wenzelm@7833
   308
 cases above is just a short form of managing block structure.
wenzelm@7833
   309
wenzelm@7833
   310
 \medskip In general, applying proof methods may split up a goal into
wenzelm@7833
   311
 separate ``cases'', i.e.\ new subgoals with individual local
wenzelm@7833
   312
 assumptions.  The corresponding proof text typically mimics this by
wenzelm@7833
   313
 establishing results in appropriate contexts, separated by blocks.
wenzelm@7833
   314
wenzelm@7860
   315
 In order to avoid too much explicit parentheses, the Isar system
wenzelm@7833
   316
 implicitly opens an additional block for any new goal, the
wenzelm@7833
   317
 \isacommand{next} statement then closes one block level, opening a
wenzelm@7833
   318
 new one.  The resulting behavior is what one might expect from
wenzelm@7833
   319
 separating cases, only that it is more flexible.  E.g. an induction
wenzelm@7833
   320
 base case (which does not introduce local assumptions) would
wenzelm@7833
   321
 \emph{not} require \isacommand{next} to separate the subsequent step
wenzelm@7833
   322
 case.
wenzelm@7833
   323
wenzelm@7833
   324
 \medskip In our example the situation is even simpler, since the two
wenzelm@7874
   325
 cases actually coincide.  Consequently the proof may be rephrased as
wenzelm@7874
   326
 follows.
wenzelm@7833
   327
*};
wenzelm@7833
   328
wenzelm@7833
   329
lemma "P | P --> P";
wenzelm@7833
   330
proof;
wenzelm@7833
   331
  assume "P | P";
wenzelm@7833
   332
  thus P;
wenzelm@6444
   333
  proof;
wenzelm@6444
   334
    assume P;
wenzelm@6444
   335
    show P; .;
wenzelm@6444
   336
    show P; .;
wenzelm@6444
   337
  qed;
wenzelm@6444
   338
qed;
wenzelm@6444
   339
wenzelm@7833
   340
text {*
wenzelm@7833
   341
 Again, the rather vacuous body of the proof may be collapsed.  Thus
wenzelm@7860
   342
 the case analysis degenerates into two assumption steps, which are
wenzelm@7860
   343
 implicitly performed when concluding the single rule step of the
wenzelm@7860
   344
 double-dot proof as follows.
wenzelm@7833
   345
*};
wenzelm@7833
   346
wenzelm@6444
   347
lemma "P | P --> P";
wenzelm@6444
   348
proof;
wenzelm@6444
   349
  assume "P | P";
wenzelm@7833
   350
  thus P; ..;
wenzelm@6444
   351
qed;
wenzelm@6444
   352
wenzelm@6444
   353
wenzelm@7833
   354
subsubsection {* A quantifier proof *};
wenzelm@7833
   355
wenzelm@7833
   356
text {*
wenzelm@7833
   357
 To illustrate quantifier reasoning, let us prove $(\ex x P \ap (f \ap
wenzelm@7833
   358
 x)) \impl (\ex x P \ap x)$.  Informally, this holds because any $a$
wenzelm@7833
   359
 with $P \ap (f \ap a)$ may be taken as a witness for the second
wenzelm@7833
   360
 existential statement.
wenzelm@6444
   361
wenzelm@7833
   362
 The first proof is rather verbose, exhibiting quite a lot of
wenzelm@7833
   363
 (redundant) detail.  It gives explicit rules, even with some
wenzelm@7833
   364
 instantiation.  Furthermore, we encounter two new language elements:
wenzelm@7833
   365
 the \isacommand{fix} command augments the context by some new
wenzelm@7833
   366
 ``arbitrary, but fixed'' element; the \isacommand{is} annotation
wenzelm@7833
   367
 binds term abbreviations by higher-order pattern matching.
wenzelm@7833
   368
*};
wenzelm@7833
   369
wenzelm@7833
   370
lemma "(EX x. P (f x)) --> (EX x. P x)";
wenzelm@6444
   371
proof;
wenzelm@7833
   372
  assume "EX x. P (f x)";
wenzelm@7833
   373
  thus "EX x. P x";
wenzelm@7833
   374
  proof (rule exE)             -- {*
wenzelm@7833
   375
    rule \name{exE}: \smash{$\infer{B}{\ex x A(x) & \infer*{B}{[A(x)]_x}}$}
wenzelm@7833
   376
  *};
wenzelm@6444
   377
    fix a;
wenzelm@7833
   378
    assume "P (f a)" (is "P ?witness");
wenzelm@7480
   379
    show ?thesis; by (rule exI [of P ?witness]);
wenzelm@6444
   380
  qed;
wenzelm@6444
   381
qed;
wenzelm@6444
   382
wenzelm@7833
   383
text {*
wenzelm@7833
   384
 While explicit rule instantiation may occasionally help to improve
wenzelm@7860
   385
 the readability of certain aspects of reasoning, it is usually quite
wenzelm@7833
   386
 redundant.  Above, the basic proof outline gives already enough
wenzelm@7833
   387
 structural clues for the system to infer both the rules and their
wenzelm@7833
   388
 instances (by higher-order unification).  Thus we may as well prune
wenzelm@7833
   389
 the text as follows.
wenzelm@7833
   390
*};
wenzelm@7833
   391
wenzelm@7833
   392
lemma "(EX x. P (f x)) --> (EX x. P x)";
wenzelm@6444
   393
proof;
wenzelm@7833
   394
  assume "EX x. P (f x)";
wenzelm@7833
   395
  thus "EX x. P x";
wenzelm@6444
   396
  proof;
wenzelm@6444
   397
    fix a;
wenzelm@7833
   398
    assume "P (f a)";
wenzelm@7480
   399
    show ?thesis; ..;
wenzelm@6444
   400
  qed;
wenzelm@6444
   401
qed;
wenzelm@6444
   402
wenzelm@6444
   403
wenzelm@7740
   404
subsubsection {* Deriving rules in Isabelle *};
wenzelm@7001
   405
wenzelm@7833
   406
text {*
wenzelm@7833
   407
 We derive the conjunction elimination rule from the projections.  The
wenzelm@7860
   408
 proof is quite straight-forward, since Isabelle/Isar supports
wenzelm@7860
   409
 non-atomic goals and assumptions fully transparently.
wenzelm@7833
   410
*};
wenzelm@7001
   411
wenzelm@7001
   412
theorem conjE: "A & B ==> (A ==> B ==> C) ==> C";
wenzelm@7133
   413
proof -;
wenzelm@7833
   414
  assume "A & B";
wenzelm@7001
   415
  assume ab_c: "A ==> B ==> C";
wenzelm@7001
   416
  show C;
wenzelm@7001
   417
  proof (rule ab_c);
wenzelm@7833
   418
    show A; by (rule conjunct1);
wenzelm@7833
   419
    show B; by (rule conjunct2);
wenzelm@7001
   420
  qed;
wenzelm@7001
   421
qed;
wenzelm@7001
   422
wenzelm@7860
   423
text {*
wenzelm@7860
   424
 Note that classic Isabelle handles higher rules in a slightly
wenzelm@7860
   425
 different way.  The tactic script as given in \cite{isabelle-intro}
wenzelm@7860
   426
 for the same example of \name{conjE} depends on the primitive
wenzelm@7860
   427
 \texttt{goal} command to decompose the rule into premises and
wenzelm@7860
   428
 conclusion.  The proper result would then emerge by discharging of
wenzelm@7860
   429
 the context at \texttt{qed} time.
wenzelm@7860
   430
*};
wenzelm@7860
   431
wenzelm@6444
   432
end;