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)


        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)


Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter

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

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