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

author | wenzelm |

Sat, 09 Oct 1999 23:19:20 +0200 | |

changeset 7818 | 1acfb8cc3720 |

parent 7817 | 76cffd7dff2e |

child 7819 | 6dd018b6cf3f |

added structured version of the proof;

--- a/src/HOL/Isar_examples/KnasterTarski.thy Sat Oct 09 23:18:01 1999 +0200 +++ b/src/HOL/Isar_examples/KnasterTarski.thy Sat Oct 09 23:19:20 1999 +0200 @@ -13,10 +13,10 @@ 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.} + According to the book ``Introduction to Lattices and Order'' + \cite[pages 93--94]{davey-priestley}, the Knaster-Tarski fixpoint + theorem is as follows.\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. @@ -32,14 +32,13 @@ *}; -subsection {* Formal version *}; +subsection {* Formal versions *}; 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. + The Isar 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. *}; theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a"; @@ -69,4 +68,41 @@ qed; qed; +text {* + Above we have used several advanced Isar language elements, such as + explicit block structure and weak assumptions. Thus we have mimicked + the particular way of reasoning of the original text. + + In the subsequent version of the proof the order of reasoning is + changed to achieve structured top-down decomposition of the problem + at the outer level, while the small inner steps of reasoning or done + in a forward manner. Note that this requires only the most basic + features of the Isar language. +*}; + +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 (rule order_antisym); + show ge: "f ?a <= ?a"; + proof (rule Inter_greatest); + 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; show "f ?a <= x"; .; + qed; + show "?a <= f ?a"; + proof (rule Inter_lower); + from mono ge; have "f (f ?a) <= f ?a"; ..; + thus "f ?a : ?H"; ..; + qed; + qed; +qed; + end;