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