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

[Martin Desharnais]

[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