[isabelle-dev] Typing problem in autogenerated axiom

[Andreas Schropp]

Dominique Unruh wrote:
> Dear all,
>   

It looks like you only replied to me. ^^

> thanks for the answers.
>
> Let me summarize how I understood things, just to make clear I did not
> misunderstand anything:
>
> * Any constant is treated by the kernel as having no sort annotations.
> Although this leads to constants defined on more types than intended
> by the user, this does not lead to inconsistencies because we could
> always imagine that the constant has some arbitrary value on the extra
> types. (And arbitrary values exist anyway because even Pure already
> ensures non-emptiness of all types.)
>
> * Some axioms that are autogenerated by definitions have no sort
> annotations. E.g., less_eq has an axiom giving its definition for all
> types of the form 'a::{}=>'a::{}=>bool instead of only
> 'a::ord=>'a::ord=>Prop.

You mean 'a::ord=>'a::ord=>bool, right?

> Although such an axiom asserts things about
> less_eq for types outside the typeclass ord (for which the definition
> then usually also does not make much sense), this again does not do
> any harm to consistency because we this simply means that we fix a
> certain meaningless value for less_eq on types for which we would not
> have fixed any value at all otherwise.
>   

Yeah, thats the way I understand it. As I mentioned, I even invent such 
meaningless values in ZF, just to make my code more regular.

> 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. 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).
>   

Let me put this into perspective, in the light of a forthcoming kernel 
extension/modification:
  in this kernel patch, all sort constaints and type class reasoning 
steps are eliminated in proofterms on theorem boundaries, and 
strip_sorted variants of the axioms are asserted on the proofterm side. 
So what remains is a proof which sort and typeclass reasoning 
internalized into the logic.
 From my POV this is needed to translate HOL into logics not involving 
Isabelle-style type classes.

BTW: I would like to hear about your experiences translating HOL->Coq. 
How are you handling type class reasoning and overloading (I prefix an 
unoverloading step) in your HOL->Coq translation? How do you handle the 
interactions between Pure and HOL, or is this even a problem when 
translating into another type theory?

I would actually like it if even axiomatized constants would get 
topsorted declared types in consts.ML
The strangeness in the HOL->ZF translation regarding "fake constants" is 
just a minor annoyance, where a Pure.undefined would help.

> Does anyone know what the reason for these design decisions are?
>
> Best,
> Dominique.
>