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

src/HOL/Isar_examples/KnasterTarski.thy

author | wenzelm |

Sat Sep 04 21:13:01 1999 +0200 (1999-09-04) | |

changeset 7480 | 0a0e0dbe1269 |

parent 7253 | a494a78fea39 |

child 7761 | 7fab9592384f |

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

replaced ?? by ?;

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

2 ID: $Id$

3 Author: Markus Wenzel, TU Muenchen

5 Typical textbook proof example.

6 *)

9 theory KnasterTarski = Main:;

11 text {*

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

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

14 fixpoint theorem is as follows (pages 93--94). Note that we have

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

17 \paragraph{The Knaster-Tarski Fixpoint Theorem.} Let $L$ be a

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

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

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

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

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

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

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

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

27 \le f(a)$.

28 *};

30 text {*

31 Our proof below closely follows this presentation. Virtually all of

32 the prose narration has been rephrased in terms of formal Isar

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

34 strong bias towards forward reasoning, and little hierarchical

35 structure.

36 *};

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

39 proof;

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

41 let ?a = "Inter ?H";

43 assume mono: "mono f";

44 show "f ?a = ?a";

45 proof -;

46 {{;

47 fix x;

48 assume mem: "x : ?H";

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

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

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

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

53 }};

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

55 {{;

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

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

58 }};

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

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

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

62 qed;

63 qed;

66 end;