# [isabelle] Knaster-Tarski fixed point theorem in HOL/Lattice/CompleteLattice

```Hi all,

I just wanted to use the Theorem CompleteLattice.Knaster_Tarski, and
noticed that it is not general enough. Though the comment states that it
should say, that every monotonic function has a *least* fixed point, the
theorem itself just proves existence of a fixed point, not necessarily a
least one:

text {*
The Knaster-Tarski Theorem (in its simplest formulation) states that
any monotone function on a complete lattice has a least fixed-point
(see \cite[pages 93--94]{Davey-Priestley:1990} for example).  This
is a consequence of the basic boundary properties of the complete
lattice operations.
*}

theorem Knaster_Tarski:
"(\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x \<sqsubseteq> f
y) \<Longrightarrow> \<exists>a::'a::complete_lattice. f a = a"

I generalized the theorem accordingly (and put it in long-goal format):

theorem Knaster_Tarski':
assumes mono: "\<And>x y. x \<sqsubseteq> y \<Longrightarrow> f x
\<sqsubseteq> f y"
shows "\<exists>a::'a::complete_lattice. f a = a \<and> (\<forall>a'.
f a' = a' \<longrightarrow> a\<sqsubseteq>a')"
proof
let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
have ge: "f ?a \<sqsubseteq> ?a"
proof
fix x assume x: "x \<in> ?H"
hence "?a \<sqsubseteq> x" ..
hence "f ?a \<sqsubseteq> f x" by (rule mono)
also from x have "... \<sqsubseteq> x" ..
finally show "f ?a \<sqsubseteq> x" .
qed
also have "?a \<sqsubseteq> f ?a"
proof
from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
thus "f ?a \<in> ?H" ..
qed
finally have "f ?a = ?a" .
moreover {
fix a'
assume "f a' = a'"
hence "a' \<in> ?H" by (auto intro: leq_refl)
hence "?a \<sqsubseteq> a'" by (rule Meet_lower)
}
ultimately show "f ?a = ?a \<and> (\<forall>a'. f a' = a'
\<longrightarrow> ?a\<sqsubseteq>a')" by blast
qed

regards,
Peter

--
Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at uni-muenster.de
Tel: 0251-83-32749
Mobil: 0163-5310380

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.