[isabelle-dev] Relation_Power.thy

[Gerwin Klein]

Florian Haftmann wrote:
> The overloaded infix syntax "^" for different power operations (natural
> power in monoids, function power, relation power) turns more and more
> unsatisfactory for a couple of reasons, e.g.:
> 
> * The abuse of the type class mechanism to achieve the "^" syntax for
> funpow and relpow hinders the enforcement of the strict class parameter
> instantiation policy and produces legacy feature warnings.
> * The nature of "^" as a class operations implies the existence of class
> recpower which leads to strange duplications in the class hierarchy in
> the HOL-Complex theories.
> * Anyway, the "^" does only cover particular cases, not e.g. "real ^
> rat" etc.

Which solution in Isabelle would cover real ^ rat without being completely 
generic?


> A short investigation yields that actually funpow and relpow are rarely
> used, relpow even not in the HOL-Complex theories but rather in
> particular application examples (typically things  like Jinja etc.).

I can see that there is a technical problem, but just because something is not 
used extensively in the repository does not mean its not extensively used out 
there. I would hope that the "dark matter" user theory base by now is much 
larger than what we can see in the AFP and repository. relpow and funpow are 
very fundamental concepts. We shouldn't change them just for convenience, but 
only for very good reasons.

I would suspect that anyone formalising more fundamental things about 
functions, relations and iteration (relational algebra stuff, semantics, that 
kind of thing) would be very annoyed with the solution below.


> There have been some thoughts to provide a mechanism of overloaded
> abbreviations or something similar to eliminate that problem, but
> meanwhile, considering the rare usages of funpow and relpow, I would
> suggest the conservative solution:
> 
> * funpow is defined as a separate primrec in theory Nat, without special
> syntax.
> * The remainder of theory Relation_Power is moved to Library, with a new
> infix syntax (e.g. "^^") for relpow.
> * The simple pow "^" then is just a primrec in class comm_monoid_mult.
> * classes power and recpower disappear, also the corresponding duplications.

I haven't understood the reason for the duplication in HOL-Complex yet, so I 
can't comment if I find it outweighs the inconvenience of random renaming and 
shifting, but I'd at least investigate if there are other solutions.

Maybe I'm just cranky this morning, but I don't find the 
different-syntax-printed-the-same solution for abbreviations nice either. In 
my experience, users have difficulties with seeing why the same thing has 
different names (even if it is not really the same, but being printed the same 
makes it the same for most).

Strangely enough, real overloading would be more acceptable, I think.

Cheers,
Gerwin