[isabelle] problem with sort inference



I'm having a problem with sort inference in Isabelle/HOL: when I enter

lemma "b = a ==> f a (g a) = f b (g b)"

the following types and sorts are inferred:

variables:
  g :: 'a => 'c
  f :: 'a => 'c => 'b
  a, b :: 'a
type variables:
  'a, 'b :: type
  'c :: {}

Note the sort {} for type variable 'c. This prevents me to do something like

lemma "b = a ==> f a (g a) = f b (g b)"
proof -
  from fun_cong have "f a = f b ==> f a (g a) = f b (g a)"

which yields

*** Type unification failed: Variable 'c::{} not of sort type
*** Type error in application: Incompatible operand type

since fun_cong expects functions between types of sort "type".

I can get around this problem by stating the lemma in the form

lemma "b = a ==> (f::'a => 'c => 'b) a ((g::'a => 'c) a) = f b (g b)"

that is by explicitly annotating the term with the inferred types (even without stating sort constraints) -- I assume that is because the explicitly given type variables receive the default sort "type". I understand that the inferred type is more general, but it is actually useless. As a user, I find that behavior quite strange -- bug or feature?

Thanks,
Stephan






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.