Re: [isabelle] The 'The' function

The following theorems (which you can find in .../src/HOL/HOL.thy) should cover all your needs.


Your first conjecture isn't true, because The is a definite description operator: the specified entity must be unique. If you want the Hilbert indefinite description operator, along with the axiom of choice, then you need Eps.

Your second conjecture is simply a syntactic identity.

Larry Paulson

On 31 Jul 2012, at 08:59, Mark Wassell wrote:

> Hi,
> 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 and that the following is true.
> The f = (THE x. f x)
> My usual tactic of grepping thy files and searching the PDF files is
> failing me here for obvious reasons.
> Mark

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