[isabelle-dev] Typing problem in autogenerated axiom
Dominique Unruh
unruh at mmci.uni-saarland.de
Sat Nov 28 13:11:58 CET 2009
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?
* If not, why is le_fun_def_raw well-typed? Where can I find a
description of Isabelle's type system?
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.
More information about the isabelle-dev
mailing list