# [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?
```