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

src/HOL/Isar_Examples/Knaster_Tarski.thy

author | haftmann |

Wed Jun 30 16:46:44 2010 +0200 (2010-06-30) | |

changeset 37659 | 14cabf5fa710 |

parent 33026 | 8f35633c4922 |

child 37671 | fa53d267dab3 |

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

more speaking names

1 (* Title: HOL/Isar_Examples/Knaster_Tarski.thy

2 Author: Markus Wenzel, TU Muenchen

4 Typical textbook proof example.

5 *)

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

9 theory Knaster_Tarski

10 imports Main Lattice_Syntax

11 begin

14 subsection {* Prose version *}

16 text {*

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

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

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

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

22 complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.

23 Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.

25 \textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =

26 \<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text

27 "f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text

28 H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove

29 the reverse one (!) and thereby complete the proof that @{text a} is

30 a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le>

31 f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.

32 *}

35 subsection {* Formal versions *}

37 text {*

38 The Isar proof below closely follows the original presentation.

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

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

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

42 the course of reasoning.

43 *}

45 theorem Knaster_Tarski:

46 fixes f :: "'a::complete_lattice \<Rightarrow> 'a"

47 assumes "mono f"

48 shows "\<exists>a. f a = a"

49 proof

50 let ?H = "{u. f u \<le> u}"

51 let ?a = "\<Sqinter>?H"

52 show "f ?a = ?a"

53 proof -

54 {

55 fix x

56 assume "x \<in> ?H"

57 then have "?a \<le> x" by (rule Inf_lower)

58 with `mono f` have "f ?a \<le> f x" ..

59 also from `x \<in> ?H` have "\<dots> \<le> x" ..

60 finally have "f ?a \<le> x" .

61 }

62 then have "f ?a \<le> ?a" by (rule Inf_greatest)

63 {

64 also presume "\<dots> \<le> f ?a"

65 finally (order_antisym) show ?thesis .

66 }

67 from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..

68 then have "f ?a \<in> ?H" ..

69 then show "?a \<le> f ?a" by (rule Inf_lower)

70 qed

71 qed

73 text {*

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

75 explicit block structure and weak assumptions. Thus we have

76 mimicked the particular way of reasoning of the original text.

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

79 achieve structured top-down decomposition of the problem at the

80 outer level, while only the inner steps of reasoning are done in a

81 forward manner. We are certainly more at ease here, requiring only

82 the most basic features of the Isar language.

83 *}

85 theorem Knaster_Tarski':

86 fixes f :: "'a::complete_lattice \<Rightarrow> 'a"

87 assumes "mono f"

88 shows "\<exists>a. f a = a"

89 proof

90 let ?H = "{u. f u \<le> u}"

91 let ?a = "\<Sqinter>?H"

92 show "f ?a = ?a"

93 proof (rule order_antisym)

94 show "f ?a \<le> ?a"

95 proof (rule Inf_greatest)

96 fix x

97 assume "x \<in> ?H"

98 then have "?a \<le> x" by (rule Inf_lower)

99 with `mono f` have "f ?a \<le> f x" ..

100 also from `x \<in> ?H` have "\<dots> \<le> x" ..

101 finally show "f ?a \<le> x" .

102 qed

103 show "?a \<le> f ?a"

104 proof (rule Inf_lower)

105 from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..

106 then show "f ?a \<in> ?H" ..

107 qed

108 qed

109 qed

111 end