[isabelle] Overloading causes strange clash of specifications



Dear all,

I am trying to overload a constant using the overloading target. However, I get an error that my specifications clash, even though I cannot see why. Here is the minimised example:

  consts R :: "'a â 'b â bool"

  overloading R' â "R :: (nat â 'a) â (nat â 'b) â bool"  begin
  definition R_nat_def: "R' f g = (âx. R (f x) (g x))"
  end

  overloading R' â "R :: ('a list â 'b) â ('c list â 'd) â bool" begin
  definition R_list_def: "R' f g = (âxs ys. R (f xs) (g ys))"
  end

The second definition raises the error, but the two definitions should be fine as the types of the overloaded constant cannot be unified and the recursive calls to R occur only at smaller types. Interestingly, if I throw out one parameter, everything works fine:

  consts P :: "'a â bool"

  overloading P' â "P :: (nat â 'a) â bool"  begin
  definition P_nat_def: "P' (f :: nat â 'a) = (âx. P (f x))"
  end

  overloading P' â "P :: ('b list â 'a) â bool" begin
  definition P_list_def: "P' (f :: 'b list â 'a) = (âx. P (f x))"
  end

So what is going on here? Why does the two parameter-case fail? And how can I avoid the failure?

Thanks in advance for any hints,
Andreas




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