Re: [isabelle] Complete Lattices
Thank you for your quick answer. I am talking however about this complete
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.
Florian Haftmann wrote:
I have noticed that there is a general theory about complete latices in
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and