*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Complete Lattices*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Tue, 02 Mar 2010 12:18:35 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <4B8CD7FD.4040705@informatik.tu-muenchen.de>*References*: <4B8C41B6.6000905@abo.fi> <4B8CD7FD.4040705@informatik.tu-muenchen.de>*User-agent*: Thunderbird 2.0.0.23 (Windows/20090812)

Hello Florian, Thank you for your quick answer. I am talking however about this complete lattice theory: http://isabelle.in.tum.de/dist/library/HOL/Lattice/CompleteLattice.html The one you pointed me does not seem to have results about fixed points and the Knaster-Tarski theorem. I also need it instantiated for a special king of predicate transformers, like L = (('b => ('a set)) => ('b => ('a set))) Moreover, I need it instantiated for monotonic predicate transformers, or at least I need to know that the fixed point of F: L -> L is monotonic when (F x) is monotonic for all x monotonic. Best regards, Viorel Florian Haftmann wrote:

Hi Viorel,I have noticed that there is a general theory about complete latices in Isabelle, however I was not able to use it. I have tried imports CompleteLattices but it did not work. I tried also imports Lattice CompleteLattices, but it did not work either.the theory you are referring to is named Complete_Lattice (without trailing s!) and is already part of the HOL-Main image; it provides a type class complete_lattice with operations Inf and Sup.The second question is how do use these abstract theories? I need to instantiate them for the lattice of predicate transformers ('a set => 'a set) with the order inherited from sets (bool).The standard instantiations of the Complete_Lattice type class already allow you to use it that way: term "Sup :: ('a set ⇒ 'a set) set ⇒ 'a set ⇒ 'a set" For applications, the type class complete_lattice should be sufficient. For meta-theory about complete lattices, theory HOL/Algebra/Lattices.thy is perhaps a better entrance point. Hope this helps, Florian

**Follow-Ups**:**Re: [isabelle] Complete Lattices***From:*Florian Haftmann

**References**:**[isabelle] Complete Lattices***From:*Viorel Preoteasa

**Re: [isabelle] Complete Lattices***From:*Florian Haftmann

- Previous by Date: Re: [isabelle] Complete Lattices
- Next by Date: Re: [isabelle] Complete Lattices
- Previous by Thread: Re: [isabelle] Complete Lattices
- Next by Thread: Re: [isabelle] Complete Lattices
- Cl-isabelle-users March 2010 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