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.