equal
deleted
inserted
replaced
5 |
5 |
6 The Knaster-Tarski Theorem for greatest fixed points. |
6 The Knaster-Tarski Theorem for greatest fixed points. |
7 *) |
7 *) |
8 |
8 |
9 (*** Proof of Knaster-Tarski Theorem using gfp ***) |
9 (*** Proof of Knaster-Tarski Theorem using gfp ***) |
|
10 |
|
11 val gfp_def = thm "gfp_def"; |
10 |
12 |
11 (* gfp(f) is the least upper bound of {u. u <= f(u)} *) |
13 (* gfp(f) is the least upper bound of {u. u <= f(u)} *) |
12 |
14 |
13 Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)"; |
15 Goalw [gfp_def] "[| X <= f(X) |] ==> X <= gfp(f)"; |
14 by (etac (CollectI RS Union_upper) 1); |
16 by (etac (CollectI RS Union_upper) 1); |