11 class semigroup = |
11 class semigroup = |
12 fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70) |
12 fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70) |
13 assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)" |
13 assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)" |
14 |
14 |
15 instance nat :: semigroup |
15 instance nat :: semigroup |
16 "m \<otimes> n == (m::nat) + n" |
16 "m \<otimes> n == m + n" |
17 proof |
17 proof |
18 fix m n q :: nat |
18 fix m n q :: nat |
19 from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp |
19 from semigroup_nat_def show "m \<otimes> n \<otimes> q = m \<otimes> (n \<otimes> q)" by simp |
20 qed |
20 qed |
21 |
21 |
22 instance int :: semigroup |
22 instance int :: semigroup |
23 "k \<otimes> l == (k::int) + l" |
23 "k \<otimes> l == k + l" |
24 proof |
24 proof |
25 fix k l j :: int |
25 fix k l j :: int |
26 from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp |
26 from semigroup_int_def show "k \<otimes> l \<otimes> j = k \<otimes> (l \<otimes> j)" by simp |
27 qed |
27 qed |
28 |
28 |
40 class monoidl = semigroup + |
40 class monoidl = semigroup + |
41 fixes one :: 'a ("\<^loc>\<one>") |
41 fixes one :: 'a ("\<^loc>\<one>") |
42 assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x" |
42 assumes neutl: "\<^loc>\<one> \<^loc>\<otimes> x = x" |
43 |
43 |
44 instance nat :: monoidl |
44 instance nat :: monoidl |
45 "\<one> == (0::nat)" |
45 "\<one> == 0" |
46 proof |
46 proof |
47 fix n :: nat |
47 fix n :: nat |
48 from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp |
48 from semigroup_nat_def monoidl_nat_def show "\<one> \<otimes> n = n" by simp |
49 qed |
49 qed |
50 |
50 |
51 instance int :: monoidl |
51 instance int :: monoidl |
52 "\<one> == (0::int)" |
52 "\<one> == 0" |
53 proof |
53 proof |
54 fix k :: int |
54 fix k :: int |
55 from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp |
55 from semigroup_int_def monoidl_int_def show "\<one> \<otimes> k = k" by simp |
56 qed |
56 qed |
57 |
57 |
299 lemma (in group) int_pow_one: |
301 lemma (in group) int_pow_one: |
300 "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>" |
302 "\<^loc>\<one> \<^loc>\<up> (k::int) = \<^loc>\<one>" |
301 using pow_def nat_pow_one inv_one by simp |
303 using pow_def nat_pow_one inv_one by simp |
302 |
304 |
303 instance group_prod_def: (group, group) * :: group |
305 instance group_prod_def: (group, group) * :: group |
304 mult_prod_def: "x \<otimes> y == let (x1, x2) = x in (let (y1, y2) = y in |
306 mult_prod_def: "x \<otimes> y == let (x1, x2) = x; (y1, y2) = y in |
305 ((x1::'a::group) \<otimes> y1, (x2::'b::group) \<otimes> y2))" |
307 (x1 \<otimes> y1, x2 \<otimes> y2)" |
306 mult_one_def: "\<one> == (\<one>::'a::group, \<one>::'b::group)" |
308 mult_one_def: "\<one> == (\<one>, \<one>)" |
307 mult_inv_def: "\<div> x == let (x1::'a::group, x2::'b::group) = x in (\<div> x1, \<div> x2)" |
309 mult_inv_def: "\<div> x == let (x1, x2) = x in (\<div> x1, \<div> x2)" |
308 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl) |
310 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl) |
309 |
311 |
310 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm |
312 instance group_comm_prod_def: (group_comm, group_comm) * :: group_comm |
311 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm) |
313 by default (simp_all add: split_paired_all group_prod_def assoc neutl invl comm) |
312 |
314 |