[isabelle] Trying to rename Lattices.thy



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.