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

author | wenzelm |

Thu, 08 Jul 1999 18:39:34 +0200 | |

changeset 6939 | c7c365b4f615 |

parent 6938 | 914233d95b23 |

child 6940 | ee6640456cbb |

removed old version;
tuned;

--- a/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 08 18:39:08 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Thu Jul 08 18:39:34 1999 +0200 @@ -12,7 +12,7 @@ theorems [dest] = monoD; (* FIXME [dest!!] *) text {* - The proofs of Knaster-Tarski below closely follows the presentation in + The proof of Knaster-Tarski below closely follows the presentation in 'Introduction to Lattices' and Order by Davey/Priestley, pages 93--94. All of their narration has been rephrased in terms of formal Isar language elements. Just as many textbook-style proofs, there is @@ -20,7 +20,7 @@ structure. *}; -theorem KnasterTarski1: "mono f ==> EX a::'a set. f a = a"; +theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; proof; let ??H = "{u. f u <= u}"; let ??a = "Inter ??H"; @@ -34,34 +34,7 @@ hence "??a <= x"; by (rule Inter_lower); with mono; have "f ??a <= f x"; ..; also; from mem; have "... <= x"; ..; - finally (order_trans); have "f ??a <= x"; .; - }}; - hence ge: "f ??a <= ??a"; by (rule Inter_greatest); - thus ??thesis; - proof (rule order_antisym); - from mono ge; have "f (f ??a) <= f ??a"; ..; - hence "f ??a : ??H"; ..; - thus "??a <= f ??a"; by (rule Inter_lower); - qed; - qed; -qed; - - -theorem KnasterTarski2: "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; - assume mem: "x : ??H"; - hence "??a <= x"; by (rule Inter_lower); - with mono; have "f ??a <= f x"; ..; - also; from mem; have "... <= x"; ..; - finally (order_trans); have "f ??a <= x"; .; + finally; have "f ??a <= x"; .; }}; hence ge: "f ??a <= ??a"; by (rule Inter_greatest); {{;