[isabelle-dev] Isabelle/HOL axiom ext is redundant

[Tobias Nipkow]

> So eq_reflection is an axiom, but we all agree to pretend it's not an
> axiom? This is just weird.

I prefer not to rely on it unless we have to in case it disappears
again. Although I notice it is used quite a lot.

>> While we're discussing it: I wonder sometimes what the role of == was in
>> earlier days of Isabelle. When viewing Pure as the natural deduction
>> framework to encode my logic, I usually interpret ==> as the "is derivable
>> from" relation, and !!x as the "this derivation can be done uniformly for
>> all x". But I have no such clear idea about ==. Rather I have the feeling
>> that with extensionality, == is quite strong compared to this... Was it
>> always like this? Or has the simplifier anything to do with this story?

eq_reflection was introduced because the simplifier works on == but
eventually needs to derive an = theorem. This may no longer be the case.

> Anyway, since eq_reflection actually *is* an axiom, and (=) actually
> *does* mean the same thing as (==), then I really don't see any reason
> why we need to have both (or separate bool and prop types, for that
> matter). I don't know of any other HOL provers that do.

Other HOL provers do not build on a logical framework. When I set up
Isabelle/HOL, I followed the standard principle of logical frameworks:
encode your object logic via the meta logic. Your suggestion is to
extend the meta logic with new axioms for the meta-level connectives. It
never occurred to me and would have lead to a hybrid situation: the
original inference rules for the logic are encoded as ML functions, the
new ones via data. It may work well or it may lead to other unforseen
complications. But it's unrealistic to change it now. Although I agree
that the two levels can get in the way.

Tobias