*To*: Alexander Krauss <krauss at in.tum.de>, cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Lattices and syntactic classes*From*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Date*: Mon, 12 Sep 2011 10:47:01 +0300*In-reply-to*: <4E694774.3000701@in.tum.de>*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> <4E5E832B.9060902@informatik.tu-muenchen.de> <4E67D689.5060307@informatik.tu-muenchen.de> <alpine.LNX.1.10.1109082254210.19909@atbroy100.informatik.tu-muenchen.de> <4E694774.3000701@in.tum.de>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.6; rv:6.0) Gecko/20110812 Thunderbird/6.0

To me this looks rather like a workaround for some specificsituations. If I understand correctly, it wouldn't work with a morecomplex class hierarchy, where parts of the instance may already beestablished etc. The issue certainly deserves more thouroughexamination at some point.For now I have just added (5e51075cbd97) the syntactic classes for infand sup, which were originally asked for by Viorel. This is a ratherstraightforward thing, and the more general typings that may ariseseem to have little impact in practice.

Thank you for this change. I did use a work around which worked well. So the alternatives suggested did not seem better to me. The work around that I used is the following: class inf = fixes inf :: "'a => 'a => 'a" (infixl "\<sqinter>" 70) class sup = fixes sup :: "'a => 'a => 'a" (infixl "\<squnion>" 65) class lattice_infix = order + inf + sup + assumes lattice: "class.lattice (op \<le>) (op <) inf sup" sublocale lattice_infix < lattice "op \<le>" "op <" inf sup by (rule lattice) After this I used lattice_infix instead of lattice. It seems that this way works better and it is more general that the ways suggested earlier. Viorel

**References**:**Re: [isabelle] Lattices and syntactic classes***From:*Florian Haftmann

**Re: [isabelle] Lattices and syntactic classes***From:*Makarius

**Re: [isabelle] Lattices and syntactic classes***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Wellsortedness error in Quickcheck
- Next by Date: [isabelle] CMCS 2012: call for papers and revised dates
- Previous by Thread: Re: [isabelle] Lattices and syntactic classes
- Next by Thread: Re: [isabelle] Unify.matchers and term representation
- Cl-isabelle-users September 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