Re: [isabelle] The 'The' function
On 07/31/2012 04:59 PM, Mark Wassell wrote:
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
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_eq_trivial: "(THE x. x = a) = (a::'a)"
(which could equivalently be written as "The (%x. x = a) = (a::'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
How can I prove theorems that involve The? For example, it would seem that
EX x. f x ==> a = The f ==> f a
lemma "Ex x. f x ==> a = The f ==> f a"
and nitpick will show you a counter-example.
This is just reflexivity of "op =", since the left-hand side and
right-hand side are equal (just using syntactic sugar on the right).
The f = (THE x. f x)
lemma "The f = (THE x. f x)"
by (rule refl)
This archive was generated by a fusion of
Pipermail (Mailman edition) and