Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Complete Lattices

Email Gateway (Aug 18 2022 at 14:51):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello,

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 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).

Best regards,

Viorel Preoteasa

Email Gateway (Aug 18 2022 at 14:54):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
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
signature.asc

Email Gateway (Aug 18 2022 at 14:55):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Viorel,

http://isabelle.in.tum.de/dist/library/HOL/Lattice/CompleteLattice.html

aha, this one should be considered more an example for type classes than
a library to actually build on.

The one you pointed me does not seem to have results about fixed
points and the Knaster-Tarski theorem.

This can be found (to some extent) in HOL/Inductive.thy.

I also need it instantiated
for a special king of predicate transformers, like

L = (('b => ('a set)) => ('b => ('a set)))

You can provide you own "interpretation"s for type classes which are a
specialized form of locales.

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.

You can express this either using the "mono" predicate or introduce your
own locale which imports complete_lattice and fixes F, together with an
assumes concerning monotonicity.

Hope this helps,
Florian
signature.asc

Email Gateway (Aug 18 2022 at 14:58):

From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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:

Last updated: Apr 26 2024 at 01:06 UTC