src/HOL/Isar_examples/KnasterTarski.thy
 author wenzelm Wed Oct 06 18:50:51 1999 +0200 (1999-10-06) changeset 7761 7fab9592384f parent 7480 0a0e0dbe1269 child 7818 1acfb8cc3720 permissions -rw-r--r--
improved presentation;
     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 header {* Textbook-style reasoning: the Knaster-Tarski Theorem *};

     9

    10 theory KnasterTarski = Main:;

    11

    12

    13 subsection {* Prose version *};

    14

    15 text {*

    16  According to the book Introduction to Lattices and Order'' (by

    17  B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski

    18  fixpoint theorem is as follows (pages 93--94).\footnote{We have

    19  dualized their argument, and tuned the notation a little bit.}

    20

    21  \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a

    22  complete lattice and $f \colon L \to L$ an order-preserving map.

    23  Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.

    24

    25  \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =   26 \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)   27 \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.

    28  We now use this inequality to prove the reverse one (!) and thereby

    29  complete the proof that $a$ is a fixpoint.  Since $f$ is

    30  order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a   31 \le f(a)$.

    32 *};

    33

    34

    35 subsection {* Formal version *};

    36

    37 text {*

    38  Our proof below closely follows the original presentation.  Virtually

    39  all of the prose narration has been rephrased in terms of formal Isar

    40  language elements.  Just as many textbook-style proofs, there is a

    41  strong bias towards forward reasoning, and little hierarchical

    42  structure.

    43 *};

    44

    45 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";

    46 proof;

    47   let ?H = "{u. f u <= u}";

    48   let ?a = "Inter ?H";

    49

    50   assume mono: "mono f";

    51   show "f ?a = ?a";

    52   proof -;

    53     {{;

    54       fix x;

    55       assume mem: "x : ?H";

    56       hence "?a <= x"; by (rule Inter_lower);

    57       with mono; have "f ?a <= f x"; ..;

    58       also; from mem; have "... <= x"; ..;

    59       finally; have "f ?a <= x"; .;

    60     }};

    61     hence ge: "f ?a <= ?a"; by (rule Inter_greatest);

    62     {{;

    63       also; presume "... <= f ?a";

    64       finally (order_antisym); show ?thesis; .;

    65     }};

    66     from mono ge; have "f (f ?a) <= f ?a"; ..;

    67     hence "f ?a : ?H"; ..;

    68     thus "?a <= f ?a"; by (rule Inter_lower);

    69   qed;

    70 qed;

    71

    72 end;