*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] Lattices and syntactic classes*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 31 Aug 2011 20:53:31 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <4E5CC902.6030007@abo.fi>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <4E5644D5.2020205@in.tum.de> <4E5745D1.9020600@abo.fi> <4E582373.80901@in.tum.de> <4E5B5646.1080408@abo.fi> <4E5CC512.2010403@in.tum.de> <4E5CC902.6030007@abo.fi>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.2.20) Gecko/20110805 Lightning/1.0b2 Thunderbird/3.1.12

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 constraints: (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, 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**

**Follow-Ups**:**Re: [isabelle] Lattices and syntactic classes***From:*Brian Huffman

- Previous by Date: Re: [isabelle] list_size_pointwise
- Next by Date: Re: [isabelle] Lattices and syntactic classes
- Previous by Thread: Re: [isabelle] Struggling with type unification
- Next by Thread: Re: [isabelle] Lattices and syntactic classes
- Cl-isabelle-users August 2011 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