Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] lemma top_empty_eq should not have attribu...


view this post on Zulip Email Gateway (Nov 22 2022 at 14:29):

From: Martin Desharnais <martin.desharnais@posteo.de>
[Repost to isabelle-dev as original email was wrongly sent to
isabelle-users]

Dear Isabelle developers,

When using the [to_pred] attribute to convert a lemma from set-based to
a predicate-based representation, the UNIV constant gets replaced by
"Collect ⊤". This is annoying for predicates that are abbreviations
using UNIV. Consider, e.g., the Relation.total and Relation.totalp
abbreviations.

abbreviation "total ≡ total_on UNIV"
abbreviation "totalp ≡ totalp_on UNIV"

If one tries to convert the following set-based lemma

thm total_inv_image
(* inj ?f ⟹ total ?r ⟹ total (inv_image ?r ?f) *)

to a predicate-based version, one gets the following.

thm total_inv_image[to_pred]
(* inj_on ?f {x. top x} ⟹ totalp_on (Collect top) ?r ⟹ totalp_on
(Collect top) (inv_imagep ?r ?f) *)

This is due to the [pred_set_conv] annotation on the top_empty_eq lemma.
It adds the theorem "⊤ = (λx. x ∈ UNIV)" to simpset when using [to_set]
annotation and theorem "UNIV = {x. ⊤ x}" to simpset when using [to_pred]
attribute. I tried to remove the annotation from this lemma and, without
it, one gets the following nicer result.

thm total_inv_image[to_pred]
(* inj ?f ⟹ totalp ?r ⟹ totalp (inv_imagep ?r ?f) *)

I tested the change on the distribution and the AFP [1] and nothing
breaks. I haven't found a concrete use case for this annotated lemma.
Because the presence of the annotation hurts in some cases and its
absence does not cause problem, I propose to remove it.

PS Note that the annotation was added in 2012 by Lars Noschinski in a
changeset [2] that added many lemmas with this annotation.

PPS The same argument could be made for top_empty_eq2, bot_empty_eq, and
bot_empty_eq2, although I don't have a use-case where the annotation
hurts for them.

[1]: https://ci.isabelle.systems/jenkins/job/testboard/762/
[2]: https://isabelle.in.tum.de/repos/isabelle/rev/eec472dae593


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 28 2022 at 09:19):

From: Tobias Nipkow <nipkow@in.tum.de>
I don't see any reason not to modify this as suggested. Does anybody else?

Tobias
smime.p7s

view this post on Zulip Email Gateway (Dec 05 2022 at 09:35):

From: Martin Desharnais <martin.desharnais@posteo.de>
I made the change in Isabelle/a7d9e34c85e6.

Regards,
Martin
OpenPGP_0x58AE985FE188789A.asc
OpenPGP_signature


Last updated: Feb 24 2024 at 04:17 UTC