Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Various ways of overloading

Email Gateway (Aug 18 2022 at 18:15):

From: John Munroe <munddr@gmail.com>
Hi all,

I'm looking into overloading and it seems that consts/axioms already
allow overloading:

typedecl A

consts
g :: "'a => bool"
a :: A

axioms
axA: "g (x::A) = True"
axB: "g (x::B) = False"

lemma "g a"
using axA
by auto

whereas, axiomatization doesn't:

axiomatization
g :: "'a => bool"
where axA: "g (x::A) = True"

which gives a type unification error:

*** Type unification failed

*** Type error in application: incompatible operand type

*** Operator: g::'a => bool :: 'a => bool
*** Operand: x::A :: A

Why is there such a discrepancy? Is it one of the reasons why
consts/axioms are legacy features? The documentation seems to imply
that overloading can only be achieved using type classes, but one
could also do a similar thing in locales:

consts
g :: "'a => bool"

locale L =
assumes "g (x::A) = True" and
"g (y::B) = False"

Any advice on this will be much appreciated!

Thanks

John

Email Gateway (Aug 18 2022 at 18:15):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>

I'm looking into overloading and it seems that consts/axioms already
allow overloading:

typedecl A

consts
g :: "'a => bool"
a :: A

axioms
axA: "g (x::A) = True"
axB: "g (x::B) = False"

Well, no wonder: axioms allow you to specify everything.

Overloaded definitions are also part of the logical primitives, but type
classes provide a neat integrated interface, which internally maps again
on overloaded definitions.

axiomatization
g :: "'a => bool"
where axA: "g (x::A) = True"

By giving an explicit constant specification, you specify a new
constant to be declared, and its type signature (with type variables
locally fixed) must match its occurences in axiom propositions.

Without the constant specification, »axiomatization« will just state an
axiom.

The documentation seems to imply
that overloading can only be achieved using type classes

The tutorial describes typical mechanisms for the end user. The more
primitive interfaces are covered in the Isar Reference Manual.

but one
could also do a similar thing in locales:

consts
g :: "'a => bool"

locale L =
assumes "g (x::A) = True" and
"g (y::B) = False"

In locale assumptions, you can state everything since it is only
hypothetical. The question is whether you can give an interpretation
actually satisfying the assumptions.

Regards,
Florian
signature.asc

Last updated: Apr 26 2024 at 01:06 UTC