1 (* ====================================================================== *)
3 (* ====================================================================== *)
5 (* ---------------------------------------------------------------------- *)
7 (* ---------------------------------------------------------------------- *)
9 let sign_INDUCT,sign_RECURSION = define_type
10 "sign = Zero | Pos | Neg | Nonzero | Unknown";;
12 let SIGN_CASES = prove_by_refinement(
13 `!s. (s = Pos) \/ (s = Neg) \/ (s = Zero) \/ (s = Nonzero) \/ (s = Unknown)`,
16 MATCH_MP_TAC sign_INDUCT;
21 let szero_tm,spos_tm,sneg_tm,snonz_tm,sunk_tm = `Zero`,`Pos`,`Neg`,`Nonzero`,`Unknown`;;
23 (* ------------------------------------------------------------------------- *)
24 (* Intepretation of signs. *)
25 (* ------------------------------------------------------------------------- *)
27 (* An interpretation of the sign of a polynomial over a set. *)
28 let interpsign = new_recursive_definition sign_RECURSION
29 `(interpsign set ply Zero = (!x:real. set x ==> (ply x = &0))) /\
30 (interpsign set ply Pos = (!x. set x ==> (ply x > &0))) /\
31 (interpsign set ply Neg = (!x. set x ==> (ply x < &0))) /\
32 (interpsign set ply Nonzero = (!x. set x ==> (ply x <> &0))) /\
33 (interpsign set ply Unknown = (!x. set x ==> (ply x = ply x)))`;;
36 let interpsign_tm = `interpsign`;;
37 let dest_interpsign interpthm =
38 let int,[set;poly;sign] = strip_ncomb 3 (concl interpthm) in
39 if not (int = interpsign_tm) then
40 failwith "not an interpsign"
45 let k0 = prove_by_refinement(
46 `interpsign (\x. x = &10) (\x. -- &10 + x * &1) Zero`,[
47 REWRITE_TAC[interpsign;poly];
55 (* A version for one set but multiple polynomials *)
56 let interpsigns = new_definition
57 `interpsigns polyl set signl = ALL2 (interpsign set) polyl signl`;;
59 let t0 = TAUT `a /\ T <=> a`;;
60 let interpsigns_thms interpthm =
61 let ret = map BETA_RULE(
62 CONJUNCTS (PURE_REWRITE_RULE[interpsign;interpsigns;ALL2;t0] interpthm)) in
66 let interpsigns_thms2 interpthm =
67 CONJUNCTS (PURE_REWRITE_RULE[interpsigns;ALL2;t0] interpthm);;
69 let interpsigns_tm = `interpsigns`;;
70 let dest_interpsigns interpthm =
71 let int,[polys;set;signs] = strip_ncomb 3 (concl interpthm) in
72 if not (int = interpsigns_tm) then
73 failwith "not an interpsigns"
78 let interp_sing = prove(
79 `interpsign set p s = interpsigns [p] set [s]`,
80 REWRITE_TAC[interpsigns;ALL2]);;
82 let interp_doub = prove(
83 `interpsigns [p1] set [s1] ==> interpsigns pl set sl ==>
84 interpsigns (CONS p1 pl) set (CONS s1 sl)`,
85 ASM_MESON_TAC[interpsigns;ALL2]);;
87 let mk_interpsigns thms =
88 let thms' = map (PURE_REWRITE_RULE[interp_sing]) thms in
89 end_itlist (fun t1 t2 -> MATCH_MPL [interp_doub;t1;t2]) thms';;
94 let t0 = ASSUME `interpsign s1 p1 Zero`;;
95 let t1 = ASSUME `interpsign s1 p2 Pos`;;
96 let t2 = ASSUME `interpsign s1 p3 Neg`;;
98 mk_interpsigns [t0;t1;t2];;
99 map (PURE_REWRITE_RULE[interp_sing]) [t0;t1;t2];;
104 let k0 = prove_by_refinement(
105 `interpsigns [(\x. &1 + x * &1); (\x. &2 + x * &3)] (\x. x = (-- &1)) [Zero; Neg]`,
107 REWRITE_TAC[interpsigns;ALL2;interpsign;poly];
112 (* ---------------------------------------------------------------------- *)
114 (* ---------------------------------------------------------------------- *)
117 let partition_line = new_recursive_definition list_RECURSION
118 `(partition_line [] = [(\x. T)]) /\
119 (partition_line (CONS h t) =
120 if t = [] then [(\x. x < h); (\x. x = h); (\x. h < x)] else
121 APPEND [(\x. x < h); (\x. x = h); (\x. h < x /\ x < HD t)]
122 (TL (partition_line t)))`;;
126 `partition_line [&1] = [(\x. x < &1); (\x. x = &1); (\x. &1 < x)]`,
127 REWRITE_TAC[partition_line])
130 `partition_line [&1; &2] =
131 [(\x. x < &1); (\x. x = &1); (\x. &1 < x /\ x < &2); (\x. x = &2); (\x. &2 < x)]`,
132 REWRITE_TAC[partition_line;APPEND;COND_CLAUSES;NOT_CONS_NIL;TL;HD]);;
136 let make_partition_list =
137 let lxt = `\x:real. T`
141 and x_lt_h = `(\x. x < h)`
142 and x_eq_h = `(\x:real. x = h)`
143 and h_lt_x = `(\x. h < x)`
144 and x_lt_h1 = `(\x. x < h1)`
145 and x_eq_h1 = `(\x:real. x = h1)`
146 and x_h1_h2 = `(\x. h1 < x /\ x < h2)` in
147 let rec make_partition_list ps =
150 | [h] -> map (subst [h,htm]) [x_lt_h; x_eq_h;h_lt_x]
151 | h1::h2::t -> (map (subst [(h1,h1tm);(h2,h2tm)])
152 [x_lt_h1; x_eq_h1;x_h1_h2]) @ tl (make_partition_list (h2::t)) in
153 make_partition_list;;
157 make_partition_list [`&1`;`&2`]
160 (* partition a line based on a list of points
161 this is just a compact representation of a list of terms
163 let part_line_tm = `partition_line`;;
164 let real_bool_ty = `:real->bool`;;
165 let PARTITION_LINE_CONV pts =
166 let ptm = mk_comb (part_line_tm,pts) in
167 let ltm = mk_list ((make_partition_list (dest_list pts)),real_bool_ty) in
168 let tm = mk_eq (ptm,ltm) in
169 prove(tm,REWRITE_TAC [partition_line;APPEND;COND_CLAUSES;NOT_CONS_NIL;TL;HD]);;
172 PARTITION_LINE_CONV `[]:real list`
173 PARTITION_LINE_CONV `[&1; &2]`
174 PARTITION_LINE_CONV `[&2; &1]`
175 PARTITION_LINE_CONV `[a:real; b]`
179 (* an interpretation of a sign matrix
180 arguments are a list of points, a list of polynomials, and a sign matrix
181 the points form an ordered list (smallest first),
182 each zero of each polynomial must appear among the list of points
183 and finally, the sign matrix corresponds to the correct sign for the polynomial
184 in the region represented by the set.
186 let interpmat = new_definition
187 `interpmat ptl polyl signll <=>
188 real_ordered_list ptl /\
189 ALL2 (interpsigns polyl) (partition_line ptl) signll`;;
191 let interpmat_tm = `interpmat`;;
193 let imat_tm = interpmat_tm in
195 let sc,args = strip_comb tm in
196 if not (sc = imat_tm) then failwith "dest_interpmat: not an interpmat term" else
197 let [ptl;polyl;signll] = args in
200 let interpmat_thms thm =
201 let [rol_thm;interpsigns_thm] = CONJUNCTS (PURE_REWRITE_RULE[interpmat] thm) in
202 rol_thm,interpsigns_thm;;
204 let mk_interpmat_thm rol_thm =
206 let ret = REWRITE_RULE[GSYM interpmat] (CONJ rol_thm all_thm) in
207 let l,_ = strip_comb (concl ret) in
208 if not (l = interpmat_tm) then failwith "mk_interpmat" else ret;;
211 let rol_thm = rol_thm'''
212 let all_thm = all_thm''
220 |- partition_line [x1; x2; x3; x4; x5] =
221 [(\x. x < x1); (\x. x = x1); (\x. x1 < x /\ x < x2); (\x. x = x2);
222 (\x. x2 < x /\ x < x3); (\x. x = x3); (\x. x3 < x /\ x < x4); (\x. x = x4);
223 (\x. x4 < x /\ x < x5); (\x. x = x5); (\x. x5 < x)]
227 [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
229 [Unknown; Pos; Pos; Pos]
236 [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
238 [Pos; Pos; Zero; Zero]
241 [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]]
243 [Unknown; Pos; Pos; Pos]
248 |- ALL2 (interpsigns [[&1; &1; &1; &1]; [&1; &2; &3]; [&2; -- &3; &1]; [-- &4; &0; &1]])
249 (partition_line [x1;x2;x3;x4;x5])
250 [[Unknown; Pos; Pos; Pos];...; [Pos; Pos; Zero; Zero]; [Unknown; Pos; Pos; Pos]]
256 let all2_thm0 = GEN_ALL(EQT_ELIM(hd (CONJUNCTS ALL2)));;
257 let all2_thm = GEN_ALL (REWRITE_RULE[AND_IMP_THM] (fst (EQ_IMP_RULE (GSYM (last (CONJUNCTS ALL2))))));;
259 let mk_all2_interpsigns part_thm is_thms =
260 let is_tm = fst(dest_comb(fst (dest_comb (concl (hd is_thms))))) in
261 let all2_thm0' = ISPEC is_tm all2_thm0 in (* it`s having trouble matching *)
262 let ret = itlist (fun x -> fun y -> MATCH_MPL[all2_thm;x;y]) is_thms all2_thm0' in
263 REWRITE_RULE[GSYM part_thm] ret;;
266 let a2,l = strip_comb tm in
267 if fst(dest_const a2) = "ALL2" then
268 let [a1;a2;a3] = l in
271 failwith "dest_all2: not an ALL2";;
273 (* ---------------------------------------------------------------------- *)
275 (* ---------------------------------------------------------------------- *)
277 let is_interval set =
279 let x,bod = dest_abs set in
281 let l,r = dest_conj bod in
282 can (dest_binop rlt) l & can (dest_binop rlt) r
283 else can (dest_binop rlt) bod
287 is_interval `\x. &4 < x /\ x < &5`;;
288 is_interval `\x. x = &4`;;
293 let x,bod = dest_abs set in
294 if is_eq bod then true else false
298 is_point `\x. x = &5`
299 is_point `\x. x = y:real`
302 (* ---------------------------------------------------------------------- *)
303 (* We generate new var names *)
304 (* ---------------------------------------------------------------------- *)
306 let new_var,reset_vars =
311 mk_var (pre ^ (string_of_int !id),ty) in