[isabelle-dev] Typing problem in autogenerated axiom

[Andreas Schropp]

Dominique Unruh wrote:
> Dear all,
>
> while trying to export proof terms from Isabelle, I stumbled upon the
> following typing issue which might be a bug.
>
> In HOL.thy, an axiom class ord is defined which fixes a constant
> less_eq (syntactic sugar is <=):
>
>   
>> term HOL.ord_class.less_eq;
>>     
> "op <="
>   :: "'a::ord => 'a::ord => bool"
>
> In Ordering.thy, an instantiation for the type constructor fun of this
> axiom class is given. Besides other things, this instantiation defines
> the axiom le_fun_def_raw:
>
>   
>> ML {* Thm.axiom (the_context()) "Orderings.le_fun_def_raw" *};
>>     
> val it =
>    "ord_fun_inst.less_eq_fun ==
>       %(f::?'a::{} => ?'b::{}) g::?'a::{} => ?'b::{}.
>          ALL x::?'a::{}. f x <= g x" : Thm.thm
>
> Notice the "f x <= g x" part which represents an application of
> HOL.ord_class.less_eq (you can verify this by adding "|> Thm.prop_of"
> before *} in the above ML command). f x and g x have type "?'b::{}"
> which does not have class ord. So less_eq needs to have type "?'b::{}
> => ?'b::{} => bool" which does does not match "'a::ord => 'a::ord =>
> bool". So, as far as I understand the type system of Isabelle, the
> axiom le_fun_def_raw is not well-typed.
>
> (NB: You cannot get the axiom le_fun_def_raw by writing "thm
> Orderings.le_fun_def_raw" in the Isabelle toplevel, this only
> retrieves the theorem with the same name. This theorem has different
> types.)
>
> My question is the following:
>
> * Is this a bug?
>   
/
/No, just idiosyncraticies, see below.
BTW: approx one year ago I also stumbled upon this, perhaps we need an 
FAQ for such things.

> * If not, why is le_fun_def_raw well-typed?

The typing rules for terms in the kernel dont check for well-sortedness.
But AFAIK the parser demands well-sortedness, thus resulting in confusion.

> Where can I find a
> description of Isabelle's type system?
>   

If you want a formal account on the current implementation, I only know 
about my own sketches of the Isa09 kernel from 2 months ago. These are 7 
pages pencil-on-paper with german comments, are not reviewed and assume 
some familiarity with the implementation.

The constant-typing rule might be of interest:

  thy |- tau :: ctyp     tau is a raw instance of thy_consttyp(c)
=======================================
   thy |- c_tau :: tau

meaning that if the type tau can be certified (which means that sort 
constaints on type variables are normalized and type constructors have 
the right arities) in theory thy and tau is a possibly non-wellsorted 
instance of the declared type thy_consttyp(c) of constant c in theory 
thy, which just means that there exists a type-substitution sigma not 
necessarily respecting sort-constraints of typvars with 
sigma(thy_consttyp(c))=tau, then
the constant c (as always annotated with type tau) can be given the type 
tau in theory thy.


> Best wishes,
> Dominique.
>
>
> PS: I noticed the following possibly related fact:
>
>   
>> ML {* the_context() |> Sign.consts_of |> (fn c => Consts.read_const c "HOL.ord_class.less_eq") *};
>>     
> val it = Const ("HOL.ord_class.less_eq", "?'a::{} => ?'a::{} => bool")
> : Term.term
>
> Now suddenly the type of less_eq does not contain type classes, in
> contrast to what "term HOL.ord_class.less_eq;" outputs. I do not
> understand why.
>   

If the definition-mechanism used is "high-level enough" (which is almost 
always the case) then constants get "topsorted" types and definitions 
(so they have no type class constraints) before they enter the kernel.
Parsing and pretty-printing seem to recover the constaints (which are 
registered by type class and overloading definitions, I guess).

Regards,
  Andy