src/HOL/Isar_examples/KnasterTarski.thy
 author wenzelm Sat Sep 04 21:13:01 1999 +0200 (1999-09-04) changeset 7480 0a0e0dbe1269 parent 7253 a494a78fea39 child 7761 7fab9592384f permissions -rw-r--r--
replaced ?? by ?;
 wenzelm@6882  1 (* Title: HOL/Isar_examples/KnasterTarski.thy  wenzelm@6882  2  ID: $Id$  wenzelm@6882  3  Author: Markus Wenzel, TU Muenchen  wenzelm@6882  4 wenzelm@6882  5 Typical textbook proof example.  wenzelm@6882  6 *)  wenzelm@6882  7 wenzelm@6882  8 wenzelm@6882  9 theory KnasterTarski = Main:;  wenzelm@6882  10 wenzelm@7153  11 text {*  wenzelm@7153  12  According to the book Introduction to Lattices and Order'' (by  wenzelm@7153  13  B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski  wenzelm@7153  14  fixpoint theorem is as follows (pages 93--94). Note that we have  wenzelm@7153  15  dualized their argument, and tuned the notation a little bit.  wenzelm@7153  16 wenzelm@7153  17  \paragraph{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a  wenzelm@7153  18  complete lattice and $f \colon L \to L$ an order-preserving map.  wenzelm@7153  19  Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.  wenzelm@7153  20 wenzelm@7153  21  \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =  wenzelm@7153  22  \bigwedge H$. For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)  wenzelm@7153  23  \le x$. Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.  wenzelm@7153  24  We now use this inequality to prove the reverse one (!) and thereby  wenzelm@7153  25  complete the proof that $a$ is a fixpoint. Since $f$ is  wenzelm@7153  26  order-preserving, $f(f(a)) \le f(a)$. This says $f(a) \in H$, so $a  wenzelm@7153  27  \le f(a)$.  wenzelm@7153  28 *};  wenzelm@6883  29 wenzelm@6893  30 text {*  wenzelm@7153  31  Our proof below closely follows this presentation. Virtually all of  wenzelm@7153  32  the prose narration has been rephrased in terms of formal Isar  wenzelm@7153  33  language elements. Just as many textbook-style proofs, there is a  wenzelm@7153  34  strong bias towards forward reasoning, and little hierarchical  wenzelm@6897  35  structure.  wenzelm@6893  36 *};  wenzelm@6882  37 wenzelm@6939  38 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";  wenzelm@6882  39 proof;  wenzelm@7480  40  let ?H = "{u. f u <= u}";  wenzelm@7480  41  let ?a = "Inter ?H";  wenzelm@6882  42 wenzelm@6897  43  assume mono: "mono f";  wenzelm@7480  44  show "f ?a = ?a";  wenzelm@7133  45  proof -;  wenzelm@6897  46  {{;  wenzelm@6897  47  fix x;  wenzelm@7480  48  assume mem: "x : ?H";  wenzelm@7480  49  hence "?a <= x"; by (rule Inter_lower);  wenzelm@7480  50  with mono; have "f ?a <= f x"; ..;  wenzelm@6897  51  also; from mem; have "... <= x"; ..;  wenzelm@7480  52  finally; have "f ?a <= x"; .;  wenzelm@6898  53  }};  wenzelm@7480  54  hence ge: "f ?a <= ?a"; by (rule Inter_greatest);  wenzelm@6898  55  {{;  wenzelm@7480  56  also; presume "... <= f ?a";  wenzelm@7480  57  finally (order_antisym); show ?thesis; .;  wenzelm@6898  58  }};  wenzelm@7480  59  from mono ge; have "f (f ?a) <= f ?a"; ..;  wenzelm@7480  60  hence "f ?a : ?H"; ..;  wenzelm@7480  61  thus "?a <= f ?a"; by (rule Inter_lower);  wenzelm@6898  62  qed;  wenzelm@6898  63 qed;  wenzelm@6898  64 wenzelm@6898  65 wenzelm@6882  66 end;