--- a/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 08 18:39:08 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 08 18:39:34 1999 +0200
@@ -12,7 +12,7 @@
theorems [dest] = monoD; (* FIXME [dest!!] *)
text {*
- The proofs of Knaster-Tarski below closely follows the presentation in
+ The proof 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 KnasterTarski1: "mono f ==> EX a::'a set. f a = a";
+theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
proof;
let ??H = "{u. f u <= u}";
let ??a = "Inter ??H";
@@ -34,34 +34,7 @@
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);
- thus ??thesis;
- proof (rule order_antisym);
- from mono ge; have "f (f ??a) <= f ??a"; ..;
- hence "f ??a : ??H"; ..;
- thus "??a <= f ??a"; by (rule Inter_lower);
- qed;
- qed;
-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"; .;
+ finally; have "f ??a <= x"; .;
}};
hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
{{;