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

[Andreas Schropp]

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.

Regards,
  Andy