src/HOL/Isar_examples/KnasterTarski.thy

--- a/src/HOL/Isar_examples/KnasterTarski.thy	Sat Oct 09 23:18:01 1999 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Sat Oct 09 23:19:20 1999 +0200
@@ -13,10 +13,10 @@
 subsection {* Prose version *};
 
 text {*
- According to the book ``Introduction to Lattices and Order'' (by
- B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
- fixpoint theorem is as follows (pages 93--94).\footnote{We have
- dualized their argument, and tuned the notation a little bit.}
+ According to the book ``Introduction to Lattices and Order''
+ \cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint
+ theorem is as follows.\footnote{We have dualized their argument, and
+ tuned the notation a little bit.}
 
  \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
  complete lattice and $f \colon L \to L$ an order-preserving map.
@@ -32,14 +32,13 @@
 *};
 
 
-subsection {* Formal version *};
+subsection {* Formal versions *};
 
 text {*
- Our proof below closely follows the original presentation.  Virtually
- all of the prose narration has been rephrased in terms of formal Isar
- language elements.  Just as many textbook-style proofs, there is a
- strong bias towards forward reasoning, and little hierarchical
- structure.
+ The Isar proof below closely follows the original presentation.
+ Virtually all of the prose narration has been rephrased in terms of
+ formal Isar language elements.  Just as many textbook-style proofs,
+ there is a strong bias towards forward reasoning.
 *};
 
 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
@@ -69,4 +68,41 @@
   qed;
 qed;
 
+text {*
+ Above we have used several advanced Isar language elements, such as
+ explicit block structure and weak assumptions.  Thus we have mimicked
+ the particular way of reasoning of the original text.
+
+ In the subsequent version of the proof the order of reasoning is
+ changed to achieve structured top-down decomposition of the problem
+ at the outer level, while the small inner steps of reasoning or done
+ in a forward manner.  Note that this requires only the most basic
+ features of the Isar language.
+*};
+
+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 (rule order_antisym);
+    show ge: "f ?a <= ?a";
+    proof (rule Inter_greatest);
+      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; show "f ?a <= x"; .;
+    qed;
+    show "?a <= f ?a";
+    proof (rule Inter_lower);
+      from mono ge; have "f (f ?a) <= f ?a"; ..;
+      thus "f ?a : ?H"; ..;
+    qed;
+  qed;
+qed;
+
 end;