Re: [isabelle] Complete Lattices



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

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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