*To*: Mark Wassell <mpwassell at gmail.com>*Subject*: Re: [isabelle] The 'The' function*From*: Joachim Breitner <breitner at kit.edu>*Date*: Tue, 31 Jul 2012 10:35:32 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAK0o7cYuqM59xZv=ab1RHn7H8wXez2rCMS_0ffYzTg4vp6RWxg@mail.gmail.com>*References*: <CAK0o7cYuqM59xZv=ab1RHn7H8wXez2rCMS_0ffYzTg4vp6RWxg@mail.gmail.com>*Sender*: Joachim Breitner <msg at joachim-breitner.de>

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**

**References**:**[isabelle] The 'The' function***From:*Mark Wassell

- Previous by Date: Re: [isabelle] The 'The' function
- Next by Date: Re: [isabelle] The 'The' function
- Previous by Thread: Re: [isabelle] The 'The' function
- Next by Thread: Re: [isabelle] The 'The' function
- Cl-isabelle-users July 2012 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