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



Surely — I'm surprised it isn't there already.
Larry Paulson


On 26 Aug 2013, at 11:52, Christoph LANGE <math.semantic.web at gmail.com> wrote:

> 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
> 
> -- 
> Christoph Lange, School of Computer Science, University of Birmingham
> http://cs.bham.ac.uk/~langec/, Skype duke4701
> 
> → Mathematics in Computer Science Special Issue on “Enabling Domain
>  Experts to use Formalised Reasoning”; submission until 31 October.
>  http://cs.bham.ac.uk/research/projects/formare/pubs/mcs-doform/
> 





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