# HG changeset patch
# User wenzelm
# Date 931112505 -7200
# Node ID cc6e50f36da84c3f9c755497de2e96c98b2cee1b
# Parent  4bdc3600ddae2b4bbc8024cb391fbe333affbb0c
fixed scope of x:??H;
improved final reasoning: fully formal now;

diff -r 4bdc3600ddae -r cc6e50f36da8 src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Sun Jul 04 20:20:36 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sun Jul 04 20:21:45 1999 +0200
@@ -15,40 +15,34 @@
  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, 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.
+ Isar language elements.  Just as many textbook-style proofs, there is
+ a strong bias towards forward reasoning, and 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";
 
-  have "f UNIV <= UNIV"; by (rule subset_UNIV);
-  hence "UNIV : ??H"; ..;
-  thus "f ??a = ??a";
+  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"; .;
+    {{;
+      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);
-    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 (order_antisym); show "f ??a = ??a"; by (rule sym);
+    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;