1 (* ====================================================================== *)
3 (* ====================================================================== *)
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 (* ------------------------------------------------------------------------- *)
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;;
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;;
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);;
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'';;
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";;
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";;
60 let aitvars,aitdiff,aitnorm,aitmat = ref [],ref TRUTH,ref TRUTH,ref TRUTH;;
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''
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
71 let sl_ty = `:sign list` in
72 let real_ty = `:real` in
73 fun vars diff_thm normal_thm mat_thm ->
76 aitnorm := normal_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
89 let sgn = (hd(tl(dest_list (hd sgnsl)))) in
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
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);;
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 [];;
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
140 let DEDMATRIX vars sgns div_thms pdiff_thm normal_thm cont mat_thm ex_thms =
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);;
173 let NOT_NIL_CONV tm =
174 let h,t = dest_cons tm in
175 ISPECL [h;t] NOT_CONS_NIL;;
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;;
183 let vars = [`x:real`];;
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]`;;
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];;
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]]` ;;
210 time (DEDMATRIX vars sgns div_thms pdiff_thm normal_thm (fun x y -> x) mat_thm) []
218 (* ---------------------------------------------------------------------- *)
220 (* ---------------------------------------------------------------------- *)
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);
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);
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);