[isabelle] Overloading causes strange clash of specifications
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))"
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))"
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))"
overloading P' â "P :: ('b list â 'a) â bool" begin
definition P_list_def: "P' (f :: 'b list â 'a) = (âx. P (f x))"
So what is going on here? Why does the two parameter-case fail? And how can I avoid the
Thanks in advance for any hints,
This archive was generated by a fusion of
Pipermail (Mailman edition) and