Rqe/pdivides.ml

   1
   2 (* ---------------------------------------------------------------------- *)
   3 (*  PDIVIDES                                                              *)
   4 (* ---------------------------------------------------------------------- *)
   5
   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
  18       r,div_thm
  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
  26       ret,mp_thm3
  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
  34       ret,mp_thm3
  35   else failwith "PDIVIDES: 1";;
  36
  37 (* ---------------------------------------------------------------------- *)
  38 (*  Timing                                                                *)
  39 (* ---------------------------------------------------------------------- *)
  40
  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);
  45     res;;
  46
  47
  48
  49 (*
  50 PDIVIDES vars sgns p
  51 let q = (ith 2 qs)
  52
  53
  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`));;
  58 PDIVIDE vars p q;;
  59 PDIVIDES vars sgns p q;;
  60
  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`));;
  65 PDIVIDE vars p q;;
  66 PDIVIDES vars sgns p q;;
  67
  68
  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`));;
  73 PDIVIDE vars p q;;
  74 PDIVIDES vars sgns p q;;
  75
  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`));;
  80 PDIVIDE vars p q;;
  81 PDIVIDES vars sgns p q
  82
  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`));;
  87 PDIVIDE vars p q;;
  88 PDIVIDES vars sgns p q;;
  89
  90 *)