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

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".



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.

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