*To*: Alessandro Coglio <coglio at kestrel.edu>*Subject*: Re: [isabelle] Questions on type classes for lattices*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Thu, 15 Nov 2012 10:33:24 +0100*Cc*: Isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <509F27FB.2000903@kestrel.edu>*Organization*: TU Munich*References*: <509F27FB.2000903@kestrel.edu>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:16.0) Gecko/20121028 Thunderbird/16.0.2

Hi Alessandro, > 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? this is a well-known restriction of type classes. The short answer is, no, this restriction cannot be lifted. This is the price you have to pay to have operations *and* assumptions about them: in order for a structure to be a complete lattice, it is not necessary that there exist operations which satisfy its properties, but these operations must be explicitly defined for that particular type. > Anyhow, given the current situation, one approach is to define > finite_lattice as above, define Inf/Sup/bot/top on finite_lattice Such definitions would be rejected, since they violate the rules for overloading: Inf/Sup/bot/top can only be instantiated on particular type constructors, not (sort-constrained) type variables. > 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. IMHO it is the cleanest one you can achieve inside the current infrastructure. E.g. > lemma finite_complete_lattice: > assumes Inf: "\<And>A. (Inf :: ('a::{Inf, Sup, bounded_lattice, finite}) set ⇒ 'a) A = > (if A = {} then top else Inf_fin A)" > assumes Sup: "\<And>A. (Sup :: ('a::{Inf, Sup, bounded_lattice, finite}) set ⇒ 'a) A = > (if A = {} then top else Sup_fin A)" > shows "OFCLASS('a::{Inf, Sup, bounded_lattice, finite}, complete_lattice_class)" > proof > 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 does indeed save you nothing on instance proofs. > 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. The issue is that class bot already demands assumptions on bot and thus you cannot instantiate bot without actually proving these. There have been two ideas around to lift this somehow: * Provide purely syntactic classes for operations without further assumptions; this has a long tradition in isabelle (cf. plus, times, zero etc.), but has the disadvantage that you can write down things syntactically which do not obey properties you would expect naively (i.e. "a + 0 = a" does not hold in general). * Build a fancy wrapper around instantiation in the spirit of Haskell default class method definitions. Since this must also cover proofs, it would be a tedious affair and maybe not worth doing it. Cheers, Florian -- PGP available: http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**References**:**[isabelle] Questions on type classes for lattices***From:*Alessandro Coglio

- Previous by Date: Re: [isabelle] Automatic derivation of a total order on datatypes
- Next by Date: Re: [isabelle] Isabelle-friendly CPUs and benchmarks
- Previous by Thread: [isabelle] Questions on type classes for lattices
- Next by Thread: [isabelle] CFP : 2nd International Workshop on Engineering Safety and Security Systems (ESSS)
- Cl-isabelle-users November 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list