Re: [isabelle] Complete Lattices

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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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