[isabelle] Various ways of overloading



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





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