1 needs "../formal_lp/ineqs/list_hypermap_defs.hl";;
10 let start = Unix.gettimeofday() in
14 Unix.time() -. start;;
21 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;
25 (******************************)
29 let HD_A_CONS = prove(`HD (CONS (h:A) t) = h`, REWRITE_TAC[HD]);;
32 let h_tm', t_tm = dest_comb(rand tm) in
33 let h_tm = rand h_tm' in
34 let list_ty = type_of t_tm in
35 let ty = type_of h_tm in
36 let h_var = mk_var("h", ty) in
37 let t_var = mk_var("t", list_ty) in
38 INST[h_tm, h_var; t_tm, t_var] (INST_TYPE[ty, aty] HD_A_CONS);;
41 let tm = `HD [1;2;3;4]`;;
43 test 1000 (REWRITE_CONV[HD]) tm;;
45 test 1000 hd_conv tm;;
55 (*******************************)
57 (* FST, SND conversions *)
60 let FST' = ISPECL[`x:A`; `y:B`] FST;;
61 let SND' = ISPECL[`x:A`; `y:B`] SND;;
65 let x_tm, y_tm = dest_pair (rand tm) in
66 let x_ty, y_ty = type_of x_tm, type_of y_tm in
67 let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
68 (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';;
71 let x_tm, y_tm = dest_pair (rand tm) in
72 let x_ty, y_ty = type_of x_tm, type_of y_tm in
73 let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
74 (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';;
78 let tm = `FST (1,2)`;;
82 test 10000 (REWRITE_CONV[]) tm;;
84 test 10000 fst_conv tm;;
88 (******************************)
90 (* LENGTH conversions *)
92 let LENGTH_A_EMPTY = prove(`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and
93 LENGTH_A_CONS = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);;
95 let suc_const = `SUC`;;
98 let length_conv_univ suc_conv tm =
99 let list_tm = rand tm in
100 let list_ty = type_of list_tm in
101 let ty = (hd o snd o dest_type) list_ty in
102 let inst_t = INST_TYPE[ty, aty] in
103 let length_empty, length_cons = inst_t LENGTH_A_EMPTY, inst_t LENGTH_A_CONS in
104 let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
106 let rec length_conv_raw = fun list_tm ->
107 if (is_comb list_tm) then
108 let ltm, t_tm = dest_comb list_tm in
109 let h_tm = rand ltm in
110 let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in
111 let th1' = length_conv_raw t_tm in
112 let th1 = AP_TERM suc_const th1' in
113 let th2 = suc_conv (rand(concl th1)) in
114 TRANS (TRANS th0 th1) th2
118 length_conv_raw list_tm;;
122 let tm = `LENGTH [&1;&4;&4;&6;&7 * &8]`;;
124 test 1000 (REWRITE_CONV[LENGTH; ARITH_SUC]) tm;; (* 0.792 *)
125 test 1000 (length_conv_univ NUM_SUC_CONV) tm;; (* 0.104 *)
129 (******************************)
131 (* MEM conversions *)
133 let MEM_A_EMPTY = prove(`MEM (x:A) [] <=> F`, REWRITE_TAC[MEM]) and
134 MEM_A_HD = UNDISCH_ALL (prove(`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
135 MEM_A_TL = UNDISCH_ALL (prove(`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]));;
140 let rec mem_conv_univ eq_conv tm =
141 let ltm, list_tm = dest_comb tm in
142 let x_tm = rand ltm in
143 let ty = type_of x_tm in
144 let inst_t = INST_TYPE[ty, aty] in
145 let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in
146 let x_var, h_var = mk_var("x", ty), mk_var("h", ty) in
147 let t_var = mk_var("t", mk_type("list", [ty])) in
149 let rec mem_conv_raw list_tm =
150 if (is_comb list_tm) then
151 let h_tm', t_tm = dest_comb list_tm in
152 let h_tm = rand h_tm' in
153 let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
154 if (rand(concl eq_th) = t_const) then
155 let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in
156 MY_PROVE_HYP eq_th th0'
158 let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in
159 let th0 = MY_PROVE_HYP eq_th th0' in
160 let th1 = mem_conv_raw t_tm in
163 INST[x_tm, x_var] mem_empty in
165 mem_conv_raw list_tm;;
169 let tm = `MEM 11 [1;2;3;4;5;6;4;5;6;7;3;4;4;6;8;9;10]`;;
170 mem_conv_univ (PURE_REWRITE_CONV[ARITH_EQ]) tm;;
172 test 100 (mem_conv_univ (REWRITE_CONV[ARITH_EQ])) tm;; (* 0.176 *)
173 test 100 (REWRITE_CONV[MEM; ARITH_EQ]) tm;; (* 0.352 *)
177 (**********************************)
179 (* FILTER conversions *)
181 let FILTER_A_EMPTY = prove(`FILTER (P:A->bool) [] = []`, REWRITE_TAC[FILTER]) and
182 FILTER_A_HD = UNDISCH_ALL (prove(`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`, SIMP_TAC[FILTER])) and
183 FILTER_A_TL = UNDISCH_ALL (prove(`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`, SIMP_TAC[FILTER]));;
187 let filter_conv_univ p_conv tm =
188 let ltm, list_tm = dest_comb tm in
189 let p_tm = rand ltm in
190 let p_ty = type_of p_tm in
191 let ty = (hd o snd o dest_type) p_ty in
192 let inst_t = INST_TYPE[ty, aty] in
193 let filter_empty, filter_hd, filter_tl =
194 inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in
195 let p_var = mk_var("P", p_ty) in
196 let h_var = mk_var("h", ty) in
197 let t_var = mk_var("t", mk_type("list",[ty])) in
199 let rec filter_conv_raw = fun list_tm ->
200 if (is_comb list_tm) then
201 let ltm, t_tm = dest_comb list_tm in
202 let h_tm = rand ltm in
203 let p_th = p_conv (mk_comb(p_tm, h_tm)) in
204 if (rand(concl p_th) = t_const) then
205 let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in
206 let th0 = MY_PROVE_HYP p_th th0' in
207 let ltm = rator(rand(concl th0)) in
208 let th1 = filter_conv_raw t_tm in
209 TRANS th0 (AP_TERM ltm th1)
211 let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in
212 let th0 = MY_PROVE_HYP p_th th0' in
213 let th1 = filter_conv_raw t_tm in
216 INST[p_tm, p_var] filter_empty in
218 filter_conv_raw list_tm;;
224 let tm = `FILTER (\n. n = 2 \/ n = 3) [1;2;3;4;2;3;1]`;;
226 REWRITE_CONV[FILTER; ARITH_EQ] tm;;
227 filter_conv_univ (REWRITE_CONV[ARITH_EQ]) tm;;
229 test 100 (REWRITE_CONV[FILTER; ARITH_EQ]) tm;; (* 7.596 *)
230 test 100 (filter_conv_univ (REWRITE_CONV[ARITH_EQ])) tm;; (* 0.236 *)
233 (***************************)
235 (* FLATTEN conversions *)
237 let FLATTEN_A_EMPTY = prove(`FLATTEN ([]:((A)list)list) = []`, REWRITE_TAC[FLATTEN; ITLIST; APPEND]) and
238 FLATTEN_A_CONS_EMPTY = prove(`FLATTEN (CONS ([]:(A)list) tt) = FLATTEN tt`, REWRITE_TAC[FLATTEN; ITLIST; APPEND]) and
239 FLATTEN_A_CONS_CONS = prove(`FLATTEN (CONS (CONS (h:A) t) tt) = CONS h (FLATTEN (CONS t tt))`, REWRITE_TAC[FLATTEN; ITLIST; APPEND]);;
243 (* Works for any list of lists *)
244 let flatten_conv_univ tm =
245 let list_list_tm = rand tm in
246 let list_list_ty = type_of list_list_tm in
247 let list_ty = (hd o snd o dest_type) list_list_ty in
248 let ty = (hd o snd o dest_type) list_ty in
249 let inst_t = INST_TYPE[ty, aty] in
250 let flatten_empty, flatten_cons_empty, flatten_cons_cons =
251 inst_t FLATTEN_A_EMPTY, inst_t FLATTEN_A_CONS_EMPTY, inst_t FLATTEN_A_CONS_CONS in
252 let tt_var = mk_var("tt", list_list_ty) in
253 let t_var = mk_var("t", list_ty) in
254 let h_var = mk_var("h", ty) in
256 let rec flatten_conv_raw list_list_tm =
257 if (is_comb list_list_tm) then
258 let hh_tm', tt_tm = dest_comb list_list_tm in
259 let hh_tm = rand hh_tm' in
260 if (is_comb hh_tm) then
261 let h_tm', t_tm = dest_comb hh_tm in
262 let h_tm = rand h_tm' in
263 let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] flatten_cons_cons in
264 let ltm, rtm = dest_comb(rand(concl th0)) in
265 let th1 = AP_TERM ltm (flatten_conv_raw (rand rtm)) in
268 let th0 = INST[tt_tm, tt_var] flatten_cons_empty in
269 let th1 = flatten_conv_raw tt_tm in
274 flatten_conv_raw list_list_tm;;
278 let tm = `FLATTEN [[1;2;3];[3];[4;5;2;1;6;7]]`;;
279 flatten_conv_univ tm;;
280 REWRITE_CONV[FLATTEN; ITLIST; APPEND] tm;;
282 test 100 (REWRITE_CONV[FLATTEN; ITLIST; APPEND]) tm;; (* 0.348 *)
283 test 100 (flatten_conv_univ) tm;; (* 0.028 *)
287 (***************************)
289 (* MAP conversions *)
292 let MAP_AB_EMPTY = prove(`MAP (f:A->B) [] = []`, REWRITE_TAC[MAP]) and
293 MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
296 let map_conv_univ f_conv tm =
297 let ltm, list_tm = dest_comb tm in
298 let ftm = rand ltm in
299 let ftm_ty = type_of ftm in
300 let f_var = mk_var("f", ftm_ty) in
301 let [a_type; b_type] = snd(dest_type ftm_ty) in
302 let h_var = mk_var("h", a_type) in
303 let t_var = mk_var("t", mk_type("list", [a_type])) in
304 let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in
305 let map_empty, map_cons =
306 inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in
308 let rec map_conv_raw list_tm =
309 if (is_comb list_tm) then
310 let h_tm', t_tm = dest_comb list_tm in
311 let h_tm = rand h_tm' in
312 let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in
313 let ltm, rtm = dest_comb (rand(concl th0)) in
314 let cons_tm, f_h_tm = dest_comb ltm in
315 let f_h_th = f_conv f_h_tm in
316 let map_t_th = map_conv_raw t_tm in
317 TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th))
321 map_conv_raw list_tm;;
325 let tm = `MAP (\x. x + 1) [1;2;3;4;5;6;7;8;9;10;11]`;;
327 REWRITE_CONV[MAP] tm;;
328 map_conv_univ BETA_CONV tm;;
330 test 100 (REWRITE_CONV[MAP]) tm;; (* 0.464 *)
331 test 100 (map_conv_univ BETA_CONV) tm;; (* 0.04 *)
333 test 100 (map_conv_univ (BETA_CONV THENC NUM_ADD_CONV)) tm;; (* 0.096 *)
337 (*****************************************)
342 let ALL_A_HD = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL])) and
343 ALL_A_TL = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]));;
346 (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *)
348 let ltm, list_tm = dest_comb (concl th) in
349 let p_tm = rand ltm in
350 let list_ty = type_of list_tm in
351 let p_ty = type_of p_tm in
352 let ty = (hd o snd o dest_type) list_ty in
353 let p_var = mk_var("P", p_ty) in
354 let h_var = mk_var("h", ty) in
355 let t_var = mk_var("t", list_ty) in
357 let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
358 let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
360 let rec get_all_raw all_th list_tm =
361 if (is_comb list_tm) then
362 let h_tm', t_tm = dest_comb list_tm in
363 let h_tm = rand h_tm' in
364 let inst_t = INST[h_tm, h_var; t_tm, t_var] in
365 let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
366 let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
367 th_hd :: get_all_raw th_tl t_tm
371 get_all_raw th list_tm;;
375 (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in)
376 where i1,...,in are given indices.
377 The list of indices should be sorted *)
378 let select_all th indices =
379 let ltm, list_tm = dest_comb (concl th) in
380 let p_tm = rand ltm in
381 let list_ty = type_of list_tm in
382 let p_ty = type_of p_tm in
383 let ty = (hd o snd o dest_type) list_ty in
384 let p_var = mk_var("P", p_ty) in
385 let h_var = mk_var("h", ty) in
386 let t_var = mk_var("t", list_ty) in
388 let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
389 let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
391 let rec get_all_raw all_th list_tm indices n =
395 let h_tm', t_tm = dest_comb list_tm in
396 let h_tm = rand h_tm' in
397 let inst_t = INST[h_tm, h_var; t_tm, t_var] in
398 let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
401 let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
402 th_hd :: get_all_raw th_tl t_tm is (n + 1)
404 get_all_raw th_tl t_tm (i::is) (n + 1) in
406 get_all_raw th list_tm indices 0;;
410 let tm = `ALL (\x. x > 3) [4; 5; 8; 10; 5; 4]`;;
411 let th = (EQT_ELIM o REWRITE_CONV[ALL; ARITH]) tm;;
414 test 100 (CONJUNCTS o REWRITE_RULE[ALL]) th;;
416 test 100 (get_all) th;;
418 test 100 (select_all th) [2;3;4];;
423 (*************************************)
425 (* list_sum conversions *)
428 let LIST_SUM_A_EMPTY = prove(`list_sum [] (f:A->real) = &0`, REWRITE_TAC[list_sum; ITLIST]) and
429 LIST_SUM_A_H = prove(`list_sum [h:A] f = f h`, REWRITE_TAC[list_sum; ITLIST; REAL_ADD_RID]) and
430 LIST_SUM_A_CONS = prove(`list_sum (CONS (h:A) t) f = f h + list_sum t f`, REWRITE_TAC[list_sum; ITLIST]);;
433 let list_sum_conv f_conv tm =
434 let ltm, f_tm = dest_comb tm in
435 let list_tm = rand ltm in
436 let list_ty = type_of list_tm in
437 let f_ty = type_of f_tm in
438 let ty = (hd o snd o dest_type) list_ty in
439 let f_var = mk_var("f", f_ty) and
440 h_var = mk_var("h", ty) and
441 t_var = mk_var("t", list_ty) in
442 let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in
443 let list_sum_h = inst_t LIST_SUM_A_H and
444 list_sum_cons = inst_t LIST_SUM_A_CONS in
446 let rec list_sum_conv_raw = fun h_tm t_tm ->
447 if (is_comb t_tm) then
448 let h_tm', t_tm' = dest_comb t_tm in
449 let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in
450 let ltm, rtm = dest_comb(rand(concl th0)) in
451 let plus_op, fh_tm = dest_comb ltm in
452 let f_th = f_conv fh_tm in
453 let th1 = list_sum_conv_raw (rand h_tm') t_tm' in
454 let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in
457 let th0 = INST[h_tm, h_var] list_sum_h in
458 let f_th = f_conv (rand(concl th0)) in
461 if (is_comb list_tm) then
462 let h_tm, t_tm = dest_comb list_tm in
463 list_sum_conv_raw (rand h_tm) t_tm
465 inst_t LIST_SUM_A_EMPTY;;
471 let tm = `list_sum [&1; &3; &4; pi; #0.1] cos`;;
473 list_sum_conv ALL_CONV tm;;
476 test 1000 (REWRITE_CONV[list_sum; ITLIST; REAL_ADD_RID]) tm;;
478 test 1000 (list_sum_conv ALL_CONV) tm;;
481 let tm = `list_sum [&1; &3; &4; pi; #0.1] (\x. cos x)`;;
483 test 1000 (list_sum_conv BETA_CONV) tm;;
488 (*****************************************)
490 (* set_of_list conversions *)
492 let SET_OF_LIST_A_EMPTY = prove(`set_of_list ([]:(A)list) = {}`, REWRITE_TAC[set_of_list]) and
493 SET_OF_LIST_A_H = prove(`set_of_list [h:A] = {h}`, REWRITE_TAC[set_of_list]) and
494 SET_OF_LIST_A_CONS = prove(`set_of_list (CONS (h:A) t) = h INSERT set_of_list t`, REWRITE_TAC[set_of_list]);;
498 let set_of_list_conv tm =
499 let list_tm = rand tm in
500 let list_ty = type_of list_tm in
501 let ty = (hd o snd o dest_type) list_ty in
502 let h_var = mk_var("h", ty) in
503 let t_var = mk_var("t", list_ty) in
504 let inst_t = INST_TYPE[ty, aty] in
505 let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in
507 let rec set_of_list_conv_raw = fun h_tm t_tm ->
508 if (is_comb t_tm) then
509 let h_tm', t_tm' = dest_comb t_tm in
510 let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in
511 let ltm, rtm = dest_comb(rand(concl th0)) in
512 TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm'))
514 INST[h_tm, h_var] set_of_list_h in
516 if (is_comb list_tm) then
517 let h_tm, t_tm = dest_comb list_tm in
518 set_of_list_conv_raw (rand h_tm) t_tm
520 inst_t SET_OF_LIST_A_EMPTY;;
525 let tm = `set_of_list [&1; &5; &6; &3; &5; &8; &9]`;;
528 test 1000 (REWRITE_CONV[set_of_list]) tm;;
530 test 1000 set_of_list_conv tm;;