1 (* ========================================================================= *)
2 (* Relatively efficient HOL conversions for canonical polynomial form. *)
4 (* (c) Copyright, John Harrison 1998-2007 *)
5 (* ========================================================================= *)
9 let SEMIRING_NORMALIZERS_CONV =
10 let SEMIRING_PTHS = prove
11 (`(!x:A y z. add x (add y z) = add (add x y) z) /\
12 (!x y. add x y = add y x) /\
14 (!x y z. mul x (mul y z) = mul (mul x y) z) /\
15 (!x y. mul x y = mul y x) /\
17 (!x. mul r0 x = r0) /\
18 (!x y z. mul x (add y z) = add (mul x y) (mul x z)) /\
20 (!x n. pwr x (SUC n) = mul x (pwr x n))
22 (add (mul a m) (mul b m) = mul (add a b) m) /\
23 (add (mul a m) m = mul (add a r1) m) /\
24 (add m (mul a m) = mul (add a r1) m) /\
25 (add m m = mul (add r1 r1) m) /\
29 (mul a b = mul b a) /\
30 (mul (add a b) c = add (mul a c) (mul b c)) /\
35 (mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)) /\
36 (mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))) /\
37 (mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)) /\
38 (mul (mul lx ly) rx = mul (mul lx rx) ly) /\
39 (mul (mul lx ly) rx = mul lx (mul ly rx)) /\
40 (mul lx rx = mul rx lx) /\
41 (mul lx (mul rx ry) = mul (mul lx rx) ry) /\
42 (mul lx (mul rx ry) = mul rx (mul lx ry)) /\
43 (add (add a b) (add c d) = add (add a c) (add b d)) /\
44 (add (add a b) c = add a (add b c)) /\
45 (add a (add c d) = add c (add a d)) /\
46 (add (add a b) c = add (add a c) b) /\
47 (add a c = add c a) /\
48 (add a (add c d) = add (add a c) d) /\
49 (mul (pwr x p) (pwr x q) = pwr x (p + q)) /\
50 (mul x (pwr x q) = pwr x (SUC q)) /\
51 (mul (pwr x q) x = pwr x (SUC q)) /\
52 (mul x x = pwr x 2) /\
53 (pwr (mul x y) q = mul (pwr x q) (pwr y q)) /\
54 (pwr (pwr x p) q = pwr x (p * q)) /\
57 (mul x (add y z) = add (mul x y) (mul x z)) /\
58 (pwr x (SUC q) = mul x (pwr x q))`,
61 `(!m:A n. add m n = add n m) /\
62 (!m n p. add (add m n) p = add m (add n p)) /\
63 (!m n p. add m (add n p) = add n (add m p)) /\
65 (!m n. mul m n = mul n m) /\
66 (!m n p. mul (mul m n) p = mul m (mul n p)) /\
67 (!m n p. mul m (mul n p) = mul n (mul m p)) /\
68 (!m n p. mul (add m n) p = add (mul m p) (mul n p)) /\
73 MAP_EVERY (fun t -> UNDISCH_THEN t (K ALL_TAC))
74 [`!x:A y z. add x (add y z) = add (add x y) z`;
75 `!x:A y. add x y :A = add y x`;
76 `!x:A y z. mul x (mul y z) = mul (mul x y) z`;
77 `!x:A y. mul x y :A = mul y x`] THEN
79 ASM_REWRITE_TAC[num_CONV `2`; num_CONV `1`] THEN
80 SUBGOAL_THEN `!m n:num x:A. pwr x (m + n) :A = mul (pwr x m) (pwr x n)`
82 [GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]; ALL_TAC] THEN
83 SUBGOAL_THEN `!x:A y:A n:num. pwr (mul x y) n = mul (pwr x n) (pwr y n)`
85 [GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[];
87 SUBGOAL_THEN `!x:A m:num n. pwr (pwr x m) n = pwr x (m * n)`
88 (fun th -> ASM_MESON_TAC[th]) THEN
89 GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES])
90 and true_tm = concl TRUTH in
91 fun sth rth (is_semiring_constant,
96 [pthm_01; pthm_02; pthm_03; pthm_04; pthm_05; pthm_06; pthm_07; pthm_08;
97 pthm_09; pthm_10; pthm_11; pthm_12; pthm_13; pthm_14; pthm_15; pthm_16;
98 pthm_17; pthm_18; pthm_19; pthm_20; pthm_21; pthm_22; pthm_23; pthm_24;
99 pthm_25; pthm_26; pthm_27; pthm_28; pthm_29; pthm_30; pthm_31; pthm_32;
100 pthm_33; pthm_34; pthm_35; pthm_36; pthm_37; pthm_38] =
101 CONJUNCTS(MATCH_MP SEMIRING_PTHS sth) in
102 let add_tm = rator(rator(lhand(concl pthm_07)))
103 and mul_tm = rator(rator(lhand(concl pthm_13)))
104 and pow_tm = rator(rator(rand(concl pthm_32)))
105 and zero_tm = rand(concl pthm_06)
106 and one_tm = rand(lhand(concl pthm_14))
107 and ty = type_of(rand(concl pthm_01)) in
113 and a_tm = mk_var("a",ty)
114 and b_tm = mk_var("b",ty)
115 and c_tm = mk_var("c",ty)
116 and d_tm = mk_var("d",ty)
117 and lx_tm = mk_var("lx",ty)
118 and ly_tm = mk_var("ly",ty)
119 and m_tm = mk_var("m",ty)
120 and rx_tm = mk_var("rx",ty)
121 and ry_tm = mk_var("ry",ty)
122 and x_tm = mk_var("x",ty)
123 and y_tm = mk_var("y",ty)
124 and z_tm = mk_var("z",ty) in
126 let dest_add = dest_binop add_tm
127 and dest_mul = dest_binop mul_tm
129 let l,r = dest_binop pow_tm tm in
130 if is_numeral r then l,r else failwith "dest_pow"
131 and is_add = is_binop add_tm
132 and is_mul = is_binop mul_tm in
134 let nthm_1,nthm_2,sub_tm,neg_tm,dest_sub,is_sub =
135 if concl rth = true_tm then rth,rth,true_tm,true_tm,
136 (fun t -> t,t),K false
138 let nthm_1 = SPEC x_tm (CONJUNCT1 rth)
139 and nthm_2 = SPECL [x_tm; y_tm] (CONJUNCT2 rth) in
140 let sub_tm = rator(rator(lhand(concl nthm_2)))
141 and neg_tm = rator(lhand(concl nthm_1)) in
142 let dest_sub = dest_binop sub_tm
143 and is_sub = is_binop sub_tm in
144 (nthm_1,nthm_2,sub_tm,neg_tm,dest_sub,is_sub) in
146 fun variable_order ->
148 (* ------------------------------------------------------------------------- *)
149 (* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *)
150 (* Also deals with "const * const", but both terms must involve powers of *)
151 (* the same variable, or both be constants, or behaviour may be incorrect. *)
152 (* ------------------------------------------------------------------------- *)
154 let POWVAR_MUL_CONV tm =
155 let l,r = dest_mul tm in
156 if is_semiring_constant l & is_semiring_constant r
157 then SEMIRING_MUL_CONV tm else
158 try let lx,ln = dest_pow l in
159 try let rx,rn = dest_pow r in
160 let th1 = INST [lx,x_tm; ln,p_tm; rn,q_tm] pthm_29 in
161 let tm1,tm2 = dest_comb(rand(concl th1)) in
162 TRANS th1 (AP_TERM tm1 (NUM_ADD_CONV tm2))
164 let th1 = INST [lx,x_tm; ln,q_tm] pthm_31 in
165 let tm1,tm2 = dest_comb(rand(concl th1)) in
166 TRANS th1 (AP_TERM tm1 (NUM_SUC_CONV tm2))
168 try let rx,rn = dest_pow r in
169 let th1 = INST [rx,x_tm; rn,q_tm] pthm_30 in
170 let tm1,tm2 = dest_comb(rand(concl th1)) in
171 TRANS th1 (AP_TERM tm1 (NUM_SUC_CONV tm2))
173 INST [l,x_tm] pthm_32 in
175 (* ------------------------------------------------------------------------- *)
176 (* Remove "1 * m" from a monomial, and just leave m. *)
177 (* ------------------------------------------------------------------------- *)
179 let MONOMIAL_DEONE th =
180 try let l,r = dest_mul(rand(concl th)) in
181 if l = one_tm then TRANS th (INST [r,x_tm] pthm_01) else th
182 with Failure _ -> th in
184 (* ------------------------------------------------------------------------- *)
185 (* Conversion for "(monomial)^n", where n is a numeral. *)
186 (* ------------------------------------------------------------------------- *)
188 let MONOMIAL_POW_CONV =
189 let rec MONOMIAL_POW tm bod ntm =
190 if not(is_comb bod) then REFL tm
191 else if is_semiring_constant bod then SEMIRING_POW_CONV tm else
192 let lop,r = dest_comb bod in
193 if not(is_comb lop) then REFL tm else
194 let op,l = dest_comb lop in
195 if op = pow_tm & is_numeral r then
196 let th1 = INST [l,x_tm; r,p_tm; ntm,q_tm] pthm_34 in
197 let l,r = dest_comb(rand(concl th1)) in
198 TRANS th1 (AP_TERM l (NUM_MULT_CONV r))
199 else if op = mul_tm then
200 let th1 = INST [l,x_tm; r,y_tm; ntm,q_tm] pthm_33 in
201 let xy,z = dest_comb(rand(concl th1)) in
202 let x,y = dest_comb xy in
203 let thl = MONOMIAL_POW y l ntm
204 and thr = MONOMIAL_POW z r ntm in
205 TRANS th1 (MK_COMB(AP_TERM x thl,thr))
208 let lop,r = dest_comb tm in
209 let op,l = dest_comb lop in
210 if op <> pow_tm or not(is_numeral r) then failwith "MONOMIAL_POW_CONV"
211 else if r = zeron_tm then INST [l,x_tm] pthm_35
212 else if r = onen_tm then INST [l,x_tm] pthm_36
213 else MONOMIAL_DEONE(MONOMIAL_POW tm l r) in
215 (* ------------------------------------------------------------------------- *)
216 (* Multiplication of canonical monomials. *)
217 (* ------------------------------------------------------------------------- *)
219 let MONOMIAL_MUL_CONV =
221 if is_semiring_constant tm then one_tm else
222 try let lop,r = dest_comb tm in
223 let op,l = dest_comb lop in
224 if op = pow_tm & is_numeral r then l else failwith ""
225 with Failure _ -> tm in
228 else if x = one_tm then -1
229 else if y = one_tm then 1
230 else if variable_order x y then -1 else 1 in
231 let rec MONOMIAL_MUL tm l r =
232 try let lx,ly = dest_mul l in
233 let vl = powvar lx in
234 try let rx,ry = dest_mul r in
235 let vr = powvar rx in
236 let ord = vorder vl vr in
239 [lx,lx_tm; ly,ly_tm; rx,rx_tm; ry,ry_tm] pthm_15 in
240 let tm1,tm2 = dest_comb(rand(concl th1)) in
241 let tm3,tm4 = dest_comb tm1 in
242 let th2 = AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2 in
243 let th3 = TRANS th1 th2 in
244 let tm5,tm6 = dest_comb(rand(concl th3)) in
245 let tm7,tm8 = dest_comb tm6 in
246 let th4 = MONOMIAL_MUL tm6 (rand tm7) tm8 in
247 TRANS th3 (AP_TERM tm5 th4)
249 let th0 = if ord < 0 then pthm_16 else pthm_17 in
251 [lx,lx_tm; ly,ly_tm; rx,rx_tm; ry,ry_tm] th0 in
252 let tm1,tm2 = dest_comb(rand(concl th1)) in
253 let tm3,tm4 = dest_comb tm2 in
254 TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 (rand tm3) tm4))
257 let ord = vorder vl vr in
259 let th1 = INST [lx,lx_tm; ly,ly_tm; r,rx_tm] pthm_18 in
260 let tm1,tm2 = dest_comb(rand(concl th1)) in
261 let tm3,tm4 = dest_comb tm1 in
262 let th2 = AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2 in
265 let th1 = INST [lx,lx_tm; ly,ly_tm; r,rx_tm] pthm_19 in
266 let tm1,tm2 = dest_comb(rand(concl th1)) in
267 let tm3,tm4 = dest_comb tm2 in
268 TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 (rand tm3) tm4))
269 else INST [l,lx_tm; r,rx_tm] pthm_20
272 try let rx,ry = dest_mul r in
273 let vr = powvar rx in
274 let ord = vorder vl vr in
276 let th1 = INST [l,lx_tm; rx,rx_tm; ry,ry_tm] pthm_21 in
277 let tm1,tm2 = dest_comb(rand(concl th1)) in
278 let tm3,tm4 = dest_comb tm1 in
279 TRANS th1 (AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2)
281 let th1 = INST [l,lx_tm; rx,rx_tm; ry,ry_tm] pthm_22 in
282 let tm1,tm2 = dest_comb(rand(concl th1)) in
283 let tm3,tm4 = dest_comb tm2 in
284 TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 (rand tm3) tm4))
288 let ord = vorder vl vr in
289 if ord = 0 then POWVAR_MUL_CONV tm
290 else if ord > 0 then INST [l,lx_tm; r,rx_tm] pthm_20
292 fun tm -> let l,r = dest_mul tm in MONOMIAL_DEONE(MONOMIAL_MUL tm l r) in
294 (* ------------------------------------------------------------------------- *)
295 (* Multiplication by monomial of a polynomial. *)
296 (* ------------------------------------------------------------------------- *)
298 let POLYNOMIAL_MONOMIAL_MUL_CONV =
299 let rec PMM_CONV tm =
300 let l,r = dest_mul tm in
301 try let y,z = dest_add r in
302 let th1 = INST [l,x_tm; y,y_tm; z,z_tm] pthm_37 in
303 let tm1,tm2 = dest_comb(rand(concl th1)) in
304 let tm3,tm4 = dest_comb tm1 in
305 let th2 = MK_COMB(AP_TERM tm3 (MONOMIAL_MUL_CONV tm4),
308 with Failure _ -> MONOMIAL_MUL_CONV tm in
311 (* ------------------------------------------------------------------------- *)
312 (* Addition of two monomials identical except for constant multiples. *)
313 (* ------------------------------------------------------------------------- *)
315 let MONOMIAL_ADD_CONV tm =
316 let l,r = dest_add tm in
317 if is_semiring_constant l & is_semiring_constant r
318 then SEMIRING_ADD_CONV tm else
320 if is_mul l & is_semiring_constant(lhand l) then
321 if is_mul r & is_semiring_constant(lhand r) then
322 INST [lhand l,a_tm; lhand r,b_tm; rand r,m_tm] pthm_02
324 INST [lhand l,a_tm; r,m_tm] pthm_03
326 if is_mul r & is_semiring_constant(lhand r) then
327 INST [lhand r,a_tm; l,m_tm] pthm_04
329 INST [r,m_tm] pthm_05 in
330 let tm1,tm2 = dest_comb(rand(concl th1)) in
331 let tm3,tm4 = dest_comb tm1 in
332 let th2 = AP_TERM tm3 (SEMIRING_ADD_CONV tm4) in
333 let th3 = TRANS th1 (AP_THM th2 tm2) in
334 let tm5 = rand(concl th3) in
335 if lhand tm5 = zero_tm then TRANS th3 (INST [rand tm5,m_tm] pthm_06)
336 else MONOMIAL_DEONE th3 in
338 (* ------------------------------------------------------------------------- *)
339 (* Ordering on monomials. *)
340 (* ------------------------------------------------------------------------- *)
343 let ptms = striplist dest_mul tm in
344 if is_semiring_constant (hd ptms) then tl ptms else ptms in
347 try let x,n = dest_pow tm in (x,dest_numeral n)
349 (tm,(if is_semiring_constant tm then num_0 else num_1)) in
352 let rec lexorder l1 l2 =
357 | ((x1,n1)::vs1),((x2,n2)::vs2) ->
358 if variable_order x1 x2 then 1
359 else if variable_order x2 x1 then -1
360 else if n1 </ n2 then -1
361 else if n2 </ n1 then 1
362 else lexorder vs1 vs2 in
364 let vdegs1 = map dest_varpow (powervars tm1)
365 and vdegs2 = map dest_varpow (powervars tm2) in
366 let deg1 = itlist ((+/) o snd) vdegs1 num_0
367 and deg2 = itlist ((+/) o snd) vdegs2 num_0 in
368 if deg1 </ deg2 then -1 else if deg1 >/ deg2 then 1
369 else lexorder vdegs1 vdegs2 in
371 (* ------------------------------------------------------------------------- *)
372 (* Addition of two polynomials. *)
373 (* ------------------------------------------------------------------------- *)
375 let POLYNOMIAL_ADD_CONV =
377 let tm = rand(concl th) in
378 if not(is_add tm) then th else
379 let lop,r = dest_comb tm in
381 if l = zero_tm then TRANS th (INST [r,a_tm] pthm_07)
382 else if r = zero_tm then TRANS th (INST [l,a_tm] pthm_08)
385 let l,r = dest_add tm in
386 if l = zero_tm then INST [r,a_tm] pthm_07
387 else if r = zero_tm then INST [l,a_tm] pthm_08 else
389 let a,b = dest_add l in
391 let c,d = dest_add r in
392 let ord = morder a c in
394 let th1 = INST [a,a_tm; b,b_tm; c,c_tm; d,d_tm] pthm_23 in
395 let tm1,tm2 = dest_comb(rand(concl th1)) in
396 let tm3,tm4 = dest_comb tm1 in
397 let th2 = AP_TERM tm3 (MONOMIAL_ADD_CONV tm4) in
398 DEZERO_RULE (TRANS th1 (MK_COMB(th2,PADD tm2)))
401 if ord > 0 then INST [a,a_tm; b,b_tm; r,c_tm] pthm_24
402 else INST [l,a_tm; c,c_tm; d,d_tm] pthm_25 in
403 let tm1,tm2 = dest_comb(rand(concl th1)) in
404 DEZERO_RULE (TRANS th1 (AP_TERM tm1 (PADD tm2)))
406 let ord = morder a r in
408 let th1 = INST [a,a_tm; b,b_tm; r,c_tm] pthm_26 in
409 let tm1,tm2 = dest_comb(rand(concl th1)) in
410 let tm3,tm4 = dest_comb tm1 in
411 let th2 = AP_THM (AP_TERM tm3 (MONOMIAL_ADD_CONV tm4)) tm2 in
412 DEZERO_RULE (TRANS th1 th2)
414 let th1 = INST [a,a_tm; b,b_tm; r,c_tm] pthm_24 in
415 let tm1,tm2 = dest_comb(rand(concl th1)) in
416 DEZERO_RULE (TRANS th1 (AP_TERM tm1 (PADD tm2)))
418 DEZERO_RULE (INST [l,a_tm; r,c_tm] pthm_27)
421 let c,d = dest_add r in
422 let ord = morder l c in
424 let th1 = INST [l,a_tm; c,c_tm; d,d_tm] pthm_28 in
425 let tm1,tm2 = dest_comb(rand(concl th1)) in
426 let tm3,tm4 = dest_comb tm1 in
427 let th2 = AP_THM (AP_TERM tm3 (MONOMIAL_ADD_CONV tm4)) tm2 in
428 DEZERO_RULE (TRANS th1 th2)
432 let th1 = INST [l,a_tm; c,c_tm; d,d_tm] pthm_25 in
433 let tm1,tm2 = dest_comb(rand(concl th1)) in
434 DEZERO_RULE (TRANS th1 (AP_TERM tm1 (PADD tm2)))
436 let ord = morder l r in
437 if ord = 0 then MONOMIAL_ADD_CONV tm
438 else if ord > 0 then DEZERO_RULE(REFL tm)
439 else DEZERO_RULE(INST [l,a_tm; r,c_tm] pthm_27) in
442 (* ------------------------------------------------------------------------- *)
443 (* Multiplication of two polynomials. *)
444 (* ------------------------------------------------------------------------- *)
446 let POLYNOMIAL_MUL_CONV =
448 let l,r = dest_mul tm in
449 if not(is_add l) then POLYNOMIAL_MONOMIAL_MUL_CONV tm
450 else if not(is_add r) then
451 let th1 = INST [l,a_tm; r,b_tm] pthm_09 in
452 TRANS th1 (POLYNOMIAL_MONOMIAL_MUL_CONV(rand(concl th1)))
454 let a,b = dest_add l in
455 let th1 = INST [a,a_tm; b,b_tm; r,c_tm] pthm_10 in
456 let tm1,tm2 = dest_comb(rand(concl th1)) in
457 let tm3,tm4 = dest_comb tm1 in
458 let th2 = AP_TERM tm3 (POLYNOMIAL_MONOMIAL_MUL_CONV tm4) in
459 let th3 = TRANS th1 (MK_COMB(th2,PMUL tm2)) in
460 TRANS th3 (POLYNOMIAL_ADD_CONV (rand(concl th3))) in
462 let l,r = dest_mul tm in
463 if l = zero_tm then INST [r,a_tm] pthm_11
464 else if r = zero_tm then INST [l,a_tm] pthm_12
465 else if l = one_tm then INST [r,a_tm] pthm_13
466 else if r = one_tm then INST [l,a_tm] pthm_14
469 (* ------------------------------------------------------------------------- *)
470 (* Power of polynomial (optimized for the monomial and trivial cases). *)
471 (* ------------------------------------------------------------------------- *)
473 let POLYNOMIAL_POW_CONV =
475 let l,n = dest_pow tm in
476 if n = zeron_tm then INST [l,x_tm] pthm_35
477 else if n = onen_tm then INST [l,x_tm] pthm_36 else
478 let th1 = num_CONV n in
479 let th2 = INST [l,x_tm; rand(rand(concl th1)),q_tm] pthm_38 in
480 let tm1,tm2 = dest_comb(rand(concl th2)) in
481 let th3 = TRANS th2 (AP_TERM tm1 (PPOW tm2)) in
482 let th4 = TRANS (AP_TERM (rator tm) th1) th3 in
483 TRANS th4 (POLYNOMIAL_MUL_CONV (rand(concl th4))) in
485 if is_add(lhand tm) then PPOW tm else MONOMIAL_POW_CONV tm in
487 (* ------------------------------------------------------------------------- *)
489 (* ------------------------------------------------------------------------- *)
491 let POLYNOMIAL_NEG_CONV =
493 let l,r = dest_comb tm in
494 if l <> neg_tm then failwith "POLYNOMIAL_NEG_CONV" else
495 let th1 = INST [r,x_tm] nthm_1 in
496 TRANS th1 (POLYNOMIAL_MONOMIAL_MUL_CONV (rand(concl th1))) in
498 (* ------------------------------------------------------------------------- *)
500 (* ------------------------------------------------------------------------- *)
502 let POLYNOMIAL_SUB_CONV =
504 let l,r = dest_sub tm in
505 let th1 = INST [l,x_tm; r,y_tm] nthm_2 in
506 let tm1,tm2 = dest_comb(rand(concl th1)) in
507 let th2 = AP_TERM tm1 (POLYNOMIAL_MONOMIAL_MUL_CONV tm2) in
508 TRANS th1 (TRANS th2 (POLYNOMIAL_ADD_CONV (rand(concl th2)))) in
510 (* ------------------------------------------------------------------------- *)
511 (* Conversion from HOL term. *)
512 (* ------------------------------------------------------------------------- *)
514 let rec POLYNOMIAL_CONV tm =
515 if not(is_comb tm) or is_semiring_constant tm then REFL tm else
516 let lop,r = dest_comb tm in
518 let th1 = AP_TERM lop (POLYNOMIAL_CONV r) in
519 TRANS th1 (POLYNOMIAL_NEG_CONV (rand(concl th1)))
520 else if not(is_comb lop) then REFL tm else
521 let op,l = dest_comb lop in
522 if op = pow_tm & is_numeral r then
523 let th1 = AP_THM (AP_TERM op (POLYNOMIAL_CONV l)) r in
524 TRANS th1 (POLYNOMIAL_POW_CONV (rand(concl th1)))
526 if op = add_tm or op = mul_tm or op = sub_tm then
527 let th1 = MK_COMB(AP_TERM op (POLYNOMIAL_CONV l),
528 POLYNOMIAL_CONV r) in
529 let fn = if op = add_tm then POLYNOMIAL_ADD_CONV
530 else if op = mul_tm then POLYNOMIAL_MUL_CONV
531 else POLYNOMIAL_SUB_CONV in
532 TRANS th1 (fn (rand(concl th1)))
534 POLYNOMIAL_NEG_CONV,POLYNOMIAL_ADD_CONV,POLYNOMIAL_SUB_CONV,
535 POLYNOMIAL_MUL_CONV,POLYNOMIAL_POW_CONV,POLYNOMIAL_CONV;;
537 (* ------------------------------------------------------------------------- *)
538 (* Instantiate it to the natural numbers. *)
539 (* ------------------------------------------------------------------------- *)
541 let NUM_NORMALIZE_CONV =
543 (`(!x y z. x + (y + z) = (x + y) + z) /\
544 (!x y. x + y = y + x) /\
546 (!x y z. x * (y * z) = (x * y) * z) /\
547 (!x y. x * y = y * x) /\
550 (!x y z. x * (y + z) = x * y + x * z) /\
552 (!x n. x EXP (SUC n) = x * x EXP n)`,
553 REWRITE_TAC[EXP; MULT_CLAUSES; ADD_CLAUSES; LEFT_ADD_DISTRIB] THEN
554 REWRITE_TAC[ADD_AC; MULT_AC])
556 and is_semiring_constant = is_numeral
557 and SEMIRING_ADD_CONV = NUM_ADD_CONV
558 and SEMIRING_MUL_CONV = NUM_MULT_CONV
559 and SEMIRING_POW_CONV = NUM_EXP_CONV in
560 let _,_,_,_,_,NUM_NORMALIZE_CONV =
561 SEMIRING_NORMALIZERS_CONV sth rth
562 (is_semiring_constant,
563 SEMIRING_ADD_CONV,SEMIRING_MUL_CONV,SEMIRING_POW_CONV)