Re: [isabelle] Trying to rename Lattices.thy
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 +
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.
On Sun, Jun 24, 2012 at 6:56 AM, Gottfried Barrow
<gottfried.barrow at gmx.com> wrote:
> 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
> 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 ⇒
> 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".
This archive was generated by a fusion of
Pipermail (Mailman edition) and