Re: [isabelle] Lattices and syntactic classes

Hi Viorel,

>>> There are some aspects of the lattice theories which creates problems
>>> for my developments. The fact that inf and sup constants are part
>>> of the lattice itself, rather than being defined just as classes with
>>> only inf and sup constants. All other constants (*, +, ...) are defined
>>> in separate classes and their reuse is much easier.
>>> Do you know if the same technique is going to be used for inf and sup?

> Ultimately the structure is a (semi-) lattice, but the axioms are
> different.
> Imagine an algebraic structure with some operations *, left_imp which
> satisfies
> some properties and in which inf can be defined
> class left_inf = inf + times + left_imp + order +
>   assumes some axioms for times and left_imp
>   and inf_l_def: "(inf a b) = (left_imp a b) * a"
>   and definition of order
> begin
> in this setting the fact that inf is a semi-lattice operation can be
> proved from the axioms of times and left_imp.
> in the context of left_inf I would state
> subclass semilattice_inf
> If I assume that left_inf is a semilattice_inf, then I would need to
> prove this fact for every instantiation of it.

> One more comment. Now in the Isabelle/HOL library the operations
> Inf and Sup of complete lattices are defined in their own classes.
> If the same is done for inf and sup, their use via semilattice will
> be the same, but it would be easier to reuse them in contexts
> where one does not want to assume the semilattice structure. 

the answer to your issue has many facets.

Historically, syntactic classes where necessary since the class +
operations & instantiation infrastructure has not yet emerged.  With the
class package my first thought was to avoid syntactic classes entirely,
since they allow to write down things for which one might expect certain
properties to hold, which, in fact, do not, only with more specific sort

	(a + b) + c = a + (b + c)
        2 + 2 = 4 -- an Isabelle classic!

(an aside: there is a similar issue with min/max which are defined
purely syntactical, not only on linear orders)

I kept the then existing syntactic classes a) for backward compatibility
and b) since they carry syntax by default.  The case for inf and sup
then was different.

Nowadays I have to admit that in situations like yours syntactic classes
for inf and sup would allow a more liberal building of the class
hierarchy.  Indeed, I recently had some thoughts how you could achieve
something like »import class parameters, but with different
specification from which the original specification follows«, in essence
a class with simultaneous subclass.  But it looked rather complicated.

I have no strong opinion whether to turn inf and sup into syntactic
classes.  But note that to simplify your instantiation proofs you can
prove a specific introduction rule for P ==> OFCLASS('a, left_inf) where
P is the body of your left_inf class.

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.