equal
deleted
inserted
replaced
145 sublocale add!: abel_semigroup plus |
145 sublocale add!: abel_semigroup plus |
146 by standard (fact add_commute) |
146 by standard (fact add_commute) |
147 |
147 |
148 declare add.left_commute [algebra_simps, field_simps] |
148 declare add.left_commute [algebra_simps, field_simps] |
149 |
149 |
150 theorems add_ac = add.assoc add.commute add.left_commute |
150 lemmas add_ac = add.assoc add.commute add.left_commute |
151 |
151 |
152 end |
152 end |
153 |
153 |
154 hide_fact add_commute |
154 hide_fact add_commute |
155 |
155 |
156 theorems add_ac = add.assoc add.commute add.left_commute |
156 lemmas add_ac = add.assoc add.commute add.left_commute |
157 |
157 |
158 class semigroup_mult = times + |
158 class semigroup_mult = times + |
159 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
159 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
160 begin |
160 begin |
161 |
161 |
173 sublocale mult!: abel_semigroup times |
173 sublocale mult!: abel_semigroup times |
174 by standard (fact mult_commute) |
174 by standard (fact mult_commute) |
175 |
175 |
176 declare mult.left_commute [algebra_simps, field_simps] |
176 declare mult.left_commute [algebra_simps, field_simps] |
177 |
177 |
178 theorems mult_ac = mult.assoc mult.commute mult.left_commute |
178 lemmas mult_ac = mult.assoc mult.commute mult.left_commute |
179 |
179 |
180 end |
180 end |
181 |
181 |
182 hide_fact mult_commute |
182 hide_fact mult_commute |
183 |
183 |
184 theorems mult_ac = mult.assoc mult.commute mult.left_commute |
184 lemmas mult_ac = mult.assoc mult.commute mult.left_commute |
185 |
185 |
186 class monoid_add = zero + semigroup_add + |
186 class monoid_add = zero + semigroup_add + |
187 assumes add_0_left: "0 + a = a" |
187 assumes add_0_left: "0 + a = a" |
188 and add_0_right: "a + 0 = a" |
188 and add_0_right: "a + 0 = a" |
189 begin |
189 begin |