summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

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

changeset 6882 | fe4e3d26fa8f |

parent 6881 | 91a2c8b8269a |

child 6883 | f898679685b7 |

added KnasterTarski.thy;

src/HOL/Isar_examples/KnasterTarski.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_examples/ROOT.ML | file | annotate | diff | comparison | revisions |

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 01 21:30:18 1999 +0200 @@ -0,0 +1,55 @@ +(* 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;