# Re: [isabelle] SOME-operator

Am Mittwoch, den 22.05.2013, 20:51 +0200 schrieb Roger H.:
> Hello,
>
>
> is this lemma true?
> lemma "Domain (SOME r. Domain r = {2,3}) = {2,3}"
Yes this lemma is true, The SOME operator returns a fixed but arbitrary
element r which has the property "Domain r = {2,3}", if such an r
exists. You only need to provide a existence proof.
> if yes, how can it be proved?
You can use find_theorems:
find_theorems "?P (SOME x. ?P x)"
This shows you a list of interesting theorems. They help you to reduce
your lemma to an existence proof.
In the existence proof you need to construct a relation with a domain of
"{2,3}" for example "{(2, 2), (3, 3)}".
- Johannes

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