50 then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto |
50 then show "w * y + x * z = w * z + x * y \<longleftrightarrow> w = x \<or> y = z" by auto |
51 qed |
51 qed |
52 |
52 |
53 setup Semiring_Normalizer.setup |
53 setup Semiring_Normalizer.setup |
54 |
54 |
55 locale normalizing_semiring = |
55 lemma (in comm_semiring_1) semiring_ops: |
56 fixes add mul pwr r0 r1 |
56 shows "TERM (x + y)" and "TERM (x * y)" and "TERM (x ^ n)" |
57 assumes add_a:"(add x (add y z) = add (add x y) z)" |
57 and "TERM 0" and "TERM 1" . |
58 and add_c: "add x y = add y x" and add_0:"add r0 x = x" |
58 |
59 and mul_a:"mul x (mul y z) = mul (mul x y) z" and mul_c:"mul x y = mul y x" |
59 lemma (in comm_semiring_1) semiring_rules: |
60 and mul_1:"mul r1 x = x" and mul_0:"mul r0 x = r0" |
60 "(a * m) + (b * m) = (a + b) * m" |
61 and mul_d:"mul x (add y z) = add (mul x y) (mul x z)" |
61 "(a * m) + m = (a + 1) * m" |
62 and pwr_0:"pwr x 0 = r1" and pwr_Suc:"pwr x (Suc n) = mul x (pwr x n)" |
62 "m + (a * m) = (a + 1) * m" |
63 begin |
63 "m + m = (1 + 1) * m" |
64 |
64 "0 + a = a" |
65 lemma mul_pwr:"mul (pwr x p) (pwr x q) = pwr x (p + q)" |
65 "a + 0 = a" |
66 proof (induct p) |
66 "a * b = b * a" |
67 case 0 |
67 "(a + b) * c = (a * c) + (b * c)" |
68 then show ?case by (auto simp add: pwr_0 mul_1) |
68 "0 * a = 0" |
69 next |
69 "a * 0 = 0" |
70 case Suc |
70 "1 * a = a" |
71 from this [symmetric] show ?case |
71 "a * 1 = a" |
72 by (auto simp add: pwr_Suc mul_1 mul_a) |
72 "(lx * ly) * (rx * ry) = (lx * rx) * (ly * ry)" |
73 qed |
73 "(lx * ly) * (rx * ry) = lx * (ly * (rx * ry))" |
74 |
74 "(lx * ly) * (rx * ry) = rx * ((lx * ly) * ry)" |
75 lemma pwr_mul: "pwr (mul x y) q = mul (pwr x q) (pwr y q)" |
75 "(lx * ly) * rx = (lx * rx) * ly" |
76 proof (induct q arbitrary: x y, auto simp add:pwr_0 pwr_Suc mul_1) |
76 "(lx * ly) * rx = lx * (ly * rx)" |
77 fix q x y |
77 "lx * (rx * ry) = (lx * rx) * ry" |
78 assume "\<And>x y. pwr (mul x y) q = mul (pwr x q) (pwr y q)" |
78 "lx * (rx * ry) = rx * (lx * ry)" |
79 have "mul (mul x y) (mul (pwr x q) (pwr y q)) = mul x (mul y (mul (pwr x q) (pwr y q)))" |
79 "(a + b) + (c + d) = (a + c) + (b + d)" |
80 by (simp add: mul_a) |
80 "(a + b) + c = a + (b + c)" |
81 also have "\<dots> = (mul (mul y (mul (pwr y q) (pwr x q))) x)" by (simp add: mul_c) |
81 "a + (c + d) = c + (a + d)" |
82 also have "\<dots> = (mul (mul y (pwr y q)) (mul (pwr x q) x))" by (simp add: mul_a) |
82 "(a + b) + c = (a + c) + b" |
83 finally show "mul (mul x y) (mul (pwr x q) (pwr y q)) = |
83 "a + c = c + a" |
84 mul (mul x (pwr x q)) (mul y (pwr y q))" by (simp add: mul_c) |
84 "a + (c + d) = (a + c) + d" |
85 qed |
85 "(x ^ p) * (x ^ q) = x ^ (p + q)" |
86 |
86 "x * (x ^ q) = x ^ (Suc q)" |
87 lemma pwr_pwr: "pwr (pwr x p) q = pwr x (p * q)" |
87 "(x ^ q) * x = x ^ (Suc q)" |
88 proof (induct p arbitrary: q) |
88 "x * x = x ^ 2" |
89 case 0 |
89 "(x * y) ^ q = (x ^ q) * (y ^ q)" |
90 show ?case using pwr_Suc mul_1 pwr_0 by (induct q) auto |
90 "(x ^ p) ^ q = x ^ (p * q)" |
91 next |
91 "x ^ 0 = 1" |
92 case Suc |
92 "x ^ 1 = x" |
93 thus ?case by (auto simp add: mul_pwr [symmetric] pwr_mul pwr_Suc) |
93 "x * (y + z) = (x * y) + (x * z)" |
94 qed |
94 "x ^ (Suc q) = x * (x ^ q)" |
95 |
95 "x ^ (2*n) = (x ^ n) * (x ^ n)" |
96 lemma semiring_ops: |
96 "x ^ (Suc (2*n)) = x * ((x ^ n) * (x ^ n))" |
97 shows "TERM (add x y)" and "TERM (mul x y)" and "TERM (pwr x n)" |
97 by (simp_all add: algebra_simps power_add power2_eq_square power_mult_distrib power_mult) |
98 and "TERM r0" and "TERM r1" . |
|
99 |
|
100 lemma semiring_rules: |
|
101 "add (mul a m) (mul b m) = mul (add a b) m" |
|
102 "add (mul a m) m = mul (add a r1) m" |
|
103 "add m (mul a m) = mul (add a r1) m" |
|
104 "add m m = mul (add r1 r1) m" |
|
105 "add r0 a = a" |
|
106 "add a r0 = a" |
|
107 "mul a b = mul b a" |
|
108 "mul (add a b) c = add (mul a c) (mul b c)" |
|
109 "mul r0 a = r0" |
|
110 "mul a r0 = r0" |
|
111 "mul r1 a = a" |
|
112 "mul a r1 = a" |
|
113 "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)" |
|
114 "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))" |
|
115 "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)" |
|
116 "mul (mul lx ly) rx = mul (mul lx rx) ly" |
|
117 "mul (mul lx ly) rx = mul lx (mul ly rx)" |
|
118 "mul lx (mul rx ry) = mul (mul lx rx) ry" |
|
119 "mul lx (mul rx ry) = mul rx (mul lx ry)" |
|
120 "add (add a b) (add c d) = add (add a c) (add b d)" |
|
121 "add (add a b) c = add a (add b c)" |
|
122 "add a (add c d) = add c (add a d)" |
|
123 "add (add a b) c = add (add a c) b" |
|
124 "add a c = add c a" |
|
125 "add a (add c d) = add (add a c) d" |
|
126 "mul (pwr x p) (pwr x q) = pwr x (p + q)" |
|
127 "mul x (pwr x q) = pwr x (Suc q)" |
|
128 "mul (pwr x q) x = pwr x (Suc q)" |
|
129 "mul x x = pwr x 2" |
|
130 "pwr (mul x y) q = mul (pwr x q) (pwr y q)" |
|
131 "pwr (pwr x p) q = pwr x (p * q)" |
|
132 "pwr x 0 = r1" |
|
133 "pwr x 1 = x" |
|
134 "mul x (add y z) = add (mul x y) (mul x z)" |
|
135 "pwr x (Suc q) = mul x (pwr x q)" |
|
136 "pwr x (2*n) = mul (pwr x n) (pwr x n)" |
|
137 "pwr x (Suc (2*n)) = mul x (mul (pwr x n) (pwr x n))" |
|
138 proof - |
|
139 show "add (mul a m) (mul b m) = mul (add a b) m" using mul_d mul_c by simp |
|
140 next show"add (mul a m) m = mul (add a r1) m" using mul_d mul_c mul_1 by simp |
|
141 next show "add m (mul a m) = mul (add a r1) m" using mul_c mul_d mul_1 add_c by simp |
|
142 next show "add m m = mul (add r1 r1) m" using mul_c mul_d mul_1 by simp |
|
143 next show "add r0 a = a" using add_0 by simp |
|
144 next show "add a r0 = a" using add_0 add_c by simp |
|
145 next show "mul a b = mul b a" using mul_c by simp |
|
146 next show "mul (add a b) c = add (mul a c) (mul b c)" using mul_c mul_d by simp |
|
147 next show "mul r0 a = r0" using mul_0 by simp |
|
148 next show "mul a r0 = r0" using mul_0 mul_c by simp |
|
149 next show "mul r1 a = a" using mul_1 by simp |
|
150 next show "mul a r1 = a" using mul_1 mul_c by simp |
|
151 next show "mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)" |
|
152 using mul_c mul_a by simp |
|
153 next show "mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))" |
|
154 using mul_a by simp |
|
155 next |
|
156 have "mul (mul lx ly) (mul rx ry) = mul (mul rx ry) (mul lx ly)" by (rule mul_c) |
|
157 also have "\<dots> = mul rx (mul ry (mul lx ly))" using mul_a by simp |
|
158 finally |
|
159 show "mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)" |
|
160 using mul_c by simp |
|
161 next show "mul (mul lx ly) rx = mul (mul lx rx) ly" using mul_c mul_a by simp |
|
162 next |
|
163 show "mul (mul lx ly) rx = mul lx (mul ly rx)" by (simp add: mul_a) |
|
164 next show "mul lx (mul rx ry) = mul (mul lx rx) ry" by (simp add: mul_a ) |
|
165 next show "mul lx (mul rx ry) = mul rx (mul lx ry)" by (simp add: mul_a,simp add: mul_c) |
|
166 next show "add (add a b) (add c d) = add (add a c) (add b d)" |
|
167 using add_c add_a by simp |
|
168 next show "add (add a b) c = add a (add b c)" using add_a by simp |
|
169 next show "add a (add c d) = add c (add a d)" |
|
170 apply (simp add: add_a) by (simp only: add_c) |
|
171 next show "add (add a b) c = add (add a c) b" using add_a add_c by simp |
|
172 next show "add a c = add c a" by (rule add_c) |
|
173 next show "add a (add c d) = add (add a c) d" using add_a by simp |
|
174 next show "mul (pwr x p) (pwr x q) = pwr x (p + q)" by (rule mul_pwr) |
|
175 next show "mul x (pwr x q) = pwr x (Suc q)" using pwr_Suc by simp |
|
176 next show "mul (pwr x q) x = pwr x (Suc q)" using pwr_Suc mul_c by simp |
|
177 next show "mul x x = pwr x 2" by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) |
|
178 next show "pwr (mul x y) q = mul (pwr x q) (pwr y q)" by (rule pwr_mul) |
|
179 next show "pwr (pwr x p) q = pwr x (p * q)" by (rule pwr_pwr) |
|
180 next show "pwr x 0 = r1" using pwr_0 . |
|
181 next show "pwr x 1 = x" unfolding One_nat_def by (simp add: nat_number' pwr_Suc pwr_0 mul_1 mul_c) |
|
182 next show "mul x (add y z) = add (mul x y) (mul x z)" using mul_d by simp |
|
183 next show "pwr x (Suc q) = mul x (pwr x q)" using pwr_Suc by simp |
|
184 next show "pwr x (2 * n) = mul (pwr x n) (pwr x n)" by (simp add: nat_number' mul_pwr) |
|
185 next show "pwr x (Suc (2 * n)) = mul x (mul (pwr x n) (pwr x n))" |
|
186 by (simp add: nat_number' pwr_Suc mul_pwr) |
|
187 qed |
|
188 |
|
189 end |
|
190 |
|
191 sublocale comm_semiring_1 |
|
192 < normalizing!: normalizing_semiring plus times power zero one |
|
193 proof |
|
194 qed (simp_all add: algebra_simps) |
|
195 |
98 |
196 lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms = |
99 lemmas (in comm_semiring_1) normalizing_comm_semiring_1_axioms = |
197 comm_semiring_1_axioms [normalizer |
100 comm_semiring_1_axioms [normalizer |
198 semiring ops: normalizing.semiring_ops |
101 semiring ops: semiring_ops |
199 semiring rules: normalizing.semiring_rules] |
102 semiring rules: semiring_rules] |
200 |
103 |
201 declaration (in comm_semiring_1) |
104 declaration (in comm_semiring_1) |
202 {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *} |
105 {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_axioms} *} |
203 |
106 |
204 locale normalizing_ring = normalizing_semiring + |
107 lemma (in comm_ring_1) ring_ops: shows "TERM (x- y)" and "TERM (- x)" . |
205 fixes sub :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
108 |
206 and neg :: "'a \<Rightarrow> 'a" |
109 lemma (in comm_ring_1) ring_rules: |
207 assumes neg_mul: "neg x = mul (neg r1) x" |
110 "- x = (- 1) * x" |
208 and sub_add: "sub x y = add x (neg y)" |
111 "x - y = x + (- y)" |
209 begin |
112 by (simp_all add: diff_minus) |
210 |
|
211 lemma ring_ops: shows "TERM (sub x y)" and "TERM (neg x)" . |
|
212 |
|
213 lemmas ring_rules = neg_mul sub_add |
|
214 |
|
215 end |
|
216 |
|
217 sublocale comm_ring_1 |
|
218 < normalizing!: normalizing_ring plus times power zero one minus uminus |
|
219 proof |
|
220 qed (simp_all add: diff_minus) |
|
221 |
113 |
222 lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms = |
114 lemmas (in comm_ring_1) normalizing_comm_ring_1_axioms = |
223 comm_ring_1_axioms [normalizer |
115 comm_ring_1_axioms [normalizer |
224 semiring ops: normalizing.semiring_ops |
116 semiring ops: semiring_ops |
225 semiring rules: normalizing.semiring_rules |
117 semiring rules: semiring_rules |
226 ring ops: normalizing.ring_ops |
118 ring ops: ring_ops |
227 ring rules: normalizing.ring_rules] |
119 ring rules: ring_rules] |
228 |
120 |
229 declaration (in comm_ring_1) |
121 declaration (in comm_ring_1) |
230 {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *} |
122 {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_ring_1_axioms} *} |
231 |
123 |
232 locale normalizing_semiring_cancel = normalizing_semiring + |
124 lemma (in comm_semiring_1_cancel_norm) noteq_reduce: |
233 assumes add_cancel: "add (x::'a) y = add x z \<longleftrightarrow> y = z" |
125 "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)" |
234 and add_mul_solve: "add (mul w y) (mul x z) = |
|
235 add (mul w z) (mul x y) \<longleftrightarrow> w = x \<or> y = z" |
|
236 begin |
|
237 |
|
238 lemma noteq_reduce: "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)" |
|
239 proof- |
126 proof- |
240 have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp |
127 have "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> \<not> (a = b \<or> c = d)" by simp |
241 also have "\<dots> \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)" |
128 also have "\<dots> \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)" |
242 using add_mul_solve by blast |
129 using add_mult_solve by blast |
243 finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> add (mul a c) (mul b d) \<noteq> add (mul a d) (mul b c)" |
130 finally show "a \<noteq> b \<and> c \<noteq> d \<longleftrightarrow> (a * c) + (b * d) \<noteq> (a * d) + (b * c)" |
244 by simp |
131 by simp |
245 qed |
132 qed |
246 |
133 |
247 lemma add_scale_eq_noteq: "\<lbrakk>r \<noteq> r0 ; (a = b) \<and> ~(c = d)\<rbrakk> |
134 lemma (in comm_semiring_1_cancel_norm) add_scale_eq_noteq: |
248 \<Longrightarrow> add a (mul r c) \<noteq> add b (mul r d)" |
135 "\<lbrakk>r \<noteq> 0 ; a = b \<and> c \<noteq> d\<rbrakk> \<Longrightarrow> a + (r * c) \<noteq> b + (r * d)" |
249 proof(clarify) |
136 proof(clarify) |
250 assume nz: "r\<noteq> r0" and cnd: "c\<noteq>d" |
137 assume nz: "r\<noteq> 0" and cnd: "c\<noteq>d" |
251 and eq: "add b (mul r c) = add b (mul r d)" |
138 and eq: "b + (r * c) = b + (r * d)" |
252 hence "mul r c = mul r d" using cnd add_cancel by simp |
139 have "(0 * d) + (r * c) = (0 * c) + (r * d)" |
253 hence "add (mul r0 d) (mul r c) = add (mul r0 c) (mul r d)" |
140 using add_imp_eq eq mult_zero_left by simp |
254 using mul_0 add_cancel by simp |
141 thus "False" using add_mult_solve[of 0 d] nz cnd by simp |
255 thus "False" using add_mul_solve nz cnd by simp |
142 qed |
256 qed |
143 |
257 |
144 lemma (in comm_semiring_1_cancel_norm) add_0_iff: |
258 lemma add_r0_iff: " x = add x a \<longleftrightarrow> a = r0" |
145 "x = x + a \<longleftrightarrow> a = 0" |
259 proof- |
146 proof- |
260 have "a = r0 \<longleftrightarrow> add x a = add x r0" by (simp add: add_cancel) |
147 have "a = 0 \<longleftrightarrow> x + a = x + 0" using add_imp_eq[of x a 0] by auto |
261 thus "x = add x a \<longleftrightarrow> a = r0" by (auto simp add: add_c add_0) |
148 thus "x = x + a \<longleftrightarrow> a = 0" by (auto simp add: add_commute) |
262 qed |
149 qed |
263 |
|
264 end |
|
265 |
|
266 sublocale comm_semiring_1_cancel_norm |
|
267 < normalizing!: normalizing_semiring_cancel plus times power zero one |
|
268 proof |
|
269 qed (simp_all add: add_mult_solve) |
|
270 |
150 |
271 declare (in comm_semiring_1_cancel_norm) |
151 declare (in comm_semiring_1_cancel_norm) |
272 normalizing_comm_semiring_1_axioms [normalizer del] |
152 normalizing_comm_semiring_1_axioms [normalizer del] |
273 |
153 |
274 lemmas (in comm_semiring_1_cancel_norm) |
154 lemmas (in comm_semiring_1_cancel_norm) |
275 normalizing_comm_semiring_1_cancel_norm_axioms = |
155 normalizing_comm_semiring_1_cancel_norm_axioms = |
276 comm_semiring_1_cancel_norm_axioms [normalizer |
156 comm_semiring_1_cancel_norm_axioms [normalizer |
277 semiring ops: normalizing.semiring_ops |
157 semiring ops: semiring_ops |
278 semiring rules: normalizing.semiring_rules |
158 semiring rules: semiring_rules |
279 idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq] |
159 idom rules: noteq_reduce add_scale_eq_noteq] |
280 |
160 |
281 declaration (in comm_semiring_1_cancel_norm) |
161 declaration (in comm_semiring_1_cancel_norm) |
282 {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *} |
162 {* Semiring_Normalizer.semiring_funs @{thm normalizing_comm_semiring_1_cancel_norm_axioms} *} |
283 |
163 |
284 locale normalizing_ring_cancel = normalizing_semiring_cancel + normalizing_ring + |
|
285 assumes subr0_iff: "sub x y = r0 \<longleftrightarrow> x = y" |
|
286 |
|
287 sublocale idom |
|
288 < normalizing!: normalizing_ring_cancel plus times power zero one minus uminus |
|
289 proof |
|
290 qed simp |
|
291 |
|
292 declare (in idom) normalizing_comm_ring_1_axioms [normalizer del] |
164 declare (in idom) normalizing_comm_ring_1_axioms [normalizer del] |
293 |
165 |
294 lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer |
166 lemmas (in idom) normalizing_idom_axioms = idom_axioms [normalizer |
295 semiring ops: normalizing.semiring_ops |
167 semiring ops: semiring_ops |
296 semiring rules: normalizing.semiring_rules |
168 semiring rules: semiring_rules |
297 ring ops: normalizing.ring_ops |
169 ring ops: ring_ops |
298 ring rules: normalizing.ring_rules |
170 ring rules: ring_rules |
299 idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq |
171 idom rules: noteq_reduce add_scale_eq_noteq |
300 ideal rules: normalizing.subr0_iff normalizing.add_r0_iff] |
172 ideal rules: right_minus_eq add_0_iff] |
301 |
173 |
302 declaration (in idom) |
174 declaration (in idom) |
303 {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *} |
175 {* Semiring_Normalizer.semiring_funs @{thm normalizing_idom_axioms} *} |
304 |
176 |
305 locale normalizing_field = normalizing_ring_cancel + |
177 lemma (in field) field_ops: |
306 fixes divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" |
178 shows "TERM (x / y)" and "TERM (inverse x)" . |
307 and inverse:: "'a \<Rightarrow> 'a" |
179 |
308 assumes divide_inverse: "divide x y = mul x (inverse y)" |
180 lemmas (in field) field_rules = divide_inverse inverse_eq_divide |
309 and inverse_divide: "inverse x = divide r1 x" |
|
310 begin |
|
311 |
|
312 lemma field_ops: shows "TERM (divide x y)" and "TERM (inverse x)" . |
|
313 |
|
314 lemmas field_rules = divide_inverse inverse_divide |
|
315 |
|
316 end |
|
317 |
|
318 sublocale field |
|
319 < normalizing!: normalizing_field plus times power zero one minus uminus divide inverse |
|
320 proof |
|
321 qed (simp_all add: divide_inverse) |
|
322 |
181 |
323 lemmas (in field) normalizing_field_axioms = |
182 lemmas (in field) normalizing_field_axioms = |
324 field_axioms [normalizer |
183 field_axioms [normalizer |
325 semiring ops: normalizing.semiring_ops |
184 semiring ops: semiring_ops |
326 semiring rules: normalizing.semiring_rules |
185 semiring rules: semiring_rules |
327 ring ops: normalizing.ring_ops |
186 ring ops: ring_ops |
328 ring rules: normalizing.ring_rules |
187 ring rules: ring_rules |
329 field ops: normalizing.field_ops |
188 field ops: field_ops |
330 field rules: normalizing.field_rules |
189 field rules: field_rules |
331 idom rules: normalizing.noteq_reduce normalizing.add_scale_eq_noteq |
190 idom rules: noteq_reduce add_scale_eq_noteq |
332 ideal rules: normalizing.subr0_iff normalizing.add_r0_iff] |
191 ideal rules: right_minus_eq add_0_iff] |
333 |
192 |
334 declaration (in field) |
193 declaration (in field) |
335 {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *} |
194 {* Semiring_Normalizer.field_funs @{thm normalizing_field_axioms} *} |
336 |
195 |
|
196 hide_fact (open) normalizing_comm_semiring_1_axioms |
|
197 normalizing_comm_semiring_1_cancel_norm_axioms semiring_ops semiring_rules |
|
198 |
|
199 hide_fact (open) normalizing_comm_ring_1_axioms |
|
200 normalizing_idom_axioms ring_ops ring_rules |
|
201 |
|
202 hide_fact (open) normalizing_field_axioms field_ops field_rules |
|
203 |
|
204 hide_fact (open) add_scale_eq_noteq noteq_reduce |
|
205 |
337 end |
206 end |