Hi Brian, thanks a lot for the pointer!
What the comment next to eq_reflection really means, would have been my next question ;). Anybody?
cheers chris On 02/17/2012 03:58 PM, Brian Huffman wrote:
Hi Christian, Please see this thread from isabelle-dev, November 2009: https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2009-November/000713.html To summarize: A theorem meta_ext (like ext but using meta-equality "==" instead of "=") is derivable using only theorem operations of Isabelle's proof kernel; this is what it means to say that extensionality is built into the meta-logic. Axiom ext is actually derivable from meta_ext, but only by using axiom eq_reflection, which is labeled as an "admissible axiom". (I guess that means that it is not one of the usual axioms of HOL, but that adding it as an axiom is somehow conservative, in that it doesn't extend the set of provable object-level formulas in HOL. I'm not exactly sure about that, though.) axiomatization where eq_reflection: "x = y ==> x == y" (*admissible axiom*) - Brian On Fri, Feb 17, 2012 at 3:46 AM, Christian Sternagel <[email protected]> wrote: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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
