1 (* ====================================================================== *)
3 (* ====================================================================== *)
5 (* ------------------------------------------------------------------------- *)
6 (* Infer sign of p(x) at points from corresponding qi(x) with pi(x) = 0 *)
7 (* ------------------------------------------------------------------------- *)
9 (* ---------------------------------------------------------------------- *)
11 (* ---------------------------------------------------------------------- *)
14 let isign_eq_zero thm =
15 let __,_,sign = dest_interpsign thm in
18 let isign_lt_zero thm =
19 let __,_,sign = dest_interpsign thm in
22 let isign_gt_zero thm =
23 let __,_,sign = dest_interpsign thm in
27 let p_thm,q_thm = ith 1 split_thms
29 let inferpsign_row vars sgns p_thm q_thm div_thms =
30 let pthms = map (BETA_RULE o (PURE_REWRITE_RULE[interpsigns])) (interpsigns_thms2 p_thm) in
31 let qthms = map (BETA_RULE o (PURE_REWRITE_RULE[interpsigns])) (interpsigns_thms2 q_thm) in
32 let _,set,_ = dest_interpsigns p_thm in
33 if can (get_index isign_eq_zero) pthms then (* there's a zero *)
34 let ind = get_index isign_eq_zero pthms in
35 let pthm = ith ind pthms in
36 let qthm = ith ind qthms in
37 let div_thm = ith ind div_thms in
38 let div_thm' = GEN (hd vars) div_thm in
39 let aks,pqr = dest_eq (concl div_thm) in
40 let ak,s = dest_mult aks in
41 let a,k = dest_pow ak in
42 let pq,r = dest_plus pqr in
43 let p,q = dest_mult pq in
44 let parity_thm = PARITY_CONV k in
45 let evenp = fst(dest_comb (concl parity_thm)) = even_tm in
46 let sign_thm = FINDSIGN vars sgns a in
47 let op,_,_ = get_binop (concl sign_thm) in
50 if op = rlt then MATCH_MP ips_lt_nz_thm sign_thm
51 else if op = rgt then MATCH_MP ips_gt_nz_thm sign_thm
52 else if op = rneq then sign_thm
53 else failwith "inferpsign: 0" in
55 CONJUNCTS(ISPEC set (MATCH_MPL[EVEN_DIV_LEM;div_thm';nz_thm;parity_thm])) in
56 let _,_,qsign = dest_interpsign qthm in
58 if qsign = sneg_tm then ith 0 imp_thms
59 else if qsign = spos_tm then ith 1 imp_thms
60 else if qsign = szero_tm then ith 2 imp_thms
61 else failwith "inferpsign: 1" in
62 let final_thm = MATCH_MPL[mp_thm;pthm;qthm] in
63 mk_interpsigns (final_thm::pthms)
65 if op = rgt then (* a > &0 *)
67 CONJUNCTS(ISPEC set (MATCH_MPL[GT_DIV_LEM;div_thm';sign_thm])) in
68 let _,_,qsign = dest_interpsign qthm in
70 if qsign = sneg_tm then ith 0 imp_thms
71 else if qsign = spos_tm then ith 1 imp_thms
72 else if qsign = szero_tm then ith 2 imp_thms
73 else failwith "inferpsign: 1" in
74 let final_thm = MATCH_MPL[mp_thm;pthm;qthm] in
75 mk_interpsigns (final_thm::pthms)
77 failwith "inferpsign: shouldn`t reach this point with an odd power and negative sign! See PDIVIDES and return the correct div_thm"
79 let p = snd(dest_mult (lhs(concl (hd div_thms)))) in
80 let p1 = mk_abs(hd vars,p) in
81 let pthm = ISPECL [set;p1] unknown_thm in
82 mk_interpsigns (pthm::pthms);;
88 [p0; p1; p2; q0; q1; q2]
90 [Pos; Pos; Pos; Neg; Neg; Neg]
107 let split_interpsigns thm =
108 let thms = interpsigns_thms2 thm in
109 let n = length thms / 2 in
110 let l,r = chop_list n thms in
111 (mk_interpsigns l,mk_interpsigns r);;
113 let INFERPSIGN vars sgns mat_thm div_thms =
114 let pts,pols,signs = dest_interpmat (concl mat_thm) in
115 let n = length (dest_list pols) / 2 in
116 let rol_thm,sgn_thm = interpmat_thms mat_thm in
117 let part_thm = PARTITION_LINE_CONV (snd (dest_comb (concl rol_thm))) in
118 let conj_thms = CONJUNCTS(REWRITE_RULE[ALL2;part_thm] sgn_thm) in
119 let split_thms = map split_interpsigns conj_thms in
120 let conj_thms' = map (fun (x,y) -> inferpsign_row vars sgns x y div_thms) split_thms in
121 let all_thm = mk_all2_interpsigns part_thm conj_thms' in
122 let mat_thm' = mk_interpmat_thm rol_thm all_thm in
125 (* ---------------------------------------------------------------------- *)
127 (* ---------------------------------------------------------------------- *)
130 let rep_tm = `REPLICATE:num -> sign -> sign list` in
131 let len_tm = `LENGTH:real list -> num` in
134 let unknown = `Unknown` in
136 let num = mk_binop np (mk_binop nm two (mk_comb(len_tm,pts))) one in
137 let len = length (dest_list pts) in
138 let num2 = MK_SUC (2 * len + 1) in
139 let lthm = ARITH_SIMP_CONV[LENGTH] num in
140 let lthm2 = TRANS lthm num2 in
141 let lthm3 = AP_THM (AP_TERM rep_tm lthm2) unknown in
142 REWRITE_RULE[REPLICATE] lthm3;;
144 let INSERT_UNKNOWN_COL =
146 let pts,_,_ = dest_interpmat (concl mat_thm) in
147 let rep_thm = MK_REP pts in
148 let mat_thm' = MATCH_MP INFERPSIGN_MATINSERT_THM mat_thm in
149 let mat_thm'' = PURE_REWRITE_RULE[MAP2;rep_thm] mat_thm' in
154 let _,pols,_ = dest_interpmat (concl mat_thm) in
155 let len = length (dest_list pols) in
156 if not (len mod 2 = 1) then failwith "odd pols?" else
157 let mat_thm' = funpow (len / 2) (MATCH_MP REMOVE_LAST) mat_thm in
158 REWRITE_RULE[MAP;BUTLAST;NOT_CONS_NIL;TL;HD;] mat_thm';;
160 let SPLIT_LIST n l ty =
161 let l' = dest_list l in
162 let l1',l2' = chop_list n l' in
163 let l1,l2 = (mk_list(l1',ty),mk_list(l2',ty)) in
164 let app_tm = mk_const("APPEND",[ty,aty]) in
165 let l3 = mk_comb(mk_comb(app_tm,l1),l2) in
166 SYM(REWRITE_CONV[APPEND] l3);;
172 let prove_nonzero thm =
173 let op,_,_ = get_binop (concl thm) in
174 if op = rgt then MATCH_MP ips_gt_nz_thm thm
175 else if op = rlt then MATCH_MP ips_lt_nz_thm thm
176 else if op = rneq then thm
177 else failwith "prove_nonzero: bad op";;
180 let mat_thm = mat_thm'
186 let unknown = `Unknown` in
191 let even_tm = `(EVEN)` in
192 let odd_tm = `(ODD)` in
193 let rr_ty = `:real -> real` in
194 let sl_ty = `:sign list` in
195 let s_ty = `:sign` in
196 let imat = `interpmat` in
197 let rr_length = mk_const("LENGTH",[rr_ty,aty]) in
198 let s_length = mk_const("LENGTH",[s_ty,aty]) in
199 let sl_length = mk_const("LENGTH",[sl_ty,aty]) in
200 let imat = `interpmat` in
201 fun vars sgns mat_thm div_thms ind ->
202 let pts,pols,signs = dest_interpmat (concl mat_thm) in
203 let pols' = dest_list pols in
204 let signsl = dest_list signs in
205 let signs' = map dest_list signsl in
206 let pols_len = length (hd signs') in
207 let pols_len2 = pols_len / 2 in
208 let pt_sgnl = ith ind signsl in
209 let pt_sgns = ith ind signs' in
210 let zind = index zero pt_sgns in
211 if zind > pols_len2 then mat_thm else (* return if not a zero of a p, only a q *)
212 let psgn = ith (pols_len2 + zind) pt_sgns in
213 let div_thm = ith (zind - 1) div_thms in
214 let a,n = dest_binop pow (fst (dest_binop rm (lhs (concl div_thm)))) in
215 let asign = FINDSIGN vars sgns a in
216 let op,_,_ = get_binop (concl asign) in
217 let par_thm = PARITY_CONV n in
218 let par = fst(dest_comb(concl par_thm)) in
220 (* note: by def of PDIVIDES, we can`t have
221 negative sign and odd power at this point *)
223 if par = even_tm then
224 if psgn = pos then INFERPSIGN_POS_EVEN
225 else if psgn = neg then INFERPSIGN_NEG_EVEN
226 else if psgn = zero then INFERPSIGN_ZERO_EVEN
227 else failwith "INFERPT: bad sign"
229 if psgn = pos then INFERPSIGN_POS_ODD_POS
230 else if psgn = neg then INFERPSIGN_NEG_ODD_POS
231 else if psgn = zero then INFERPSIGN_ZERO_ODD_POS
232 else failwith "INFERPT: bad sign" in
234 let split_pols1 = SPLIT_LIST zind pols rr_ty in
235 let _,l2 = chop_list zind pols' in
236 let split_pols2 = SPLIT_LIST pols_len2 (mk_list(l2,rr_ty)) rr_ty in
237 let s1,t1 = dest_comb (rhs (concl split_pols1)) in
238 let split_pols_thm = TRANS split_pols1 (AP_TERM s1 split_pols2) in
240 let split_sgns1 = SPLIT_LIST zind pt_sgnl s_ty in
241 let _,l3 = chop_list zind pt_sgns in
242 let split_sgns2 = SPLIT_LIST pols_len2 (mk_list(l3,s_ty)) s_ty in
243 let s2,t2 = dest_comb (rhs (concl split_sgns1)) in
244 let split_pt_sgns_thm = TRANS split_sgns1 (AP_TERM s2 split_sgns2) in
246 let split_signs = SPLIT_LIST ind signs sl_ty in
247 let r1,r3 = dest_comb(rhs (concl split_signs)) in
248 let tl_thm = HD_CONV (ONCE_REWRITE_CONV[split_pt_sgns_thm]) r3 in
249 let r4,_ = dest_comb (rhs (concl split_signs)) in
250 let split_sgns_thm = TRANS split_signs (AP_TERM r4 tl_thm) in
252 let mat1 = mk_comb(imat,pts) in
253 let mat_thm1 = AP_TERM mat1 split_pols_thm in
254 let mat_thm2 = MK_COMB(mat_thm1,split_sgns_thm) in
255 let mat_thm3 = EQ_MP mat_thm2 mat_thm in
257 (* LENGTH ps = LENGTH s1 *)
258 let ps = mk_list(tl(dest_list(snd(dest_comb s1))),rr_ty) in
259 let ps_len = REWRITE_CONV[LENGTH] (mk_comb(rr_length,ps)) in
260 let ss = mk_list(tl(dest_list(snd(dest_comb s2))),s_ty) in
261 let ss_len = REWRITE_CONV[LENGTH] (mk_comb(s_length,ss)) in
262 let ps_s1_thm = TRANS ps_len (SYM ss_len) in
263 (* LENGTH qs = LENGTH s2 *)
264 let k1 = tl (fst (chop_list pols_len2 (dest_list t1))) in
265 let qs = mk_list(k1,rr_ty) in
266 let qs_len = REWRITE_CONV[LENGTH] (mk_comb(rr_length,qs)) in
267 let k2 = tl (fst (chop_list pols_len2 (dest_list t2))) in
268 let s2s = mk_list(k2,s_ty) in
269 let s2s_len = REWRITE_CONV[LENGTH] (mk_comb(s_length,s2s)) in
270 let qs_s2_thm = TRANS qs_len (SYM s2s_len) in
271 (* ODD (LENGTH sgns) *)
272 let _,hdsgns = dest_comb r1 in
273 let odd_thm = EQT_ELIM(REWRITE_CONV[LENGTH;ODD;EVEN;NOT_ODD;NOT_EVEN] (mk_comb(odd_tm,mk_comb(sl_length,hdsgns)))) in
276 if par = even_tm then prove_nonzero asign
278 let div_thm' = GEN (hd vars) div_thm in
280 let thm1 = BETA_RULE(MATCH_MPL[mp_thm;mat_thm3;ps_s1_thm;qs_s2_thm;odd_thm]) in
282 if par = even_tm then MATCH_MPL[thm1;div_thm';a_thm;par_thm]
283 else MATCH_MPL[thm1;div_thm';a_thm] in
284 REWRITE_RULE[APPEND] thm2;;
287 let mat_thm = mat_thm'
289 let INFERPTS vars sgns mat_thm div_thms =
290 let pts,_,_ = dest_interpmat (concl mat_thm) in
291 let len = 2 * length (dest_list pts) in
292 let ods = filter odd (1--len) in
293 itlist (fun i matthm -> INFERPT vars sgns matthm div_thms i) ods mat_thm;;
296 let itvars,itsgns,itmat,itdivs = ref [],ref [],ref TRUTH,ref [];;
298 let vars,sgns,mat_thm,div_thms = !itvars,!itsgns,!itmat,!itdivs
301 let INFERPSIGN2 vars sgns mat_thm div_thms =
306 let _,bod = dest_binop rm (lhs (concl (hd div_thms))) in
307 let p = mk_abs(hd vars,bod) in
308 let mat_thm' = INSERT_UNKNOWN_COL mat_thm p in
309 let mat_thm'' = INFERPTS vars sgns mat_thm' div_thms in
310 REMOVE_QS mat_thm'';;
313 (* ---------------------------------------------------------------------- *)
315 (* ---------------------------------------------------------------------- *)
317 let INFERPSIGN vars sgns mat_thm div_thms =
318 let start_time = Sys.time() in
319 let res = INFERPSIGN vars sgns mat_thm div_thms in
320 inferpsign_timer +.= (Sys.time() -. start_time);
325 let l1 = PDIVIDE [`x:real`]
326 `&1 + x * (&1 + x * (&1 + x * &1))` `&1 + x * (&2 + x * &3)`;;
327 let l2 = PDIVIDE [`x:real`]
328 `&1 + x * (&1 + x * (&1 + x * &1))` `&2 + x * (-- &3 + x * &1)`;;
329 let l3 = PDIVIDE [`x:real`]
330 `&1 + x * (&1 + x * (&1 + x * &1))` `-- &4 + x * (&0 + x * &1)`;;
332 let div_thms = [l1;l2;l3];;
333 let vars = [`x:real`];;
334 let sgns = [ARITH_RULE `&1 > &0`];;
337 `interpmat [x1; x2; x3; x4; x5]
338 [\x. &1 + x * (&2 + x * &3); \x. &2 + x * (-- &3 + x * &1); \x. -- &4 + x * (&0 + x * &1);
339 \x. &8 + x * &4; \x. -- &7 + x * &11; \x. &5 + x * &5]
340 [[Pos; Pos; Pos; Neg; Neg; Neg];
341 [Pos; Pos; Zero; Zero; Neg; Neg];
342 [Pos; Pos; Neg; Pos; Neg; Neg];
343 [Pos; Pos; Neg; Pos; Neg; Zero];
344 [Pos; Pos; Neg; Pos; Neg; Pos];
345 [Pos; Pos; Neg; Pos; Zero; Pos];
346 [Pos; Pos; Neg; Pos; Pos; Pos];
347 [Pos; Zero; Neg; Pos; Pos; Pos];
348 [Pos; Neg; Neg; Pos; Pos; Pos];
349 [Pos; Zero; Zero; Pos; Pos; Pos];
350 [Pos; Pos; Pos; Pos; Pos; Pos]]` ;;
352 INFERPSIGN vars sgns mat_thm div_thms