88 assumes right_neutral [simp]: "a * 1 = a" |
88 assumes right_neutral [simp]: "a * 1 = a" |
89 |
89 |
90 locale comm_monoid = abel_semigroup + |
90 locale comm_monoid = abel_semigroup + |
91 fixes z :: 'a ("1") |
91 fixes z :: 'a ("1") |
92 assumes comm_neutral: "a * 1 = a" |
92 assumes comm_neutral: "a * 1 = a" |
93 |
93 begin |
94 sublocale comm_monoid < monoid |
94 |
|
95 sublocale monoid |
95 by default (simp_all add: commute comm_neutral) |
96 by default (simp_all add: commute comm_neutral) |
|
97 |
|
98 end |
96 |
99 |
97 |
100 |
98 subsection {* Generic operations *} |
101 subsection {* Generic operations *} |
99 |
102 |
100 class zero = |
103 class zero = |
146 |
149 |
147 subsection {* Semigroups and Monoids *} |
150 subsection {* Semigroups and Monoids *} |
148 |
151 |
149 class semigroup_add = plus + |
152 class semigroup_add = plus + |
150 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" |
153 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" |
151 |
154 begin |
152 sublocale semigroup_add < add!: semigroup plus |
155 |
|
156 sublocale add!: semigroup plus |
153 by default (fact add_assoc) |
157 by default (fact add_assoc) |
|
158 |
|
159 end |
154 |
160 |
155 class ab_semigroup_add = semigroup_add + |
161 class ab_semigroup_add = semigroup_add + |
156 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" |
162 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" |
157 |
163 begin |
158 sublocale ab_semigroup_add < add!: abel_semigroup plus |
164 |
|
165 sublocale add!: abel_semigroup plus |
159 by default (fact add_commute) |
166 by default (fact add_commute) |
160 |
|
161 context ab_semigroup_add |
|
162 begin |
|
163 |
167 |
164 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute |
168 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute |
165 |
169 |
166 theorems add_ac = add_assoc add_commute add_left_commute |
170 theorems add_ac = add_assoc add_commute add_left_commute |
167 |
171 |
169 |
173 |
170 theorems add_ac = add_assoc add_commute add_left_commute |
174 theorems add_ac = add_assoc add_commute add_left_commute |
171 |
175 |
172 class semigroup_mult = times + |
176 class semigroup_mult = times + |
173 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
177 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
174 |
178 begin |
175 sublocale semigroup_mult < mult!: semigroup times |
179 |
|
180 sublocale mult!: semigroup times |
176 by default (fact mult_assoc) |
181 by default (fact mult_assoc) |
|
182 |
|
183 end |
177 |
184 |
178 class ab_semigroup_mult = semigroup_mult + |
185 class ab_semigroup_mult = semigroup_mult + |
179 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" |
186 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" |
180 |
187 begin |
181 sublocale ab_semigroup_mult < mult!: abel_semigroup times |
188 |
|
189 sublocale mult!: abel_semigroup times |
182 by default (fact mult_commute) |
190 by default (fact mult_commute) |
183 |
|
184 context ab_semigroup_mult |
|
185 begin |
|
186 |
191 |
187 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute |
192 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute |
188 |
193 |
189 theorems mult_ac = mult_assoc mult_commute mult_left_commute |
194 theorems mult_ac = mult_assoc mult_commute mult_left_commute |
190 |
195 |
193 theorems mult_ac = mult_assoc mult_commute mult_left_commute |
198 theorems mult_ac = mult_assoc mult_commute mult_left_commute |
194 |
199 |
195 class monoid_add = zero + semigroup_add + |
200 class monoid_add = zero + semigroup_add + |
196 assumes add_0_left: "0 + a = a" |
201 assumes add_0_left: "0 + a = a" |
197 and add_0_right: "a + 0 = a" |
202 and add_0_right: "a + 0 = a" |
198 |
203 begin |
199 sublocale monoid_add < add!: monoid plus 0 |
204 |
|
205 sublocale add!: monoid plus 0 |
200 by default (fact add_0_left add_0_right)+ |
206 by default (fact add_0_left add_0_right)+ |
201 |
207 |
|
208 end |
|
209 |
202 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" |
210 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" |
203 by (rule eq_commute) |
211 by (fact eq_commute) |
204 |
212 |
205 class comm_monoid_add = zero + ab_semigroup_add + |
213 class comm_monoid_add = zero + ab_semigroup_add + |
206 assumes add_0: "0 + a = a" |
214 assumes add_0: "0 + a = a" |
207 |
215 begin |
208 sublocale comm_monoid_add < add!: comm_monoid plus 0 |
216 |
|
217 sublocale add!: comm_monoid plus 0 |
209 by default (insert add_0, simp add: ac_simps) |
218 by default (insert add_0, simp add: ac_simps) |
210 |
219 |
211 subclass (in comm_monoid_add) monoid_add |
220 subclass monoid_add |
212 by default (fact add.left_neutral add.right_neutral)+ |
221 by default (fact add.left_neutral add.right_neutral)+ |
|
222 |
|
223 end |
213 |
224 |
214 class comm_monoid_diff = comm_monoid_add + minus + |
225 class comm_monoid_diff = comm_monoid_add + minus + |
215 assumes diff_zero [simp]: "a - 0 = a" |
226 assumes diff_zero [simp]: "a - 0 = a" |
216 and zero_diff [simp]: "0 - a = 0" |
227 and zero_diff [simp]: "0 - a = 0" |
217 and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b" |
228 and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b" |
263 end |
274 end |
264 |
275 |
265 class monoid_mult = one + semigroup_mult + |
276 class monoid_mult = one + semigroup_mult + |
266 assumes mult_1_left: "1 * a = a" |
277 assumes mult_1_left: "1 * a = a" |
267 and mult_1_right: "a * 1 = a" |
278 and mult_1_right: "a * 1 = a" |
268 |
279 begin |
269 sublocale monoid_mult < mult!: monoid times 1 |
280 |
|
281 sublocale mult!: monoid times 1 |
270 by default (fact mult_1_left mult_1_right)+ |
282 by default (fact mult_1_left mult_1_right)+ |
271 |
283 |
|
284 end |
|
285 |
272 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" |
286 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" |
273 by (rule eq_commute) |
287 by (fact eq_commute) |
274 |
288 |
275 class comm_monoid_mult = one + ab_semigroup_mult + |
289 class comm_monoid_mult = one + ab_semigroup_mult + |
276 assumes mult_1: "1 * a = a" |
290 assumes mult_1: "1 * a = a" |
277 |
291 begin |
278 sublocale comm_monoid_mult < mult!: comm_monoid times 1 |
292 |
|
293 sublocale mult!: comm_monoid times 1 |
279 by default (insert mult_1, simp add: ac_simps) |
294 by default (insert mult_1, simp add: ac_simps) |
280 |
295 |
281 subclass (in comm_monoid_mult) monoid_mult |
296 subclass monoid_mult |
282 by default (fact mult.left_neutral mult.right_neutral)+ |
297 by default (fact mult.left_neutral mult.right_neutral)+ |
|
298 |
|
299 end |
283 |
300 |
284 class cancel_semigroup_add = semigroup_add + |
301 class cancel_semigroup_add = semigroup_add + |
285 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
302 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
286 assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" |
303 assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" |
287 begin |
304 begin |