[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')"
  let ?H = "{u. f u \<sqsubseteq> u}" let ?a = "\<Sqinter>?H"
  have ge: "f ?a \<sqsubseteq> ?a"
    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" .
  also have "?a \<sqsubseteq> f ?a"
    from ge have "f (f ?a) \<sqsubseteq> f ?a" by (rule mono)
    thus "f ?a \<in> ?H" ..
  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


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.