summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Fri, 02 Jul 1999 15:04:12 +0200 | |

changeset 6884 | a05159fbead0 |

parent 6883 | f898679685b7 |

child 6885 | 1dcac1789759 |

tuned;

--- a/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 01 22:20:58 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Fri Jul 02 15:04:12 1999 +0200 @@ -14,37 +14,41 @@ (* The proof of Knaster-Tarski below closely follows the presentation in 'Introduction to Lattices' and Order by Davey/Priestley, pages - 93--94. Only one statement of their narration has not been rephrased - in formal Isar language elements, but left as a comment. Also note - that Davey/Priestley do not point out non-emptyness of the set ??H, - (which is obvious, but not vacous). + 93--94. All of their narration has been rephrased in terms of formal + Isar language elements, except one stament only that has been left as + a comment. Also note that Davey/Priestley do not point out + non-emptyness of the set @term{??H}, (which is obvious, but not + vacous). + + Just as many textbook-style proofs, there is a strong bias towards + forward reasoning, with little hierarchical structure. *) theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; proof; + assume mono: "mono f"; + let ??H = "{u. f u <= u}"; let ??a = "Inter ??H"; - assume mono: "mono f"; - show "f ??a = ??a"; + have "f UNIV <= UNIV"; by (rule subset_UNIV); + hence "UNIV : ??H"; ..; + thus "f ??a = ??a"; proof same; fix x; - presume mem: "x : ??H"; + assume mem: "x : ??H"; hence "??a <= x"; by (rule Inter_lower); with mono; have "f ??a <= f x"; ..; - also; from mem; have "f x <= x"; ..; + also; from mem; have "... <= x"; ..; finally (order_trans); have "f ??a <= x"; .; hence ge: "f ??a <= ??a"; by (rule Inter_greatest); - (* text {* We now use this inequality to prove the reverse one (!) - and thereby complete the proof that @term{??a} is a fixpoint. *}; *) + txt {* We now use this inequality to prove the reverse one (!) + and thereby complete the proof that @term{??a} is a fixpoint. *}; with mono; have "f (f ??a) <= f ??a"; ..; hence "f ??a : ??H"; ..; hence "??a <= f ??a"; by (rule Inter_lower); also; note ge; - finally; show "f ??a = ??a"; by (rule sym); - next; - have "f UNIV <= UNIV"; by (rule subset_UNIV); - thus "UNIV : ??H"; ..; + finally (order_antisym); show "f ??a = ??a"; by (rule sym); qed; qed;