# HG changeset patch # User wenzelm # Date 930860458 -7200 # Node ID f898679685b76a954a66c78cfcd7895ca5b45855 # Parent fe4e3d26fa8f64fa771314e4f01d276fdefe1054 fixed order_trans; diff -r fe4e3d26fa8f -r f898679685b7 src/HOL/Isar_examples/KnasterTarski.thy --- a/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 01 21:30:18 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 01 22:20:58 1999 +0200 @@ -8,21 +8,18 @@ theory KnasterTarski = Main:; -(* + +theorems [dest] = monoD; (* FIXME [dest!!] *) -text {* +(* The proof of Knaster-Tarski below closely follows the presentation in - 'Introduction to Lattices and Order' by Davey/Priestley, pages + '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). -*}; *) -theorems [dest] = monoD; (* FIXME [dest!!] *) - - theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; proof; let ??H = "{u. f u <= u}"; @@ -36,15 +33,15 @@ hence "??a <= x"; by (rule Inter_lower); with mono; have "f ??a <= f x"; ..; also; from mem; have "f x <= x"; ..; - finally; have "f ??a <= 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. *}; *) with mono; have "f (f ??a) <= f ??a"; ..; hence "f ??a : ??H"; ..; hence "??a <= f ??a"; by (rule Inter_lower); - also (order_antisym); note ge; - finally; show "f ??a = ??a"; proof same; + also; note ge; + finally; show "f ??a = ??a"; by (rule sym); next; have "f UNIV <= UNIV"; by (rule subset_UNIV); thus "UNIV : ??H"; ..;