# HG changeset patch
# User wenzelm
# Date 931161145 -7200
# Node ID 2650bd68c0ba43eb8c3da6ffa5132fdd3712e6c8
# Parent  cc6e50f36da84c3f9c755497de2e96c98b2cee1b
variant version;

diff -r cc6e50f36da8 -r 2650bd68c0ba src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Sun Jul 04 20:21:45 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Mon Jul 05 09:52:25 1999 +0200
@@ -12,7 +12,7 @@
 theorems [dest] = monoD;  (* FIXME [dest!!] *)
 
 text {*
- The proof of Knaster-Tarski below closely follows the presentation in
+ The proofs of Knaster-Tarski below closely follows the presentation in
  'Introduction to Lattices' and Order by Davey/Priestley, pages
  93--94.  All of their narration has been rephrased in terms of formal
  Isar language elements.  Just as many textbook-style proofs, there is
@@ -20,7 +20,7 @@
  structure.
 *};
 
-theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
+theorem KnasterTarski1: "mono f ==> EX a::'a set. f a = a";
 proof;
   let ??H = "{u. f u <= u}";
   let ??a = "Inter ??H";
@@ -47,4 +47,32 @@
 qed;
 
 
+theorem KnasterTarski2: "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;
+      assume mem: "x : ??H";
+      hence "??a <= x"; by (rule Inter_lower);
+      with mono; have "f ??a <= f x"; ..;
+      also; from mem; have "... <= x"; ..;
+      finally (order_trans); have "f ??a <= x"; .;
+    }};
+    hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
+    {{;
+      also; presume "... <= f ??a";
+      finally (order_antisym); show ??thesis; .;
+    }};
+    from mono ge; have "f (f ??a) <= f ??a"; ..;
+    hence "f ??a : ??H"; ..;
+    thus "??a <= f ??a"; by (rule Inter_lower);
+  qed;
+qed;
+
+
 end;