[isabelle-dev] Explanation required

[Tobias Nipkow]

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
>> <c-sterna at jaist.ac.jp>  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
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>>>
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev