70 ML_file "Tools/semiring_normalizer.ML" |
70 ML_file "Tools/semiring_normalizer.ML" |
71 |
71 |
72 context comm_semiring_1 |
72 context comm_semiring_1 |
73 begin |
73 begin |
74 |
74 |
75 declaration \<open> |
75 lemma semiring_normalization_rules: |
76 let |
76 "(a * m) + (b * m) = (a + b) * m" |
77 val rules = @{lemma |
77 "(a * m) + m = (a + 1) * m" |
78 "(a * m) + (b * m) = (a + b) * m" |
78 "m + (a * m) = (a + 1) * m" |
79 "(a * m) + m = (a + 1) * m" |
79 "m + m = (1 + 1) * m" |
80 "m + (a * m) = (a + 1) * m" |
80 "0 + a = a" |
81 "m + m = (1 + 1) * m" |
81 "a + 0 = a" |
82 "0 + a = a" |
82 "a * b = b * a" |
83 "a + 0 = a" |
83 "(a + b) * c = (a * c) + (b * c)" |
84 "a * b = b * a" |
84 "0 * a = 0" |
85 "(a + b) * c = (a * c) + (b * c)" |
85 "a * 0 = 0" |
86 "0 * a = 0" |
86 "1 * a = a" |
87 "a * 0 = 0" |
87 "a * 1 = a" |
88 "1 * a = a" |
88 "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" |
89 "a * 1 = a" |
89 "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" |
90 "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" |
90 "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" |
91 "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" |
91 "(lx * ly) * rx = (lx * rx) * ly" |
92 "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" |
92 "(lx * ly) * rx = lx * (ly * rx)" |
93 "(lx * ly) * rx = (lx * rx) * ly" |
93 "lx * (rx * ry) = (lx * rx) * ry" |
94 "(lx * ly) * rx = lx * (ly * rx)" |
94 "lx * (rx * ry) = rx * (lx * ry)" |
95 "lx * (rx * ry) = (lx * rx) * ry" |
95 "(a + b) + (c + d) = (a + c) + (b + d)" |
96 "lx * (rx * ry) = rx * (lx * ry)" |
96 "(a + b) + c = a + (b + c)" |
97 "(a + b) + (c + d) = (a + c) + (b + d)" |
97 "a + (c + d) = c + (a + d)" |
98 "(a + b) + c = a + (b + c)" |
98 "(a + b) + c = (a + c) + b" |
99 "a + (c + d) = c + (a + d)" |
99 "a + c = c + a" |
100 "(a + b) + c = (a + c) + b" |
100 "a + (c + d) = (a + c) + d" |
101 "a + c = c + a" |
101 "(x ^ p) * (x ^ q) = x ^ (p + q)" |
102 "a + (c + d) = (a + c) + d" |
102 "x * (x ^ q) = x ^ (Suc q)" |
103 "(x ^ p) * (x ^ q) = x ^ (p + q)" |
103 "(x ^ q) * x = x ^ (Suc q)" |
104 "x * (x ^ q) = x ^ (Suc q)" |
104 "x * x = x\<^sup>2" |
105 "(x ^ q) * x = x ^ (Suc q)" |
105 "(x * y) ^ q = (x ^ q) * (y ^ q)" |
106 "x * x = x\<^sup>2" |
106 "(x ^ p) ^ q = x ^ (p * q)" |
107 "(x * y) ^ q = (x ^ q) * (y ^ q)" |
107 "x ^ 0 = 1" |
108 "(x ^ p) ^ q = x ^ (p * q)" |
108 "x ^ 1 = x" |
109 "x ^ 0 = 1" |
109 "x * (y + z) = (x * y) + (x * z)" |
110 "x ^ 1 = x" |
110 "x ^ (Suc q) = x * (x ^ q)" |
111 "x * (y + z) = (x * y) + (x * z)" |
111 "x ^ (2*n) = (x ^ n) * (x ^ n)" |
112 "x ^ (Suc q) = x * (x ^ q)" |
112 by (simp_all add: algebra_simps power_add power2_eq_square |
113 "x ^ (2*n) = (x ^ n) * (x ^ n)" |
113 power_mult_distrib power_mult del: one_add_one) |
114 by (simp_all add: algebra_simps power_add power2_eq_square |
114 |
115 power_mult_distrib power_mult del: one_add_one)} |
115 local_setup \<open> |
116 in |
|
117 Semiring_Normalizer.declare @{thm comm_semiring_1_axioms} |
116 Semiring_Normalizer.declare @{thm comm_semiring_1_axioms} |
118 {semiring = ([@{cpat "?x + ?y"}, @{cpat "?x * ?y"}, @{cpat "?x ^ ?n"}, @{cpat 0}, @{cpat 1}], |
117 {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], |
119 rules), ring = ([], []), field = ([], []), idom = [], ideal = []} |
118 @{thms semiring_normalization_rules}), |
120 end\<close> |
119 ring = ([], []), |
|
120 field = ([], []), |
|
121 idom = [], |
|
122 ideal = []} |
|
123 \<close> |
121 |
124 |
122 end |
125 end |
123 |
126 |
124 context comm_ring_1 |
127 context comm_ring_1 |
125 begin |
128 begin |
126 |
129 |
127 declaration \<open> |
130 lemma ring_normalization_rules: |
128 let |
131 "- x = (- 1) * x" |
129 val rules = @{lemma |
132 "x - y = x + (- y)" |
130 "- x = (- 1) * x" |
133 by simp_all |
131 "x - y = x + (- y)" |
134 |
132 by simp_all} |
135 local_setup \<open> |
133 in |
|
134 Semiring_Normalizer.declare @{thm comm_ring_1_axioms} |
136 Semiring_Normalizer.declare @{thm comm_ring_1_axioms} |
135 {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, |
137 {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], |
136 ring = ([@{cpat "?x - ?y"}, @{cpat "- ?x"}], rules), field = ([], []), idom = [], ideal = []} |
138 @{thms semiring_normalization_rules}), |
137 end\<close> |
139 ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), |
|
140 field = ([], []), |
|
141 idom = [], |
|
142 ideal = []} |
|
143 \<close> |
138 |
144 |
139 end |
145 end |
140 |
146 |
141 context comm_semiring_1_cancel_crossproduct |
147 context comm_semiring_1_cancel_crossproduct |
142 begin |
148 begin |
143 |
149 |
144 declaration \<open>Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} |
150 local_setup \<open> |
145 {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_semiring_1_axioms}, |
151 Semiring_Normalizer.declare @{thm comm_semiring_1_cancel_crossproduct_axioms} |
146 ring = ([], []), field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, ideal = []}\<close> |
152 {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], |
|
153 @{thms semiring_normalization_rules}), |
|
154 ring = ([], []), |
|
155 field = ([], []), |
|
156 idom = @{thms crossproduct_noteq add_scale_eq_noteq}, |
|
157 ideal = []} |
|
158 \<close> |
147 |
159 |
148 end |
160 end |
149 |
161 |
150 context idom |
162 context idom |
151 begin |
163 begin |
152 |
164 |
153 declaration \<open>Semiring_Normalizer.declare @{thm idom_axioms} |
165 local_setup \<open> |
154 {semiring = Semiring_Normalizer.the_semiring @{context} @{thm comm_ring_1_axioms}, |
166 Semiring_Normalizer.declare @{thm idom_axioms} |
155 ring = Semiring_Normalizer.the_ring @{context} @{thm comm_ring_1_axioms}, |
167 {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], |
156 field = ([], []), idom = @{thms crossproduct_noteq add_scale_eq_noteq}, |
168 @{thms semiring_normalization_rules}), |
157 ideal = @{thms right_minus_eq add_0_iff}}\<close> |
169 ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), |
|
170 field = ([], []), |
|
171 idom = @{thms crossproduct_noteq add_scale_eq_noteq}, |
|
172 ideal = @{thms right_minus_eq add_0_iff}} |
|
173 \<close> |
158 |
174 |
159 end |
175 end |
160 |
176 |
161 context field |
177 context field |
162 begin |
178 begin |
163 |
179 |
164 declaration \<open>Semiring_Normalizer.declare @{thm field_axioms} |
180 local_setup \<open> |
165 {semiring = Semiring_Normalizer.the_semiring @{context} @{thm idom_axioms}, |
181 Semiring_Normalizer.declare @{thm field_axioms} |
166 ring = Semiring_Normalizer.the_ring @{context} @{thm idom_axioms}, |
182 {semiring = ([@{term "x + y"}, @{term "x * y"}, @{term "x ^ n"}, @{term 0}, @{term 1}], |
167 field = ([@{cpat "?x / ?y"}, @{cpat "inverse ?x"}], @{thms divide_inverse inverse_eq_divide}), |
183 @{thms semiring_normalization_rules}), |
168 idom = Semiring_Normalizer.the_idom @{context} @{thm idom_axioms}, |
184 ring = ([@{term "x - y"}, @{term "- x"}], @{thms ring_normalization_rules}), |
169 ideal = Semiring_Normalizer.the_ideal @{context} @{thm idom_axioms}}\<close> |
185 field = ([@{term "x / y"}, @{term "inverse x"}], @{thms divide_inverse inverse_eq_divide}), |
|
186 idom = @{thms crossproduct_noteq add_scale_eq_noteq}, |
|
187 ideal = @{thms right_minus_eq add_0_iff}} |
|
188 \<close> |
170 |
189 |
171 end |
190 end |
172 |
191 |
173 code_identifier |
192 code_identifier |
174 code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |
193 code_module Semiring_Normalization \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith |