Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Issues with unnamed top-level facts in Isa...


view this post on Zulip 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:

I see three possible ways to do improve this:

  1. 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)

  2. Make unnamed top level facts accessible as theory facts, and improve
    the tools to use them properly

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Mar 04 2024 at 10:08 UTC