src/HOL/Isar_examples/KnasterTarski.thy

added KnasterTarski.thy;

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

Typical textbook proof example.
*)


theory KnasterTarski = Main:;

(*

text {*
 The proof of Knaster-Tarski below closely follows the presentation in
 'Introduction to Lattices and Order' by Davey/Priestley, pages
 93--94.  Only one statement of their narration has not been rephrased
 in formal Isar language elements, but left as a comment.  Also note
 that Davey/Priestley do not point out non-emptyness of the set ??H,
 (which is obvious, but not vacous).
*};
*)

theorems [dest] = monoD;  (* FIXME [dest!!] *)


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 same;
    fix x;
    presume mem: "x : ??H";
    hence "??a <= x"; by (rule Inter_lower);
    with mono; have "f ??a <= f x"; ..;
    also; from mem; have "f x <= x"; ..;
    finally; have "f ??a <= x"; .;
    hence ge: "f ??a <= ??a"; by (rule Inter_greatest);
    (* text {* We now use this inequality to prove the reverse one (!)
      and thereby complete the proof that @term{??a} is a fixpoint. *};  *)
    with mono; have "f (f ??a) <= f ??a"; ..;
    hence "f ??a : ??H"; ..;
    hence "??a <= f ??a"; by (rule Inter_lower);
    also (order_antisym); note ge;
    finally; show "f ??a = ??a"; proof same;
  next;
    have "f UNIV <= UNIV"; by (rule subset_UNIV);
    thus "UNIV : ??H"; ..;
  qed;
qed;


end;