I have found the following definition in HOL/Power.thy
:
primrec power :: "'a ⇒ nat ⇒ 'a" (infixr "^" 80) where
power_0: "a ^ 0 = 1"
| power_Suc: "a ^ Suc n = a * a ^ n"
(Control + Click gets you to the respecitve definition! So I clicked on "^", I just wrote "1 ^ 1 = 1" as a lemma first.
Here is the definition for the power of a matrice.
(As I only use square matrices this is fine, but a more general type of ^'n^'m
would be nice.)
primrec powerM :: "(('a::semiring_1) ^'n^'n) ⇒ nat ⇒ (('a::semiring_1) ^'n^'n)"
(infixr "^^^" 80) where
powerM_0: "A ^^^(0::nat) = mat 1"
| powerM_Suc: "A ^^^(Suc n) = A ** (powerM A n)"