*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Trying to rename Lattices.thy*From*: Brian Huffman <huffman at in.tum.de>*Date*: Sun, 24 Jun 2012 09:50:08 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <4FE69DF2.7000204@gmx.com>*References*: <4FE69DF2.7000204@gmx.com>

Hi Gottfried, I tried renaming Lattices.thy to "Attices.thy", as you suggested. It appears that the errors you get are caused by various locale predicates (like class.boolean_algebra or class.semilattice_inf) having different argument orders. If you rearrange the arguments into the right order again, everything else should work. For example, here are the argument orders for the boolean_algebra locale predicate, before and after: "Lattices.thy": class.boolean_algebra ?minus ?uminus ?inf ?less_eq ?less ?sup ?bot ?top "Attices.thy": class.boolean_algebra ?inf ?less_eq ?less ?sup ?bot ?top ?minus ?uminus I have no idea why the the argument order would depend on the theory name. This seems like a really undesirable "feature". I would suggest to the other developers that we adopt a more predictable behavior: How about having the class/locale definition determine the argument order? For example, with class boolean_algebra = distrib_lattice + bounded_lattice + minus + uminus + assumes ... the class.boolean_algebra predicate should first have arguments of class.distrib_lattice, followed by those of class.bounded_lattice (filtering out duplicates), and finally minus and uminus. - Brian On Sun, Jun 24, 2012 at 6:56 AM, Gottfried Barrow <gottfried.barrow at gmx.com> wrote: > Hi, > > I'm trying to rename HOL/Lattices.thy so I can load it, experiment with it, > and mark it up, but it's picky about what it's name can be. > > I renamed the first three HOL theories, replaced any use commands in them, > such as `use "Tools/abel_cancel.ML"`, with the actual ML, and replaced any > fully qualified names with the new theory name. > > They all load without any errors. The renaming is like this: > > HOL.thy is renamed i12H02hol_0ed.thy > Orderings.thy is renamed i12H03ord_0ed.thy > Groups.thy is renamed i12H04grp_0ed.thy > > I try to rename Lattices.thy, but it appears that the main requirement is > that the first letter of the name be capital "L". Names that have worked are > these: > > L2.thy > Lattice2.thy > Lattices_i12H05lat_0ed.thy > > If the first letter of the name is lowercase, such as "lattices.thy" or > "iLattices.thy", it gets down to line 75, > > lemma dual_semilattice: > "class.semilattice_inf sup greater_eq greater" > > and it gives this error: > > Type unification failed: No type arity HOL.bool :: iLattices.sup > Failed to meet type constraint: > Term: op ⊔ :: (??'a∷iLattices.sup ⇒ (??'a∷iLattices.sup ⇒ > ??'a∷iLattices.sup)) > Type: (HOL.bool ⇒ (HOL.bool ⇒ HOL.bool)) > > If the first letter of the name is capitalized, but not "L", such as > "Attices.thy", it gets to line 431, > > lemma dual_boolean_algebra: > > and gives the error: > > Type unification failed: Occurs check! [and so forth] > > It's no big deal. It just messes up my naming scheme, and the fact that I've > renamed the other three files causes me to wonder about this. > > If there's no problem, maybe someone can at least tell me something like, > "Yea, don't do that". > > Thanks, > GB > > > > > > > > > >

**Follow-Ups**:**Re: [isabelle] Trying to rename Lattices.thy***From:*Gottfried Barrow

**References**:**[isabelle] Trying to rename Lattices.thy***From:*Gottfried Barrow

- Previous by Date: [isabelle] Trying to rename Lattices.thy
- Next by Date: Re: [isabelle] Trying to rename Lattices.thy
- Previous by Thread: [isabelle] Trying to rename Lattices.thy
- Next by Thread: Re: [isabelle] Trying to rename Lattices.thy
- Cl-isabelle-users June 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