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;