*To*: "Roger H." <s57076 at hotmail.com>*Subject*: Re: [isabelle] SOME-operator*From*: René Thiemann <rene.thiemann at uibk.ac.at>*Date*: Thu, 23 May 2013 10:05:28 +0200*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DUB124-W326DE4FC20519D726587B48FA90@phx.gbl>*References*: <DUB124-W326DE4FC20519D726587B48FA90@phx.gbl>

Dear Roger, yes it is True, and the crucial lemma is "someI": lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}" proof (rule someI) let ?a = "SOME x. True" show "Domain {(2,?a), (3,?a)} = {2,3}" by auto qed the "SOME x. True" is just some arbitrary element in the range of your relation. (You did not specify the type of the relation, hence the usage of the polymorphic SOME. Kind regards, René Am 22.05.2013 um 20:51 schrieb "Roger H." <s57076 at hotmail.com>: > > > Hello, > > > is this lemma true? > > > lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}" > > > if yes, how can it be proved? > > > Thank you! > > > >

**Follow-Ups**:**Re: [isabelle] SOME-operator***From:*Lars Noschinski

**References**:**[isabelle] SOME-operator***From:*Roger H .

- Previous by Date: Re: [isabelle] SOME-operator
- Next by Date: Re: [isabelle] Set of functions
- Previous by Thread: Re: [isabelle] SOME-operator
- Next by Thread: Re: [isabelle] SOME-operator
- Cl-isabelle-users May 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