6 |
6 |
7 theory Groups |
7 theory Groups |
8 imports Orderings |
8 imports Orderings |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Fact collections *} |
11 subsection {* Dynamic facts *} |
12 |
12 |
13 ML {* |
13 named_theorems ac_simps "associativity and commutativity simplification rules" |
14 structure Ac_Simps = Named_Thms |
14 |
15 ( |
|
16 val name = @{binding ac_simps} |
|
17 val description = "associativity and commutativity simplification rules" |
|
18 ) |
|
19 *} |
|
20 |
|
21 setup Ac_Simps.setup |
|
22 |
15 |
23 text{* The rewrites accumulated in @{text algebra_simps} deal with the |
16 text{* The rewrites accumulated in @{text algebra_simps} deal with the |
24 classical algebraic structures of groups, rings and family. They simplify |
17 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 |
18 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 |
19 products into a canonical form (by ordered rewriting). As a result it decides |
27 group and ring equalities but also helps with inequalities. |
20 group and ring equalities but also helps with inequalities. |
28 |
21 |
29 Of course it also works for fields, but it knows nothing about multiplicative |
22 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}. *} |
23 inverses or division. This is catered for by @{text field_simps}. *} |
31 |
24 |
32 ML {* |
25 named_theorems algebra_simps "algebra simplification rules" |
33 structure Algebra_Simps = Named_Thms |
26 |
34 ( |
|
35 val name = @{binding algebra_simps} |
|
36 val description = "algebra simplification rules" |
|
37 ) |
|
38 *} |
|
39 |
|
40 setup Algebra_Simps.setup |
|
41 |
27 |
42 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations |
28 text{* Lemmas @{text field_simps} multiply with denominators in (in)equations |
43 if they can be proved to be non-zero (for equations) or positive/negative |
29 if they can be proved to be non-zero (for equations) or positive/negative |
44 (for inequations). Can be too aggressive and is therefore separate from the |
30 (for inequations). Can be too aggressive and is therefore separate from the |
45 more benign @{text algebra_simps}. *} |
31 more benign @{text algebra_simps}. *} |
46 |
32 |
47 ML {* |
33 named_theorems field_simps "algebra simplification rules for fields" |
48 structure Field_Simps = Named_Thms |
|
49 ( |
|
50 val name = @{binding field_simps} |
|
51 val description = "algebra simplification rules for fields" |
|
52 ) |
|
53 *} |
|
54 |
|
55 setup Field_Simps.setup |
|
56 |
34 |
57 |
35 |
58 subsection {* Abstract structures *} |
36 subsection {* Abstract structures *} |
59 |
37 |
60 text {* |
38 text {* |