summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

src/HOL/Isar_examples/KnasterTarski.thy

author | wenzelm |

Thu, 01 Jul 1999 21:30:18 +0200 | |

changeset 6882 | fe4e3d26fa8f |

child 6883 | f898679685b7 |

permissions | -rw-r--r-- |

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;