[isabelle] The 'The' function


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 MHonArc.