src/HOL/WF.ML
 changeset 5330 8c9fadda81f4 parent 5318 72bf8039b53f child 5337 2f7d09a927c4
```     1.1 --- a/src/HOL/WF.ML	Tue Aug 18 10:24:09 1998 +0200
1.2 +++ b/src/HOL/WF.ML	Tue Aug 18 10:24:54 1998 +0200
1.3 @@ -136,6 +136,21 @@
1.4   * Wellfoundedness of `disjoint union'
1.5   *---------------------------------------------------------------------------*)
1.6
1.7 +(*Intuition behind this proof for the case of binary union:
1.8 +
1.9 +  Goal: find an (R u S)-min element of a nonempty subset A.
1.10 +  by case distinction:
1.11 +  1. There is a step a -R-> b with a,b : A.
1.12 +     Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}.
1.13 +     By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the
1.14 +     subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot
1.15 +     have an S-successor and is thus S-min in A as well.
1.16 +  2. There is no such step.
1.17 +     Pick an S-min element of A. In this case it must be an R-min
1.18 +     element of A as well.
1.19 +
1.20 +*)
1.21 +
1.22  Goal "[| !i:I. wf(r i); \
1.23  \        !i:I.!j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \
1.24  \                                  Domain(r j) Int Range(r i) = {} \
```