summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/KnasterTarski.thy

author | wenzelm |

Wed Oct 06 18:50:51 1999 +0200 (1999-10-06) | |

changeset 7761 | 7fab9592384f |

parent 7480 | 0a0e0dbe1269 |

child 7818 | 1acfb8cc3720 |

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

improved presentation;

1 (* Title: HOL/Isar_examples/KnasterTarski.thy

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

5 Typical textbook proof example.

6 *)

8 header {* Textbook-style reasoning: the Knaster-Tarski Theorem *};

10 theory KnasterTarski = Main:;

13 subsection {* Prose version *};

15 text {*

16 According to the book ``Introduction to Lattices and Order'' (by

17 B. A. Davey and H. A. Priestley, CUP 1990), the Knaster-Tarski

18 fixpoint theorem is as follows (pages 93--94).\footnote{We have

19 dualized their argument, and tuned the notation a little bit.}

21 \medskip \textbf{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a

22 complete lattice and $f \colon L \to L$ an order-preserving map.

23 Then $\bigwedge \{ x \in L \mid f(x) \le x \}$ is a fixpoint of $f$.

25 \textbf{Proof.} Let $H = \{x \in L \mid f(x) \le x\}$ and $a =

26 \bigwedge H$. For all $x \in H$ we have $a \le x$, so $f(a) \le f(x)

27 \le x$. Thus $f(a)$ is a lower bound of $H$, whence $f(a) \le a$.

28 We now use this inequality to prove the reverse one (!) and thereby

29 complete the proof that $a$ is a fixpoint. Since $f$ is

30 order-preserving, $f(f(a)) \le f(a)$. This says $f(a) \in H$, so $a

31 \le f(a)$.

32 *};

35 subsection {* Formal version *};

37 text {*

38 Our proof below closely follows the original presentation. Virtually

39 all of the prose narration has been rephrased in terms of formal Isar

40 language elements. Just as many textbook-style proofs, there is a

41 strong bias towards forward reasoning, and little hierarchical

42 structure.

43 *};

45 theorem KnasterTarski: "mono f ==> EX a::'a set. f a = a";

46 proof;

47 let ?H = "{u. f u <= u}";

48 let ?a = "Inter ?H";

50 assume mono: "mono f";

51 show "f ?a = ?a";

52 proof -;

53 {{;

54 fix x;

55 assume mem: "x : ?H";

56 hence "?a <= x"; by (rule Inter_lower);

57 with mono; have "f ?a <= f x"; ..;

58 also; from mem; have "... <= x"; ..;

59 finally; have "f ?a <= x"; .;

60 }};

61 hence ge: "f ?a <= ?a"; by (rule Inter_greatest);

62 {{;

63 also; presume "... <= f ?a";

64 finally (order_antisym); show ?thesis; .;

65 }};

66 from mono ge; have "f (f ?a) <= f ?a"; ..;

67 hence "f ?a : ?H"; ..;

68 thus "?a <= f ?a"; by (rule Inter_lower);

69 qed;

70 qed;

72 end;