Re: [isabelle] Overloading causes strange clash of specifications



Hi Ondrej,

Thanks for the hint. In the single-parameter case, I had added the type constraints, which made it go through, but I forgot to do the same for the two-parameter case.

Still, I wonder why they are necessary in the first place. In the end, I have already fixed the type of R' in the overloading part.

Best,
Andreas

On 01/06/15 14:40, OndÅej KunÄar wrote:
Hi Andreas,
the problem is that R in R_nat_def is defined with type "('c => 'd) => ('c => 'e) => bool".

The following works around the problem:

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

Ondrej

On 06/01/2015 01:58 PM, Andreas Lochbihler wrote:
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.