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.