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

src/HOL/Isar_Examples/Knaster_Tarski.thy

author | nipkow |

Mon Jan 30 21:49:41 2012 +0100 (2012-01-30) | |

changeset 46372 | 6fa9cdb8b850 |

parent 41413 | 64cd30d6b0b8 |

child 58614 | 7338eb25226c |

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

added "'a rel"

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 "~~/src/HOL/Library/Lattice_Syntax"

11 begin

14 subsection {* Prose version *}

16 text {* According to the textbook \cite[pages

17 93--94]{davey-priestley}, the Knaster-Tarski fixpoint theorem is as

18 follows.\footnote{We have dualized the argument, and tuned the

19 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)"}. *}

34 subsection {* Formal versions *}

36 text {* The Isar proof below closely follows the original

37 presentation. Virtually all of the prose narration has been

38 rephrased in terms of formal Isar language elements. Just as many

39 textbook-style proofs, there is a strong bias towards forward proof,

40 and several bends in the course of reasoning. *}

42 theorem Knaster_Tarski:

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

44 assumes "mono f"

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

46 proof

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

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

49 show "f ?a = ?a"

50 proof -

51 {

52 fix x

53 assume "x \<in> ?H"

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

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

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

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

58 }

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

60 {

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

62 finally (order_antisym) show ?thesis .

63 }

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

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

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

67 qed

68 qed

70 text {* Above we have used several advanced Isar language elements,

71 such as explicit block structure and weak assumptions. Thus we have

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

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

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

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

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

78 the most basic features of the Isar language. *}

80 theorem Knaster_Tarski':

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

82 assumes "mono f"

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

84 proof

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

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

87 show "f ?a = ?a"

88 proof (rule order_antisym)

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

90 proof (rule Inf_greatest)

91 fix x

92 assume "x \<in> ?H"

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

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

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

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

97 qed

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

99 proof (rule Inf_lower)

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

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

102 qed

103 qed

104 qed

106 end