Email Gateway (Nov 05 2020 at 15:39): Email Gateway (Nov 05 2020 at 15:39):From: Fabian Huch <huch@in.tum.de>
Hi,
unnamed facts at the top level of a theory (i.e., unnamed lemmas or
theorems) don't work smoothly with the rest of Isabelle.
For instance:
they appear nowhere in the theory exports (naively, one could think
they appear as literal facts)
unused_thms ignores them and thus will report facts that are only used
by unnamed facts as unused
I see three possible ways to do improve this:
Make it explicit that unnamed top level facts are for "demonstration
purposes only" and should otherwise not be used
(for instance by creating a distinct command for unnamed
lemmas/theorems and requiring a name otherwise)
Make unnamed top level facts accessible as theory facts, and improve
the tools to use them properly
Keep the handling for unnamed facts as is, but tweak the tools a bit
(for instance, assume [simp] lemmas always used in unused_thms)
Which route should we go?
Fabian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2020 at 15:48):From: Makarius <makarius@sketis.net>
This behaviour it formal items with empty name binding is rather profound in
Isabelle.
The treatment of unnamed facts in particular is also fairly canonical
concerning our own standards.
Can you say what is wrong with this, and why it needs to be "improved"?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2020 at 15:52):From: Tobias Nipkow <nipkow@in.tum.de>
I don't see any reason for allowing unnamed toplevel lemmas in a theory. Why
should we continue to offer it? They are not useful, except for demo purposes,
but then there are alternatives and it is also a bad idea to demo something that
should be avoided.
Tobias
smime.p7s
Email Gateway (Nov 05 2020 at 15:56):From: Makarius <makarius@sketis.net>
Such a profound change of how Isabelle works needs good justifications. And
afterwards it usually takes years to get such a change through.
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2020 at 16:04):From: Fabian Huch <huch@in.tum.de>
unused_thms reporting thms that are not unused does seem strange to me.
Fabian
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Nov 05 2020 at 16:06):From: Tobias Nipkow <nipkow@in.tum.de>
I gave some good reasons. In fact such unnamed lemmas can be a downright pain, eg
lemma [simp]: "..."
Can you give a good reason to keep them other than "we always did it like that"?
I mean a real reason like "they are required because" or "it would break X".
Can you explain why you think it will take years to add names to existing
unnamed thms? Not that it matters that much if we agree that it should be changed.
Tobias
smime.p7s
Email Gateway (Nov 09 2020 at 13:40):From: Makarius <makarius@sketis.net>
I will come back to this soon (presently diverging into other old mails).
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Last updated: Dec 21 2024 at 16:20 UTC