18 ) |
18 ) |
19 *} |
19 *} |
20 |
20 |
21 setup Ac_Simps.setup |
21 setup Ac_Simps.setup |
22 |
22 |
|
23 text{* The rewrites accumulated in @{text algebra_simps} deal with the |
|
24 classical algebraic structures of groups, rings and family. They simplify |
|
25 terms by multiplying everything out (in case of a ring) and bringing sums and |
|
26 products into a canonical form (by ordered rewriting). As a result it decides |
|
27 group and ring equalities but also helps with inequalities. |
|
28 |
|
29 Of course it also works for fields, but it knows nothing about multiplicative |
|
30 inverses or division. This is catered for by @{text field_simps}. *} |
|
31 |
23 ML {* |
32 ML {* |
24 structure Algebra_Simps = Named_Thms( |
33 structure Algebra_Simps = Named_Thms( |
25 val name = "algebra_simps" |
34 val name = "algebra_simps" |
26 val description = "algebra simplification rules" |
35 val description = "algebra simplification rules" |
27 ) |
36 ) |
28 *} |
37 *} |
29 |
38 |
30 setup Algebra_Simps.setup |
39 setup Algebra_Simps.setup |
31 |
40 |
32 text{* The rewrites accumulated in @{text algebra_simps} deal with the |
41 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations |
33 classical algebraic structures of groups, rings and family. They simplify |
42 if they can be proved to be non-zero (for equations) or positive/negative |
34 terms by multiplying everything out (in case of a ring) and bringing sums and |
43 (for inequations). Can be too aggressive and is therefore separate from the |
35 products into a canonical form (by ordered rewriting). As a result it decides |
44 more benign @{text algebra_simps}. *} |
36 group and ring equalities but also helps with inequalities. |
45 |
37 |
46 ML {* |
38 Of course it also works for fields, but it knows nothing about multiplicative |
47 structure Field_Simps = Named_Thms( |
39 inverses or division. This is catered for by @{text field_simps}. *} |
48 val name = "field_simps" |
|
49 val description = "algebra simplification rules for fields" |
|
50 ) |
|
51 *} |
|
52 |
|
53 setup Field_Simps.setup |
40 |
54 |
41 |
55 |
42 subsection {* Abstract structures *} |
56 subsection {* Abstract structures *} |
43 |
57 |
44 text {* |
58 text {* |
136 |
150 |
137 |
151 |
138 subsection {* Semigroups and Monoids *} |
152 subsection {* Semigroups and Monoids *} |
139 |
153 |
140 class semigroup_add = plus + |
154 class semigroup_add = plus + |
141 assumes add_assoc [algebra_simps]: "(a + b) + c = a + (b + c)" |
155 assumes add_assoc [algebra_simps, field_simps]: "(a + b) + c = a + (b + c)" |
142 |
156 |
143 sublocale semigroup_add < add!: semigroup plus proof |
157 sublocale semigroup_add < add!: semigroup plus proof |
144 qed (fact add_assoc) |
158 qed (fact add_assoc) |
145 |
159 |
146 class ab_semigroup_add = semigroup_add + |
160 class ab_semigroup_add = semigroup_add + |
147 assumes add_commute [algebra_simps]: "a + b = b + a" |
161 assumes add_commute [algebra_simps, field_simps]: "a + b = b + a" |
148 |
162 |
149 sublocale ab_semigroup_add < add!: abel_semigroup plus proof |
163 sublocale ab_semigroup_add < add!: abel_semigroup plus proof |
150 qed (fact add_commute) |
164 qed (fact add_commute) |
151 |
165 |
152 context ab_semigroup_add |
166 context ab_semigroup_add |
153 begin |
167 begin |
154 |
168 |
155 lemmas add_left_commute [algebra_simps] = add.left_commute |
169 lemmas add_left_commute [algebra_simps, field_simps] = add.left_commute |
156 |
170 |
157 theorems add_ac = add_assoc add_commute add_left_commute |
171 theorems add_ac = add_assoc add_commute add_left_commute |
158 |
172 |
159 end |
173 end |
160 |
174 |
161 theorems add_ac = add_assoc add_commute add_left_commute |
175 theorems add_ac = add_assoc add_commute add_left_commute |
162 |
176 |
163 class semigroup_mult = times + |
177 class semigroup_mult = times + |
164 assumes mult_assoc [algebra_simps]: "(a * b) * c = a * (b * c)" |
178 assumes mult_assoc [algebra_simps, field_simps]: "(a * b) * c = a * (b * c)" |
165 |
179 |
166 sublocale semigroup_mult < mult!: semigroup times proof |
180 sublocale semigroup_mult < mult!: semigroup times proof |
167 qed (fact mult_assoc) |
181 qed (fact mult_assoc) |
168 |
182 |
169 class ab_semigroup_mult = semigroup_mult + |
183 class ab_semigroup_mult = semigroup_mult + |
170 assumes mult_commute [algebra_simps]: "a * b = b * a" |
184 assumes mult_commute [algebra_simps, field_simps]: "a * b = b * a" |
171 |
185 |
172 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof |
186 sublocale ab_semigroup_mult < mult!: abel_semigroup times proof |
173 qed (fact mult_commute) |
187 qed (fact mult_commute) |
174 |
188 |
175 context ab_semigroup_mult |
189 context ab_semigroup_mult |
176 begin |
190 begin |
177 |
191 |
178 lemmas mult_left_commute [algebra_simps] = mult.left_commute |
192 lemmas mult_left_commute [algebra_simps, field_simps] = mult.left_commute |
179 |
193 |
180 theorems mult_ac = mult_assoc mult_commute mult_left_commute |
194 theorems mult_ac = mult_assoc mult_commute mult_left_commute |
181 |
195 |
182 end |
196 end |
183 |
197 |
368 by (simp add: diff_minus add_assoc) |
382 by (simp add: diff_minus add_assoc) |
369 |
383 |
370 lemma add_diff_cancel: "a + b - b = a" |
384 lemma add_diff_cancel: "a + b - b = a" |
371 by (simp add: diff_minus add_assoc) |
385 by (simp add: diff_minus add_assoc) |
372 |
386 |
373 declare diff_minus[symmetric, algebra_simps] |
387 declare diff_minus[symmetric, algebra_simps, field_simps] |
374 |
388 |
375 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0" |
389 lemma eq_neg_iff_add_eq_0: "a = - b \<longleftrightarrow> a + b = 0" |
376 proof |
390 proof |
377 assume "a = - b" then show "a + b = 0" by simp |
391 assume "a = - b" then show "a + b = 0" by simp |
378 next |
392 next |
399 then have "- a + a + b = - a + a + c" |
413 then have "- a + a + b = - a + a + c" |
400 unfolding add_assoc by simp |
414 unfolding add_assoc by simp |
401 then show "b = c" by simp |
415 then show "b = c" by simp |
402 qed |
416 qed |
403 |
417 |
404 lemma uminus_add_conv_diff[algebra_simps]: |
418 lemma uminus_add_conv_diff[algebra_simps, field_simps]: |
405 "- a + b = b - a" |
419 "- a + b = b - a" |
406 by (simp add:diff_minus add_commute) |
420 by (simp add:diff_minus add_commute) |
407 |
421 |
408 lemma minus_add_distrib [simp]: |
422 lemma minus_add_distrib [simp]: |
409 "- (a + b) = - a + - b" |
423 "- (a + b) = - a + - b" |
411 |
425 |
412 lemma minus_diff_eq [simp]: |
426 lemma minus_diff_eq [simp]: |
413 "- (a - b) = b - a" |
427 "- (a - b) = b - a" |
414 by (simp add: diff_minus add_commute) |
428 by (simp add: diff_minus add_commute) |
415 |
429 |
416 lemma add_diff_eq[algebra_simps]: "a + (b - c) = (a + b) - c" |
430 lemma add_diff_eq[algebra_simps, field_simps]: "a + (b - c) = (a + b) - c" |
417 by (simp add: diff_minus add_ac) |
431 by (simp add: diff_minus add_ac) |
418 |
432 |
419 lemma diff_add_eq[algebra_simps]: "(a - b) + c = (a + c) - b" |
433 lemma diff_add_eq[algebra_simps, field_simps]: "(a - b) + c = (a + c) - b" |
420 by (simp add: diff_minus add_ac) |
434 by (simp add: diff_minus add_ac) |
421 |
435 |
422 lemma diff_eq_eq[algebra_simps]: "a - b = c \<longleftrightarrow> a = c + b" |
436 lemma diff_eq_eq[algebra_simps, field_simps]: "a - b = c \<longleftrightarrow> a = c + b" |
423 by (auto simp add: diff_minus add_assoc) |
437 by (auto simp add: diff_minus add_assoc) |
424 |
438 |
425 lemma eq_diff_eq[algebra_simps]: "a = c - b \<longleftrightarrow> a + b = c" |
439 lemma eq_diff_eq[algebra_simps, field_simps]: "a = c - b \<longleftrightarrow> a + b = c" |
426 by (auto simp add: diff_minus add_assoc) |
440 by (auto simp add: diff_minus add_assoc) |
427 |
441 |
428 lemma diff_diff_eq[algebra_simps]: "(a - b) - c = a - (b + c)" |
442 lemma diff_diff_eq[algebra_simps, field_simps]: "(a - b) - c = a - (b + c)" |
429 by (simp add: diff_minus add_ac) |
443 by (simp add: diff_minus add_ac) |
430 |
444 |
431 lemma diff_diff_eq2[algebra_simps]: "a - (b - c) = (a + c) - b" |
445 lemma diff_diff_eq2[algebra_simps, field_simps]: "a - (b - c) = (a + c) - b" |
432 by (simp add: diff_minus add_ac) |
446 by (simp add: diff_minus add_ac) |
433 |
447 |
434 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0" |
448 lemma eq_iff_diff_eq_0: "a = b \<longleftrightarrow> a - b = 0" |
435 by (simp add: algebra_simps) |
449 by (simp add: algebra_simps) |
436 |
450 |
747 by (simp only: add_less_cancel_right) |
761 by (simp only: add_less_cancel_right) |
748 also have "... = (a - b < 0)" by (simp add: diff_minus) |
762 also have "... = (a - b < 0)" by (simp add: diff_minus) |
749 finally show ?thesis . |
763 finally show ?thesis . |
750 qed |
764 qed |
751 |
765 |
752 lemma diff_less_eq[algebra_simps]: "a - b < c \<longleftrightarrow> a < c + b" |
766 lemma diff_less_eq[algebra_simps, field_simps]: "a - b < c \<longleftrightarrow> a < c + b" |
753 apply (subst less_iff_diff_less_0 [of a]) |
767 apply (subst less_iff_diff_less_0 [of a]) |
754 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) |
768 apply (rule less_iff_diff_less_0 [of _ c, THEN ssubst]) |
755 apply (simp add: diff_minus add_ac) |
769 apply (simp add: diff_minus add_ac) |
756 done |
770 done |
757 |
771 |
758 lemma less_diff_eq[algebra_simps]: "a < c - b \<longleftrightarrow> a + b < c" |
772 lemma less_diff_eq[algebra_simps, field_simps]: "a < c - b \<longleftrightarrow> a + b < c" |
759 apply (subst less_iff_diff_less_0 [of "a + b"]) |
773 apply (subst less_iff_diff_less_0 [of "a + b"]) |
760 apply (subst less_iff_diff_less_0 [of a]) |
774 apply (subst less_iff_diff_less_0 [of a]) |
761 apply (simp add: diff_minus add_ac) |
775 apply (simp add: diff_minus add_ac) |
762 done |
776 done |
763 |
777 |
764 lemma diff_le_eq[algebra_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b" |
778 lemma diff_le_eq[algebra_simps, field_simps]: "a - b \<le> c \<longleftrightarrow> a \<le> c + b" |
765 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) |
779 by (auto simp add: le_less diff_less_eq diff_add_cancel add_diff_cancel) |
766 |
780 |
767 lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c" |
781 lemma le_diff_eq[algebra_simps, field_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c" |
768 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) |
782 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) |
769 |
783 |
770 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
784 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
771 by (simp add: algebra_simps) |
785 by (simp add: algebra_simps) |
772 |
786 |
773 text{*Legacy - use @{text algebra_simps} *} |
787 end |
774 lemmas group_simps[no_atp] = algebra_simps |
|
775 |
|
776 end |
|
777 |
|
778 text{*Legacy - use @{text algebra_simps} *} |
|
779 lemmas group_simps[no_atp] = algebra_simps |
|
780 |
788 |
781 class linordered_ab_semigroup_add = |
789 class linordered_ab_semigroup_add = |
782 linorder + ordered_ab_semigroup_add |
790 linorder + ordered_ab_semigroup_add |
783 |
791 |
784 class linordered_cancel_ab_semigroup_add = |
792 class linordered_cancel_ab_semigroup_add = |