# Re: [isabelle] The 'The' function

Dear Mark,
On 07/31/2012 04:59 PM, 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.

`Well, it's not an abbreviation but a syntax translation (sorry for
``nitpicking, but those differences occasionally matter). The net outcome
``is that we can write "THE x. f x" interchangeably with "The f". What I'm
``trying to say is that everything you find on 'THE' (where lemma names
``usually use the lowercase "the") is in fact a statement about 'The'
``(i.e., informally speaking The and THE are the same). The axiomatization
``in HOL is
`
the_eq_trivial: "(THE x. x = a) = (a::'a)"
(which could equivalently be written as "The (%x. x = a) = (a::'a)").

How can I prove theorems that involve The? For example, it would seem that
EX x. f x ==> a = The f ==> f a

`This is not a valid fact as can be found out by nitpicking again (sorry
``for the joke, I mean the Isabelle tool nitpick this time). Just type
`
lemma "Ex x. f x ==> a = The f ==> f a"
nitpick
and nitpick will show you a counter-example.

The f = (THE x. f x)

`This is just reflexivity of "op =", since the left-hand side and
``right-hand side are equal (just using syntactic sugar on the right).
`
lemma "The f = (THE x. f x)"
by (rule refl)
cheers
chris

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