[isabelle-dev] Typing problem in autogenerated axiom
krauss at in.tum.de
Mon Nov 30 22:13:04 CET 2009
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.
More information about the isabelle-dev