Re: [isabelle] Complete Lattices



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







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