swh:1:snp:b5e574652797da1d8f8957c7aca1dc4d6520b70d
Tip revision: b27a524086caf73530b7c2c5da1b237d3539f143 authored by Jacques Carette on 24 August 2020, 14:18:07 UTC
Merge pull request #35 from sjjs7/final-changes
Merge pull request #35 from sjjs7/final-changes
Tip revision: b27a524
normalizer.ml
(* ========================================================================= *)
(* Relatively efficient HOL conversions for canonical polynomial form. *)
(* *)
(* (c) Copyright, John Harrison 1998-2007 *)
(* ========================================================================= *)
needs "calc_num.ml";;
let SEMIRING_NORMALIZERS_CONV =
let SEMIRING_PTHS = prove
(`(!x:A y z. add x (add y z) = add (add x y) z) /\
(!x y. add x y = add y x) /\
(!x. add r0 x = x) /\
(!x y z. mul x (mul y z) = mul (mul x y) z) /\
(!x y. mul x y = mul y x) /\
(!x. mul r1 x = x) /\
(!x. mul r0 x = r0) /\
(!x y z. mul x (add y z) = add (mul x y) (mul x z)) /\
(!x. pwr x 0 = r1) /\
(!x n. pwr x (SUC n) = mul x (pwr x n))
==> (mul r1 x = x) /\
(add (mul a m) (mul b m) = mul (add a b) m) /\
(add (mul a m) m = mul (add a r1) m) /\
(add m (mul a m) = mul (add a r1) m) /\
(add m m = mul (add r1 r1) m) /\
(mul r0 m = r0) /\
(add r0 a = a) /\
(add a r0 = a) /\
(mul a b = mul b a) /\
(mul (add a b) c = add (mul a c) (mul b c)) /\
(mul r0 a = r0) /\
(mul a r0 = r0) /\
(mul r1 a = a) /\
(mul a r1 = a) /\
(mul (mul lx ly) (mul rx ry) = mul (mul lx rx) (mul ly ry)) /\
(mul (mul lx ly) (mul rx ry) = mul lx (mul ly (mul rx ry))) /\
(mul (mul lx ly) (mul rx ry) = mul rx (mul (mul lx ly) ry)) /\
(mul (mul lx ly) rx = mul (mul lx rx) ly) /\
(mul (mul lx ly) rx = mul lx (mul ly rx)) /\
(mul lx rx = mul rx lx) /\
(mul lx (mul rx ry) = mul (mul lx rx) ry) /\
(mul lx (mul rx ry) = mul rx (mul lx ry)) /\
(add (add a b) (add c d) = add (add a c) (add b d)) /\
(add (add a b) c = add a (add b c)) /\
(add a (add c d) = add c (add a d)) /\
(add (add a b) c = add (add a c) b) /\
(add a c = add c a) /\
(add a (add c d) = add (add a c) d) /\
(mul (pwr x p) (pwr x q) = pwr x (p + q)) /\
(mul x (pwr x q) = pwr x (SUC q)) /\
(mul (pwr x q) x = pwr x (SUC q)) /\
(mul x x = pwr x 2) /\
(pwr (mul x y) q = mul (pwr x q) (pwr y q)) /\
(pwr (pwr x p) q = pwr x (p * q)) /\
(pwr x 0 = r1) /\
(pwr x 1 = x) /\
(mul x (add y z) = add (mul x y) (mul x z)) /\
(pwr x (SUC q) = mul x (pwr x q))`,
STRIP_TAC THEN
SUBGOAL_THEN
`(!m:A n. add m n = add n m) /\
(!m n p. add (add m n) p = add m (add n p)) /\
(!m n p. add m (add n p) = add n (add m p)) /\
(!x. add x r0 = x) /\
(!m n. mul m n = mul n m) /\
(!m n p. mul (mul m n) p = mul m (mul n p)) /\
(!m n p. mul m (mul n p) = mul n (mul m p)) /\
(!m n p. mul (add m n) p = add (mul m p) (mul n p)) /\
(!x. mul x r1 = x) /\
(!x. mul x r0 = r0)`
MP_TAC THENL
[ASM_MESON_TAC[];
MAP_EVERY (fun t -> UNDISCH_THEN t (K ALL_TAC))
[`!x:A y z. add x (add y z) = add (add x y) z`;
`!x:A y. add x y :A = add y x`;
`!x:A y z. mul x (mul y z) = mul (mul x y) z`;
`!x:A y. mul x y :A = mul y x`] THEN
STRIP_TAC] THEN
ASM_REWRITE_TAC[num_CONV `2`; num_CONV `1`] THEN
SUBGOAL_THEN `!m n:num x:A. pwr x (m + n) :A = mul (pwr x m) (pwr x n)`
ASSUME_TAC THENL
[GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES]; ALL_TAC] THEN
SUBGOAL_THEN `!x:A y:A n:num. pwr (mul x y) n = mul (pwr x n) (pwr y n)`
ASSUME_TAC THENL
[GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[];
ALL_TAC] THEN
SUBGOAL_THEN `!x:A m:num n. pwr (pwr x m) n = pwr x (m * n)`
(fun th -> ASM_MESON_TAC[th]) THEN
GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[MULT_CLAUSES])
and true_tm = concl TRUTH in
fun sth rth (is_semiring_constant,
SEMIRING_ADD_CONV,
SEMIRING_MUL_CONV,
SEMIRING_POW_CONV) ->
let
[pthm_01; pthm_02; pthm_03; pthm_04; pthm_05; pthm_06; pthm_07; pthm_08;
pthm_09; pthm_10; pthm_11; pthm_12; pthm_13; pthm_14; pthm_15; pthm_16;
pthm_17; pthm_18; pthm_19; pthm_20; pthm_21; pthm_22; pthm_23; pthm_24;
pthm_25; pthm_26; pthm_27; pthm_28; pthm_29; pthm_30; pthm_31; pthm_32;
pthm_33; pthm_34; pthm_35; pthm_36; pthm_37; pthm_38] =
CONJUNCTS(MATCH_MP SEMIRING_PTHS sth) in
let add_tm = rator(rator(lhand(concl pthm_07)))
and mul_tm = rator(rator(lhand(concl pthm_13)))
and pow_tm = rator(rator(rand(concl pthm_32)))
and zero_tm = rand(concl pthm_06)
and one_tm = rand(lhand(concl pthm_14))
and ty = type_of(rand(concl pthm_01)) in
let p_tm = `p:num`
and q_tm = `q:num`
and zeron_tm = `0`
and onen_tm = `1`
and a_tm = mk_var("a",ty)
and b_tm = mk_var("b",ty)
and c_tm = mk_var("c",ty)
and d_tm = mk_var("d",ty)
and lx_tm = mk_var("lx",ty)
and ly_tm = mk_var("ly",ty)
and m_tm = mk_var("m",ty)
and rx_tm = mk_var("rx",ty)
and ry_tm = mk_var("ry",ty)
and x_tm = mk_var("x",ty)
and y_tm = mk_var("y",ty)
and z_tm = mk_var("z",ty) in
let dest_add = dest_binop add_tm
and dest_mul = dest_binop mul_tm
and dest_pow tm =
let l,r = dest_binop pow_tm tm in
if is_numeral r then l,r else failwith "dest_pow"
and is_add = is_binop add_tm
and is_mul = is_binop mul_tm in
let nthm_1,nthm_2,sub_tm,neg_tm,dest_sub,is_sub =
if concl rth = true_tm then rth,rth,true_tm,true_tm,
(fun t -> t,t),K false
else
let nthm_1 = SPEC x_tm (CONJUNCT1 rth)
and nthm_2 = SPECL [x_tm; y_tm] (CONJUNCT2 rth) in
let sub_tm = rator(rator(lhand(concl nthm_2)))
and neg_tm = rator(lhand(concl nthm_1)) in
let dest_sub = dest_binop sub_tm
and is_sub = is_binop sub_tm in
(nthm_1,nthm_2,sub_tm,neg_tm,dest_sub,is_sub) in
fun variable_order ->
(* ------------------------------------------------------------------------- *)
(* Conversion for "x^n * x^m", with either x^n = x and/or x^m = x possible. *)
(* Also deals with "const * const", but both terms must involve powers of *)
(* the same variable, or both be constants, or behaviour may be incorrect. *)
(* ------------------------------------------------------------------------- *)
let POWVAR_MUL_CONV tm =
let l,r = dest_mul tm in
if is_semiring_constant l && is_semiring_constant r
then SEMIRING_MUL_CONV tm else
try let lx,ln = dest_pow l in
try let rx,rn = dest_pow r in
let th1 = INST [lx,x_tm; ln,p_tm; rn,q_tm] pthm_29 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
TRANS th1 (AP_TERM tm1 (NUM_ADD_CONV tm2))
with Failure _ ->
let th1 = INST [lx,x_tm; ln,q_tm] pthm_31 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
TRANS th1 (AP_TERM tm1 (NUM_SUC_CONV tm2))
with Failure _ ->
try let rx,rn = dest_pow r in
let th1 = INST [rx,x_tm; rn,q_tm] pthm_30 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
TRANS th1 (AP_TERM tm1 (NUM_SUC_CONV tm2))
with Failure _ ->
INST [l,x_tm] pthm_32 in
(* ------------------------------------------------------------------------- *)
(* Remove "1 * m" from a monomial, and just leave m. *)
(* ------------------------------------------------------------------------- *)
let MONOMIAL_DEONE th =
try let l,r = dest_mul(rand(concl th)) in
if l = one_tm then TRANS th (INST [r,x_tm] pthm_01) else th
with Failure _ -> th in
(* ------------------------------------------------------------------------- *)
(* Conversion for "(monomial)^n", where n is a numeral. *)
(* ------------------------------------------------------------------------- *)
let MONOMIAL_POW_CONV =
let rec MONOMIAL_POW tm bod ntm =
if not(is_comb bod) then REFL tm
else if is_semiring_constant bod then SEMIRING_POW_CONV tm else
let lop,r = dest_comb bod in
if not(is_comb lop) then REFL tm else
let op,l = dest_comb lop in
if op = pow_tm && is_numeral r then
let th1 = INST [l,x_tm; r,p_tm; ntm,q_tm] pthm_34 in
let l,r = dest_comb(rand(concl th1)) in
TRANS th1 (AP_TERM l (NUM_MULT_CONV r))
else if op = mul_tm then
let th1 = INST [l,x_tm; r,y_tm; ntm,q_tm] pthm_33 in
let xy,z = dest_comb(rand(concl th1)) in
let x,y = dest_comb xy in
let thl = MONOMIAL_POW y l ntm
and thr = MONOMIAL_POW z r ntm in
TRANS th1 (MK_COMB(AP_TERM x thl,thr))
else REFL tm in
fun tm ->
let lop,r = dest_comb tm in
let op,l = dest_comb lop in
if op <> pow_tm || not(is_numeral r) then failwith "MONOMIAL_POW_CONV"
else if r = zeron_tm then INST [l,x_tm] pthm_35
else if r = onen_tm then INST [l,x_tm] pthm_36
else MONOMIAL_DEONE(MONOMIAL_POW tm l r) in
(* ------------------------------------------------------------------------- *)
(* Multiplication of canonical monomials. *)
(* ------------------------------------------------------------------------- *)
let MONOMIAL_MUL_CONV =
let powvar tm =
if is_semiring_constant tm then one_tm else
try let lop,r = dest_comb tm in
let op,l = dest_comb lop in
if op = pow_tm && is_numeral r then l else failwith ""
with Failure _ -> tm in
let vorder x y =
if x = y then 0
else if x = one_tm then -1
else if y = one_tm then 1
else if variable_order x y then -1 else 1 in
let rec MONOMIAL_MUL tm l r =
try let lx,ly = dest_mul l in
let vl = powvar lx in
try let rx,ry = dest_mul r in
let vr = powvar rx in
let ord = vorder vl vr in
if ord = 0 then
let th1 = INST
[lx,lx_tm; ly,ly_tm; rx,rx_tm; ry,ry_tm] pthm_15 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2 in
let th3 = TRANS th1 th2 in
let tm5,tm6 = dest_comb(rand(concl th3)) in
let tm7,tm8 = dest_comb tm6 in
let th4 = MONOMIAL_MUL tm6 (rand tm7) tm8 in
TRANS th3 (AP_TERM tm5 th4)
else
let th0 = if ord < 0 then pthm_16 else pthm_17 in
let th1 = INST
[lx,lx_tm; ly,ly_tm; rx,rx_tm; ry,ry_tm] th0 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm2 in
TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 (rand tm3) tm4))
with Failure _ ->
let vr = powvar r in
let ord = vorder vl vr in
if ord = 0 then
let th1 = INST [lx,lx_tm; ly,ly_tm; r,rx_tm] pthm_18 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2 in
TRANS th1 th2
else if ord < 0 then
let th1 = INST [lx,lx_tm; ly,ly_tm; r,rx_tm] pthm_19 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm2 in
TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 (rand tm3) tm4))
else INST [l,lx_tm; r,rx_tm] pthm_20
with Failure _ ->
let vl = powvar l in
try let rx,ry = dest_mul r in
let vr = powvar rx in
let ord = vorder vl vr in
if ord = 0 then
let th1 = INST [l,lx_tm; rx,rx_tm; ry,ry_tm] pthm_21 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
TRANS th1 (AP_THM (AP_TERM tm3 (POWVAR_MUL_CONV tm4)) tm2)
else if ord > 0 then
let th1 = INST [l,lx_tm; rx,rx_tm; ry,ry_tm] pthm_22 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm2 in
TRANS th1 (AP_TERM tm1 (MONOMIAL_MUL tm2 (rand tm3) tm4))
else REFL tm
with Failure _ ->
let vr = powvar r in
let ord = vorder vl vr in
if ord = 0 then POWVAR_MUL_CONV tm
else if ord > 0 then INST [l,lx_tm; r,rx_tm] pthm_20
else REFL tm in
fun tm -> let l,r = dest_mul tm in MONOMIAL_DEONE(MONOMIAL_MUL tm l r) in
(* ------------------------------------------------------------------------- *)
(* Multiplication by monomial of a polynomial. *)
(* ------------------------------------------------------------------------- *)
let POLYNOMIAL_MONOMIAL_MUL_CONV =
let rec PMM_CONV tm =
let l,r = dest_mul tm in
try let y,z = dest_add r in
let th1 = INST [l,x_tm; y,y_tm; z,z_tm] pthm_37 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = MK_COMB(AP_TERM tm3 (MONOMIAL_MUL_CONV tm4),
PMM_CONV tm2) in
TRANS th1 th2
with Failure _ -> MONOMIAL_MUL_CONV tm in
PMM_CONV in
(* ------------------------------------------------------------------------- *)
(* Addition of two monomials identical except for constant multiples. *)
(* ------------------------------------------------------------------------- *)
let MONOMIAL_ADD_CONV tm =
let l,r = dest_add tm in
if is_semiring_constant l && is_semiring_constant r
then SEMIRING_ADD_CONV tm else
let th1 =
if is_mul l && is_semiring_constant(lhand l) then
if is_mul r && is_semiring_constant(lhand r) then
INST [lhand l,a_tm; lhand r,b_tm; rand r,m_tm] pthm_02
else
INST [lhand l,a_tm; r,m_tm] pthm_03
else
if is_mul r && is_semiring_constant(lhand r) then
INST [lhand r,a_tm; l,m_tm] pthm_04
else
INST [r,m_tm] pthm_05 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_TERM tm3 (SEMIRING_ADD_CONV tm4) in
let th3 = TRANS th1 (AP_THM th2 tm2) in
let tm5 = rand(concl th3) in
if lhand tm5 = zero_tm then TRANS th3 (INST [rand tm5,m_tm] pthm_06)
else MONOMIAL_DEONE th3 in
(* ------------------------------------------------------------------------- *)
(* Ordering on monomials. *)
(* ------------------------------------------------------------------------- *)
let powervars tm =
let ptms = striplist dest_mul tm in
if is_semiring_constant (hd ptms) then tl ptms else ptms in
let dest_varpow tm =
try let x,n = dest_pow tm in (x,dest_numeral n)
with Failure _ ->
(tm,(if is_semiring_constant tm then num_0 else num_1)) in
let morder =
let rec lexorder l1 l2 =
match (l1,l2) with
[],[] -> 0
| vps,[] -> -1
| [],vps -> 1
| ((x1,n1)::vs1),((x2,n2)::vs2) ->
if variable_order x1 x2 then 1
else if variable_order x2 x1 then -1
else if n1 </ n2 then -1
else if n2 </ n1 then 1
else lexorder vs1 vs2 in
fun tm1 tm2 ->
let vdegs1 = map dest_varpow (powervars tm1)
and vdegs2 = map dest_varpow (powervars tm2) in
let deg1 = itlist ((+/) o snd) vdegs1 num_0
and deg2 = itlist ((+/) o snd) vdegs2 num_0 in
if deg1 </ deg2 then -1 else if deg1 >/ deg2 then 1
else lexorder vdegs1 vdegs2 in
(* ------------------------------------------------------------------------- *)
(* Addition of two polynomials. *)
(* ------------------------------------------------------------------------- *)
let POLYNOMIAL_ADD_CONV =
let DEZERO_RULE th =
let tm = rand(concl th) in
if not(is_add tm) then th else
let lop,r = dest_comb tm in
let l = rand lop in
if l = zero_tm then TRANS th (INST [r,a_tm] pthm_07)
else if r = zero_tm then TRANS th (INST [l,a_tm] pthm_08)
else th in
let rec PADD tm =
let l,r = dest_add tm in
if l = zero_tm then INST [r,a_tm] pthm_07
else if r = zero_tm then INST [l,a_tm] pthm_08 else
if is_add l then
let a,b = dest_add l in
if is_add r then
let c,d = dest_add r in
let ord = morder a c in
if ord = 0 then
let th1 = INST [a,a_tm; b,b_tm; c,c_tm; d,d_tm] pthm_23 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_TERM tm3 (MONOMIAL_ADD_CONV tm4) in
DEZERO_RULE (TRANS th1 (MK_COMB(th2,PADD tm2)))
else
let th1 =
if ord > 0 then INST [a,a_tm; b,b_tm; r,c_tm] pthm_24
else INST [l,a_tm; c,c_tm; d,d_tm] pthm_25 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
DEZERO_RULE (TRANS th1 (AP_TERM tm1 (PADD tm2)))
else
let ord = morder a r in
if ord = 0 then
let th1 = INST [a,a_tm; b,b_tm; r,c_tm] pthm_26 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_THM (AP_TERM tm3 (MONOMIAL_ADD_CONV tm4)) tm2 in
DEZERO_RULE (TRANS th1 th2)
else if ord > 0 then
let th1 = INST [a,a_tm; b,b_tm; r,c_tm] pthm_24 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
DEZERO_RULE (TRANS th1 (AP_TERM tm1 (PADD tm2)))
else
DEZERO_RULE (INST [l,a_tm; r,c_tm] pthm_27)
else
if is_add r then
let c,d = dest_add r in
let ord = morder l c in
if ord = 0 then
let th1 = INST [l,a_tm; c,c_tm; d,d_tm] pthm_28 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_THM (AP_TERM tm3 (MONOMIAL_ADD_CONV tm4)) tm2 in
DEZERO_RULE (TRANS th1 th2)
else if ord > 0 then
REFL tm
else
let th1 = INST [l,a_tm; c,c_tm; d,d_tm] pthm_25 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
DEZERO_RULE (TRANS th1 (AP_TERM tm1 (PADD tm2)))
else
let ord = morder l r in
if ord = 0 then MONOMIAL_ADD_CONV tm
else if ord > 0 then DEZERO_RULE(REFL tm)
else DEZERO_RULE(INST [l,a_tm; r,c_tm] pthm_27) in
PADD in
(* ------------------------------------------------------------------------- *)
(* Multiplication of two polynomials. *)
(* ------------------------------------------------------------------------- *)
let POLYNOMIAL_MUL_CONV =
let rec PMUL tm =
let l,r = dest_mul tm in
if not(is_add l) then POLYNOMIAL_MONOMIAL_MUL_CONV tm
else if not(is_add r) then
let th1 = INST [l,a_tm; r,b_tm] pthm_09 in
TRANS th1 (POLYNOMIAL_MONOMIAL_MUL_CONV(rand(concl th1)))
else
let a,b = dest_add l in
let th1 = INST [a,a_tm; b,b_tm; r,c_tm] pthm_10 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let tm3,tm4 = dest_comb tm1 in
let th2 = AP_TERM tm3 (POLYNOMIAL_MONOMIAL_MUL_CONV tm4) in
let th3 = TRANS th1 (MK_COMB(th2,PMUL tm2)) in
TRANS th3 (POLYNOMIAL_ADD_CONV (rand(concl th3))) in
fun tm ->
let l,r = dest_mul tm in
if l = zero_tm then INST [r,a_tm] pthm_11
else if r = zero_tm then INST [l,a_tm] pthm_12
else if l = one_tm then INST [r,a_tm] pthm_13
else if r = one_tm then INST [l,a_tm] pthm_14
else PMUL tm in
(* ------------------------------------------------------------------------- *)
(* Power of polynomial (optimized for the monomial and trivial cases). *)
(* ------------------------------------------------------------------------- *)
let POLYNOMIAL_POW_CONV =
let rec PPOW tm =
let l,n = dest_pow tm in
if n = zeron_tm then INST [l,x_tm] pthm_35
else if n = onen_tm then INST [l,x_tm] pthm_36 else
let th1 = num_CONV n in
let th2 = INST [l,x_tm; rand(rand(concl th1)),q_tm] pthm_38 in
let tm1,tm2 = dest_comb(rand(concl th2)) in
let th3 = TRANS th2 (AP_TERM tm1 (PPOW tm2)) in
let th4 = TRANS (AP_TERM (rator tm) th1) th3 in
TRANS th4 (POLYNOMIAL_MUL_CONV (rand(concl th4))) in
fun tm ->
if is_add(lhand tm) then PPOW tm else MONOMIAL_POW_CONV tm in
(* ------------------------------------------------------------------------- *)
(* Negation. *)
(* ------------------------------------------------------------------------- *)
let POLYNOMIAL_NEG_CONV =
fun tm ->
let l,r = dest_comb tm in
if l <> neg_tm then failwith "POLYNOMIAL_NEG_CONV" else
let th1 = INST [r,x_tm] nthm_1 in
TRANS th1 (POLYNOMIAL_MONOMIAL_MUL_CONV (rand(concl th1))) in
(* ------------------------------------------------------------------------- *)
(* Subtraction. *)
(* ------------------------------------------------------------------------- *)
let POLYNOMIAL_SUB_CONV =
fun tm ->
let l,r = dest_sub tm in
let th1 = INST [l,x_tm; r,y_tm] nthm_2 in
let tm1,tm2 = dest_comb(rand(concl th1)) in
let th2 = AP_TERM tm1 (POLYNOMIAL_MONOMIAL_MUL_CONV tm2) in
TRANS th1 (TRANS th2 (POLYNOMIAL_ADD_CONV (rand(concl th2)))) in
(* ------------------------------------------------------------------------- *)
(* Conversion from HOL term. *)
(* ------------------------------------------------------------------------- *)
let rec POLYNOMIAL_CONV tm =
if not(is_comb tm) || is_semiring_constant tm then REFL tm else
let lop,r = dest_comb tm in
if lop = neg_tm then
let th1 = AP_TERM lop (POLYNOMIAL_CONV r) in
TRANS th1 (POLYNOMIAL_NEG_CONV (rand(concl th1)))
else if not(is_comb lop) then REFL tm else
let op,l = dest_comb lop in
if op = pow_tm && is_numeral r then
let th1 = AP_THM (AP_TERM op (POLYNOMIAL_CONV l)) r in
TRANS th1 (POLYNOMIAL_POW_CONV (rand(concl th1)))
else
if op = add_tm || op = mul_tm || op = sub_tm then
let th1 = MK_COMB(AP_TERM op (POLYNOMIAL_CONV l),
POLYNOMIAL_CONV r) in
let fn = if op = add_tm then POLYNOMIAL_ADD_CONV
else if op = mul_tm then POLYNOMIAL_MUL_CONV
else POLYNOMIAL_SUB_CONV in
TRANS th1 (fn (rand(concl th1)))
else REFL tm in
POLYNOMIAL_NEG_CONV,POLYNOMIAL_ADD_CONV,POLYNOMIAL_SUB_CONV,
POLYNOMIAL_MUL_CONV,POLYNOMIAL_POW_CONV,POLYNOMIAL_CONV;;
(* ------------------------------------------------------------------------- *)
(* Instantiate it to the natural numbers. *)
(* ------------------------------------------------------------------------- *)
let NUM_NORMALIZE_CONV =
let sth = prove
(`(!x y z. x + (y + z) = (x + y) + z) /\
(!x y. x + y = y + x) /\
(!x. 0 + x = x) /\
(!x y z. x * (y * z) = (x * y) * z) /\
(!x y. x * y = y * x) /\
(!x. 1 * x = x) /\
(!x. 0 * x = 0) /\
(!x y z. x * (y + z) = x * y + x * z) /\
(!x. x EXP 0 = 1) /\
(!x n. x EXP (SUC n) = x * x EXP n)`,
REWRITE_TAC[EXP; MULT_CLAUSES; ADD_CLAUSES; LEFT_ADD_DISTRIB] THEN
REWRITE_TAC[ADD_AC; MULT_AC])
and rth = TRUTH
and is_semiring_constant = is_numeral
and SEMIRING_ADD_CONV = NUM_ADD_CONV
and SEMIRING_MUL_CONV = NUM_MULT_CONV
and SEMIRING_POW_CONV = NUM_EXP_CONV in
let _,_,_,_,_,NUM_NORMALIZE_CONV =
SEMIRING_NORMALIZERS_CONV sth rth
(is_semiring_constant,
SEMIRING_ADD_CONV,SEMIRING_MUL_CONV,SEMIRING_POW_CONV)
(<) in
NUM_NORMALIZE_CONV;;