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