# Re: [isabelle] The 'The' function

```Hi Mark,

Am Dienstag, den 31.07.2012, 08:59 +0100 schrieb Mark Wassell:
> I am looking for some information on The :: ('a => bool) => 'a
>
> I see in HOL.thy that it is listed in the axioms and there is an
> abbreviation for THE that uses it. The tutorial covers THE in the section
> on the definite description operator and I see a number of lemmas involving
> THE. However I can find very little on The.
>
> How can I prove theorems that involve The? For example, it would seem that
>
> EX x. f x ==> a = The f ==> f a
>
> should hold

You seem to confuse The and Eps (aka "SOME x. f x", from
Hilbert_Choice.thy) The is only defined when there is exactly one
element that satisfies the predicate. So you can either prove

lemma "∃! x. f x ==> a = The f ==> f a"
by(erule ssubst, erule the1I2)

or

lemma "∃ x. f x ==> a = Eps f ==> f a"
by(erule ssubst, erule exE, rule someI)

> and that the following is true.
>
> The f = (THE x. f x)

Yes, this is true and only looks different:

lemma "The f = (THE x. f x)"
by (rule refl)

Greetings,
Joachim

--
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.info.uni-karlsruhe.de/~breitner
```

Attachment: signature.asc
Description: This is a digitally signed message part

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