Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Overloading causes strange clash of specificat...

Email Gateway (Aug 22 2022 at 10:15):

From: Ondřej Kunčar <kuncar@in.tum.de>
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

Email Gateway (Aug 22 2022 at 10:16):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Email Gateway (Aug 22 2022 at 10:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 26 2024 at 20:16 UTC