1 let empty_mat = prove_by_refinement(
2 `interpmat [] [] [[]]`,
6 REWRITE_TAC[interpmat;ROL_EMPTY;interpsigns;ALL2;partition_line];
11 let empty_sgns = [ARITH_RULE `&1 > &0`];;
13 let monic_isign_lem = prove(
14 `(!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Pos ==> interpsign s p Pos) /\
15 (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Pos ==> interpsign s p Neg) /\
16 (!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Neg ==> interpsign s p Neg) /\
17 (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Neg ==> interpsign s p Pos) /\
18 (!s c mp p. (!x. c * p x = mp x) ==> c > &0 ==> interpsign s mp Zero ==> interpsign s p Zero) /\
19 (!s c mp p. (!x. c * p x = mp x) ==> c < &0 ==> interpsign s mp Zero ==> interpsign s p Zero)`,
22 REWRITE_TAC[interpsign] THEN REPEAT STRIP_TAC THEN
23 POP_ASSUM (fun x -> POP_ASSUM (fun y -> MP_TAC (MATCH_MP y x))) THEN
25 POP_ASSUM (ASSUME_TAC o GSYM o (ISPEC `x:real`)) THEN
26 ASM_REWRITE_TAC[REAL_MUL_LT;REAL_MUL_GT;real_gt;REAL_ENTIRE] THEN
31 let gtpos::ltpos::gtneg::ltneg::gtzero::ltzero::[] = CONJUNCTS monic_isign_lem;;
33 let main_lem000 = prove_by_refinement(
34 `!l n. (LENGTH l = SUC n) ==> 0 < LENGTH l`,
46 let main_lem001 = prove_by_refinement(
47 `x <> &0 ==> (LAST l = x) ==> LAST l <> &0`,
50 let main_lem002 = prove_by_refinement(
51 `(x <> y ==> x <> y) /\
54 (~(x >= y) ==> x <> y) /\
55 (~(x <= y) ==> x <> y) /\
56 (~(x = y) ==> x <> y)`,
60 REWRITE_TAC[NEQ] THEN REAL_ARITH_TAC
65 let factor_pos_pos = prove_by_refinement(
66 `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Pos ==>
67 (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
70 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
72 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
73 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
75 REWRITE_TAC[REAL_MUL_GT;real_gt];
77 ASM_MESON_TAC[REAL_POW_LT;real_gt];
81 let factor_pos_neg = prove_by_refinement(
82 `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Neg ==>
83 (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
86 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
88 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
89 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
91 REWRITE_TAC[REAL_MUL_LT;real_gt];
93 ASM_MESON_TAC[REAL_POW_LT;real_gt];
97 let factor_pos_zero = prove_by_refinement(
98 `interpsign s (\x. &0 + x * &1) Pos ==> interpsign s p Zero ==>
99 (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
102 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
104 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
105 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
107 REWRITE_TAC[REAL_MUL_LT;REAL_ENTIRE;real_gt];
111 let factor_zero_pos = prove_by_refinement(
112 `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Pos ==> ~(k = 0) ==>
113 (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
116 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
118 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
119 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
121 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;REAL_ENTIRE];
123 ASM_MESON_TAC[POW_0;num_CASES;];
127 let factor_zero_neg = prove_by_refinement(
128 `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Neg ==> ~(k = 0) ==>
129 (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
132 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
134 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
135 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
137 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;REAL_ENTIRE];
139 ASM_MESON_TAC[POW_0;num_CASES;];
143 let factor_zero_zero = prove_by_refinement(
144 `interpsign s (\x. &0 + x * &1) Zero ==> interpsign s p Zero ==> ~(k = 0) ==>
145 (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
148 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
150 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
151 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
157 let factor_neg_even_pos = prove_by_refinement(
158 `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Pos ==> EVEN k ==> ~(k = 0) ==>
159 (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
162 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
164 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
165 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
167 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt];
169 ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
173 let factor_neg_even_neg = prove_by_refinement(
174 `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Neg ==> EVEN k ==> ~(k = 0) ==>
175 (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
178 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
180 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
181 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
183 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt];
185 ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
189 let factor_neg_even_zero = prove_by_refinement(
190 `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Zero ==> EVEN k ==> ~(k = 0) ==>
191 (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
194 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
196 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
197 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
199 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
203 let factor_neg_odd_pos = prove_by_refinement(
204 `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Pos ==> ODD k ==> ~(k = 0) ==>
205 (!x. x pow k * p x = q x) ==> interpsign s q Neg`,
208 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
210 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
211 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
213 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
215 ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
219 let factor_neg_odd_neg = prove_by_refinement(
220 `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Neg ==> ODD k ==> ~(k = 0) ==>
221 (!x. x pow k * p x = q x) ==> interpsign s q Pos`,
224 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
226 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
227 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
229 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];
231 ASM_MESON_TAC[REAL_POW_LT;real_gt;PARITY_POW_LT];
235 let factor_neg_odd_zero = prove_by_refinement(
236 `interpsign s (\x. &0 + x * &1) Neg ==> interpsign s p Zero ==> ODD k ==> ~(k = 0) ==>
237 (!x. x pow k * p x = q x) ==> interpsign s q Zero`,
240 REWRITE_TAC[interpsign;REAL_ADD_LID;REAL_MUL_RID;];
242 POP_ASSUM (fun x -> (RULE_ASSUM_TAC (fun y -> try MATCH_MP y x with _ -> y)));
243 POP_ASSUM (ASSUME_TAC o ISPEC rx o GSYM);
245 REWRITE_TAC[REAL_MUL_GT;REAL_MUL_LT;real_gt;REAL_ENTIRE];