Rqe/rqe_main.ml

   1 let TRAPOUT cont mat_thm ex_thms fm =
   2   try
   3     cont mat_thm ex_thms
   4   with Isign (false_thm,ex_thms) ->
   5     let ftm = mk_eq(fm,f_tm) in
   6     let fthm = CONTR ftm false_thm in
   7     let ex_thms' = sort (fun x y -> xterm_lt (fst y) (fst x)) ex_thms in
   8     let fthm' = rev_itlist CHOOSE ex_thms' fthm in
   9       fthm';;
  10
  11 let get_repeats l =
  12   let rec get_repeats l seen ind =
  13     match l with
  14         [] -> []
  15       | h::t ->
  16           if mem h seen then ind::get_repeats t seen (ind + 1)
  17           else get_repeats t (h::seen) (ind + 1) in
  18     get_repeats l [] 0;;
  19
  20 let subtract_index l =
  21   let rec subtract_index l ind =
  22     match l with
  23         [] -> []
  24       | h::t -> (h - ind):: (subtract_index t (ind + 1)) in
  25     subtract_index l 0;;
  26
  27 (*
  28 subtract_index (get_repeats [1; 2; 1; 2 ; 3])
  29 *)
  30
  31 let remove_column n isigns_thm =
  32   let thms = interpsigns_thms2 isigns_thm in
  33   let l,r = chop_list n thms in
  34   let thms' = l @ tl r in
  35     mk_interpsigns thms';;
  36
  37 let REMOVE_COLUMN n mat_thm =
  38   let rol_thm,all_thm = interpmat_thms mat_thm in
  39   let ints,part,signs = dest_all2 (concl all_thm) in
  40   let part_thm = PARTITION_LINE_CONV (snd (dest_comb part)) in
  41   let isigns_thms = CONJUNCTS (REWRITE_RULE[ALL2;part_thm] all_thm) in
  42   let isigns_thms' = map (remove_column n) isigns_thms in
  43   let all_thm' = mk_all2_interpsigns part_thm isigns_thms' in
  44   let all_thm'' = REWRITE_RULE[GSYM part_thm] all_thm' in
  45   let mat_thm' = mk_interpmat_thm rol_thm all_thm'' in
  46     mat_thm';;
  47
  48 let SETIFY_CONV mat_thm =
  49   let _,pols,_ = dest_interpmat(concl mat_thm) in
  50   let pols' = dest_list pols in
  51   let sols = setify (dest_list pols) in
  52   let indices = map (fun p -> try index p sols with _ -> failwith "SETIFY: no index") pols' in
  53   let subtract_cols = subtract_index (get_repeats indices) in
  54     rev_itlist REMOVE_COLUMN subtract_cols mat_thm;;
  55
  56
  57 (*
  58 SETIFY_CONV
  59 (ASSUME `interpmat [] [(\x. x + &1); (\x. x + &1); (\x. x + &2); (\x. x + &3); (\x. x + &1); (\x. x + &2)][[Pos; Pos; Pos; Pos; Neg; Zero]]`)
  60
  61 *)
  62 (*
  63 let duplicate_column i j isigns_thm =
  64   let thms = interpsigns_thms2 isigns_thm in
  65   let col = ith i thms in
  66   let l,r = chop_list j thms in
  67   let thms' = l @ (col :: r) in
  68     mk_interpsigns thms';;
  69
  70 let DUPLICATE_COLUMN i j mat_thm =
  71   let rol_thm,all_thm = interpmat_thms mat_thm in
  72   let ints,part,signs = dest_all2 (concl all_thm) in
  73   let part_thm = PARTITION_LINE_CONV (snd (dest_comb part)) in
  74   let isigns_thms = CONJUNCTS (REWRITE_RULE[ALL2;part_thm] all_thm) in
  75   let isigns_thms' = map (duplicate_column i j) isigns_thms in
  76   let all_thm' = mk_all2_interpsigns part_thm isigns_thms' in
  77   let all_thm'' = REWRITE_RULE[GSYM part_thm] all_thm' in
  78   let mat_thm' = mk_interpmat_thm rol_thm all_thm'' in
  79     mat_thm';;
  80 *)
  81
  82 let duplicate_columns new_cols isigns_thm =
  83   let thms = interpsigns_thms2 isigns_thm in
  84   let thms' = map (fun i -> el i thms) new_cols in
  85     mk_interpsigns thms';;
  86
  87 let DUPLICATE_COLUMNS mat_thm ls =
  88   if ls = [] then if mat_thm = empty_mat then empty_mat else failwith "empty duplication list" else
  89   let rol_thm,all_thm = interpmat_thms mat_thm in
  90   let ints,part,signs = dest_all2 (concl all_thm) in
  91   let part_thm = PARTITION_LINE_CONV (snd (dest_comb part)) in
  92   let isigns_thms = CONJUNCTS (REWRITE_RULE[ALL2;part_thm] all_thm) in
  93   let isigns_thms' = map (duplicate_columns ls) isigns_thms in
  94   let all_thm' = mk_all2_interpsigns part_thm isigns_thms' in
  95   let all_thm'' = REWRITE_RULE[GSYM part_thm] all_thm' in
  96   let mat_thm' = mk_interpmat_thm rol_thm all_thm'' in
  97     mat_thm';;
  98
  99
 100 let DUPLICATE_COLUMNS mat_thm ls =
 101   let start_time = Sys.time() in
 102   let res = DUPLICATE_COLUMNS mat_thm ls in
 103     duplicate_columns_timer +.= (Sys.time() -. start_time);
 104     res;;
 105
 106
 107 let UNMONICIZE_ISIGN vars monic_thm isign_thm =
 108   let _,_,sign = dest_interpsign isign_thm in
 109   let const = (fst o dest_mult o lhs o concl) monic_thm in
 110   let const_thm = SIGN_CONST const in
 111   let op,_,_ = get_binop (concl const_thm) in
 112   let mp_thm =
 113     if op = rgt then
 114       if sign = spos_tm then gtpos
 115       else if sign = sneg_tm then gtneg
 116       else if sign = szero_tm then gtzero
 117       else failwith "bad sign"
 118     else if op = rlt then
 119       if sign = spos_tm then ltpos
 120       else if sign = sneg_tm then ltneg
 121       else if sign = szero_tm then ltzero
 122       else failwith "bad sign"
 123     else (failwith "bad op") in
 124   let monic_thm' = GEN (hd vars) monic_thm in
 125     MATCH_MPL[mp_thm;monic_thm';const_thm;isign_thm];;
 126
 127 let UNMONICIZE_ISIGNS vars monic_thms isigns_thm =
 128   let isign_thms = interpsigns_thms2 isigns_thm in
 129   let isign_thms' = map2 (UNMONICIZE_ISIGN vars) monic_thms isign_thms in
 130     mk_interpsigns isign_thms';;
 131
 132 let UNMONICIZE_MAT vars monic_thms mat_thm =
 133   if monic_thms = [] then mat_thm else
 134   let rol_thm,all_thm = interpmat_thms mat_thm in
 135   let ints,part,signs = dest_all2 (concl all_thm) in
 136   let part_thm = PARTITION_LINE_CONV (snd (dest_comb part)) in
 137   let consts = map (fst o dest_mult o lhs o concl) monic_thms in
 138   let isigns_thms = CONJUNCTS (REWRITE_RULE[ALL2;part_thm] all_thm) in
 139   let isigns_thms' = map (UNMONICIZE_ISIGNS vars monic_thms) isigns_thms in
 140   let all_thm' = mk_all2_interpsigns part_thm isigns_thms' in
 141   let all_thm'' = REWRITE_RULE[GSYM part_thm] all_thm' in
 142   let mat_thm' = mk_interpmat_thm rol_thm all_thm'' in
 143     mat_thm';;
 144
 145 let UNMONICIZE_MAT vars monic_thms mat_thm =
 146   let start_time = Sys.time() in
 147   let res = UNMONICIZE_MAT vars monic_thms mat_thm in
 148     unmonicize_mat_timer +.= (Sys.time() -. start_time);
 149     res;;
 150
 151
 152 (* {{{ Examples *)
 153
 154 (*
 155 let vars,monic_thms,mat_thm =
 156  [], [], empty_mat
 157
 158
 159 let monic_thm = hd monic_thms
 160 length isigns_thms
 161
 162 MONIC_CONV [rx] `&1 + x * (&1 + x * (&1 + x * &7))`
 163
 164 let isign_thm = hd isign_thms
 165
 166 let isigns_thm = hd isigns_thms
 167
 168     mk_interpsigns [TRUTH];;
 169 let ls = [0;1;2;0;1;2]
 170  let mat_thm,ls = empty_mat,[]
 171 1,3,
 172
 173 DUPLICATE_COLUMNS
 174 (ASSUME `interpmat [] [(\x. x + &1); (\x. x + &1); (\x. x + &2); (\x. x + &3); (\x. x + &1); (\x. x + &2)][[Pos; Pos; Pos; Pos; Neg; Zero]]`)
 175 [5]
 176
 177 duplicate_columns [] (ASSUME `interpsigns [] (\x. T) []`)
 178 let new_cols, isigns_thm = [],(ASSUME `interpsigns [] (\x. T) []`)
 179
 180 let isigns_thm = hd isigns_thms
 181
 182 *)
 183
 184 (* }}} *)
 185
 186
 187 let SWAP_HEAD_COL_ROW i isigns_thm =
 188   let s_thms = interpsigns_thms2 isigns_thm in
 189   let s_thms' = insertat i (hd s_thms) (tl s_thms) in
 190     mk_interpsigns s_thms';;
 191
 192 let SWAP_HEAD_COL i mat_thm =
 193   let rol_thm,all_thm = interpmat_thms mat_thm in
 194   let ints,part,signs = dest_all2 (concl all_thm) in
 195   let part_thm = PARTITION_LINE_CONV (snd (dest_comb part)) in
 196   let isigns_thms = CONJUNCTS (REWRITE_RULE[ALL2;part_thm] all_thm) in
 197   let isigns_thms' = map (SWAP_HEAD_COL_ROW i) isigns_thms in
 198   let all_thm' = mk_all2_interpsigns part_thm isigns_thms' in
 199     mk_interpmat_thm rol_thm all_thm';;
 200
 201 let SWAP_HEAD_COL i mat_thm =
 202   let start_time = Sys.time() in
 203   let res = SWAP_HEAD_COL i mat_thm in
 204     swap_head_col_timer +.= (Sys.time() -. start_time);
 205     res;;
 206
 207
 208 let LENGTH_CONV =
 209   let alength_tm = `LENGTH:(A list) -> num` in
 210   fun tm ->
 211     try
 212       let ty = type_of tm in
 213       let lty,[cty] = dest_type ty in
 214         if lty <> "list" then failwith "LENGTH_CONV: not a list" else
 215         let ltm = mk_comb(inst[cty,aty] alength_tm,tm) in
 216         let lthm = REWRITE_CONV[LENGTH] ltm in
 217           MATCH_MP main_lem000 lthm
 218     with _ -> failwith "LENGTH_CONV";;
 219
 220 let LAST_NZ_CONV =
 221   let alast_tm = `LAST:(A list) -> A` in
 222   fun nz_thm tm ->
 223     try
 224       let ty = type_of tm in
 225       let lty,[cty] = dest_type ty in
 226       if lty <> "list" then failwith "LAST_NZ_CONV: not a list" else
 227         let ltm = mk_comb(inst[cty,aty] alast_tm,tm) in
 228         let lthm = REWRITE_CONV[LAST;NOT_CONS_NIL] ltm in
 229           MATCH_MPL[main_lem001;nz_thm;lthm]
 230     with _ -> failwith "LAST_NZ_CONV";;
 231
 232 let rec first f l =
 233   match l with
 234       [] -> failwith "first"
 235     | h::t -> if can f h then f h else first f t;;
 236
 237 let NEQ_RULE thm =
 238   let thms = CONJUNCTS main_lem002 in
 239     first (C MATCH_MP thm) thms;;
 240
 241 (*
 242 NEQ_CONV (ARITH_RULE `~(&11 <= &2)`)
 243 *)
 244
 245 let NORMAL_LIST_CONV nz_thm tm =
 246   let nz_thm' = NEQ_RULE nz_thm in
 247   let len_thm = LENGTH_CONV tm in
 248   let last_thm = LAST_NZ_CONV nz_thm' tm in
 249   let cthm = CONJ len_thm last_thm in
 250     MATCH_EQ_MP (GSYM (REWRITE_RULE[GSYM NEQ] NORMAL_ID)) cthm;;
 251
 252 (*
 253 |- poly_diff [&0; &0; &0 + a * &1] = [&0; &0 + a * &2]
 254 let tm = `poly_diff [&0; &0 + a * &1]`
 255 *)
 256 let pdiff_tm = `poly_diff`;;
 257 let GEN_POLY_DIFF_CONV vars tm =
 258   let thm1 = POLY_ENLIST_CONV vars tm in
 259   let l,x = dest_poly (rhs (concl thm1)) in
 260   let thm2 = CANON_POLY_DIFF_CONV (mk_comb(pdiff_tm,l)) in
 261   let thm3 = CONV_RULE (RAND_CONV (LIST_CONV (POLYNATE_CONV vars))) thm2 in
 262     thm3;;
 263
 264 (*
 265    if \x. p = \x. q, where \x. p is the leading polynomial
 266    replace p by q in mat_thm,
 267 *)
 268
 269
 270 (*
 271 let peq,mat_thm = !rppeq,!rpmat
 272 *)
 273 let rppeq,rpmat = ref TRUTH,ref TRUTH;;
 274 let REPLACE_POL =
 275   let imat_tm = `interpmat` in
 276   fun peq mat_thm ->
 277     rppeq := peq;
 278     rpmat := mat_thm;
 279     let pts,pols,sgnll = dest_interpmat (concl mat_thm) in
 280     let rep_p = lhs(concl peq) in
 281     let i = try index rep_p (dest_list pols) with _ -> failwith "REPLACE_POL: index" in
 282     let thm1 = EL_CONV (fun x -> GEN_REWRITE_CONV I [peq] x) i pols in
 283       end_itlist (C (curry MK_COMB)) (rev [REFL imat_tm;REFL pts;thm1;REFL sgnll]);;
 284
 285
 286 let REPLACE_POL peq mat_thm =
 287   let start_time = Sys.time() in
 288   let res = REPLACE_POL peq mat_thm in
 289     replace_pol_timer +.= (Sys.time() -. start_time);
 290     res;;
 291
 292 (* {{{ Examples *)
 293
 294 (*
 295
 296 let peq,mat_thm =
 297 ASSUME  `(\x. &0) =
 298         (\x. &0 + a * ((&0 + b * (&0 + b * -- &1)) + a * (&0 + c * &4)))`,
 299 ASSUME `interpmat [x_44] [\x. (&0 + b * &1) + x * (&0 + a * &2); \x. &0]
 300         [[Pos; Zero]; [Zero; Zero]; [Neg; Zero]]`
 301
 302 let peq = ASSUME `(\x. &1 + x * (&1 + x * (&1 + x * &1))) = (\x. &1 + x)`
 303
 304 REPLACE_POL peq mat_thm
 305
 306 is_constant [`y:real`] `&1 + x * -- &1`
 307
 308 let vars,pols,cont,sgns,ex_thms =
 309 [`c:real`; `b:real`; `a:real`],
 310 [`&0 + c * &1`],
 311 (fun x y -> x),
 312 [ASSUME `&0 + b * (&0 + b * -- &1) = &0`;
 313 ASSUME ` &0 + b * (&0 + b * (&0 + a * -- &1)) = &0`;
 314 ASSUME  `&0 + a * (&0 + a * &1) = &0`;ASSUME `&0 + b * &1 = &0`;
 315 ASSUME `&0 + a * &1 = &0`; ASSUME ` &1 > &0`],
 316 []
 317
 318 *)
 319
 320 (* }}} *)
 321
 322
 323
 324 (* ---------------------------------------------------------------------- *)
 325 (*  Factoring                                                             *)
 326 (* ---------------------------------------------------------------------- *)
 327
 328 let UNFACTOR_ISIGN vars xsign_thm pol isign_thm =
 329   let x = hd vars in
 330   let k,pol' = weakfactor x pol in
 331   if k = 0 then isign_thm else
 332   let fact_thm = GEN x (GSYM (WEAKFACTOR_CONV x pol)) in
 333   let par_thm = PARITY_CONV (mk_small_numeral k) in
 334   let _,_,xsign = dest_interpsign xsign_thm in
 335   let _,_,psign = dest_interpsign isign_thm in
 336   let parity,_ = dest_comb (concl par_thm) in
 337   if xsign = spos_tm then
 338     let mp_thm =
 339       if psign = spos_tm then factor_pos_pos
 340       else if psign = sneg_tm then factor_pos_neg
 341       else if psign = szero_tm then factor_pos_zero
 342       else failwith "bad sign" in
 343       let ret = BETA_RULE(MATCH_MPL[mp_thm;xsign_thm;isign_thm]) in
 344         MATCH_MP ret fact_thm
 345   else if xsign = szero_tm then
 346     let k_thm = prove(mk_neg(mk_eq(mk_small_numeral k,nzero)),ARITH_TAC) in
 347     let mp_thm =
 348       if psign = spos_tm then factor_zero_pos
 349       else if psign = sneg_tm then factor_zero_neg
 350       else if psign = szero_tm then factor_zero_zero
 351       else failwith "bad sign" in
 352       let ret = BETA_RULE(MATCH_MPL[mp_thm;xsign_thm;isign_thm;k_thm]) in
 353         MATCH_MP ret fact_thm
 354   else if xsign = sneg_tm & parity = even_tm then
 355     let k_thm = prove(mk_neg(mk_eq(mk_small_numeral k,nzero)),ARITH_TAC) in
 356     let mp_thm =
 357       if psign = spos_tm then factor_neg_even_pos
 358       else if psign = sneg_tm then factor_neg_even_neg
 359       else if psign = szero_tm then factor_neg_even_zero
 360       else failwith "bad sign" in
 361       let ret = BETA_RULE(MATCH_MPL[mp_thm;xsign_thm;isign_thm;par_thm;k_thm]) in
 362         MATCH_MP ret fact_thm
 363   else if xsign = sneg_tm & parity = odd_tm then
 364     let k_thm = prove(mk_neg(mk_eq(mk_small_numeral k,nzero)),ARITH_TAC) in
 365     let mp_thm =
 366       if psign = spos_tm then factor_neg_odd_pos
 367       else if psign = sneg_tm then factor_neg_odd_neg
 368       else if psign = szero_tm then factor_neg_odd_zero
 369       else failwith "bad sign" in
 370       let ret = BETA_RULE(MATCH_MPL[mp_thm;xsign_thm;isign_thm;par_thm;k_thm]) in
 371         MATCH_MP ret fact_thm
 372   else failwith "bad something...";;
 373
 374 (* {{{ Examples *)
 375
 376 (*
 377
 378 let vars,xsign_thm,pol,isign_thm =
 379 [ry;rx],
 380 `interpsign (\x. x < x1) (\x. x) Pos`,
 381 ASSUME `interpsign (\x. x < x_254) (\y. &0 + y * &1) Neg`
 382
 383 `\x. &0 + x * (&4 + x * &6)`,
 384 ASSUME `interpsign (\x. x < x1) (\x. &4 + x * &6) Pos`
 385
 386
 387 let xsign_thm,pol,isign_thm =
 388 ASSUME `interpsign (\x. x < x1) (\x. x) Pos`,
 389 `\x. &0 + x * (&4 + x * &6)`,
 390 ASSUME `interpsign (\x. x < x1) (\x. &4 + x * &6) Pos`
 391
 392
 393 *)
 394
 395 (* }}} *)
 396
 397 let UNFACTOR_ISIGNS vars pols isigns_thm =
 398   let isign_thms = interpsigns_thms2 isigns_thm in
 399   let isign_thms' = map2 (UNFACTOR_ISIGN vars (hd isign_thms)) pols (tl isign_thms) in
 400     mk_interpsigns isign_thms';;
 401
 402 let UNFACTOR_MAT vars pols mat_thm =
 403   let rol_thm,all_thm = interpmat_thms mat_thm in
 404   let ints,part,signs = dest_all2 (concl all_thm) in
 405   let part_thm = PARTITION_LINE_CONV (snd (dest_comb part)) in
 406   let isigns_thms = CONJUNCTS (REWRITE_RULE[ALL2;part_thm] all_thm) in
 407   let isigns_thms' = map (UNFACTOR_ISIGNS vars pols) isigns_thms in
 408   let all_thm' = mk_all2_interpsigns part_thm isigns_thms' in
 409   let all_thm'' = REWRITE_RULE[GSYM part_thm] all_thm' in
 410   let mat_thm' = mk_interpmat_thm rol_thm all_thm'' in
 411     mat_thm';;
 412
 413 let UNFACTOR_MAT vars pols mat_thm =
 414   let start_time = Sys.time() in
 415   let res = UNFACTOR_MAT vars pols mat_thm in
 416     unfactor_mat_timer +.= (Sys.time() -. start_time);
 417     res;;
 418
 419 (* {{{ Examples *)
 420
 421 (*
 422 #untrace UNFACTOR_ISIGN
 423
 424 let isigns_thm = el 0 isigns_thms
 425 UNFACTOR_ISIGNS pols isigns_thm
 426
 427 let isign_thm = el 1 isign_thm
 428
 429 pols
 430   let isigns_thms' = map (UNFACTOR_ISIGNS pols) isigns_thms in
 431
 432 let xsign_thm = hd isign_thms
 433 let xsign_thm = ASSUME `interpsign (\x. x < x1) (\x. x) Neg`
 434 let isign_thm = hd (tl isign_thms)
 435 let pol = hd pols
 436 let pol = `\x. &0 + x * (&0 + x * (&0 + x * (&0 + y * &1)))`
 437
 438 let isigns_thm = hd isigns_thms
 439 let vars = [rx;ry;rz]
 440
 441
 442 let pols =
 443   [`\x. &0 + x * (&0 + x * (&0 + y * &1))`; `\x. &0 + x * (&4 + x * &6)`; `\x. &3 + x * (&6 + x * &9)`;
 444       `\x. &0 + x * (&0 + x * (&0 + x * (&0 + z * &1)))`; `\x. -- &4 + x * (&0 + x * &1)`]
 445
 446 let mat_thm = ASSUME
 447   `interpmat [x1; x2; x3; x4; x5]
 448   [\x. x; \x. &0 + y * &1; \x. &4 + x * &6; \x. &3 + x * (&6 + x * &9);
 449       \x. &0 + z * &1; \x. -- &4 + x * (&0 + x * &1)]
 450       [[Pos; Pos; Pos; Neg; Neg; Neg];
 451       [Neg; Pos; Zero; Zero; Neg; Neg];
 452       [Neg; Pos; Neg; Pos; Neg; Neg];
 453       [Neg; Pos; Neg; Pos; Neg; Zero];
 454       [Neg; Pos; Neg; Pos; Neg; Pos];
 455       [Zero; Pos; Neg; Pos; Zero; Pos];
 456       [Pos; Pos; Neg; Pos; Pos; Pos];
 457       [Pos; Zero; Neg; Pos; Pos; Pos];
 458       [Pos; Neg; Neg; Pos; Pos; Pos];
 459       [Pos; Zero; Zero; Pos; Pos; Pos];
 460       [Pos; Pos; Pos; Pos; Pos; Pos]]`
 461
 462 UNFACTOR_MAT pols mat_thm
 463
 464 *)
 465
 466 (* }}} *)
 467
 468 let message_time s f x =
 469   report s;
 470   time f x;;
 471
 472
 473 (* ---------------------------------------------------------------------- *)
 474 (*  Matrix                                                                *)
 475 (* ---------------------------------------------------------------------- *)
 476
 477 let matrix_count,splitzero_count,splitsigns_count,monicize_count = ref 0,ref 0,ref 0,ref 0;;
 478 let reset_counts() = matrix_count := 0;splitzero_count := 0;splitsigns_count := 0;monicize_count := 0;;
 479 let print_counts() = !matrix_count,!splitzero_count,!splitsigns_count,!monicize_count;;
 480
 481
 482 (*
 483 let vars,dun,pols,cont,sgns,ex_thms,fm = !szvars,!szdun,!szpols,!szcont,!szsgns,!szex_thms,!szfm
 484 *)
 485
 486
 487 let rec MATRIX vars pols cont sgns ex_thms fm =
 488   incr matrix_count;
 489   if pols = [] then TRAPOUT cont empty_mat [] fm else
 490   if exists (is_constant vars) pols then
 491     let p = find (is_constant vars) pols in
 492     let i = try index p pols with _ -> failwith "MATRIX: no such pol" in
 493     let pols1,pols2 = chop_list i pols in
 494     let pols' = pols1 @ tl pols2 in
 495     let cont' = MATINSERT vars i (FINDSIGN vars sgns p) cont in
 496       MATRIX vars pols' cont' sgns ex_thms fm
 497   else
 498     let kqs = map (weakfactor (hd vars)) pols in
 499       if exists (fun (k,q) -> k <> 0 & not(is_constant vars q)) kqs then
 500         let pols' = poly_var(hd vars) :: map snd kqs in
 501         let ks = map fst kqs in
 502         let cont' mat_thm ex_thms = cont (UNFACTOR_MAT vars pols mat_thm) ex_thms in
 503           MATRIX vars pols' cont' sgns ex_thms fm
 504       else
 505       let d = itlist (max o degree_ vars) pols (-1) in
 506       let p = find (fun p -> degree_ vars p = d) pols in
 507       let pl_thm = POLY_ENLIST_CONV vars p in
 508       let pl = rhs(concl pl_thm) in
 509       let l,x = dest_poly pl in
 510       let pdiff_thm = GEN_POLY_DIFF_CONV vars p in
 511       let p'l = rhs (concl pdiff_thm) in
 512       let p' = mk_comb(mk_comb(poly_tm,p'l),hd vars) in
 513       let p'thm = (POLY_DELIST_CONV THENC (POLYNATE_CONV vars)) p' in
 514       let p'c = rhs (concl p'thm) in
 515       let hdp' = last (dest_list p'l) in
 516       let sign_thm = FINDSIGN vars sgns hdp' in
 517       let normal_thm = NORMAL_LIST_CONV sign_thm p'l in
 518       let i = try index p pols with _ -> failwith "MATRIX: no such pol1" in
 519       let qs = let p1,p2 = chop_list i pols in p'c::p1 @ tl p2 in
 520       let gs,div_thms = unzip (map (PDIVIDES vars sgns p) qs) in
 521       let cont' mat_thm = cont (SWAP_HEAD_COL i mat_thm) in
 522       let dedcont mat_thm ex_thms =
 523         DEDMATRIX vars sgns div_thms pdiff_thm normal_thm cont' mat_thm ex_thms in
 524         SPLITZERO vars qs gs dedcont sgns ex_thms fm
 525
 526 and SPLITZERO vars dun pols cont sgns ex_thms fm =
 527   incr splitzero_count;
 528   match pols with
 529       [] -> SPLITSIGNS vars [] dun cont sgns ex_thms fm
 530     | p::ops ->
 531         if p = rzero then
 532           let cont' mat_thm ex_thms = MATINSERT vars (length dun) (REFL rzero) cont mat_thm ex_thms in
 533             SPLITZERO vars dun ops cont' sgns ex_thms fm
 534         else
 535           let hp = behead vars p in
 536           let h = head vars p in
 537           let nzcont =
 538             let tmp = SPLITZERO vars (dun@[p]) ops cont in
 539               fun sgns ex_thms -> tmp sgns ex_thms fm in
 540           let zcont =
 541             let tmp = SPLITZERO vars dun (hp :: ops) in
 542             fun sgns ex_thms ->
 543               let zthm = FINDSIGN vars sgns h in
 544               let b_thm = GSYM (BEHEAD vars zthm p) in
 545               let lam_thm = ABS (hd vars) b_thm in
 546               let cont' mat_thm ex_thms =
 547                 let mat_thm' = REPLACE_POL (lam_thm) mat_thm in
 548                 let mat_thm'' = MATCH_EQ_MP mat_thm' mat_thm in
 549                   cont mat_thm'' ex_thms in
 550                 tmp cont' sgns ex_thms fm in
 551             SPLIT_ZERO (tl vars) sgns (head vars p) zcont nzcont ex_thms
 552
 553 and SPLITSIGNS vars dun pols cont sgns ex_thms fm =
 554   incr splitsigns_count;
 555   match pols with
 556       [] -> MONICIZE vars dun cont sgns ex_thms fm
 557 (*         [] -> MATRIX vars dun cont sgns ex_thms fm *)
 558     | p::ops ->
 559         let cont' sgns ex_thms = SPLITSIGNS vars (dun@[p]) ops cont sgns ex_thms fm in
 560           SPLIT_SIGN (tl vars) sgns (head vars p) cont' cont' ex_thms
 561
 562 and MONICIZE vars pols cont sgns ex_thms fm =
 563   incr monicize_count;
 564   let monic_thms = map (MONIC_CONV vars) pols in
 565   let monic_pols = map (rhs o concl) monic_thms in
 566   let sols = setify monic_pols in
 567   let indices = map (fun p -> try index p sols with _ -> failwith "MONICIZE: no such pol") monic_pols in
 568   let transform mat_thm =
 569     let mat_thm' = DUPLICATE_COLUMNS mat_thm indices in
 570 (*       mat_thm'  *)
 571       UNMONICIZE_MAT vars monic_thms mat_thm' in
 572   let cont' mat_thm ex_thms = cont (transform mat_thm) ex_thms in
 573     MATRIX vars sols cont' sgns ex_thms fm
 574 ;;
 575
 576 (* {{{ Examples *)
 577
 578 (*
 579 let vars,pols,sgns,ex_thms = [],[],[],[]
 580
 581 let mat_thm = mat_thm'
 582 monic_thms
 583
 584 let vars = [rx]
 585 let mat_thm = ASSUME
 586   `interpmat [x1; x2; x3; x4; x5]
 587      [(\x. &1 + x * (&2 + x * &3)); (\x. &2 + x * (&4 + x * &6)); \x. &3 + x * (&6 + x * &9); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1); \x. &8 + x * &4]
 588       [[Pos; Pos; Pos; Neg; Neg; Neg];
 589       [Pos; Pos; Zero; Zero; Neg; Neg];
 590       [Pos; Pos; Neg; Pos; Neg; Neg];
 591       [Pos; Pos; Neg; Pos; Neg; Zero];
 592       [Pos; Pos; Neg; Pos; Neg; Pos];
 593       [Pos; Pos; Neg; Pos; Zero; Pos];
 594       [Pos; Pos; Neg; Pos; Pos; Pos];
 595       [Pos; Zero; Neg; Pos; Pos; Pos];
 596       [Pos; Neg; Neg; Pos; Pos; Pos];
 597       [Pos; Zero; Zero; Pos; Pos; Pos];
 598       [Pos; Pos; Pos; Pos; Pos; Pos]]`
 599
 600 let mat_thm = ASSUME
 601  `interpmat [x1; x2; x3; x4; x5]
 602   [\x. -- &4 + x * (&0 + x * &1); \x. &2 + x * &1; \x. &2 + x * (-- &3 + x * &1); \x. &1 / &3 + x * (&2 / &3 + x * &1)]
 603       [[Pos; Pos; Pos; Neg];
 604       [Pos; Pos; Zero; Zero];
 605       [Pos; Pos; Neg; Pos];
 606       [Pos; Pos; Neg; Pos];
 607       [Pos; Pos; Neg; Pos];
 608       [Pos; Pos; Neg; Pos];
 609       [Pos; Pos; Neg; Pos];
 610       [Pos; Zero; Neg; Pos];
 611       [Pos; Neg; Neg; Pos];
 612       [Pos; Zero; Zero; Pos];
 613       [Pos; Pos; Pos; Pos]]`;;
 614
 615 let vars = [rx]
 616 let pols = [`&1 + x * (&2 + x * &3)`;`&2 + x * (&4 + x * &6)`;`&3 + x * (&6 + x * &9)`; `&2 + x * (-- &3 + x * &1)`;`-- &4 + x * (&0 + x * &1)`;`&8 + x * &4`]
 617
 618
 619 *)
 620 (* }}} *)
 621
 622
 623 (* ---------------------------------------------------------------------- *)
 624 (*  Set up RQE                                                            *)
 625 (* ---------------------------------------------------------------------- *)
 626
 627 let polynomials tm =
 628   let rec polynomials tm =
 629     if tm = t_tm or tm = f_tm then []
 630     else if is_conj tm or is_disj tm or is_imp tm or is_iff tm then
 631       let _,l,r = get_binop tm in polynomials l @ polynomials r
 632     else if is_neg tm then polynomials (dest_neg tm)
 633     else if
 634       can (dest_binop rlt) tm or
 635       can (dest_binop rgt) tm or
 636       can (dest_binop rle) tm or
 637       can (dest_binop rge) tm or
 638       can (dest_binop req) tm or
 639       can (dest_binop rneq) tm then
 640         let _,l,_ = get_binop tm in [l]
 641     else failwith "not a fol atom" in
 642     setify (polynomials tm);;
 643 (* {{{ Examples *)
 644
 645 (*
 646 let pols = polynomials `(poly [&1; -- &2] x > &0 ==> poly [&1; -- &2] x >= &0 /\ (poly [&8] x = &0)) /\ ~(poly [y] x <= &0)`
 647 *)
 648
 649 (* }}} *)
 650
 651
 652 let BASIC_REAL_QELIM_CONV vars fm =
 653   let x,bod = dest_exists fm in
 654   let pols = polynomials bod in
 655   let cont mat_thm ex_thms =
 656     let ex_thms' = sort (fun x y -> xterm_lt (fst y) (fst x)) ex_thms in
 657     let comb_thm = COMBINE_TESTFORMS x mat_thm bod in
 658     let comb_thm' = rev_itlist CHOOSE ex_thms' comb_thm in
 659       comb_thm' in
 660   let ret_thm = SPLITZERO (x::vars) [] pols cont empty_sgns [] fm in
 661     PURE_REWRITE_RULE[NEQ] ret_thm;;
 662
 663 let REAL_QELIM_CONV fm =
 664   reset_counts();
 665   ((LIFT_QELIM_CONV POLYATOM_CONV (EVALC_CONV THENC SIMPLIFY_CONV)
 666      BASIC_REAL_QELIM_CONV) THENC EVALC_CONV THENC SIMPLIFY_CONV) fm;;
 667
 668 (* ---------------------------------------------------------------------- *)
 669 (*  timers                                                                *)
 670 (* ---------------------------------------------------------------------- *)
 671