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;
```