[isabelle-dev] Typing problem in autogenerated axiom
Andreas Schropp
schropp at in.tum.de
Sat Nov 28 15:45:48 CET 2009
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
More information about the isabelle-dev
mailing list