normalizer.ml

   1 (* ========================================================================= *)
   2 (* Relatively efficient HOL conversions for canonical polynomial form.       *)
   3 (*                                                                           *)
   4 (*              (c) Copyright, John Harrison 1998-2007                       *)
   5 (* ========================================================================= *)
   6
   7 needs "calc_num.ml";;
   8
   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) /\
  13      (!x. add r0 x = x) /\
  14      (!x y z. mul x (mul y z) = mul (mul x y) z) /\
  15      (!x y. mul x y = mul y x) /\
  16      (!x. mul r1 x = x) /\
  17      (!x. mul r0 x = r0) /\
  18      (!x y z. mul x (add y z) = add (mul x y) (mul x z)) /\
  19      (!x. pwr x 0 = r1) /\
  20      (!x n. pwr x (SUC n) = mul x (pwr x n))
  21      ==> (mul r1 x = x) /\
  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) /\
  26          (mul r0 m = r0) /\
  27          (add r0 a = a) /\
  28          (add a r0 = a) /\
  29          (mul a b = mul b a) /\
  30          (mul (add a b) c = add (mul a c) (mul b c)) /\
  31          (mul r0 a = r0) /\
  32          (mul a r0 = r0) /\
  33          (mul r1 a = a) /\
  34          (mul a r1 = a) /\
  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)) /\
  55          (pwr x 0 = r1) /\
  56          (pwr x 1 = x) /\
  57          (mul x (add y z) = add (mul x y) (mul x z)) /\
  58          (pwr x (SUC q) = mul x (pwr x q))`,
  59     STRIP_TAC THEN
  60     SUBGOAL_THEN
  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)) /\
  64       (!x. add x r0 = x) /\
  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)) /\
  69       (!x. mul x r1 = x) /\
  70       (!x. mul x r0 = r0)`
  71     MP_TAC THENL
  72      [ASM_MESON_TAC[];
  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
  78       STRIP_TAC] 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)`
  81     ASSUME_TAC THENL
  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)`
  84     ASSUME_TAC THENL
  85      [GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[];
  86       ALL_TAC] THEN
  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,
  92                SEMIRING_ADD_CONV,
  93                SEMIRING_MUL_CONV,
  94                SEMIRING_POW_CONV) ->
  95     let
  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
 108
 109     let p_tm = `p:num`
 110     and q_tm = `q:num`
 111     and zeron_tm = `0`
 112     and onen_tm = `1`
 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
 125
 126     let dest_add = dest_binop add_tm
 127     and dest_mul = dest_binop mul_tm
 128     and dest_pow 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
 133
 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
 137       else
 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
 145
 146     fun variable_order ->
 147
 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 (* ------------------------------------------------------------------------- *)
 153
 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))
 163           with Failure _ ->
 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))
 167       with Failure _ ->
 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))
 172           with Failure _ ->
 173               INST [l,x_tm] pthm_32 in
 174
 175 (* ------------------------------------------------------------------------- *)
 176 (* Remove "1 * m" from a monomial, and just leave m.                         *)
 177 (* ------------------------------------------------------------------------- *)
 178
 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
 183
 184 (* ------------------------------------------------------------------------- *)
 185 (* Conversion for "(monomial)^n", where n is a numeral.                      *)
 186 (* ------------------------------------------------------------------------- *)
 187
 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))
 206         else REFL tm in
 207       fun tm ->
 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
 214
 215 (* ------------------------------------------------------------------------- *)
 216 (* Multiplication of canonical monomials.                                    *)
 217 (* ------------------------------------------------------------------------- *)
 218
 219     let MONOMIAL_MUL_CONV =
 220       let powvar tm =
 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
 226       let vorder x y =
 227         if x = y then 0
 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
 237                 if ord = 0 then
 238                   let th1 = INST
 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)
 248                 else
 249                   let th0 = if ord < 0 then pthm_16 else pthm_17 in
 250                   let th1 = INST
 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))
 255             with Failure _ ->
 256                 let vr = powvar r in
 257                 let ord = vorder vl vr in
 258                 if ord = 0 then
 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
 263                   TRANS th1 th2
 264                 else if ord < 0 then
 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
 270         with Failure _ ->
 271             let vl = powvar l in
 272             try let rx,ry = dest_mul r in
 273                 let vr = powvar rx in
 274                 let ord = vorder vl vr in
 275                 if ord = 0 then
 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)
 280                 else if ord > 0 then
 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))
 285                 else REFL tm
 286             with Failure _ ->
 287                 let vr = powvar r in
 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
 291                 else REFL tm in
 292       fun tm -> let l,r = dest_mul tm in MONOMIAL_DEONE(MONOMIAL_MUL tm l r) in
 293
 294 (* ------------------------------------------------------------------------- *)
 295 (* Multiplication by monomial of a polynomial.                               *)
 296 (* ------------------------------------------------------------------------- *)
 297
 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),
 306                               PMM_CONV tm2) in
 307             TRANS th1 th2
 308         with Failure _ -> MONOMIAL_MUL_CONV tm in
 309       PMM_CONV in
 310
 311 (* ------------------------------------------------------------------------- *)
 312 (* Addition of two monomials identical except for constant multiples.        *)
 313 (* ------------------------------------------------------------------------- *)
 314
 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
 319       let th1 =
 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
 323           else
 324             INST [lhand l,a_tm; r,m_tm] pthm_03
 325         else
 326           if is_mul r & is_semiring_constant(lhand r) then
 327             INST [lhand r,a_tm; l,m_tm] pthm_04
 328           else
 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
 337
 338 (* ------------------------------------------------------------------------- *)
 339 (* Ordering on monomials.                                                    *)
 340 (* ------------------------------------------------------------------------- *)
 341
 342     let powervars tm =
 343       let ptms = striplist dest_mul tm in
 344       if is_semiring_constant (hd ptms) then tl ptms else ptms in
 345
 346     let dest_varpow tm =
 347       try let x,n = dest_pow tm in (x,dest_numeral n)
 348       with Failure _ ->
 349        (tm,(if is_semiring_constant tm then num_0 else num_1)) in
 350
 351     let morder =
 352       let rec lexorder l1 l2 =
 353         match (l1,l2) with
 354           [],[] -> 0
 355         | vps,[] -> -1
 356         | [],vps -> 1
 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
 363       fun tm1 tm2 ->
 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
 370
 371 (* ------------------------------------------------------------------------- *)
 372 (* Addition of two polynomials.                                              *)
 373 (* ------------------------------------------------------------------------- *)
 374
 375     let POLYNOMIAL_ADD_CONV =
 376       let DEZERO_RULE th =
 377         let tm = rand(concl th) in
 378         if not(is_add tm) then th else
 379         let lop,r = dest_comb tm in
 380         let l = rand lop 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)
 383         else th in
 384       let rec PADD tm =
 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
 388         if is_add l then
 389           let a,b = dest_add l in
 390           if is_add r then
 391             let c,d = dest_add r in
 392             let ord = morder a c in
 393             if ord = 0 then
 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)))
 399             else
 400               let th1 =
 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)))
 405           else
 406             let ord = morder a r in
 407             if ord = 0 then
 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)
 413             else if ord > 0 then
 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)))
 417             else
 418               DEZERO_RULE (INST [l,a_tm; r,c_tm] pthm_27)
 419         else
 420           if is_add r then
 421             let c,d = dest_add r in
 422             let ord = morder l c in
 423             if ord = 0 then
 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)
 429             else if ord > 0 then
 430               REFL tm
 431             else
 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)))
 435           else
 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
 440       PADD in
 441
 442 (* ------------------------------------------------------------------------- *)
 443 (* Multiplication of two polynomials.                                        *)
 444 (* ------------------------------------------------------------------------- *)
 445
 446     let POLYNOMIAL_MUL_CONV =
 447       let rec PMUL tm =
 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)))
 453         else
 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
 461       fun tm ->
 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
 467         else PMUL tm in
 468
 469 (* ------------------------------------------------------------------------- *)
 470 (* Power of polynomial (optimized for the monomial and trivial cases).       *)
 471 (* ------------------------------------------------------------------------- *)
 472
 473     let POLYNOMIAL_POW_CONV =
 474       let rec PPOW tm =
 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
 484       fun tm ->
 485         if is_add(lhand tm) then PPOW tm else MONOMIAL_POW_CONV tm in
 486
 487 (* ------------------------------------------------------------------------- *)
 488 (* Negation.                                                                 *)
 489 (* ------------------------------------------------------------------------- *)
 490
 491     let POLYNOMIAL_NEG_CONV =
 492       fun tm ->
 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
 497
 498 (* ------------------------------------------------------------------------- *)
 499 (* Subtraction.                                                              *)
 500 (* ------------------------------------------------------------------------- *)
 501
 502     let POLYNOMIAL_SUB_CONV =
 503       fun tm ->
 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
 509
 510 (* ------------------------------------------------------------------------- *)
 511 (* Conversion from HOL term.                                                 *)
 512 (* ------------------------------------------------------------------------- *)
 513
 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
 517       if lop = neg_tm then
 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)))
 525          else
 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)))
 533            else REFL tm in
 534     POLYNOMIAL_NEG_CONV,POLYNOMIAL_ADD_CONV,POLYNOMIAL_SUB_CONV,
 535     POLYNOMIAL_MUL_CONV,POLYNOMIAL_POW_CONV,POLYNOMIAL_CONV;;
 536
 537 (* ------------------------------------------------------------------------- *)
 538 (* Instantiate it to the natural numbers.                                    *)
 539 (* ------------------------------------------------------------------------- *)
 540
 541 let NUM_NORMALIZE_CONV =
 542   let sth = prove
 543    (`(!x y z. x + (y + z) = (x + y) + z) /\
 544      (!x y. x + y = y + x) /\
 545      (!x. 0 + x = x) /\
 546      (!x y z. x * (y * z) = (x * y) * z) /\
 547      (!x y. x * y = y * x) /\
 548      (!x. 1 * x = x) /\
 549      (!x. 0 * x = 0) /\
 550      (!x y z. x * (y + z) = x * y + x * z) /\
 551      (!x. x EXP 0 = 1) /\
 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])
 555   and rth = TRUTH
 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)
 564      (<) in
 565   NUM_NORMALIZE_CONV;;