[isabelle-dev] Relation_Power.thy

[Brian Huffman]

Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:

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

I agree with this plan (except that "^" needs to be defined in class  
monoid_mult, not comm_monoid_mult - I want exponentiation on matrices  
and other non-commutative monoids too!)

It is certainly annoying to have recpower as a separate class, since  
many theorems (especially in HOL-Complex) currently require extra sort  
annotations. Another annoyance (which will be fixed by this change) is  
the inconsistent setup of power_Suc with simplification: Currently,  
the polymorphic power_Suc is not a simp rule, but most type-specific  
versions of it are. This causes some difficulty when generalizing a  
proof, say from the reals to a more general class.

- Brian