[isabelle-dev] Isabelle/HOL axiom ext is redundant
schropp at in.tum.de
Tue Nov 17 21:33:37 CET 2009
Brian Huffman wrote:
>>> I would consider this as an "implementation detail", and not worry about
>>> it any further.
>>> Tools that operate on the level of proof terms can then eliminate
>>> eq_reflection, as was pointed out first by Stefan Berghofer some years ago,
>>> IIRC. (I also learned from him that it is better to speak about Pure as
>>> "logical framework", and not use term "meta logic" anymore.)
>> Yeah, Stefan does this in HOL/Tools/rewrite_hol_proof.ML (which was tested
>> quite thoroughly since 5e20f9c20086, so also in Isa09).
> This is very interesting... I'd like to learn more about the status of
> eq_reflection as a meta-theorem. Is there a paper about this?
I dont know a paper, but Stefan's thesis has a section on the
elimination of eq_reflection and meta_eq_to_obj_eq:
the idea for the elimination is to propagate (by using respective HOL
theorems iffD1,iffD2, trans, refl, sym, cong) the invocation of the
meta_eq_to_obj_eq theorem as far down as possible, so that it should (if
this is a well-behaved HOL proof) be applied to an invocation of the
eq_reflection axiom and both can be eliminated.
AFAIK rewrite_hol_proof also tries to normalize the proof (to make it
"more constructive, less extensional"?), especially by using the real
intro/elim/cong rules for logical connectives instead of the
"artificial" rewriting proofs with iffD1,iffD2. This is also in Stefan's
thesis I think.
Problems arise when "HOL proofs" arent exactly well-behaved, for example
using directly == instead of = in the proposition, or if there are
fragments of locale or type class reasoning in them, which often involve
meta-and (&&&) and sometimes can't be easily internalized. Those are
some of the reasons why I preferred to be robust against any
interactions of Pure and HOL in the translation to ZF.
More information about the isabelle-dev