[isabelle-dev] Explanation required
Christian Sternagel
c-sterna at jaist.ac.jp
Fri Feb 17 03:46:41 CET 2012
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?
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
More information about the isabelle-dev
mailing list