Re: [isabelle] Various ways of overloading

> 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

> 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.




PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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