# HG changeset patch
# User wenzelm
# Date 930857418 -7200
# Node ID fe4e3d26fa8f64fa771314e4f01d276fdefe1054
# Parent  91a2c8b8269af2e1bf9771813aaabc841f6f4a64
added KnasterTarski.thy;

diff -r 91a2c8b8269a -r fe4e3d26fa8f src/HOL/Isar_examples/KnasterTarski.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Thu Jul 01 21:30:18 1999 +0200
@@ -0,0 +1,55 @@
+(*  Title:      HOL/Isar_examples/KnasterTarski.thy
+    ID:         $Id$
+    Author:     Markus Wenzel, TU Muenchen
+
+Typical textbook proof example.
+*)
+
+
+theory KnasterTarski = Main:;
+
+(*
+
+text {*
+ 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).
+*};
+*)
+
+theorems [dest] = monoD;  (* FIXME [dest!!] *)
+
+
+theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
+proof;
+  let ??H = "{u. f u <= u}";
+  let ??a = "Inter ??H";
+
+  assume mono: "mono f";
+  show "f ??a = ??a";
+  proof same;
+    fix x;
+    presume mem: "x : ??H";
+    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"; .;
+    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;
+  next;
+    have "f UNIV <= UNIV"; by (rule subset_UNIV);
+    thus "UNIV : ??H"; ..;
+  qed;
+qed;
+
+
+end;
diff -r 91a2c8b8269a -r fe4e3d26fa8f src/HOL/Isar_examples/ROOT.ML
--- a/src/HOL/Isar_examples/ROOT.ML	Thu Jul 01 21:29:53 1999 +0200
+++ b/src/HOL/Isar_examples/ROOT.ML	Thu Jul 01 21:30:18 1999 +0200
@@ -11,3 +11,4 @@
 use_thy "ExprCompiler";
 use_thy "Group";
 use_thy "NatSum";
+use_thy "KnasterTarski";