Rqe/dedmatrix.ml

   1 (* ====================================================================== *)
   2 (*  DEDMATRIX                                                             *)
   3 (* ====================================================================== *)
   4
   5 (* ------------------------------------------------------------------------- *)
   6 (* Deduce matrix for p,p1,...,pn from matrix for p',p1,...,pn,q0,...,qn      *)
   7 (* where qi = rem(p,pi) with p0 = p'                                         *)
   8 (* ------------------------------------------------------------------------- *)
   9
  10 let prove_nonconstant =
  11   let nonconstant_tm = `nonconstant` in
  12     fun pdiff_thm normal_thm ->
  13       let thm = ONCE_REWRITE_RULE[GSYM pdiff_thm] normal_thm in
  14       let ret = REWRITE_RULE[GSYM NORMAL_PDIFF] thm in
  15       let f,_ = strip_comb (concl ret) in
  16         if not (f = nonconstant_tm) then failwith "prove_nonconstant" else ret;;
  17
  18 let REMOVE_COLUMN1 mat_thm =
  19   let mat_thm1 = MATCH_MP REMOVE_COL1 mat_thm in
  20     REWRITE_RULE[MAP;HD;TL] mat_thm1;;
  21
  22 let APPENDIZE l n =
  23   let lty = type_of l in
  24   let ty = hd(snd(dest_type lty)) in
  25   let app_tm = mk_const("APPEND",[ty,aty]) in
  26   let l1,l2 = chop_list n (dest_list l) in
  27   let app = mk_comb(mk_comb(app_tm,mk_list(l1,ty)),mk_list(l2,ty)) in
  28     GSYM (REWRITE_CONV[APPEND] app);;
  29
  30 let REMOVE_INFINITIES thm =
  31   let thm' = MATCH_MP INTERPMAT_TRIO thm in
  32   let pts,_,sgns = dest_interpmat (concl thm') in
  33   let p_thm = APPENDIZE pts (length (dest_list pts) - 2) in
  34   let pts',_,sgns = dest_interpmat (concl thm') in
  35   let s_thm = APPENDIZE sgns (length (dest_list sgns) - 5) in
  36   let thm'' = MATCH_MP INTERPMAT_TRIO_TL (ONCE_REWRITE_RULE[p_thm;s_thm] thm') in
  37     REWRITE_RULE[APPEND] thm'';;
  38
  39 let get_dirs =
  40   let pos = `Pos` in
  41   let neg = `Neg` in
  42   fun lb_deriv ub_deriv ->
  43     if lb_deriv = pos && ub_deriv = pos then INFIN_POS_POS
  44     else if lb_deriv = pos && ub_deriv = neg then INFIN_POS_NEG
  45     else if lb_deriv = neg && ub_deriv = pos then INFIN_NEG_POS
  46     else if lb_deriv = neg && ub_deriv = neg then INFIN_NEG_NEG
  47     else failwith "get_dirs: bad signs";;
  48
  49 let get_sing_dirs =
  50   let pos = `Pos` in
  51   let neg = `Neg` in
  52   fun lb_deriv ub_deriv ->
  53     if lb_deriv = pos && ub_deriv = pos then INFIN_SING_POS_POS
  54     else if lb_deriv = pos && ub_deriv = neg then INFIN_SING_POS_NEG
  55     else if lb_deriv = neg && ub_deriv = pos then INFIN_SING_NEG_POS
  56     else if lb_deriv = neg && ub_deriv = neg then INFIN_SING_NEG_NEG
  57     else failwith "get_dirs: bad signs";;
  58
  59
  60 let aitvars,aitdiff,aitnorm,aitmat = ref [],ref TRUTH,ref TRUTH,ref TRUTH;;
  61 (*
  62 let vars,diff_thm,normal_thm,mat_thm = !aitvars,!aitdiff,!tnorm,!tmat
  63 let vars,diff_thm,normal_thm,mat_thm = vars, pdiff_thm, normal_thm, mat_thm''
  64 *)
  65 let ADD_INFINITIES =
  66   let real_app = `APPEND:real list -> real list -> real list` in
  67   let sign_app = `APPEND:(sign list) list -> (sign list) list -> (sign list) list` in
  68   let imat = `interpmat` in
  69   let pos = `Pos` in
  70   let neg = `Neg` in
  71   let sl_ty = `:sign list` in
  72   let real_ty = `:real` in
  73   fun vars diff_thm normal_thm mat_thm ->
  74     aitvars := vars;
  75     aitdiff := diff_thm;
  76     aitnorm := normal_thm;
  77     aitmat := mat_thm;
  78     let nc_thm = prove_nonconstant diff_thm normal_thm in
  79     let pts,pols,sgns = dest_interpmat (concl mat_thm) in
  80     let polsl = dest_list pols in
  81     let p::p'::_ = polsl in
  82     let p_thm = ABS (hd vars) (POLY_ENLIST_CONV vars (snd(dest_abs p))) in
  83     let p'_thm = ONCE_REWRITE_RULE[GSYM diff_thm] (ABS (hd vars) (POLY_ENLIST_CONV vars (snd(dest_abs p')))) in
  84     let pols_thm = REWRITE_CONV[p_thm;p'_thm] pols in
  85     let sgnsl = dest_list sgns in
  86     let sgns_len = length sgnsl in
  87     let thm1 =
  88       if sgns_len = 1 then
  89         let sgn = (hd(tl(dest_list (hd sgnsl)))) in
  90         let mp_thm =
  91           if sgn = pos then INFIN_NIL_POS
  92           else if sgn = neg then INFIN_NIL_NEG
  93           else failwith "bad sign in mat" in
  94         let mat_thm1 = MK_COMB(MK_COMB(AP_TERM imat (REFL pts), pols_thm),REFL sgns) in
  95         let mat_thm2 = EQ_MP mat_thm1 mat_thm in
  96           MATCH_MP (MATCH_MP mp_thm mat_thm2) nc_thm
  97       else if sgns_len = 3 then
  98         let lb_deriv = hd (tl (dest_list (hd sgnsl))) in
  99         let ub_deriv = hd (tl (dest_list (last sgnsl))) in
 100         let mp_thm = get_sing_dirs lb_deriv ub_deriv in
 101         let mat_thm1 = MK_COMB(MK_COMB(AP_TERM imat (REFL pts), pols_thm),REFL sgns) in
 102         let mat_thm2 = EQ_MP mat_thm1 mat_thm in
 103           MATCH_MP (MATCH_MP mp_thm mat_thm2) nc_thm
 104       else
 105         let s1,s2 = chop_list (sgns_len - 3) sgnsl in
 106         let s3 = mk_list(s1,sl_ty) in
 107         let s4 = mk_comb(mk_comb(sign_app,s3),mk_list(s2,sl_ty)) in
 108         let sgns_thm = prove(mk_eq(sgns,s4),REWRITE_TAC[APPEND]) in
 109         let mat_thm1 = MK_COMB(MK_COMB(AP_TERM imat (REFL pts), pols_thm),sgns_thm) in
 110         let mat_thm2 = EQ_MP mat_thm1 mat_thm in
 111         let lb_deriv = hd (tl (dest_list (hd sgnsl))) in
 112         let ub_deriv = hd (tl (dest_list (last sgnsl))) in
 113         let mp_thm = get_dirs lb_deriv ub_deriv in
 114           MATCH_MP (MATCH_MP mp_thm mat_thm2) nc_thm in
 115     let thm2 = REWRITE_RULE[APPEND;GSYM pols_thm] thm1 in
 116     let c = concl thm2 in
 117     let x,bod = dest_exists c in
 118     let x' = new_var real_ty in
 119     let bod1 = subst [x',x] bod in
 120     let assume_thm1 = ASSUME bod1 in
 121     let x2,bod2 = dest_exists bod1 in
 122     let x'' = new_var real_ty in
 123     let assume_thm2 = ASSUME (subst [x'',x2] bod2) in
 124       assume_thm2,(x',thm2),(x'',assume_thm1);;
 125
 126
 127 (*
 128 print_timers()
 129 print_times()
 130 reset_timers()
 131 *)
 132
 133
 134 let tvars,tsgns,tdivs,tdiff,tnorm,tcont,tmat,tex = ref [],ref [],ref [], ref TRUTH,ref TRUTH, ref (fun x y -> x), ref TRUTH,  ref [];;
 135 (*
 136 let vars,sgns,div_thms,pdiff_thm,normal_thm,cont,mat_thm,ex_thms = !tvars,!tsgns,!tdivs,!tdiff,!tnorm,!tcont,!tmat,!tex
 137 DEDMATRIX vars sgns div_thms pdiff_thm normal_thm cont mat_thm ex_thms
 138 *)
 139
 140 let DEDMATRIX vars sgns div_thms pdiff_thm normal_thm cont mat_thm ex_thms =
 141   try
 142     tvars := vars;
 143     tsgns := sgns;
 144     tdivs := div_thms;
 145     tdiff := pdiff_thm;
 146     tnorm := normal_thm;
 147     tmat := mat_thm;
 148     tex := ex_thms;
 149     tcont := cont;
 150     let start_time = Sys.time() in
 151     let pts,pols,signll = dest_interpmat (concl mat_thm) in
 152     let mat_thm' = INFERPSIGN vars sgns mat_thm div_thms in
 153     let mat_thm'' = CONDENSE mat_thm' in
 154     let mat_thm''',(v1,exthm1),(v2,exthm2) = ADD_INFINITIES vars pdiff_thm normal_thm mat_thm'' in
 155     let mat_thm4,new_ex_pairs = INFERISIGN vars pdiff_thm mat_thm''' ((v1,exthm1)::(v2,exthm2)::ex_thms) in
 156     let mat_thm5 = REMOVE_INFINITIES mat_thm4 in
 157     let mat_thm6 = REMOVE_COLUMN1 mat_thm5 in
 158     let mat_thm7 = CONDENSE mat_thm6 in
 159     (* hack for changing renamed vars *)
 160     let mat_thm8 = CONV_RULE (RATOR_CONV (RAND_CONV (LIST_CONV (ALPHA_CONV (hd vars))))) mat_thm7 in
 161     let ex_pairs = [(v1,exthm1);(v2,exthm2)] @ new_ex_pairs in
 162     let cont' mat_thm ex_thms = cont mat_thm (ex_thms @ ex_pairs) in
 163       cont' mat_thm8 ex_thms
 164   with (Isign (false_thm,ex_thms)) ->
 165     raise (Isign (false_thm,ex_thms))
 166   | Failure x -> failwith ("DEDMATRIX: " ^ x);;
 167
 168 (* {{{ Examples *)
 169
 170 (*
 171
 172
 173 let NOT_NIL_CONV tm =
 174   let h,t = dest_cons tm in
 175     ISPECL [h;t] NOT_CONS_NIL;;
 176
 177 let NORMAL_CONV tm =
 178   let normalize_thm = POLY_NORMALIZE_CONV (mk_comb (`normalize`,tm)) in
 179   let nonnil_thm = NOT_NIL_CONV tm in
 180   let conj_thm = CONJ normalize_thm nonnil_thm in
 181     REWRITE_RULE[GSYM normal] conj_thm;;
 182
 183 let vars = [`x:real`];;
 184 let cont a b = a;;
 185 let sgns = [ARITH_RULE `&1 > &0`];;
 186 let normal_thm = NORMAL_CONV `[&1; &2; &3]`;;
 187 let pdiff_thm = POLY_DIFF_CONV `poly_diff [&1; &1; &1; &1]`;;
 188 let ex_thms = [];;
 189 let _,l1 = PDIVIDES vars sgns `(&1 + x * (&1 + x * (&1 + x * &1)))` `(&1 + x * (&2 + x * &3))`;;
 190 let _,l2 = PDIVIDES vars sgns `(&1 + x * (&1 + x * (&1 + x * &1)))` `(&2 + x * (-- &3 + x * &1))`;;
 191 let _,l3 = PDIVIDES vars sgns `(&1 + x * (&1 + x * (&1 + x * &1)))` `(-- &4 + x * (&0 + x * &1))`;;
 192 let div_thms = [l1;l2;l3];;
 193
 194 let mat_thm = ASSUME
 195   `interpmat [x1; x2; x3; x4; x5]
 196      [\x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1);
 197       \x. &8 + x * &4; \x. -- &7 + x * &11; \x. &5 + x * &5]
 198       [[Pos; Pos; Pos; Neg; Neg; Neg];
 199       [Pos; Pos; Zero; Zero; Neg; Neg];
 200       [Pos; Pos; Neg; Pos; Neg; Neg];
 201       [Pos; Zero; Neg; Pos; Neg; Zero];
 202       [Pos; Pos; Neg; Pos; Neg; Pos];
 203       [Pos; Pos; Zero; Pos; Zero; Pos];
 204       [Pos; Pos; Neg; Pos; Pos; Pos];
 205       [Pos; Zero; Neg; Pos; Zero; Pos];
 206       [Pos; Neg; Neg; Pos; Pos; Pos];
 207       [Pos; Zero; Zero; Pos; Pos; Pos];
 208       [Pos; Pos; Pos; Pos; Pos; Pos]]` ;;
 209
 210 time (DEDMATRIX vars sgns div_thms pdiff_thm normal_thm (fun x y -> x) mat_thm) []
 211
 212
 213 *)
 214
 215 (* }}} *)
 216
 217
 218 (* ---------------------------------------------------------------------- *)
 219 (*  Timing                                                                *)
 220 (* ---------------------------------------------------------------------- *)
 221
 222 let REMOVE_COLUMN1 mat_thm =
 223   let start_time = Sys.time() in
 224   let res = REMOVE_COLUMN1 mat_thm in
 225     remove_column1_timer +.= (Sys.time() -. start_time);
 226     res;;
 227
 228 let ADD_INFINITIES vars pdiff_thm normal_thm mat_thm =
 229   let start_time = Sys.time() in
 230   let res = ADD_INFINITIES vars pdiff_thm normal_thm mat_thm in
 231     add_infinities_timer +.= (Sys.time() -. start_time);
 232     res;;
 233
 234 let REMOVE_INFINITIES thm =
 235   let start_time = Sys.time() in
 236   let res = REMOVE_INFINITIES thm in
 237     remove_infinities_timer +.= (Sys.time() -. start_time);
 238     res;;