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 |
94 sublocale comm_monoid < monoid proof |
94 sublocale comm_monoid < monoid |
95 qed (simp_all add: commute comm_neutral) |
95 by default (simp_all add: commute comm_neutral) |
96 |
96 |
97 |
97 |
98 subsection {* Generic operations *} |
98 subsection {* Generic operations *} |
99 |
99 |
100 class zero = |
100 class zero = |
149 subsection {* Semigroups and Monoids *} |
149 subsection {* Semigroups and Monoids *} |
150 |
150 |
151 class semigroup_add = plus + |
151 class semigroup_add = plus + |
152 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" |
152 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" |
153 |
153 |
154 sublocale semigroup_add < add!: semigroup plus proof |
154 sublocale semigroup_add < add!: semigroup plus |
155 qed (fact add_assoc) |
155 by default (fact add_assoc) |
156 |
156 |
157 class ab_semigroup_add = semigroup_add + |
157 class ab_semigroup_add = semigroup_add + |
158 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" |
158 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" |
159 |
159 |
160 sublocale ab_semigroup_add < add!: abel_semigroup plus proof |
160 sublocale ab_semigroup_add < add!: abel_semigroup plus |
161 qed (fact add_commute) |
161 by default (fact add_commute) |
162 |
162 |
163 context ab_semigroup_add |
163 context ab_semigroup_add |
164 begin |
164 begin |
165 |
165 |
166 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute |
166 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute |
172 theorems add_ac = add_assoc add_commute add_left_commute |
172 theorems add_ac = add_assoc add_commute add_left_commute |
173 |
173 |
174 class semigroup_mult = times + |
174 class semigroup_mult = times + |
175 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
175 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
176 |
176 |
177 sublocale semigroup_mult < mult!: semigroup times proof |
177 sublocale semigroup_mult < mult!: semigroup times |
178 qed (fact mult_assoc) |
178 by default (fact mult_assoc) |
179 |
179 |
180 class ab_semigroup_mult = semigroup_mult + |
180 class ab_semigroup_mult = semigroup_mult + |
181 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" |
181 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" |
182 |
182 |
183 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof |
183 sublocale ab_semigroup_mult < mult!: abel_semigroup times |
184 qed (fact mult_commute) |
184 by default (fact mult_commute) |
185 |
185 |
186 context ab_semigroup_mult |
186 context ab_semigroup_mult |
187 begin |
187 begin |
188 |
188 |
189 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute |
189 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute |
196 |
196 |
197 class monoid_add = zero + semigroup_add + |
197 class monoid_add = zero + semigroup_add + |
198 assumes add_0_left: "0 + a = a" |
198 assumes add_0_left: "0 + a = a" |
199 and add_0_right: "a + 0 = a" |
199 and add_0_right: "a + 0 = a" |
200 |
200 |
201 sublocale monoid_add < add!: monoid plus 0 proof |
201 sublocale monoid_add < add!: monoid plus 0 |
202 qed (fact add_0_left add_0_right)+ |
202 by default (fact add_0_left add_0_right)+ |
203 |
203 |
204 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" |
204 lemma zero_reorient: "0 = x \<longleftrightarrow> x = 0" |
205 by (rule eq_commute) |
205 by (rule eq_commute) |
206 |
206 |
207 class comm_monoid_add = zero + ab_semigroup_add + |
207 class comm_monoid_add = zero + ab_semigroup_add + |
208 assumes add_0: "0 + a = a" |
208 assumes add_0: "0 + a = a" |
209 |
209 |
210 sublocale comm_monoid_add < add!: comm_monoid plus 0 proof |
210 sublocale comm_monoid_add < add!: comm_monoid plus 0 |
211 qed (insert add_0, simp add: ac_simps) |
211 by default (insert add_0, simp add: ac_simps) |
212 |
212 |
213 subclass (in comm_monoid_add) monoid_add proof |
213 subclass (in comm_monoid_add) monoid_add |
214 qed (fact add.left_neutral add.right_neutral)+ |
214 by default (fact add.left_neutral add.right_neutral)+ |
215 |
215 |
216 class comm_monoid_diff = comm_monoid_add + minus + |
216 class comm_monoid_diff = comm_monoid_add + minus + |
217 assumes diff_zero [simp]: "a - 0 = a" |
217 assumes diff_zero [simp]: "a - 0 = a" |
218 and zero_diff [simp]: "0 - a = 0" |
218 and zero_diff [simp]: "0 - a = 0" |
219 and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b" |
219 and add_diff_cancel_left [simp]: "(c + a) - (c + b) = a - b" |
266 |
266 |
267 class monoid_mult = one + semigroup_mult + |
267 class monoid_mult = one + semigroup_mult + |
268 assumes mult_1_left: "1 * a = a" |
268 assumes mult_1_left: "1 * a = a" |
269 and mult_1_right: "a * 1 = a" |
269 and mult_1_right: "a * 1 = a" |
270 |
270 |
271 sublocale monoid_mult < mult!: monoid times 1 proof |
271 sublocale monoid_mult < mult!: monoid times 1 |
272 qed (fact mult_1_left mult_1_right)+ |
272 by default (fact mult_1_left mult_1_right)+ |
273 |
273 |
274 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" |
274 lemma one_reorient: "1 = x \<longleftrightarrow> x = 1" |
275 by (rule eq_commute) |
275 by (rule eq_commute) |
276 |
276 |
277 class comm_monoid_mult = one + ab_semigroup_mult + |
277 class comm_monoid_mult = one + ab_semigroup_mult + |
278 assumes mult_1: "1 * a = a" |
278 assumes mult_1: "1 * a = a" |
279 |
279 |
280 sublocale comm_monoid_mult < mult!: comm_monoid times 1 proof |
280 sublocale comm_monoid_mult < mult!: comm_monoid times 1 |
281 qed (insert mult_1, simp add: ac_simps) |
281 by default (insert mult_1, simp add: ac_simps) |
282 |
282 |
283 subclass (in comm_monoid_mult) monoid_mult proof |
283 subclass (in comm_monoid_mult) monoid_mult |
284 qed (fact mult.left_neutral mult.right_neutral)+ |
284 by default (fact mult.left_neutral mult.right_neutral)+ |
285 |
285 |
286 class cancel_semigroup_add = semigroup_add + |
286 class cancel_semigroup_add = semigroup_add + |
287 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
287 assumes add_left_imp_eq: "a + b = a + c \<Longrightarrow> b = c" |
288 assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" |
288 assumes add_right_imp_eq: "b + a = c + a \<Longrightarrow> b = c" |
289 begin |
289 begin |