Re: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy



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

Am 26/08/2013 12:52, schrieb Christoph LANGE:
> 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
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.