# [isabelle] Questions on type classes for lattices

*To*: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>
*Subject*: [isabelle] Questions on type classes for lattices
*From*: Alessandro Coglio <coglio at kestrel.edu>
*Date*: Sat, 10 Nov 2012 20:22:19 -0800
*Organization*: Kestrel Institute
*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:16.0) Gecko/20121026 Thunderbird/16.0.2

Hello,
Since a (non-empty) finite lattice is also complete, I would like to define
class finite_lattice = finite + lattice
and then prove
instance finite_lattice < complete_lattice
after giving suitable definitions for Inf/Sup/bot/top.
But apparently
instance A < B

`requires A to have (at definition time) all the operators of B. Are
``there "deep" reasons for this requirement, or could it be relaxed with
``relative ease to allow the extra operators to be defined after A has
``been defined and then used to show that A is a subclass of B?
`

`Anyhow, given the current situation, one approach is to define
``finite_lattice as above, define Inf/Sup/bot/top on finite_lattice, and
``prove that finite_lattice is a sublocale of complete_lattice. In this
``way, after proving that a type L has class finite_lattice, all the
``operators and theorems of complete_lattice should be available for L.
``The drawback of this approach is that L will not have class
``complete_lattice, and so, for example, existing operations that take
``complete_lattice arguments cannot be used on L.
`

`Another approach is to define class finite_lattice to include
``Inf/Sup/bot/top, along with assumptions that define these four operators
``in terms of the existing operators of finite_lattice. In this way,
``finite_lattice can be a subclass of complete_lattice. The drawback is
``that proving that a type L has class finite_lattice will require more
``work because of the extra operators and assumptions that must be
``satisfied (but perhaps this work can be eased by proving and using
``general lemmas that relate Inf/Sup/bot/top to inf and sup). Furthermore,
``the approach seems (to me) methodologically less clean than the previous
``one.
`
A third approach is to define
class finite_lattice = finite + complete_lattice

`and avoid proving subclass relations altogether. The drawback is that
``proving that a type L has class finite_lattice is even more work (but
``again perhaps this work can be eased by suitable general lemmas). This
``seems to be the approach taken in the library definition of class
``complete_lattice, which includes bounded_lattice explicitly, even though
``Inf and Sup suffice. Also, this approach seems (to me) methodologically
``less clean than the previous two.
`

`Does anybody have comments on the three approaches sketched above?
``Relative pros and cons? Other approaches?
`
Thank you in advance!

**Attachment:
**`smime.p7s`

*Description:* S/MIME Cryptographic Signature

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