equal
deleted
inserted
replaced
25 subsection \<open>Powers for Arbitrary Monoids\<close> |
25 subsection \<open>Powers for Arbitrary Monoids\<close> |
26 |
26 |
27 class power = one + times |
27 class power = one + times |
28 begin |
28 begin |
29 |
29 |
30 primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where |
30 primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) |
31 power_0: "a ^ 0 = 1" |
31 where |
32 | power_Suc: "a ^ Suc n = a * a ^ n" |
32 power_0: "a ^ 0 = 1" |
|
33 | power_Suc: "a ^ Suc n = a * a ^ n" |
33 |
34 |
34 notation (latex output) |
35 notation (latex output) |
35 power ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
36 power ("(_\<^bsup>_\<^esup>)" [1000] 1000) |
36 |
37 |
37 text \<open>Special syntax for squares.\<close> |
38 text \<open>Special syntax for squares.\<close> |
38 |
39 abbreviation power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999) |
39 abbreviation (xsymbols) |
40 where "x\<^sup>2 \<equiv> x ^ 2" |
40 power2 :: "'a \<Rightarrow> 'a" ("(_\<^sup>2)" [1000] 999) where |
|
41 "x\<^sup>2 \<equiv> x ^ 2" |
|
42 |
|
43 notation (latex output) |
|
44 power2 ("(_\<^sup>2)" [1000] 999) |
|
45 |
41 |
46 end |
42 end |
47 |
43 |
48 context monoid_mult |
44 context monoid_mult |
49 begin |
45 begin |