Re: [isabelle] Complete Lattices

Hi Viorel,


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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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