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

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

From: Martin Desharnais <martin.desharnais@posteo.de>

I made the change in Isabelle/a7d9e34c85e6.

Regards,

Martin

OpenPGP_0x58AE985FE188789A.asc

OpenPGP_signature

Last updated: Feb 24 2024 at 04:17 UTC