*To*: isabelle-users at cl.cam.ac.uk*Subject*: [isabelle] Knaster-Tarski fixed point theorem in HOL/Lattice/CompleteLattice*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 22 Nov 2007 12:01:25 +0100*User-agent*: Thunderbird 1.5.0.9 (X11/20060911)

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

- Previous by Date: Re: [isabelle] [Code-Generation] 'No type arity (..)' - Problem
- Next by Date: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph
- Previous by Thread: [isabelle] Tools and Techniques for Verification of System Infrastructure (Announce)
- Next by Thread: [isabelle] Dual version of HOL/Lattice/Lattice.meet_semimorph
- Cl-isabelle-users November 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list