equal
deleted
inserted
replaced
5 header {* Semiring normalization *} |
5 header {* Semiring normalization *} |
6 |
6 |
7 theory Semiring_Normalization |
7 theory Semiring_Normalization |
8 imports Numeral_Simprocs Nat_Transfer |
8 imports Numeral_Simprocs Nat_Transfer |
9 begin |
9 begin |
10 |
|
11 ML_file "Tools/semiring_normalizer.ML" |
|
12 |
10 |
13 text {* Prelude *} |
11 text {* Prelude *} |
14 |
12 |
15 class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + |
13 class comm_semiring_1_cancel_crossproduct = comm_semiring_1_cancel + |
16 assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |
14 assumes crossproduct_eq: "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" |
67 by (auto simp add: neq_iff dest!: aux) |
65 by (auto simp add: neq_iff dest!: aux) |
68 qed |
66 qed |
69 |
67 |
70 text {* Semiring normalization proper *} |
68 text {* Semiring normalization proper *} |
71 |
69 |
72 setup Semiring_Normalizer.setup |
70 ML_file "Tools/semiring_normalizer.ML" |
73 |
71 |
74 context comm_semiring_1 |
72 context comm_semiring_1 |
75 begin |
73 begin |
76 |
74 |
77 lemma normalizing_semiring_ops: |
75 lemma normalizing_semiring_ops: |