Email Gateway (Aug 18 2022 at 20:11): Email Gateway (Aug 18 2022 at 20:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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
Email Gateway (Aug 18 2022 at 20:11):From: Brian Huffman <huffman@in.tum.de>
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.
Email Gateway (Aug 18 2022 at 20:11):From: Tjark Weber <webertj@in.tum.de>
"Yea, don't do that."
Isabelle/HOL is based upon a complex bootstrapping process, with
intertwined setup of theories and proof tools. If you import Main, you
get a reasonably clean entry point. If you import anything below Main,
you may be exposed to the intricacies of this process.
If you are sure this is what you want, you can load Lattices.thy (and
other theories that are part of Isabelle/HOL) by choosing Pure as the
logic image for your session: e.g.,
isabelle jedit -l Pure Isabelle2012/src/HOL/Lattices.thy
Best regards,
Tjark
Email Gateway (Aug 18 2022 at 20:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
Tjark,
One of the main purposes is to open up HOL distribution sources for
reference purposes while I'm doing my own HOL theories. And it's nice to
do that in jEdit so that I can copy and paste original lemmas, etc.,
rename them, and experiment with them in the same file.
Renaming Lattices.thy to Li12H05lat.thy works, so that's good enough.
However, when renaming other theories, if I have a problem, I'll use
Pure as the logic to make sure that the problem is not a conflict due to
having HOL loaded as the logic.
Regards,
GB
Email Gateway (Aug 18 2022 at 20:11):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 6/24/2012 2:50 AM, Brian Huffman wrote:
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.
I wouldn't want to be rearranging anything in a distribution source to
"fix it", but that might be good information for the future.
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...
Thanks for the help. No reason for me to be in the loop beyond this.
Regards,
GB
Email Gateway (Aug 18 2022 at 20:12):From: Lars Noschinski <noschinl@in.tum.de>
Loading the HOL theories starting from Pure in jEdit can be done, but it
is not straight-forward. Files need to be opened in a specific order
(and/or you need a lot of reloading files), as jEdit does not yet handle
the definition of new commands very well.
-- Lars
Email Gateway (Aug 18 2022 at 20:12):From: Lawrence Paulson <lp15@cam.ac.uk>
I have often done this using PG (both for HOL theories and for ZF ones), where it has always worked perfectly.
Larry
Email Gateway (Aug 18 2022 at 20:13):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Files need to be opened in a specific order (and/or you need a lot of reloading files), as jEdit does not yet handle the definition of new commands very well.
AFAIK this restriction does not hold any longer.
Florian
Email Gateway (Aug 18 2022 at 20:13):From: Makarius <makarius@sketis.net>
On Sun, 24 Jun 2012, Tjark Weber wrote:
On Sat, 2012-06-23 at 23:56 -0500, Gottfried Barrow 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."Yea, don't do that."
Isabelle/HOL is based upon a complex bootstrapping process, with
intertwined setup of theories and proof tools. If you import Main, you
get a reasonably clean entry point. If you import anything below Main,
you may be exposed to the intricacies of this process.
Indeed. Importing anything apart from Main or Complex_Main means you
investigate the way Isabelle/HOL is bootstrapped, so it is no good for
applications, but sometimes helps to understand how things work.
If you are sure this is what you want, you can load Lattices.thy (and
other theories that are part of Isabelle/HOL) by choosing Pure as the
logic image for your session: e.g.,isabelle jedit -l Pure Isabelle2012/src/HOL/Lattices.thy
Yes, this is the official workaround to peek into parts of the
Isabelle/HOL session, until the next big reform of the theory loader in
connection with the interactive document model.
In rare cases one does have to rename such an intermediate theory, but
then the obvious thing is to turn Lattices into Lattices1, say. This
might require some other renaming nonetheless, as you have noticed
already.
Makarius
Email Gateway (Aug 18 2022 at 20:13):From: Makarius <makarius@sketis.net>
See Isabelle2012/NEWS:
* Prover IDE (PIDE) improvements:
- support for user-defined Isar commands within the running session
For most practical situation you just load the theory that you have in
mind, and it should all work as expected. (There might still be an odd
boundary case where one final "File / Reload" in jEdit is needed after all
new commands have been defined via loading the imports.)
Makarius
Last updated: Nov 21 2024 at 12:39 UTC