It allows to have one simplifier for == and translate the result from == into =. It is a convenience and we could eliminate all occurences of it from proofs if we cared.
Tobias Am 17/02/2012 08:11, schrieb Christian Sternagel: > 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
