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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and