*To*: TIMOTHY KREMANN <twksoa262 at verizon.net>*Subject*: Re: [isabelle] Question about sets?*From*: Amine Chaieb <ac638 at cam.ac.uk>*Date*: Wed, 04 Feb 2009 09:19:21 +0000*Cc*: Isabelle List <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <908398.4842.qm@web84007.mail.mud.yahoo.com>*References*: <908398.4842.qm@web84007.mail.mud.yahoo.com>*User-agent*: Thunderbird 2.0.0.19 (Macintosh/20081209)

Your goal can be solved e.g. like this: unfolding Collect_def by blast

Hope it helps, Amine. TIMOTHY KREMANN wrote:

I have the following subgoal: \<And> (n::nat) (f::nat=>'a) (x::'a). {y. \<exists> j < n . y = f j} x ==> \<exists> i < n . f i = xI need to get the j where x = f j and then instantiate the i to that value.I am such a neophyte that I do not know how to do this.Any suggestions would be appreciated.Tim

**References**:**[isabelle] Question about sets?***From:*TIMOTHY KREMANN

- Previous by Date: [isabelle] TPHOLs'09 Last Call for Papers
- Next by Date: [isabelle] Any one seen this error before?
- Previous by Thread: [isabelle] Question about sets?
- Next by Thread: [isabelle] postdoc position on compliance
- Cl-isabelle-users February 2009 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