*To*: Viorel Preoteasa <viorel.preoteasa at abo.fi>*Subject*: Re: [isabelle] problem with class and sulocale declarations*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Wed, 08 Sep 2010 13:42:33 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4C874E4B.5090207@abo.fi>*Organization*: TU München, Lehrstuhl Software and Systems Engineering*References*: <4C873677.6010001@abo.fi> <4C873BA2.6030603@informatik.tu-muenchen.de> <4C874E4B.5090207@abo.fi>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.11) Gecko/20100713 Thunderbird/3.0.6

Hi Viorel, sorry for that problem. Its technical source is rather obscure (c.f. http://isabelle.in.tum.de/repos/isabelle/rev/95a41e6ef5a8). Until the next Isabelle release however we somehow have to live with it. Since an explicit annotation fails in your example, I would suggest an auxiliary class with zero and one: > class sup_a = > fixes sup_a :: "'a => 'a => 'a" (infixl "⊔1" 65) > > class inf_a = > fixes inf_a :: "'a => 'a => 'a" (infixl "⊓1" 65) > > class test = ord + times + one + sup_a + inf_a + > assumes a[simp]: "a = 1" > and b[simp]:"a = b" > and [simp]: "a ≤ b" > and [simp]: "¬ a < b" > begin > end > > sublocale test < testlattice!: lattice "op ≤" "op <" "op ⊓1" "op ⊔1" > apply unfold_locales > by simp_all > > class zero_one = zero + one > > class bounded = zero_one + test The obscure problem is likely to occur if classes are combined with different parameters which are not mentioned in the body of the class declaration, e.g. by assume. > 1. Why squnion and sqinter symbols are not defined in separate classes > as most of the other symbols? This would make there reuse simpler. The point is that inf and sup carry *no* syntax by default, so you are free to use squnion and sqinter in syntax as you like; only by importing Lattice_Syntax from the library this gets attached to inf and sup. > 2. Why the proof for the above sublocale fails if I remove assumption b > from test? > assumption a should replace any element with 1. a is not applied by the simplifier since it would loop: "a = 1 = 1 = 1 = ...". You can apply it manually e.g. using apply (subst a). 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] problem with class and sulocale declarations***From:*Viorel Preoteasa

**References**:**[isabelle] problem with class and sulocale declarations***From:*Viorel Preoteasa

**Re: [isabelle] problem with class and sulocale declarations***From:*Florian Haftmann

**Re: [isabelle] problem with class and sulocale declarations***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] adm and fixrec’s induct rules
- Next by Date: Re: [isabelle] problem with class and sulocale declarations
- Previous by Thread: Re: [isabelle] problem with class and sulocale declarations
- Next by Thread: Re: [isabelle] problem with class and sulocale declarations
- Cl-isabelle-users September 2010 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