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;