[isabelle-dev] Explanation required

[Tobias Nipkow]

Am 17/02/2012 03:46, schrieb Christian Sternagel:
> Dear all,
> 
> please forgive my annoying questioning. Could anybody elaborate on the
> following comment (to be found in HOL.thy):
> 
>   ext: "(!!x::'a. (f x ::'b) = g x) ==> (%x. f x) = (%x. g x)"
>   -- {*Extensionality is built into the meta-logic, and this rule
>        expresses a related property.  It is an eta-expanded version
>        of the traditional rule, and similar to the ABS rule of HOL*}
> 
> How is extensionality already part of the meta-logic (and how could it
> be applied, e.g., in Isabelle/ML)? And why is "ext" needed? Shouldn't
> this be derivable if we have extensionality?

You can derive extensionality in the meta-logic, but for ==. This is
what "related" means. It so happens that I later added eq_reflection,
for conveniece, which could now be used to derive ext, but I would not
like to depend on eq_reflection too much.

Tobias

> I know that I read about this in some HOL book, but I forgot in which
> one. Maybe someone could clarify also the following:
> 
> For me, extensionality in the meta-logic would be something like "(!!x.
> f x == g x) ==> f == g", i.e., (almost) the eta-contracted variant of
> "ext" above. Is the eta-expanded version (i.e., ext) merely convenient
> or really needed?
> 
> cheers
> 
> chris
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev