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
