brianh at cs.pdx.edu
Tue Sep 2 23:52:03 CEST 2008
Quoting Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>:
> * funpow is defined as a separate primrec in theory Nat, without special
> * 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 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.
More information about the isabelle-dev