author wenzelm Mon, 05 Jul 1999 09:52:25 +0200 changeset 6898 2650bd68c0ba parent 6897 cc6e50f36da8 child 6899 020314dadebd
variant version;
```--- 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;```