1 (* =========================================================== *)
2 (* Efficient formal list conversions *)
3 (* Author: Alexey Solovyev *)
5 (* =========================================================== *)
7 needs "../formal_lp/hypermap/arith_link.hl";;
9 needs "Examples/seq-compiled.hl";;
11 module type List_conversions_sig =
14 val eval_pair_eq_univ : (term -> thm) * (term -> thm) -> term -> term -> thm
15 val pair_eq_conv_univ : (term -> thm) * (term -> thm) -> term -> thm
16 val eval_pair_eq_num : term -> term -> thm
17 val pair_eq_conv_num : term -> thm
19 val eval_hd : term -> thm
20 val hd_conv : term -> thm
22 val eval_el : term -> term -> thm
23 val el_conv : term -> thm
25 val fst_conv : term -> thm
26 val snd_conv : term -> thm
28 val eval_length : term -> thm
29 val length_conv : term -> thm
31 val eval_zip : term -> term -> thm
33 val all_conv_univ : (term -> thm) -> term -> thm
35 val all2_conv_univ : (term -> thm) -> term -> thm
37 val eval_mem_univ : (term -> thm) -> term -> term -> thm
38 val mem_conv_univ : (term -> thm) -> term -> thm
40 val filter_conv_univ : (term -> thm) -> term -> thm
42 val map_conv_univ : (term -> thm) -> term -> thm
44 val get_all : thm -> thm list
45 val select_all : thm -> int list -> thm list
47 val eval_set_of_list : term -> thm
48 val set_of_list_conv : term -> thm
50 val eval_flatten : term -> thm
51 val flatten_conv : term -> thm
53 val eval_uniq_univ : (term -> thm) -> term -> thm
54 val uniq_conv_univ : (term -> thm) -> term -> thm
56 val eval_undup_univ : (term -> thm) -> term -> thm
57 val undup_conv_univ : (term -> thm) -> term -> thm
59 val eval_cat : term -> term -> thm
60 val cat_conv : term -> thm
62 val eval_butlast_last : term -> thm * thm
64 val eval_take : term -> term -> thm
65 val eval_drop : term -> term -> thm
66 val eval_take_drop : term -> term -> thm * thm
68 val eval_rot : term -> term -> thm
69 val eval_rot1 : term -> thm
70 val eval_rotr1 : term -> thm
72 val eval_index_univ : (term -> thm) -> term -> term -> thm
73 val index_conv_univ : (term -> thm) -> term -> thm
77 module List_conversions : List_conversions_sig = struct
85 let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
86 let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
87 let TO_NUM = REWRITE_RULE[Arith_hash.NUM_THM] o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
88 let to_num = rand o concl o TO_NUM;;
92 (***********************************************)
95 let PAIR_EQ_TT = (MY_RULE o prove)(`(n = x <=> T) /\ (m = y <=> T) ==> (n:A,m:B = x,y <=> T)`, SIMP_TAC[PAIR_EQ]) and
96 PAIR_NEQ_FST = (MY_RULE o prove)(`(n = x <=> F) ==> (n:A,m:B = x,y <=> F)`, SIMP_TAC[PAIR_EQ]) and
97 PAIR_NEQ_SND = (MY_RULE o prove)(`(m = y <=> F) ==> (n:A,m:B = x,y <=> F)`, SIMP_TAC[PAIR_EQ]);;
100 let eval_pair_eq_univ (eq1_f, eq2_f) p1_tm p2_tm =
101 if (p1_tm = p2_tm) then
102 EQT_INTRO (REFL p1_tm)
104 let n_tm, m_tm = dest_pair p1_tm in
105 let x_tm, y_tm = dest_pair p2_tm in
106 let ty1 = type_of n_tm and
107 ty2 = type_of m_tm in
108 let n_var, m_var = mk_var("n", ty1), mk_var("m", ty2) and
109 x_var, y_var = mk_var("x", ty1), mk_var("y", ty2) in
110 let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
111 let inst = INST[n_tm, n_var; m_tm, m_var; x_tm, x_var; y_tm, y_var] in
112 let fst_th = eq1_f (mk_eq (n_tm, x_tm)) in
113 if (rand(concl fst_th) = f_const) then
114 MY_PROVE_HYP fst_th ((inst o inst_t) PAIR_NEQ_FST)
116 let snd_th = eq2_f (mk_eq (m_tm, y_tm)) in
117 if (rand(concl snd_th) = f_const) then
118 MY_PROVE_HYP snd_th ((inst o inst_t) PAIR_NEQ_SND)
120 let th0 = (inst o inst_t) PAIR_EQ_TT in
121 MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0);;
124 let pair_eq_conv_univ (eq1_f, eq2_f) eq_tm =
125 let lhs, rhs = dest_eq eq_tm in
126 eval_pair_eq_univ (eq1_f, eq2_f) lhs rhs;;
129 let eval_pair_eq_num =
130 let inst_t = INST_TYPE[num_type, aty; num_type, bty] in
131 let pair_eq, pair_neq_fst, pair_neq_snd =
132 inst_t PAIR_EQ_TT, inst_t PAIR_NEQ_FST, inst_t PAIR_NEQ_SND in
134 if (p1_tm = p2_tm) then
135 EQT_INTRO (REFL p1_tm)
137 let n_tm, m_tm = dest_pair p1_tm in
138 let x_tm, y_tm = dest_pair p2_tm in
139 let inst = INST[n_tm, n_var_num; m_tm, m_var_num; x_tm, x_var_num; y_tm, y_var_num] in
140 let fst_th = raw_eq_hash_conv (mk_eq (n_tm, x_tm)) in
141 if (rand(concl fst_th) = f_const) then
142 MY_PROVE_HYP fst_th (inst pair_neq_fst)
144 let snd_th = raw_eq_hash_conv (mk_eq (m_tm, y_tm)) in
145 if (rand(concl snd_th) = f_const) then
146 MY_PROVE_HYP snd_th (inst pair_neq_snd)
148 let th0 = inst pair_eq in
149 MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0);;
152 let pair_eq_conv_num eq_tm =
153 let lhs, rhs = dest_eq eq_tm in
154 eval_pair_eq_num lhs rhs;;
158 (******************************)
162 let HD_A_CONS = prove(`HD (CONS (h:A) t) = h`, REWRITE_TAC[HD]);;
164 (* Takes a term `[a;...]` and returns the theorem |- HD [a;...] = a *)
165 let eval_hd list_tm =
166 let ltm, t_tm = dest_comb list_tm in
167 let h_tm = rand ltm in
168 let list_ty = type_of t_tm and
170 let h_var = mk_var("h", ty) and
171 t_var = mk_var("t", list_ty) in
172 (INST[h_tm, h_var; t_tm, t_var] o INST_TYPE[ty, aty]) HD_A_CONS;;
174 (* Takes a term `HD [a;...]` and returns the theorem |- HD [a;...] = a *)
176 if (fst o dest_const o rator) hd_tm <> "HD" then failwith "hd_conv"
177 else eval_hd (rand hd_tm);;
181 (*********************************)
184 let EL_0' = (MY_RULE_NUM o prove)(`EL 0 (CONS (h:A) t) = h`, REWRITE_TAC[EL; HD]);;
185 let EL_n' = (MY_RULE_NUM o prove)(`0 < n /\ PRE n = m ==> EL n (CONS (h:A) t) = EL m t`,
186 STRIP_TAC THEN SUBGOAL_THEN `n = SUC m` ASSUME_TAC THENL
187 [ REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC ] THEN ASM_REWRITE_TAC[EL; TL]);;
190 (* Takes a raw numeral term and a list term and returns the theorem |- EL n [...] = x *)
191 let eval_el n_tm list_tm =
192 let list_ty = type_of list_tm in
193 let ty = (hd o snd o dest_type) list_ty in
194 let inst_t = INST_TYPE[ty, aty] in
195 let el_0, el_n = inst_t EL_0', inst_t EL_n' in
196 let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
198 let rec el_conv_raw = fun n_tm list_tm ->
199 let h_tm, t_tm = dest_cons list_tm in
200 let inst0 = INST[h_tm, h_var; t_tm, t_var] in
201 if n_tm = zero_const then
204 let n_gt0 = (EQT_ELIM o raw_gt0_hash_conv) n_tm in
205 let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
206 let m_tm = (rand o concl) pre_n in
207 let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o
208 INST[n_tm, n_var_num; m_tm, m_var_num] o inst0) el_n in
209 let th1 = el_conv_raw m_tm t_tm in
211 el_conv_raw n_tm list_tm;;
215 (* Takes a term `EL n [...]` and returns the theorem |- EL n [...] = x *)
216 (* Note: n must be a raw numeral term Dx (Dy ... _0) *)
218 let ltm, list_tm = dest_comb el_tm in
219 let el, n_tm = dest_comb ltm in
220 if (fst o dest_const) el <> "EL" then failwith "el_conv"
221 else eval_el n_tm list_tm;;
225 (*******************************)
226 (* FST, SND conversions *)
228 let FST' = ISPECL[`x:A`; `y:B`] FST;;
229 let SND' = ISPECL[`x:A`; `y:B`] SND;;
232 let x_tm, y_tm = dest_pair (rand tm) in
233 let x_ty, y_ty = type_of x_tm, type_of y_tm in
234 let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
235 (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';;
238 let x_tm, y_tm = dest_pair (rand tm) in
239 let x_ty, y_ty = type_of x_tm, type_of y_tm in
240 let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
241 (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';;
245 (******************************)
246 (* LENGTH conversions *)
248 let LENGTH_0' = (MY_RULE_NUM o prove) (`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and
249 LENGTH_CONS' = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);;
251 (* Takes a term `[...]` and returns the theorem |- LENGTH [...] = n *)
252 let eval_length list_tm =
253 let list_ty = type_of list_tm in
254 let ty = (hd o snd o dest_type) list_ty in
255 let inst_t = INST_TYPE[ty, aty] in
256 let length_empty, length_cons = inst_t LENGTH_0', inst_t LENGTH_CONS' in
257 let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
259 let rec length_conv_raw = fun list_tm ->
260 if (is_comb list_tm) then
261 let ltm, t_tm = dest_comb list_tm in
262 let h_tm = rand ltm in
263 let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in
264 let th1' = length_conv_raw t_tm in
265 let th1 = AP_TERM suc_op_num th1' in
266 let th2 = raw_suc_conv_hash (rand(concl th1)) in
267 TRANS (TRANS th0 th1) th2
270 length_conv_raw list_tm;;
273 (* Takes a term `LENGTH [...]` and returns the theorem |- LENGTH [...] = n *)
274 let length_conv length_tm =
275 if (fst o dest_const o rator) length_tm <> "LENGTH" then failwith "length_conv"
276 else eval_length (rand length_tm);;
281 (************************)
284 let ZIP_0' = prove(`ZIP ([]:(A)list) ([]:(B)list) = []`, REWRITE_TAC[ZIP]) and
285 ZIP_CONS' = prove(`ZIP (CONS (h1:A) t1) (CONS (h2:B) t2) = CONS (h1, h2) (ZIP t1 t2)`,
288 let eval_zip list1_tm list2_tm =
289 let list1_ty = type_of list1_tm and
290 list2_ty = type_of list2_tm in
291 let ty1 = (hd o snd o dest_type) list1_ty and
292 ty2 = (hd o snd o dest_type) list2_ty in
293 let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
294 let zip0, zip_cons = inst_t ZIP_0', inst_t ZIP_CONS' in
295 let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
296 h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) in
298 let rec zip_conv_rec = fun list1_tm list2_tm ->
299 if (is_comb list1_tm) then
300 let ltm1, t1_tm = dest_comb list1_tm and
301 ltm2, t2_tm = dest_comb list2_tm in
302 let h1_tm, h2_tm = rand ltm1, rand ltm2 in
303 let th0 = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var] zip_cons in
304 let cons_tm = (rator o rand o concl) th0 in
305 let th1' = zip_conv_rec t1_tm t2_tm in
306 let th1 = AP_TERM cons_tm th1' in
310 zip_conv_rec list1_tm list2_tm;;
317 let ALL_0' = prove(`ALL P ([]:(A)list) <=> T`, REWRITE_TAC[ALL]) and
318 ALL_CONS_T' = (MY_RULE o prove)(`(P h <=> T) /\ (ALL P t <=> T) ==> (ALL P (CONS (h:A) t) <=> T)`,
319 REWRITE_TAC[ALL]) and
320 ALL_CONS_F2' = (MY_RULE o prove)(`(ALL P t <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
322 ALL_CONS_F1' = (MY_RULE o prove)(`(P h <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
326 (* Note: p_conv should return theorems of the form |- P a <=> T *)
327 let all_conv_univ p_conv tm =
328 let ltm, list_tm = dest_comb tm in
329 let p_tm = rand ltm in
331 let list_ty = type_of list_tm and
332 p_ty = type_of p_tm in
333 let ty = (hd o snd o dest_type) list_ty in
334 let inst_t = INST_TYPE[ty, aty] in
336 let all_0, all_t, all_f1, all_f2 = inst_t ALL_0', inst_t ALL_CONS_T',
337 inst_t ALL_CONS_F1', inst_t ALL_CONS_F2' in
338 let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) and
339 p_var = mk_var("P", p_ty) in
341 let rec all_conv_rec = fun list_tm ->
342 if is_comb list_tm then
343 let ltm, t_tm = dest_comb list_tm in
344 let h_tm = rand ltm in
345 let p_th = p_conv (mk_comb (p_tm, h_tm)) in
346 let inst = INST[h_tm, h_var; t_tm, t_var; p_tm, p_var] in
347 if (rand o concl) p_th = t_const then
348 let all_th = all_conv_rec t_tm in
349 if (rand o concl) all_th = t_const then
350 (MY_PROVE_HYP all_th o MY_PROVE_HYP p_th o inst) all_t
352 (MY_PROVE_HYP all_th o inst) all_f2
354 (MY_PROVE_HYP p_th o inst) all_f1
356 INST[p_tm, p_var] all_0 in
357 all_conv_rec list_tm;;
361 (*******************)
362 (* ALL2 conversion *)
363 (*******************)
365 let ALL2_0' = prove(`ALL2 P ([]:(A)list) ([]:(B)list) <=> T`, REWRITE_TAC[ALL2]) and
366 ALL2_CONS_T' = (MY_RULE o prove)(`(P h1 h2 <=> T) /\ (ALL2 P t1 t2 <=> T) ==>
367 (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> T)`,
368 REWRITE_TAC[ALL2]) and
369 ALL2_CONS_F2' = (MY_RULE o prove)(`(ALL2 P t1 t2 <=> F) ==>
370 (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
372 ALL2_CONS_F1' = (MY_RULE o prove)(`(P h1 h2 <=> F) ==>
373 (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
377 (* Note: p_conv should return theorems of the form |- P a b <=> T *)
378 let all2_conv_univ p_conv tm =
379 let ltm, list2_tm = dest_comb tm in
380 let ltm2, list1_tm = dest_comb ltm in
381 let p_tm = rand ltm2 in
383 let list1_ty = type_of list1_tm and
384 list2_ty = type_of list2_tm and
385 p_ty = type_of p_tm in
386 let ty1 = (hd o snd o dest_type) list1_ty and
387 ty2 = (hd o snd o dest_type) list2_ty in
388 let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
390 let all2_0, all2_t, all2_f1, all2_f2 = inst_t ALL2_0', inst_t ALL2_CONS_T',
391 inst_t ALL2_CONS_F1', inst_t ALL2_CONS_F2' in
392 let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
393 h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) and
394 p_var = mk_var("P", p_ty) in
396 let rec all2_conv_rec = fun list1_tm list2_tm ->
397 if is_comb list1_tm then
398 let ltm1, t1_tm = dest_comb list1_tm and
399 ltm2, t2_tm = dest_comb list2_tm in
400 let h1_tm, h2_tm = rand ltm1, rand ltm2 in
401 let p_th = p_conv (mk_binop p_tm h1_tm h2_tm) in
402 let inst = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var; p_tm, p_var] in
403 if (rand o concl) p_th = t_const then
404 let all2_th = all2_conv_rec t1_tm t2_tm in
405 if (rand o concl) all2_th = t_const then
406 (MY_PROVE_HYP all2_th o MY_PROVE_HYP p_th o inst) all2_t
408 (MY_PROVE_HYP all2_th o inst) all2_f2
410 (MY_PROVE_HYP p_th o inst) all2_f1
412 if is_comb list2_tm then failwith ("all2_conv_univ: l1 = []; l2 = "^string_of_term list2_tm) else
413 INST[p_tm, p_var] all2_0 in
414 all2_conv_rec list1_tm list2_tm;;
418 (******************************)
419 (* MEM conversions *)
421 let MEM_A_EMPTY = prove(`MEM (x:A) [] <=> F`, REWRITE_TAC[MEM]) and
422 MEM_A_HD = (MY_RULE o prove) (`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`, SIMP_TAC[MEM]) and
423 MEM_A_TL = (MY_RULE o prove) (`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]);;
426 let rec eval_mem_univ eq_conv x_tm list_tm =
427 let ty = type_of x_tm in
428 let inst_t = INST_TYPE[ty, aty] in
429 let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in
430 let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and
431 t_var = mk_var("t", mk_type("list", [ty])) in
433 let rec mem_conv_raw list_tm =
434 if (is_comb list_tm) then
435 let h_tm', t_tm = dest_comb list_tm in
436 let h_tm = rand h_tm' in
437 let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
438 if (rand(concl eq_th) = t_const) then
439 let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in
440 MY_PROVE_HYP eq_th th0'
442 let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in
443 let th0 = MY_PROVE_HYP eq_th th0' in
444 let th1 = mem_conv_raw t_tm in
447 INST[x_tm, x_var] mem_empty in
449 mem_conv_raw list_tm;;
452 let mem_conv_univ eq_conv mem_tm =
453 let ltm, list_tm = dest_comb mem_tm in
454 let c_tm, x_tm = dest_comb ltm in
455 if (fst o dest_const) c_tm <> "MEM" then failwith "mem_conv_univ" else
456 eval_mem_univ eq_conv x_tm list_tm;;
460 (**********************************)
461 (* FILTER conversions *)
463 let FILTER_A_EMPTY = prove(`FILTER (P:A->bool) [] = []`, REWRITE_TAC[FILTER]) and
464 FILTER_A_HD = (MY_RULE o prove) (`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`,
465 SIMP_TAC[FILTER]) and
466 FILTER_A_TL = (MY_RULE o prove) (`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`,
470 let filter_conv_univ p_conv tm =
471 let ltm, list_tm = dest_comb tm in
472 let p_tm = rand ltm in
473 let p_ty = type_of p_tm in
474 let ty = (hd o snd o dest_type) p_ty in
475 let inst_t = INST_TYPE[ty, aty] in
476 let filter_empty, filter_hd, filter_tl =
477 inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in
478 let p_var = mk_var("P", p_ty) in
479 let h_var = mk_var("h", ty) in
480 let t_var = mk_var("t", mk_type("list",[ty])) in
482 let rec filter_conv_raw = fun list_tm ->
483 if (is_comb list_tm) then
484 let ltm, t_tm = dest_comb list_tm in
485 let h_tm = rand ltm in
486 let p_th = p_conv (mk_comb(p_tm, h_tm)) in
487 if (rand(concl p_th) = t_const) then
488 let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in
489 let th0 = MY_PROVE_HYP p_th th0' in
490 let ltm = rator(rand(concl th0)) in
491 let th1 = filter_conv_raw t_tm in
492 TRANS th0 (AP_TERM ltm th1)
494 let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in
495 let th0 = MY_PROVE_HYP p_th th0' in
496 let th1 = filter_conv_raw t_tm in
499 INST[p_tm, p_var] filter_empty in
500 filter_conv_raw list_tm;;
503 (***************************)
504 (* MAP conversions *)
506 let MAP_AB_EMPTY = prove(`MAP (f:A->B) [] = []`, REWRITE_TAC[MAP]) and
507 MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
510 let map_conv_univ f_conv tm =
511 let ltm, list_tm = dest_comb tm in
512 let ftm = rand ltm in
513 let ftm_ty = type_of ftm in
514 let f_var = mk_var("f", ftm_ty) in
515 let [a_type; b_type] = snd(dest_type ftm_ty) in
516 let h_var = mk_var("h", a_type) in
517 let t_var = mk_var("t", mk_type("list", [a_type])) in
518 let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in
519 let map_empty, map_cons =
520 inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in
522 let rec map_conv_raw list_tm =
523 if (is_comb list_tm) then
524 let h_tm', t_tm = dest_comb list_tm in
525 let h_tm = rand h_tm' in
526 let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in
527 let ltm, rtm = dest_comb (rand(concl th0)) in
528 let cons_tm, f_h_tm = dest_comb ltm in
529 let f_h_th = f_conv f_h_tm in
530 let map_t_th = map_conv_raw t_tm in
531 TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th))
535 map_conv_raw list_tm;;
538 (*****************************************)
541 let ALL_A_HD = (MY_RULE o prove) (`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL]) and
542 ALL_A_TL = (MY_RULE o prove) (`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]);;
545 (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *)
547 let ltm, list_tm = dest_comb (concl th) in
548 let p_tm = rand ltm in
549 let list_ty = type_of list_tm in
550 let p_ty = type_of p_tm in
551 let ty = (hd o snd o dest_type) list_ty in
552 let p_var = mk_var("P", p_ty) in
553 let h_var = mk_var("h", ty) in
554 let t_var = mk_var("t", list_ty) in
556 let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
557 let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
559 let rec get_all_raw all_th list_tm =
560 if (is_comb list_tm) then
561 let h_tm', t_tm = dest_comb list_tm in
562 let h_tm = rand h_tm' in
563 let inst_t = INST[h_tm, h_var; t_tm, t_var] in
564 let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
565 let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
566 th_hd :: get_all_raw th_tl t_tm
569 get_all_raw th list_tm;;
573 (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in)
574 where i1,...,in are given indices.
575 The list of indices should be sorted *)
576 let select_all th indices =
577 let ltm, list_tm = dest_comb (concl th) in
578 let p_tm = rand ltm in
579 let list_ty = type_of list_tm in
580 let p_ty = type_of p_tm in
581 let ty = (hd o snd o dest_type) list_ty in
582 let p_var = mk_var("P", p_ty) in
583 let h_var = mk_var("h", ty) in
584 let t_var = mk_var("t", list_ty) in
586 let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
587 let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
589 let rec get_all_raw all_th list_tm indices n =
593 let h_tm', t_tm = dest_comb list_tm in
594 let h_tm = rand h_tm' in
595 let inst_t = INST[h_tm, h_var; t_tm, t_var] in
596 let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
599 let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
600 th_hd :: get_all_raw th_tl t_tm is (n + 1)
602 get_all_raw th_tl t_tm (i::is) (n + 1) in
603 get_all_raw th list_tm indices 0;;
606 (*****************************************)
607 (* set_of_list conversions *)
609 let SET_OF_LIST_A_EMPTY = prove(`set_of_list ([]:(A)list) = {}`, REWRITE_TAC[set_of_list]) and
610 SET_OF_LIST_A_H = prove(`set_of_list [h:A] = {h}`, REWRITE_TAC[set_of_list]) and
611 SET_OF_LIST_A_CONS = prove(`set_of_list (CONS (h:A) t) = h INSERT set_of_list t`, REWRITE_TAC[set_of_list]);;
614 let eval_set_of_list list_tm =
615 let list_ty = type_of list_tm in
616 let ty = (hd o snd o dest_type) list_ty in
617 let h_var = mk_var("h", ty) in
618 let t_var = mk_var("t", list_ty) in
619 let inst_t = INST_TYPE[ty, aty] in
620 let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in
622 let rec set_of_list_conv_raw = fun h_tm t_tm ->
623 if (is_comb t_tm) then
624 let h_tm', t_tm' = dest_comb t_tm in
625 let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in
626 let ltm, rtm = dest_comb(rand(concl th0)) in
627 TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm'))
629 INST[h_tm, h_var] set_of_list_h in
631 if (is_comb list_tm) then
632 let h_tm, t_tm = dest_comb list_tm in
633 set_of_list_conv_raw (rand h_tm) t_tm
635 inst_t SET_OF_LIST_A_EMPTY;;
637 let set_of_list_conv tm =
638 if (fst o dest_const o rator) tm <> "set_of_list" then failwith "set_of_list_conv"
639 else eval_set_of_list (rand tm);;
642 (*****************************************)
643 (* flatten conversions *)
645 let flatten_empty = prove(`flatten ([]:((A)list)list) = []`, REWRITE_TAC[flatten; foldr; cat]) and
646 flatten_cons_empty = prove(`flatten (CONS ([]:(A)list) tt) = flatten tt`, REWRITE_TAC[flatten; foldr; cat]) and
647 flatten_cons_cons = prove(`flatten (CONS (CONS (h:A) t) tt) = CONS h (flatten (CONS t tt))`, REWRITE_TAC[flatten; foldr; cat]);;
650 (* Works for any list of lists *)
651 let eval_flatten list_list_tm =
652 let list_list_ty = type_of list_list_tm in
653 let list_ty = (hd o snd o dest_type) list_list_ty in
654 let ty = (hd o snd o dest_type) list_ty in
655 let inst_t = INST_TYPE[ty, aty] in
656 let flatten_empty, flatten_cons_empty, flatten_cons_cons =
657 inst_t flatten_empty, inst_t flatten_cons_empty, inst_t flatten_cons_cons in
658 let tt_var = mk_var("tt", list_list_ty) in
659 let t_var = mk_var("t", list_ty) in
660 let h_var = mk_var("h", ty) in
662 let rec flatten_conv_raw list_list_tm =
663 if (is_comb list_list_tm) then
664 let hh_tm', tt_tm = dest_comb list_list_tm in
665 let hh_tm = rand hh_tm' in
666 if (is_comb hh_tm) then
667 let h_tm', t_tm = dest_comb hh_tm in
668 let h_tm = rand h_tm' in
669 let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] flatten_cons_cons in
670 let ltm, rtm = dest_comb(rand(concl th0)) in
671 let th1 = AP_TERM ltm (flatten_conv_raw (rand rtm)) in
674 let th0 = INST[tt_tm, tt_var] flatten_cons_empty in
675 let th1 = flatten_conv_raw tt_tm in
680 flatten_conv_raw list_list_tm;;
683 let flatten_conv flatten_tm =
684 if (fst o dest_const o rator) flatten_tm <> "flatten" then failwith "flatten_conv"
685 else eval_flatten (rand flatten_tm);;
688 (********************************)
689 (* uniq conversion *)
691 let uniq_empty = prove(`uniq ([]:(A)list) <=> T`, REWRITE_TAC[uniq]) and
692 uniq_cons_F = (MY_RULE o prove) (`(MEM (h:A) t <=> F) ==> (uniq (CONS h t) <=> uniq t)`, SIMP_TAC[uniq]) and
693 uniq_cons_T = (MY_RULE o prove) (`(MEM (h:A) t <=> T) ==> (uniq (CONS h t) <=> F)`, SIMP_TAC[uniq]);;
696 let eval_uniq_univ eq_conv list_tm =
697 let list_ty = type_of list_tm in
698 let ty = (hd o snd o dest_type) list_ty in
699 let h_var = mk_var("h", ty) in
700 let t_var = mk_var("t", list_ty) in
701 let inst_t = INST_TYPE[ty, aty] in
702 let uniq_empty, uniq_cons_F, uniq_cons_T =
703 inst_t uniq_empty, inst_t uniq_cons_F, inst_t uniq_cons_T in
704 let rec uniq_rec list_tm =
705 if (is_comb list_tm) then
706 let h_tm', t_tm = dest_comb list_tm in
707 let h_tm = rand h_tm' in
708 let inst = INST[h_tm, h_var; t_tm, t_var] in
709 let mem_th = eval_mem_univ eq_conv h_tm t_tm in
710 if (rand (concl mem_th) = t_const) then
711 MY_PROVE_HYP mem_th (inst uniq_cons_T)
713 let th0 = MY_PROVE_HYP mem_th (inst uniq_cons_F) in
714 let th1 = uniq_rec t_tm in
721 let uniq_conv_univ eq_conv tm =
722 if (fst o dest_const o rator) tm <> "uniq" then failwith "uniq_conv"
723 else eval_uniq_univ eq_conv (rand tm);;
726 (**********************************)
727 (* undup conversion *)
729 let undup_empty = prove(`undup ([]:(num)list) = []`, REWRITE_TAC[undup]) and
730 undup_mem_T = (MY_RULE o prove) (`(MEM (h:A) t <=> T) ==> undup (CONS h t) = undup t`, SIMP_TAC[undup]) and
731 undup_mem_F = (MY_RULE o prove) (`(MEM (h:A) t <=> F) ==> undup (CONS h t) = CONS h (undup t)`, SIMP_TAC[undup]);;
734 let eval_undup_univ eq_conv list_tm =
735 let list_ty = type_of list_tm in
736 let ty = (hd o snd o dest_type) list_ty in
737 let h_var = mk_var("h", ty) in
738 let t_var = mk_var("t", list_ty) in
739 let inst_t = INST_TYPE[ty, aty] in
740 let empty, mem_T, mem_F =
741 inst_t undup_empty, inst_t undup_mem_T, inst_t undup_mem_F in
743 let rec undup_rec list_tm =
744 if (is_comb list_tm) then
745 let h_tm', t_tm = dest_comb list_tm in
746 let h_tm = rand h_tm' in
747 let inst = INST[h_tm, h_var; t_tm, t_var] in
748 let mem_th = eval_mem_univ eq_conv h_tm t_tm in
749 if (rand(concl mem_th) = t_const) then
750 let th0 = MY_PROVE_HYP mem_th (inst mem_T) in
751 let th1 = undup_rec t_tm in
754 let th0 = MY_PROVE_HYP mem_th (inst mem_F) in
755 let ltm, rtm = dest_comb (rand(concl th0)) in
756 let th1 = undup_rec (rand rtm) in
757 TRANS th0 (AP_TERM ltm th1)
764 let undup_conv_univ eq_conv tm =
765 if (fst o dest_const o rator) tm <> "undup" then failwith "undup_conv"
766 else eval_undup_univ eq_conv (rand tm);;
769 (**********************************)
772 let cat_empty' = prove(`cat [] (s:(A)list) = s`, REWRITE_TAC[cat]) and
773 cat_cons' = prove(`cat (CONS (h:A) t) s = CONS h (cat t s)`, REWRITE_TAC[cat]);;
776 let eval_cat list1_tm list2_tm =
777 let list_ty = type_of list1_tm in
778 let ty = (hd o snd o dest_type) list_ty in
779 let h_var = mk_var("h", ty) and
780 t_var = mk_var("t", list_ty) and
781 s_var = mk_var("s", list_ty) in
782 let inst_t = INST_TYPE[ty, aty] in
783 let empty, cons = inst_t cat_empty', inst_t cat_cons' in
784 let rec cat_rec list_tm =
785 if (is_comb list_tm) then
786 let h_tm', t_tm = dest_comb list_tm in
787 let h_tm = rand h_tm' in
788 let inst = INST[h_tm, h_var; t_tm, t_var; list2_tm, s_var] in
789 let th0 = inst cons in
790 let ltm = rator (rand (concl th0)) in
791 let th1 = cat_rec t_tm in
792 TRANS th0 (AP_TERM ltm th1)
794 INST[list2_tm, s_var] empty in
800 let ltm, list2_tm = dest_comb tm in
801 let cat, list1_tm = dest_comb ltm in
802 if (fst o dest_const) cat <> "cat" then failwith "cat_conv"
803 else eval_cat list1_tm list2_tm;;
806 (**********************************)
807 (* BUTLAST and LAST conversions *)
809 let last1' = prove(`LAST [h:A] = h`, REWRITE_TAC[LAST]) and
810 last_cons2' = prove(`LAST (CONS (h:A) (CONS h2 s)) = LAST (CONS h2 s)`, REWRITE_TAC[LAST; NOT_CONS_NIL]) and
811 butlast1' = prove(`BUTLAST [h:A] = []`, REWRITE_TAC[BUTLAST]) and
812 butlast_cons2' = prove(`BUTLAST (CONS (h:A) (CONS h2 s)) = CONS h (BUTLAST (CONS h2 s))`,
813 REWRITE_TAC[BUTLAST; NOT_CONS_NIL]);;
816 let eval_butlast_last list_tm =
817 let list_ty = type_of list_tm in
818 let ty = (hd o snd o dest_type) list_ty in
819 let inst_t = INST_TYPE[ty, aty] in
820 let last1, last2 = inst_t last1', inst_t last_cons2' in
821 let butlast1, butlast2 = inst_t butlast1', inst_t butlast_cons2' in
822 let h_var, h2_var, s_var = mk_var("h", ty), mk_var("h2", ty), mk_var("s", list_ty) in
824 let rec butlast_last_rec list_tm =
825 let h_tm', t_tm = dest_comb list_tm in
826 let h_tm = rand h_tm' in
828 let h_tm', s_tm = dest_comb t_tm in
829 let h2_tm = rand h_tm' in
830 let inst = INST[h_tm, h_var; h2_tm, h2_var; s_tm, s_var] in
831 let butlast_th0 = inst butlast2 in
832 let last_th0 = inst last2 in
833 let butlast_th1, last_th1 = butlast_last_rec t_tm in
834 let ltm = (rator o rand o concl) butlast_th0 in
835 TRANS butlast_th0 (AP_TERM ltm butlast_th1), TRANS last_th0 last_th1
837 let inst = INST[h_tm, h_var; t_tm, s_var] in
838 inst butlast1, inst last1 in
840 butlast_last_rec list_tm;;
844 (**********************************)
845 (* take and drop conversions *)
847 let take0' = (MY_RULE_NUM o prove)(`take 0 (s:(A)list) = []`, REWRITE_TAC[take]) and
848 take_nil' = prove(`take n ([]:(A)list) = []`, REWRITE_TAC[take]) and
849 take_pre' = (MY_RULE_NUM o prove)(`!n. (0 < n <=> T) /\ PRE n = m ==> take n (CONS (h:A) s) = CONS h (take m s)`,
850 INDUCT_TAC THEN SIMP_TAC[take; PRE] THEN ARITH_TAC);;
853 let eval_take n_tm list_tm =
854 let list_ty = type_of list_tm in
855 let ty = (hd o snd o dest_type) list_ty in
856 let inst_t = INST_TYPE[ty, aty] in
857 let take0, take_nil, take_pre = inst_t take0', inst_t take_nil', inst_t take_pre' in
858 let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
860 let rec take_rec n_tm list_tm =
861 if is_comb list_tm then
862 if n_tm = zero_const then
863 INST[list_tm, s_var] take0
865 let h_tm', t_tm = dest_comb list_tm in
866 let h_tm = rand h_tm' in
867 let n_gt0 = raw_gt0_hash_conv n_tm in
868 let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
869 let m_tm = (rand o concl) pre_n in
870 let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in
871 let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) take_pre in
872 let ltm = (rator o rand o concl) th0 in
873 let th1 = take_rec m_tm t_tm in
874 TRANS th0 (AP_TERM ltm th1)
876 INST[n_tm, n_var_num] take_nil in
878 take_rec n_tm list_tm;;
882 let drop0' = (MY_RULE_NUM o prove)(`dropl 0 (s:(A)list) = s`, REWRITE_TAC[drop]) and
883 drop_nil' = prove(`dropl n ([]:(A)list) = []`, REWRITE_TAC[drop]) and
884 drop_pre' = (MY_RULE_NUM o prove)(`!n. (0 < n <=> T) /\ PRE n = m ==> dropl n (CONS (h:A) s) = dropl m s`,
885 INDUCT_TAC THEN SIMP_TAC[drop; PRE] THEN ARITH_TAC);;
888 let eval_drop n_tm list_tm =
889 let list_ty = type_of list_tm in
890 let ty = (hd o snd o dest_type) list_ty in
891 let inst_t = INST_TYPE[ty, aty] in
892 let drop0, drop_nil, drop_pre = inst_t drop0', inst_t drop_nil', inst_t drop_pre' in
893 let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
895 let rec drop_rec n_tm list_tm =
896 if is_comb list_tm then
897 if n_tm = zero_const then
898 INST[list_tm, s_var] drop0
900 let h_tm', t_tm = dest_comb list_tm in
901 let h_tm = rand h_tm' in
902 let n_gt0 = raw_gt0_hash_conv n_tm in
903 let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
904 let m_tm = (rand o concl) pre_n in
905 let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in
906 let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) drop_pre in
907 let th1 = drop_rec m_tm t_tm in
910 INST[n_tm, n_var_num] drop_nil in
912 drop_rec n_tm list_tm;;
917 let eval_take_drop n_tm list_tm =
918 let list_ty = type_of list_tm in
919 let ty = (hd o snd o dest_type) list_ty in
920 let inst_t = INST_TYPE[ty, aty] in
921 let drop0, drop_nil, drop_pre = inst_t drop0', inst_t drop_nil', inst_t drop_pre' in
922 let take0, take_nil, take_pre = inst_t take0', inst_t take_nil', inst_t take_pre' in
923 let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
925 let rec take_drop_rec n_tm list_tm =
926 if is_comb list_tm then
927 if n_tm = zero_const then
928 let inst = INST[list_tm, s_var] in
929 inst take0, inst drop0
931 let h_tm', t_tm = dest_comb list_tm in
932 let h_tm = rand h_tm' in
933 let n_gt0 = raw_gt0_hash_conv n_tm in
934 let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
935 let m_tm = (rand o concl) pre_n in
936 let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in
937 let drop_th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) drop_pre in
938 let take_th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) take_pre in
939 let take_th1, drop_th1 = take_drop_rec m_tm t_tm in
940 let take_ltm = (rator o rand o concl) take_th0 in
941 TRANS take_th0 (AP_TERM take_ltm take_th1), TRANS drop_th0 drop_th1
943 let inst = INST[n_tm, n_var_num] in
944 inst take_nil, inst drop_nil in
946 take_drop_rec n_tm list_tm;;
949 (**************************)
952 let rot' = prove(`rot n (s:(A)list) = cat (dropl n s) (take n s)`, REWRITE_TAC[rot]);;
954 let eval_rot n_tm list_tm =
955 let list_ty = type_of list_tm in
956 let ty = (hd o snd o dest_type) list_ty in
957 let s_var = mk_var("s", list_ty) in
958 let inst_t = INST_TYPE[ty, aty] in
959 let take_th, drop_th = eval_take_drop n_tm list_tm in
960 let cat_th = eval_cat (rand (concl drop_th)) (rand (concl take_th)) in
961 let cat_tm = (rator o rator o lhand o concl) cat_th in
962 let th0 = (INST[n_tm, n_var_num; list_tm, s_var] o inst_t) rot' in
963 let th1 = MK_COMB (AP_TERM cat_tm drop_th, take_th) in
964 TRANS (TRANS th0 th1) cat_th;;
967 (*******************************)
968 (* shift_left = rot 1 *)
970 let shift_left_empty' = prove(`rot 1 [] = ([]:(A)list)`, REWRITE_TAC[rot; take; drop; cat]) and
971 shift_left_cons' = prove(`rot 1 (CONS (h:A) s) = cat s [h]`, REWRITE_TAC[rot1_cons; GSYM cats1]);;
974 let eval_rot1 list_tm =
975 let list_ty = type_of list_tm in
976 let ty = (hd o snd o dest_type) list_ty in
977 let inst_t = INST_TYPE[ty, aty] in
978 let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
979 if is_comb list_tm then
980 let h_tm', t_tm = dest_comb list_tm in
981 let h_tm = rand h_tm' in
982 let th0 = (INST[h_tm, h_var; t_tm, s_var] o inst_t) shift_left_cons' in
983 let h_list = (rand o rand o concl) th0 in
984 let th1 = eval_cat t_tm h_list in
987 inst_t shift_left_empty';;
990 (* shift_right = rotr 1 *)
991 let shift_right_empty' = prove(`rotr 1 [] = ([]:(A)list)`, REWRITE_TAC[rotr; rot; take; drop; cat]) and
992 shift_right_cons' = prove(`rotr 1 (CONS (h:A) s) = CONS (LAST (CONS h s)) (BUTLAST (CONS h s))`,
993 MP_TAC (ISPECL [`h:A`; `s:(A)list`] lastI) THEN
994 DISCH_THEN (fun th -> REWRITE_TAC[th; rotr1_rcons]) THEN
995 REWRITE_TAC[GSYM lastI] THEN SPEC_TAC (`h:A`, `h:A`) THEN
996 SPEC_TAC (`s:(A)list`, `s:(A)list`) THEN
997 LIST_INDUCT_TAC THEN REWRITE_TAC[last; belast; last1'; butlast1'] THEN GEN_TAC THEN
998 REWRITE_TAC[last_cons2'; butlast_cons2'] THEN
999 POP_ASSUM (MP_TAC o SPEC `h:A`) THEN
1000 REWRITE_TAC[injectivity "list"]);;
1003 let eval_rotr1 list_tm =
1004 let list_ty = type_of list_tm in
1005 let ty = (hd o snd o dest_type) list_ty in
1006 let inst_t = INST_TYPE[ty, aty] in
1007 let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
1008 if is_comb list_tm then
1009 let h_tm', t_tm = dest_comb list_tm in
1010 let h_tm = rand h_tm' in
1011 let th0 = (INST[h_tm, h_var; t_tm, s_var] o inst_t) shift_right_cons' in
1012 let butlast_th, last_th = eval_butlast_last list_tm in
1013 let cons_tm = (rator o rator o rand o concl) th0 in
1014 TRANS th0 (MK_COMB (AP_TERM cons_tm last_th, butlast_th))
1016 inst_t shift_right_empty';;
1020 (******************************)
1021 (* index conversions *)
1023 let index_empty = (MY_RULE_NUM o prove)(`indexl (x:A) [] = 0`, REWRITE_TAC[index; find]) and
1024 index_cons_eq = (MY_RULE_NUM o prove)(`(x = h <=> T) ==> indexl (x:A) (CONS h t) = 0`,
1025 SIMP_TAC[index; find; pred1]) and
1026 index_cons_neq = (MY_RULE o prove)(`(x = h <=> F) ==> indexl (x:A) (CONS h t) = SUC (indexl x t)`,
1027 SIMP_TAC[index; find; pred1]);;
1030 let rec eval_index_univ eq_conv x_tm list_tm =
1031 let ty = type_of x_tm in
1032 let inst_t = INST_TYPE[ty, aty] in
1033 let index_empty, index_eq, index_neq =
1034 inst_t index_empty, inst_t index_cons_eq, inst_t index_cons_neq in
1035 let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and
1036 t_var = mk_var("t", mk_type("list", [ty])) in
1038 let rec index_rec list_tm =
1039 if (is_comb list_tm) then
1040 let h_tm', t_tm = dest_comb list_tm in
1041 let h_tm = rand h_tm' in
1042 let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
1043 if (rand(concl eq_th) = t_const) then
1044 let th0 = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] index_eq in
1045 MY_PROVE_HYP eq_th th0
1047 let th0 = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] index_neq in
1048 let th1 = MY_PROVE_HYP eq_th th0 in
1049 let th2 = AP_TERM suc_op_num (index_rec t_tm) in
1050 let suc_th = raw_suc_conv_hash (rand (concl th2)) in
1051 TRANS th1 (TRANS th2 suc_th)
1053 INST[x_tm, x_var] index_empty in
1058 let index_conv_univ eq_conv mem_tm =
1059 let ltm, list_tm = dest_comb mem_tm in
1060 let c_tm, x_tm = dest_comb ltm in
1061 if (fst o dest_const) c_tm <> "indexl" then failwith "index_conv_univ" else
1062 eval_index_univ eq_conv x_tm list_tm;;