2 (* ---------------------------------------------------------------------- *)
4 (* ---------------------------------------------------------------------- *)
6 let PDIVIDES vars sgns p q =
7 let s_thm = FINDSIGN vars sgns (head vars q) in
8 let op,l1,r1 = get_binop (concl s_thm) in
9 if op = req then failwith "PDIVIDES : head coefficient is zero" else
10 let div_thm = PDIVIDE vars p q in
11 let asx,pqr = dest_eq (concl div_thm) in
12 let pq,r = dest_plus pqr in
13 let p',q' = dest_mult pq in
14 let ak,s = dest_mult asx in
15 let a,k = dest_pow ak in
16 let k' = dest_small_numeral k in
17 if op = rgt or even k' then
19 else if odd k' & op = rlt then
20 let par_thm = PARITY_CONV k in
21 let mp_thm = MATCH_MPL[neg_odd_lem;div_thm;par_thm] in
22 let mp_thm1 = (CONV_RULE (LAND_CONV (LAND_CONV (LAND_CONV POLY_NEG_CONV)))) mp_thm in
23 let mp_thm2 = (CONV_RULE (RAND_CONV (LAND_CONV (LAND_CONV (POLY_NEG_CONV))))) mp_thm1 in
24 let mp_thm3 = (CONV_RULE (RAND_CONV (RAND_CONV POLY_NEG_CONV))) mp_thm2 in
25 let ret = (snd o dest_plus o rhs o concl) mp_thm3 in
27 else if odd k' & op = rneq then
28 let par_thm = PARITY_CONV k in
29 let mp_thm = MATCH_MPL[mul_odd_lem;div_thm;par_thm] in
30 let mp_thm1 = (CONV_RULE (LAND_CONV (LAND_CONV (LAND_CONV (POLYNATE_CONV vars))))) mp_thm in
31 let mp_thm2 = (CONV_RULE (RAND_CONV (LAND_CONV (POLYNATE_CONV vars)))) mp_thm1 in
32 let mp_thm3 = (CONV_RULE (RAND_CONV (RAND_CONV (POLY_MUL_CONV vars)))) mp_thm2 in
33 let ret = (snd o dest_plus o rhs o concl) mp_thm3 in
35 else failwith "PDIVIDES: 1";;
37 (* ---------------------------------------------------------------------- *)
39 (* ---------------------------------------------------------------------- *)
41 let PDIVIDES vars sgns mat_thm div_thms =
42 let start_time = Sys.time() in
43 let res = PDIVIDES vars sgns mat_thm div_thms in
44 pdivides_timer +.= (Sys.time() -. start_time);
54 let vars = [`x:real`;`y:real`];;
55 let sgns = [ARITH_RULE `&1 > &0`;ASSUME `&0 + y * &1 < &0`];;
56 let q = rhs(concl (POLYNATE_CONV vars `x * y`));;
57 let p = rhs(concl (POLYNATE_CONV vars `&1 + y * x * x + x * x * x * &5 * y`));;
59 PDIVIDES vars sgns p q;;
61 let vars = [`x:real`;`y:real`];;
62 let sgns = [ARITH_RULE `&1 > &0`;ASSUME `&0 + y * &1 > &0`];;
63 let q = rhs(concl (POLYNATE_CONV vars `x * x * y`));;
64 let p = rhs(concl (POLYNATE_CONV vars `&1 + x * x + x * x * x * y`));;
66 PDIVIDES vars sgns p q;;
69 let vars = [`x:real`;`y:real`];;
70 let sgns = [ARITH_RULE `&1 > &0`;ASSUME `&0 + y * &1 < &0`];;
71 let q = rhs(concl (POLYNATE_CONV vars `x * x * y`));;
72 let p = rhs(concl (POLYNATE_CONV vars `&1 + x * x + x * x * x * y`));;
74 PDIVIDES vars sgns p q;;
76 let vars = [`x:real`;`y:real`];;
77 let sgns = [ASSUME `&0 + y * &1 < &0`];;
78 let q = rhs(concl (POLYNATE_CONV vars `-- x:real`));;
79 let p = rhs(concl (POLYNATE_CONV vars `x * x * y`));;
81 PDIVIDES vars sgns p q
83 let vars = [`x:real`;`y:real`];;
84 let sgns = [ARITH_RULE `&1 > &0`;ASSUME `&0 + y * &1 <> &0`];;
85 let q = rhs(concl (POLYNATE_CONV vars `x * x * y`));;
86 let p = rhs(concl (POLYNATE_CONV vars `&1 + x * x + x * x * x * y`));;
88 PDIVIDES vars sgns p q;;