Re: [isabelle] Trying to rename Lattices.thy



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
>
>
>
>
>
>
>
>
>
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.