1 (* Title: HOL/AxClasses/Group.thy |
|
2 ID: $Id$ |
|
3 Author: Markus Wenzel, TU Muenchen |
|
4 *) |
|
5 |
|
6 theory Group imports Main begin |
|
7 |
|
8 subsection {* Monoids and Groups *} |
|
9 |
|
10 consts |
|
11 times :: "'a => 'a => 'a" (infixl "[*]" 70) |
|
12 invers :: "'a => 'a" |
|
13 one :: 'a |
|
14 |
|
15 |
|
16 axclass monoid < type |
|
17 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
|
18 left_unit: "one [*] x = x" |
|
19 right_unit: "x [*] one = x" |
|
20 |
|
21 axclass semigroup < type |
|
22 assoc: "(x [*] y) [*] z = x [*] (y [*] z)" |
|
23 |
|
24 axclass group < semigroup |
|
25 left_unit: "one [*] x = x" |
|
26 left_inverse: "invers x [*] x = one" |
|
27 |
|
28 axclass agroup < group |
|
29 commute: "x [*] y = y [*] x" |
|
30 |
|
31 |
|
32 subsection {* Abstract reasoning *} |
|
33 |
|
34 theorem group_right_inverse: "x [*] invers x = (one::'a::group)" |
|
35 proof - |
|
36 have "x [*] invers x = one [*] (x [*] invers x)" |
|
37 by (simp only: group_class.left_unit) |
|
38 also have "... = one [*] x [*] invers x" |
|
39 by (simp only: semigroup_class.assoc) |
|
40 also have "... = invers (invers x) [*] invers x [*] x [*] invers x" |
|
41 by (simp only: group_class.left_inverse) |
|
42 also have "... = invers (invers x) [*] (invers x [*] x) [*] invers x" |
|
43 by (simp only: semigroup_class.assoc) |
|
44 also have "... = invers (invers x) [*] one [*] invers x" |
|
45 by (simp only: group_class.left_inverse) |
|
46 also have "... = invers (invers x) [*] (one [*] invers x)" |
|
47 by (simp only: semigroup_class.assoc) |
|
48 also have "... = invers (invers x) [*] invers x" |
|
49 by (simp only: group_class.left_unit) |
|
50 also have "... = one" |
|
51 by (simp only: group_class.left_inverse) |
|
52 finally show ?thesis . |
|
53 qed |
|
54 |
|
55 theorem group_right_unit: "x [*] one = (x::'a::group)" |
|
56 proof - |
|
57 have "x [*] one = x [*] (invers x [*] x)" |
|
58 by (simp only: group_class.left_inverse) |
|
59 also have "... = x [*] invers x [*] x" |
|
60 by (simp only: semigroup_class.assoc) |
|
61 also have "... = one [*] x" |
|
62 by (simp only: group_right_inverse) |
|
63 also have "... = x" |
|
64 by (simp only: group_class.left_unit) |
|
65 finally show ?thesis . |
|
66 qed |
|
67 |
|
68 |
|
69 subsection {* Abstract instantiation *} |
|
70 |
|
71 instance monoid < semigroup |
|
72 proof intro_classes |
|
73 fix x y z :: "'a::monoid" |
|
74 show "x [*] y [*] z = x [*] (y [*] z)" |
|
75 by (rule monoid_class.assoc) |
|
76 qed |
|
77 |
|
78 instance group < monoid |
|
79 proof intro_classes |
|
80 fix x y z :: "'a::group" |
|
81 show "x [*] y [*] z = x [*] (y [*] z)" |
|
82 by (rule semigroup_class.assoc) |
|
83 show "one [*] x = x" |
|
84 by (rule group_class.left_unit) |
|
85 show "x [*] one = x" |
|
86 by (rule group_right_unit) |
|
87 qed |
|
88 |
|
89 |
|
90 subsection {* Concrete instantiation *} |
|
91 |
|
92 defs (overloaded) |
|
93 times_bool_def: "x [*] y == x ~= (y::bool)" |
|
94 inverse_bool_def: "invers x == x::bool" |
|
95 unit_bool_def: "one == False" |
|
96 |
|
97 instance bool :: agroup |
|
98 proof (intro_classes, |
|
99 unfold times_bool_def inverse_bool_def unit_bool_def) |
|
100 fix x y z |
|
101 show "((x ~= y) ~= z) = (x ~= (y ~= z))" by blast |
|
102 show "(False ~= x) = x" by blast |
|
103 show "(x ~= x) = False" by blast |
|
104 show "(x ~= y) = (y ~= x)" by blast |
|
105 qed |
|
106 |
|
107 |
|
108 subsection {* Lifting and Functors *} |
|
109 |
|
110 defs (overloaded) |
|
111 times_prod_def: "p [*] q == (fst p [*] fst q, snd p [*] snd q)" |
|
112 |
|
113 instance * :: (semigroup, semigroup) semigroup |
|
114 proof (intro_classes, unfold times_prod_def) |
|
115 fix p q r :: "'a::semigroup * 'b::semigroup" |
|
116 show |
|
117 "(fst (fst p [*] fst q, snd p [*] snd q) [*] fst r, |
|
118 snd (fst p [*] fst q, snd p [*] snd q) [*] snd r) = |
|
119 (fst p [*] fst (fst q [*] fst r, snd q [*] snd r), |
|
120 snd p [*] snd (fst q [*] fst r, snd q [*] snd r))" |
|
121 by (simp add: semigroup_class.assoc) |
|
122 qed |
|
123 |
|
124 end |
|