Email Gateway (Nov 22 2022 at 14:29): 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
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
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: Apr 23 2024 at 20:15 UTC