[isabelle-dev] Typing problem in autogenerated axiom

[Alexander Krauss]

Dominique Unruh wrote:
>> This answers the question why there is no harm in removing sorts (at
>> least from constants and definitions, not of course from class
>> axioms). I am still wondering what the reasons for doing so are. At a
>> first glance, at least, it would seem more natural to me if the
>> constants and definitional axioms would have sort annotation. Also,
>> the argument given by Florian ("definitions not only *can* ignore sort
>> constraints, but *must* ignore sort constraints, otherwise this
>> unfolding would not be possible in all situations.") does not convince
>> me, because since in a normal proof, we would never even have an
>> occurrence of a constant with the "wrong" sorts, so there is no need
>> for a definition that allows unfolding in such situations.

I also think that the "unfolding principle" would still work with class 
constraints, under the assumption that the terms are well-sorted, which 
would then also have to be checked on the low level...

On the other hand, the fact that definitions can be class-less shows 
that the two concepts are mostly orthogonal, which I guess does simplify 
the kernel a little bit. Making the other axioms also class-less 
(possibly with internalized OFCLASS constraints) would make things more 
regular... As Andy mentioned, there will be some changes in the 
management of type classes in the near future, but a few problems need 
to be sorted out first.

With the situation as in Isabelle 2009 or 2009-1, it is probably very 
hard to translate proofs that involve type classes, since the 
Thm.class_triv and Thm.unconstrainT inference rules do not produce 
proper proof terms. The missing information can probably be 
reconstructed, but this is not fun at all.

>> Also, as
>> mentioned by Andreas, stripping sort constraints may make it much
>> harder to interpret Isabelle/HOL in other logics (be it ZF as in
>> Andreas case, or my experiments of translating Isabelle/HOL to Coq).

Our hope is to be able to eliminate classes from proof terms (and, in a 
separate step, also from definitions) entirely, which makes such 
translations much simpler again.

Alex