[isabelle-dev] Typing problem in autogenerated axiom

[Florian Haftmann]

Hi Dominique,

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

This might seem astonishing at first sight but is perfectly ok.  A
"definition" is the introduction of a new constant as being equal to an
existing term which does not contain the constant itself.  Such
definitions are "definitional" since the new constants can be completely
dropped by unfolding them.  So in the strict sense, definitions not only
*can* ignore sort constraints, but *must* ignore sort constraints,
otherwise this unfolding would not be possible in all situations. For
historic reasons, as Andy hinted at, some legacy mechanisms introducing
new definitions produce primitive definitions which carry sort
constraints, but these can be thought of as been derived from
platonistically exisiting unconstrained "more primitive" definitions.

The Isar command "definition" is already a derived specification
mechanisms which, e.g. in the HOL default setup allows parameters on the
left hand side, HOL equality, sort constraints and preconditions.  But
all these are boilt down to a primitive definition from which the
specification as given by the user is derived.

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

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

Sort constraints on constants are just a pecularity of the parser (and
can be changed internally, c.f. Sign.add_const_constraint), *not* a part
of the logical foundation.  To understand, imagine you write down a
"nonsense" term like "(x, y) = 0" ignoring the sort constraint ::zero on
0.  But this does not lead to problems since the only way to give
"meaning" to this term is to instantiate it into theorems, where all
relevant theorems involving 0 have a ::zero constraint.

So, sort constraints are not relevant to definitions or constant
signatures, but to theorems where they carry logical content.

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

The matter of definitions and type classes is dealt with in

http://www4.in.tum.de/~haftmann/pdf/constructive_type_classes_haftmann_wenzel.pdf

A somehow related focus can also be found in

http://www4.in.tum.de/~haftmann/pdf/local_theory_specifications_haftmann_wenzel.pdf


Hope this helps
	Flroain

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 252 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091128/582c9145/attachment.sig>