*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Mon, 26 Aug 2013 14:32:02 +0200*In-reply-to*: <521B335D.4030104@gmail.com>*References*: <521B335D.4030104@gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.8; rv:17.0) Gecko/20130801 Thunderbird/17.0.8

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 >

**References**:**[isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy***From:*Christoph LANGE

- Previous by Date: Re: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
- Next by Date: Re: [isabelle] frequent jEdit crash (Mac OS10.8.4; Isabelle 2013)
- Previous by Thread: Re: [isabelle] An easy (?) set comprehension lemma that should probably be in Set.thy
- Next by Thread: [isabelle] Kleene's Ternary Logic
- Cl-isabelle-users August 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list