Re: [isabelle] [isabelle-dev] Relations vs. Predicates



actually I was talking about the development version (hence the dev
list) but the situation is essentially the same in Isabelle2011-1 I
guess. By "adhoc overloading" I was referring to the theory
Adhoc_Overloading (e.g., used for do-notation) which could (I think) be
used to unify the syntax (independently from what you said about generic
lemmas) of funpow, relpow, compow, and what is more.

this won't work: Adhoc_Overloading can only disambiguate disjoint type
signatures (neglecting sort constraints).

I think this isn't quite accurate.

IIRC, Adhoc_Overloading does respect sort constraints as expected, since it runs in tandem with the normal type inference.

So the approach suggested by Chris could in fact work, with the effect that

- "op ^ :: 'nat => ('a * 'a) set => ('a * 'a) set" would become "relpow"

- "op ^ :: 'nat => 'a::power => 'a::power" would become "power"

- "op ^ :: nat => 'a => 'a => 'a => 'a" would become "funpow"

- "op ^ :: nat => 'a => 'a" without further constraints would be ambiguous and generate an error during the term check phase.

- compow would disappear and the (few) facts about it would be duplicated for the two instances funpow and relpow.

This effectively moves the existing ad-hoc oveloading from the logic back into the syntax layer, where it can now be handled rather smoothly. The good thing would be that there is just one power operation (if we forget about the reals for the moment :-) )

When introducing Adhoc_Overloading, I was aware of this possibility, but I hesitated, because

- Throwing more code into HOL-Main needs great care, especially when syntax is involved.

- The whole check/uncheck business is highly non-compositional. When making Adhoc_Overloading part of HOL-Main, we would have to make sure that it coexists nicely with other extensions, such as the class-related type refinement, or coercive subtyping. I am sure there are a number of unforeseen effects hidden here.

- ...and actually, the current situation is not too bad.

Alex





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