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