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.
On 31 Jul 2012, at 08:59, Mark Wassell wrote:
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and