[isabelle-dev] lemma top_empty_eq should not have attribute pred_set_conv

[Tobias Nipkow]

I don't see any reason not to modify this as suggested. Does anybody else?

Tobias

On 22/11/2022 15:29, Martin Desharnais wrote:
> [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 at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5535 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20221128/7b555a87/attachment.bin>