equal
deleted
inserted
replaced
13 begin |
13 begin |
14 |
14 |
15 subsection \<open>Dynamic facts\<close> |
15 subsection \<open>Dynamic facts\<close> |
16 |
16 |
17 named_theorems ac_simps "associativity and commutativity simplification rules" |
17 named_theorems ac_simps "associativity and commutativity simplification rules" |
18 and algebra_simps "algebra simplification rules" |
18 and algebra_simps "algebra simplification rules for rings" |
19 and field_simps "algebra simplification rules for fields" |
19 and field_simps "algebra simplification rules for fields" |
|
20 and sign_simps "algebra simplification rules for comparision with zero" |
20 |
21 |
21 text \<open> |
22 text \<open> |
22 The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical |
23 The rewrites accumulated in \<open>algebra_simps\<close> deal with the classical |
23 algebraic structures of groups, rings and family. They simplify terms by |
24 algebraic structures of groups, rings and family. They simplify terms by |
24 multiplying everything out (in case of a ring) and bringing sums and |
25 multiplying everything out (in case of a ring) and bringing sums and |
30 |
31 |
31 Facts in \<open>field_simps\<close> multiply with denominators in (in)equations if they |
32 Facts in \<open>field_simps\<close> multiply with denominators in (in)equations if they |
32 can be proved to be non-zero (for equations) or positive/negative (for |
33 can be proved to be non-zero (for equations) or positive/negative (for |
33 inequalities). Can be too aggressive and is therefore separate from the more |
34 inequalities). Can be too aggressive and is therefore separate from the more |
34 benign \<open>algebra_simps\<close>. |
35 benign \<open>algebra_simps\<close>. |
|
36 |
|
37 Lemmas \<open>sign_simps\<close> is a first attempt to automate proofs |
|
38 of positivity/negativity needed for \<open>field_simps\<close>. Have not added \<open>sign_simps\<close> to \<open>field_simps\<close> |
|
39 because the former can lead to case explosions. |
35 \<close> |
40 \<close> |
36 |
41 |
37 |
42 |
38 subsection \<open>Abstract structures\<close> |
43 subsection \<open>Abstract structures\<close> |
39 |
44 |