[isabelle-dev] Relation_Power.thy

[Florian Haftmann]

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.

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

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.

Opinions?

	Florian
-------------- next part --------------
A non-text attachment was scrubbed...
Name: florian.haftmann.vcf
Type: text/x-vcard
Size: 654 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080902/d526bc4b/attachment.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 185 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20080902/d526bc4b/attachment.pgp>