1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
|
(********** This file is from the Isabelle distribution **********)
(* Title: HOL/Isar_examples/KnasterTarski.thy
Author: Markus Wenzel, TU Muenchen
Typical textbook proof example.
*)
header {* Textbook-style reasoning: the Knaster-Tarski Theorem *}
theory KnasterTarski
imports Main Lattice_Syntax
begin
subsection {* Prose version *}
text {*
According to the textbook \cite[pages 93--94]{davey-priestley}, the
Knaster-Tarski fixpoint theorem is as follows.\footnote{We have
dualized the argument, and tuned the notation a little bit.}
\textbf{The Knaster-Tarski Fixpoint Theorem.} Let @{text L} be a
complete lattice and @{text "f: L \<rightarrow> L"} an order-preserving map.
Then @{text "\<Sqinter>{x \<in> L | f(x) \<le> x}"} is a fixpoint of @{text f}.
\textbf{Proof.} Let @{text "H = {x \<in> L | f(x) \<le> x}"} and @{text "a =
\<Sqinter>H"}. For all @{text "x \<in> H"} we have @{text "a \<le> x"}, so @{text
"f(a) \<le> f(x) \<le> x"}. Thus @{text "f(a)"} is a lower bound of @{text
H}, whence @{text "f(a) \<le> a"}. We now use this inequality to prove
the reverse one (!) and thereby complete the proof that @{text a} is
a fixpoint. Since @{text f} is order-preserving, @{text "f(f(a)) \<le>
f(a)"}. This says @{text "f(a) \<in> H"}, so @{text "a \<le> f(a)"}.
*}
subsection {* Formal versions *}
text {*
The Isar proof below closely follows the original presentation.
Virtually all of the prose narration has been rephrased in terms of
formal Isar language elements. Just as many textbook-style proofs,
there is a strong bias towards forward proof, and several bends in
the course of reasoning.
*}
theorem Knaster_Tarski:
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
assumes "mono f"
shows "\<exists>a. f a = a"
proof
let ?H = "{u. f u \<le> u}"
let ?a = "\<Sqinter>?H"
show "f ?a = ?a"
proof -
{
fix x
assume "x \<in> ?H"
then have "?a \<le> x" by (rule Inf_lower)
with `mono f` have "f ?a \<le> f x" ..
also from `x \<in> ?H` have "\<dots> \<le> x" ..
finally have "f ?a \<le> x" .
}
then have "f ?a \<le> ?a" by (rule Inf_greatest)
{
also presume "\<dots> \<le> f ?a"
finally (order_antisym) show ?thesis .
}
from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
then have "f ?a \<in> ?H" ..
then show "?a \<le> f ?a" by (rule Inf_lower)
qed
qed
text {*
Above we have used several advanced Isar language elements, such as
explicit block structure and weak assumptions. Thus we have
mimicked the particular way of reasoning of the original text.
In the subsequent version the order of reasoning is changed to
achieve structured top-down decomposition of the problem at the
outer level, while only the inner steps of reasoning are done in a
forward manner. We are certainly more at ease here, requiring only
the most basic features of the Isar language.
*}
theorem Knaster_Tarski':
fixes f :: "'a::complete_lattice \<Rightarrow> 'a"
assumes "mono f"
shows "\<exists>a. f a = a"
proof
let ?H = "{u. f u \<le> u}"
let ?a = "\<Sqinter>?H"
show "f ?a = ?a"
proof (rule order_antisym)
show "f ?a \<le> ?a"
proof (rule Inf_greatest)
fix x
assume "x \<in> ?H"
then have "?a \<le> x" by (rule Inf_lower)
with `mono f` have "f ?a \<le> f x" ..
also from `x \<in> ?H` have "\<dots> \<le> x" ..
finally show "f ?a \<le> x" .
qed
show "?a \<le> f ?a"
proof (rule Inf_lower)
from `mono f` and `f ?a \<le> ?a` have "f (f ?a) \<le> f ?a" ..
then show "f ?a \<in> ?H" ..
qed
qed
qed
end
|
