equal
deleted
inserted
replaced
11 imports Nat |
11 imports Nat |
12 begin |
12 begin |
13 |
13 |
14 subsection{*Powers for Arbitrary Monoids*} |
14 subsection{*Powers for Arbitrary Monoids*} |
15 |
15 |
16 axclass recpower \<subseteq> monoid_mult, power |
16 class recpower = monoid_mult + power + |
17 power_0 [simp]: "a ^ 0 = 1" |
17 assumes power_0 [simp]: "a \<^loc>^ 0 = \<^loc>1" |
18 power_Suc: "a ^ (Suc n) = a * (a ^ n)" |
18 assumes power_Suc: "a \<^loc>^ Suc n = a \<^loc>* (a \<^loc>^ n)" |
19 |
19 |
20 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0" |
20 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0" |
21 by (simp add: power_Suc) |
21 by (simp add: power_Suc) |
22 |
22 |
23 text{*It looks plausible as a simprule, but its effect can be strange.*} |
23 text{*It looks plausible as a simprule, but its effect can be strange.*} |