src/HOL/Isar_examples/KnasterTarski.thy

improved presentation;

(*  Title:      HOL/Isar_examples/KnasterTarski.thy
    ID:         $Id$
    Author:     Markus Wenzel, TU Muenchen

Typical textbook proof example.
*)

header {* Textbook-style reasoning: the Knaster-Tarski Theorem *};

theory KnasterTarski = Main:;


subsection {* Prose version *};

text {*
 According to the book ``Introduction to Lattices and Order'' (by
 B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski
 fixpoint theorem is as follows (pages 93--94).\footnote{We have
 dualized their argument, and tuned the notation a little bit.}

 \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.}  Let $L$ be a
 complete lattice and $f \colon L \to L$ an order-preserving map.
 Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.

 \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =
 \bigwedge H$.  For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)
 \le x$.  Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.
 We now use this inequality to prove the reverse one (!) and thereby
 complete the proof that $a$ is a fixpoint.  Since $f$ is
 order-preserving, $f(f(a)) \le f(a)$.  This says $f(a) \in H$, so $a
 \le f(a)$.
*};


subsection {* Formal version *};

text {*
 Our proof below closely follows the original presentation.  Virtually
 all of the prose narration has been rephrased in terms of formal Isar
 language elements.  Just as many textbook-style proofs, there is a
 strong bias towards forward reasoning, and little hierarchical
 structure.
*};

theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";
proof;
  let ?H = "{u. f u <= u}";
  let ?a = "Inter ?H";

  assume mono: "mono f";
  show "f ?a = ?a";
  proof -;
    {{;
      fix x;
      assume mem: "x : ?H";
      hence "?a <= x"; by (rule Inter_lower);
      with mono; have "f ?a <= f x"; ..;
      also; from mem; have "... <= x"; ..;
      finally; have "f ?a <= x"; .;
    }};
    hence ge: "f ?a <= ?a"; by (rule Inter_greatest);
    {{;
      also; presume "... <= f ?a";
      finally (order_antisym); show ?thesis; .;
    }};
    from mono ge; have "f (f ?a) <= f ?a"; ..;
    hence "f ?a : ?H"; ..;
    thus "?a <= f ?a"; by (rule Inter_lower);
  qed;
qed;

end;