Email Gateway (Nov 22 2022 at 14:06): Email Gateway (Nov 22 2022 at 14:06):From: Martin Desharnais <martin.desharnais@posteo.de>
Dear Isabelle developpers,
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
Last updated: Apr 20 2024 at 01:05 UTC