Email Gateway (Aug 19 2022 at 11:42): Email Gateway (Aug 19 2022 at 11:42):From: Christoph LANGE <math.semantic.web@gmail.com>
Hi all,
I wanted to improve the readability of an easy lemma about set theory
and used the following set comprehension syntax, for some concrete
function f and set S:
{ f x | x . x ∈ S }
After this step my lemma turned out to be very hard to prove.
But it turned out that, once I had the following lemma in place, my
original lemma was again quite easy to prove with metis:
lemma "{ f x | x . x ∈ S } = f ` S" by auto
So maybe this lemma should be part of Set.thy? I didn't know how to
name it appropriately, but I think the name should somehow contain the
parts "image", "Collect" and "mem".
Cheers,
Christoph
Email Gateway (Aug 19 2022 at 11:42):From: Lawrence Paulson <lp15@cam.ac.uk>
Surely — I'm surprised it isn't there already.
Larry Paulson
Email Gateway (Aug 19 2022 at 11:42):From: Tobias Nipkow <nipkow@in.tum.de>
I am reluctant to add this lemma because there are many related lemmas one might
also want, eg {f x|x. x : S & P x} = f {x:S. P x}. This looks like it would
better be treated by a general procedure for converting set comprehensions into
pointfree form. In fact, Lukas installed such a simproc, but it is only
activated when the set comprehension occurs inside "finite". For example,
"finite{f x|x. x:S}" is rewritten to "finite (f S)", although this is not
always a blessing. If we provided the underlying rewrite procedure explicitly,
it would perform all the rewrites you want, but you would first need to know
that it exists at all.
In short, I am not quite sure how to handle such conversions best and am not
convinced that one such lemma helps that much, esp since auto already proves it
(but not s/h...).
Tobias
Last updated: Apr 19 2024 at 12:27 UTC