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

src/HOL/Isar_examples/KnasterTarski.thy

author | paulson |

Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) | |

changeset 16587 | b34c8aa657a5 |

parent 16417 | 9bc16273c2d4 |

child 26812 | c0fa62fa0e5b |

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

Constant "If" is now local

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 imports Main begin

13 subsection {* Prose version *}

15 text {*

16 According to the textbook \cite[pages 93--94]{davey-priestley}, the

17 Knaster-Tarski fixpoint theorem is as follows.\footnote{We have

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

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

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

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

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

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

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

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

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

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

30 \le f(a)$.

31 *}

34 subsection {* Formal versions *}

36 text {*

37 The Isar proof below closely follows the original presentation.

38 Virtually all of the prose narration has been rephrased in terms of

39 formal Isar language elements. Just as many textbook-style proofs,

40 there is a strong bias towards forward proof, and several bends

41 in the course of reasoning.

42 *}

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

45 proof

46 let ?H = "{u. f u <= u}"

47 let ?a = "Inter ?H"

49 assume mono: "mono f"

50 show "f ?a = ?a"

51 proof -

52 {

53 fix x

54 assume H: "x : ?H"

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

56 with mono have "f ?a <= f x" ..

57 also from H have "... <= x" ..

58 finally have "f ?a <= x" .

59 }

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

61 {

62 also presume "... <= f ?a"

63 finally (order_antisym) show ?thesis .

64 }

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

66 hence "f ?a : ?H" ..

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

68 qed

69 qed

71 text {*

72 Above we have used several advanced Isar language elements, such as

73 explicit block structure and weak assumptions. Thus we have mimicked

74 the particular way of reasoning of the original text.

76 In the subsequent version the order of reasoning is changed to

77 achieve structured top-down decomposition of the problem at the outer

78 level, while only the inner steps of reasoning are done in a forward

79 manner. We are certainly more at ease here, requiring only the most

80 basic features of the Isar language.

81 *}

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

84 proof

85 let ?H = "{u. f u <= u}"

86 let ?a = "Inter ?H"

88 assume mono: "mono f"

89 show "f ?a = ?a"

90 proof (rule order_antisym)

91 show ge: "f ?a <= ?a"

92 proof (rule Inter_greatest)

93 fix x

94 assume H: "x : ?H"

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

96 with mono have "f ?a <= f x" ..

97 also from H have "... <= x" ..

98 finally show "f ?a <= x" .

99 qed

100 show "?a <= f ?a"

101 proof (rule Inter_lower)

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

103 thus "f ?a : ?H" ..

104 qed

105 qed

106 qed

108 end