# HG changeset patch
# User wenzelm
# Date 1238501368 -7200
# Node ID 4de62c902f9a7222b5eba6fac071d0610769f697
# Parent  e96498265a05f1a79dd0927f238f53332ca25aae
replaced 'a set by abstract 'a::complete_lattice, and recover plain reasoning instead of adhoc automation (by simp);
modernized and tuned document;

diff -r e96498265a05 -r 4de62c902f9a src/HOL/Isar_examples/KnasterTarski.thy
--- a/src/HOL/Isar_examples/KnasterTarski.thy	Tue Mar 31 13:34:48 2009 +0200
+++ b/src/HOL/Isar_examples/KnasterTarski.thy	Tue Mar 31 14:09:28 2009 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Isar_examples/KnasterTarski.thy
-    ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
 Typical textbook proof example.
@@ -7,100 +6,104 @@
 
 header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
 
-theory KnasterTarski imports Main begin
+theory KnasterTarski
+imports Main Lattice_Syntax
+begin
 
 
 subsection {* Prose version *}
 
 text {*
- According to the textbook \cite[pages 93--94]{davey-priestley}, the
- Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
- dualized the argument, and tuned the notation a little bit.}
+  According to the textbook \cite[pages 93--94]{davey-priestley}, the
+  Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
+  dualized the 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.
- Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.
+  \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let @{text L} be a
+  complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
+  Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
 
- \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =
- \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)
- \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.
- We now use this inequality to prove the reverse one (!) and thereby
- complete the proof that $a$ is a fixpoint.  Since $f$ is
- order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a
- \le f(a)$.
+  \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
+  \<Sqinter>H"}.  For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
+  "f(a) \<le> f(x) \<le> x"}.  Thus @{text "f(a)"} is a lower bound of @{text
+  H}, whence @{text "f(a) \<le> a"}.  We now use this inequality to prove
+  the reverse one (!) and thereby complete the proof that @{text a} is
+  a fixpoint.  Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
+  f(a)"}.  This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
 *}
 
 
 subsection {* Formal versions *}
 
 text {*
- 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 proof, and several bends
- in the course of reasoning.
+  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 proof, and several bends in
+  the course of reasoning.
 *}
 
-theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"
+theorem Knaster_Tarski:
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f"
+  shows "\<exists>a. f a = a"
 proof
-  let ?H = "{u. f u <= u}"
-  let ?a = "Inter ?H"
-
-  assume mono: "mono f"
+  let ?H = "{u. f u \<le> u}"
+  let ?a = "\<Sqinter>?H"
   show "f ?a = ?a"
   proof -
     {
       fix x
-      assume H: "x : ?H"
-      hence "?a <= x" by (rule Inter_lower)
-      with mono have "f ?a <= f x" ..
-      also from H have "... <= x" ..
-      finally have "f ?a <= x" .
+      assume "x \<in> ?H"
+      then have "?a \<le> x" by (rule Inf_lower)
+      with `mono f` have "f ?a \<le> f x" ..
+      also from `x \<in> ?H` have "\<dots> \<le> x" ..
+      finally have "f ?a \<le> x" .
     }
-    hence ge: "f ?a <= ?a" by (rule Inter_greatest)
+    then have "f ?a \<le> ?a" by (rule Inf_greatest)
     {
-      also presume "... <= f ?a"
+      also presume "\<dots> \<le> f ?a"
       finally (order_antisym) show ?thesis .
     }
-    from mono ge have "f (f ?a) <= f ?a" ..
-    hence "f ?a : ?H" by simp
-    thus "?a <= f ?a" by (rule Inter_lower)
+    from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+    then have "f ?a \<in> ?H" ..
+    then show "?a \<le> f ?a" by (rule Inf_lower)
   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.
+  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 the order of reasoning is changed to
- achieve structured top-down decomposition of the problem at the outer
- level, while only the inner steps of reasoning are done in a forward
- manner.  We are certainly more at ease here, requiring only the most
- basic features of the Isar language.
+  In the subsequent version the order of reasoning is changed to
+  achieve structured top-down decomposition of the problem at the
+  outer level, while only the inner steps of reasoning are done in a
+  forward manner.  We are certainly more at ease here, requiring only
+  the most basic features of the Isar language.
 *}
 
-theorem KnasterTarski': "mono f ==> EX a::'a set. f a = a"
+theorem Knaster_Tarski':
+  fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
+  assumes "mono f"
+  shows "\<exists>a. f a = a"
 proof
-  let ?H = "{u. f u <= u}"
-  let ?a = "Inter ?H"
-
-  assume mono: "mono f"
+  let ?H = "{u. f u \<le> u}"
+  let ?a = "\<Sqinter>?H"
   show "f ?a = ?a"
   proof (rule order_antisym)
-    show ge: "f ?a <= ?a"
-    proof (rule Inter_greatest)
+    show "f ?a \<le> ?a"
+    proof (rule Inf_greatest)
       fix x
-      assume H: "x : ?H"
-      hence "?a <= x" by (rule Inter_lower)
-      with mono have "f ?a <= f x" ..
-      also from H have "... <= x" ..
-      finally show "f ?a <= x" .
+      assume "x \<in> ?H"
+      then have "?a \<le> x" by (rule Inf_lower)
+      with `mono f` have "f ?a \<le> f x" ..
+      also from `x \<in> ?H` have "\<dots> \<le> x" ..
+      finally show "f ?a \<le> x" .
     qed
-    show "?a <= f ?a"
-    proof (rule Inter_lower)
-      from mono ge have "f (f ?a) <= f ?a" ..
-      thus "f ?a : ?H" by simp
+    show "?a \<le> f ?a"
+    proof (rule Inf_lower)
+      from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
+      then show "f ?a \<in> ?H" ..
     qed
   qed
 qed