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

src/HOL/Isar_Examples/Knaster_Tarski.thy

author | wenzelm |

Tue Sep 26 20:54:40 2017 +0200 (23 months ago) | |

changeset 66695 | 91500c024c7f |

parent 66453 | cc19f7ca2ed6 |

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

tuned;

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

2 Author: Makarius

4 Typical textbook proof example.

5 *)

7 section \<open>Textbook-style reasoning: the Knaster-Tarski Theorem\<close>

9 theory Knaster_Tarski

10 imports Main "HOL-Library.Lattice_Syntax"

11 begin

14 subsection \<open>Prose version\<close>

16 text \<open>

17 According to the textbook @{cite \<open>pages 93--94\<close> "davey-priestley"}, the

18 Knaster-Tarski fixpoint theorem is as follows.\<^footnote>\<open>We have dualized the

19 argument, and tuned the notation a little bit.\<close>

21 \<^bold>\<open>The Knaster-Tarski Fixpoint Theorem.\<close> Let \<open>L\<close> be a complete lattice and

22 \<open>f: L \<rightarrow> L\<close> an order-preserving map. Then \<open>\<Sqinter>{x \<in> L | f(x) \<le> x}\<close> is a fixpoint

23 of \<open>f\<close>.

25 \<^bold>\<open>Proof.\<close> Let \<open>H = {x \<in> L | f(x) \<le> x}\<close> and \<open>a = \<Sqinter>H\<close>. For all \<open>x \<in> H\<close> we have

26 \<open>a \<le> x\<close>, so \<open>f(a) \<le> f(x) \<le> x\<close>. Thus \<open>f(a)\<close> is a lower bound of \<open>H\<close>, whence

27 \<open>f(a) \<le> a\<close>. We now use this inequality to prove the reverse one (!) and

28 thereby complete the proof that \<open>a\<close> is a fixpoint. Since \<open>f\<close> is

29 order-preserving, \<open>f(f(a)) \<le> f(a)\<close>. This says \<open>f(a) \<in> H\<close>, so \<open>a \<le> f(a)\<close>.\<close>

32 subsection \<open>Formal versions\<close>

34 text \<open>

35 The Isar proof below closely follows the original presentation. Virtually

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

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

38 bias towards forward proof, and several bends in the course of reasoning.

39 \<close>

41 theorem Knaster_Tarski:

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

43 assumes "mono f"

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

45 proof

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

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

48 show "f ?a = ?a"

49 proof -

50 {

51 fix x

52 assume "x \<in> ?H"

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

54 with \<open>mono f\<close> have "f ?a \<le> f x" ..

55 also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..

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

57 }

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

59 {

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

61 finally (order_antisym) show ?thesis .

62 }

63 from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..

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

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

66 qed

67 qed

69 text \<open>

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

71 block structure and weak assumptions. Thus we have mimicked the particular

72 way of reasoning of the original text.

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

75 structured top-down decomposition of the problem at the outer level, while

76 only the inner steps of reasoning are done in a forward manner. We are

77 certainly more at ease here, requiring only the most basic features of the

78 Isar language.

79 \<close>

81 theorem Knaster_Tarski':

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

83 assumes "mono f"

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

85 proof

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

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

88 show "f ?a = ?a"

89 proof (rule order_antisym)

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

91 proof (rule Inf_greatest)

92 fix x

93 assume "x \<in> ?H"

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

95 with \<open>mono f\<close> have "f ?a \<le> f x" ..

96 also from \<open>x \<in> ?H\<close> have "\<dots> \<le> x" ..

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

98 qed

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

100 proof (rule Inf_lower)

101 from \<open>mono f\<close> and \<open>f ?a \<le> ?a\<close> have "f (f ?a) \<le> f ?a" ..

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

103 qed

104 qed

105 qed

107 end