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

[Martin Desharnais]

I made the change in Isabelle/a7d9e34c85e6.

Regards,
Martin

Le 2022-11-28 à 10 h 19, Tobias Nipkow a écrit :
> 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
> 
> _______________________________________________
> 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: OpenPGP_0x58AE985FE188789A.asc
Type: application/pgp-keys
Size: 3139 bytes
Desc: OpenPGP public key
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20221205/37b076fd/attachment.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: OpenPGP_signature
Type: application/pgp-signature
Size: 840 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20221205/37b076fd/attachment.sig>