1 (* Explicit computations for hypermap_of_list *)
9 needs "../formal_lp/ineqs/list_hypermap.hl";;
10 needs "../formal_lp/ineqs/list_conversions.hl";;
13 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;
17 let start = Sys.time() in
24 (* Constants and variables *)
25 let hd_var_num = `hd:num` and
26 h_var_num = `h:num` and
27 h1_var_num = `h1:num` and
28 h2_var_num = `h2:num` and
29 t_var = `t:(num)list` and
30 x_var_pair = `x:num#num` and
31 acc_var = `acc:(num#num)list` and
32 f_var_fun = `f:num#num->num#num`;;
34 let num_type = `:num`;;
35 let num_list_type = `:(num)list`;;
36 let num_list_list_type = `:((num)list)list`;;
38 let mem_const = `MEM:(num#num)->(num#num)list->bool` and
42 let hypermap_of_list_const = `hypermap_of_list:((num)list)list->(num#num)hypermap` and
43 list_of_darts_const = `list_of_darts:((num)list)list->(num#num)list` and
44 list_of_edges_const = `list_of_edges:((num)list)list->((num#num)#(num#num))list` and
45 list_of_faces_const = `list_of_faces:((num)list)list->((num#num)list)list` and
46 list_of_nodes_const = `list_of_nodes:((num)list)list->((num#num)list)list` and
47 list_of_elements_const = `list_of_elements:((num)list)list->(num)list` and
48 list_of_faces3_const = `list_of_faces3:((num)list)list->((num#num)list)list` and
49 list_of_faces4_const = `list_of_faces4:((num)list)list->((num#num)list)list` and
50 list_of_faces5_const = `list_of_faces5:((num)list)list->((num#num)list)list` and
51 list_of_faces6_const = `list_of_faces6:((num)list)list->((num#num)list)list` and
52 list_of_darts3_const = `list_of_darts3:((num)list)list->(num#num)list` and
53 list_of_darts4_const = `list_of_darts4:((num)list)list->(num#num)list` and
54 list_of_dartsX_const = `list_of_dartsX:((num)list)list->(num#num)list` and
55 good_list_const = `good_list:((num)list)list->bool` and
56 good_list_nodes_const = `good_list_nodes:((num)list)list->bool`;;
60 (* example of java style string from hypermap generator. *)
61 let pentstring = "13_150834109178 18 3 0 1 2 3 3 2 7 3 3 0 2 4 5 4 0 3 4 6 1 0 4 3 7 2 8 3 8 2 1 4 8 1 6 9 3 9 6 10 3 10 6 4 3 10 4 5 4 5 3 7 11 3 10 5 11 3 11 7 12 3 12 7 8 3 12 8 9 3 9 10 11 3 11 12 9 ";;
62 let test_string = "149438122187 18 6 0 1 2 3 4 5 4 0 5 6 7 3 6 5 4 3 6 4 8 3 8 4 3 3 8 3 9 3 9 3 2 3 9 2 10 3 10 2 11 3 11 2 1 3 11 1 0 3 11 0 7 3 10 11 7 3 10 7 12 3 12 7 6 3 12 6 8 3 12 8 9 3 9 10 12 ";;
64 (* conversion to list. e.g. convert_to_list pentstring *)
67 let split_sp= Str.split (regexp " +") in
68 let strip_ = global_replace (regexp "_") "" in
69 let rec movelist n (x,a) =
70 if n=0 then (x,a) else match x with y::ys -> movelist (n-1) (ys, y::a) in
71 let getone (x,a) = match x with
73 | y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in
74 let rec getall (x,a) =
75 if (x=[]) then (x,a) else getall (getone (x,a)) in
77 let h::ss = (split_sp (strip_ s)) in
78 let _::ns = map int_of_string ss in
79 let (_,a) = getall (ns,[]) in
84 let create_hol_list str =
85 let ll = snd (convert_to_list str) in
86 let s1 = map (map mk_small_numeral) ll in
87 let s2 = map (fun l -> mk_list (l, num_type)) s1 in
88 mk_list (s2, num_list_type);;
92 (********************************************)
94 (* MEM_CONV and related conversions *)
99 let NUMERAL_EQ = prove(`NUMERAL m = NUMERAL n <=> m = n`, REWRITE_TAC[NUMERAL]) and
100 NUM_EQ_00 = prove(`BIT0 m = BIT0 n <=> m = n`, REWRITE_TAC[BIT0] THEN ARITH_TAC) and
101 NUM_EQ_10 = prove(`BIT1 m = BIT0 n <=> F`, REWRITE_TAC[ARITH]) and
102 NUM_EQ_01 = prove(`BIT0 m = BIT1 n <=> F`, REWRITE_TAC[ARITH]) and
103 NUM_EQ_11 = prove(`BIT1 m = BIT1 n <=> m = n`, REWRITE_TAC[ARITH]) and
104 NUM_EQ_ZERO_B0 = prove(`_0 = BIT0 n <=> _0 = n`, REWRITE_TAC[ARITH]) and
105 NUM_EQ_B0_ZERO = prove(`BIT0 n = _0 <=> n = _0`, REWRITE_TAC[ARITH]) and
106 NUM_EQ_ZERO_B1 = prove(`_0 = BIT1 n <=> F`, REWRITE_TAC[ARITH]) and
107 NUM_EQ_B1_ZERO = prove(`BIT1 n = _0 <=> F`, REWRITE_TAC[ARITH]) and
108 NUM_EQ_ZERO_ZERO = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH]);;
111 let zero_const = `_0` and
112 numeral_const = `NUMERAL` and
113 n_var_num = `n:num` and
114 m_var_num = `m:num`;;
116 let rec raw_num_eq_conv tm =
117 let lhs, rhs = dest_eq tm in
118 if (is_comb lhs) then
119 let bm, m_tm = dest_comb lhs in
120 let bm_c = fst(dest_const bm) in
121 if (is_comb rhs) then
122 let bn, n_tm = dest_comb rhs in
123 let bn_c = fst(dest_const bn) in
124 if (bm_c = bn_c) then
125 let th0 = INST[m_tm, m_var_num; n_tm, n_var_num]
126 (if (bm_c = "BIT0") then NUM_EQ_00 else NUM_EQ_11) in
127 let th1 = raw_num_eq_conv (mk_eq (m_tm, n_tm)) in
130 INST[m_tm, m_var_num; n_tm, n_var_num]
131 (if (bm_c = "BIT0") then NUM_EQ_01 else NUM_EQ_10)
133 if bm_c = "BIT0" then
134 let th0 = INST[m_tm, n_var_num] NUM_EQ_B0_ZERO in
135 let th1 = raw_num_eq_conv (mk_eq (m_tm, zero_const)) in
138 INST[m_tm, n_var_num] NUM_EQ_B1_ZERO
140 if (is_comb rhs) then
141 let bn, n_tm = dest_comb rhs in
142 let bn_c = fst(dest_const bn) in
143 if (bn_c = "BIT0") then
144 let th0 = INST[n_tm, n_var_num] NUM_EQ_ZERO_B0 in
145 let th1 = raw_num_eq_conv (mk_eq (zero_const, n_tm)) in
148 INST[n_tm, n_var_num] NUM_EQ_ZERO_B1
153 let MY_NUM_EQ_CONV tm =
154 let lhs, rhs = dest_eq tm in
155 if lhs = rhs then EQT_INTRO (REFL lhs) else
156 let th0 = INST[rand lhs, m_var_num; rand rhs, n_var_num] NUMERAL_EQ in
157 let ltm, rtm = dest_eq (concl th0) in
159 failwith "MY_NUM_EQ_CONV"
161 TRANS th0 (raw_num_eq_conv rtm);;
164 let tm1 = `65535 = 32767`;;
165 let tm2 = `65535 = 65535`;;
167 test 1000 NUM_EQ_CONV tm1;; (* 0.448 *)
168 test 1000 NUM_EQ_CONV tm2;; (* 0.488 *)
170 test 1000 MY_NUM_EQ_CONV tm1;; (* 0.144 *)
171 test 1000 MY_NUM_EQ_CONV tm2;; (* 0.136 *)
174 (* NUM_PAIR_EQ_CONV *)
176 let NUM_PAIR_EQ = UNDISCH_ALL (prove(`(n:num = x <=> T) ==> (m:num = y <=> T) ==> (n, m = x, y <=> T)`, SIMP_TAC[PAIR_EQ])) and
177 NUM_PAIR_NOT_EQ1 = UNDISCH_ALL (prove(`(n = x <=> F) ==> (n:num,m:num = x,y <=> F)`, SIMP_TAC[PAIR_EQ])) and
178 NUM_PAIR_NOT_EQ2 = UNDISCH_ALL (prove(`(m = y <=> F) ==> (n:num,m:num = x,y <=> F)`, SIMP_TAC[PAIR_EQ]));;
181 let t_const = `T` and f_const = `F` and
182 x_var_num = `x:num` and y_var_num = `y:num`;;
185 let NUM_PAIR_EQ_CONV tm =
186 let lhs, rhs = dest_eq tm in
190 let n_tm, m_tm = dest_pair lhs in
191 let x_tm, y_tm = dest_pair rhs in
192 let inst = INST[n_tm, n_var_num; m_tm, m_var_num; x_tm, x_var_num; y_tm, y_var_num] in
193 let fst_th = MY_NUM_EQ_CONV (mk_eq (n_tm, x_tm)) in
194 if (rand(concl fst_th) = t_const) then
195 let snd_th = MY_NUM_EQ_CONV (mk_eq (m_tm, y_tm)) in
196 if (rand(concl snd_th) = t_const) then
197 let th0 = inst NUM_PAIR_EQ in
198 MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0)
200 let th0 = inst NUM_PAIR_NOT_EQ2 in
201 MY_PROVE_HYP snd_th th0
203 let th0 = inst NUM_PAIR_NOT_EQ1 in
204 MY_PROVE_HYP fst_th th0;;
210 let tm1 = `(12,4) = (12,4)` and
211 tm2 = `(12,4) = (12,5)`;;
213 NUM_PAIR_EQ_CONV tm1;;
214 NUM_PAIR_EQ_CONV tm2;;
215 test 1000 NUM_PAIR_EQ_CONV tm1;; (* 0.016 *)
216 test 1000 NUM_PAIR_EQ_CONV tm2;; (* 0.040 *)
222 let MEM_NUM_EMPTY = prove(`MEM (n:num) [] <=> F`, REWRITE_TAC[MEM]) and
223 MEM_NUM_HD = UNDISCH_ALL (prove(`(n = h <=> T) ==> (MEM (n:num) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
224 MEM_NUM_TL = UNDISCH_ALL (prove(`(n = h <=> F) ==> (MEM (n:num) (CONS h t) <=> MEM n t)`, SIMP_TAC[MEM]));;
227 let h_var_num = `h:num` and
228 t_var_numlist = `t:(num)list`;;
231 let rec MEM_NUM_CONV tm =
232 let ltm, list_tm = dest_comb tm in
233 let n_tm = rand ltm in
234 if (is_comb list_tm) then
235 let h_tm', t_tm = dest_comb list_tm in
236 let h_tm = rand h_tm' in
237 let eq_th = MY_NUM_EQ_CONV (mk_eq (n_tm, h_tm)) in
238 if (rand(concl eq_th) = t_const) then
239 let th0' = INST[n_tm, n_var_num; h_tm, h_var_num; t_tm, t_var_numlist] MEM_NUM_HD in
240 MY_PROVE_HYP eq_th th0'
242 let th0' = INST[n_tm, n_var_num; h_tm, h_var_num; t_tm, t_var_numlist] MEM_NUM_TL in
243 let th0 = MY_PROVE_HYP eq_th th0' in
244 let th1 = MEM_NUM_CONV (rand(concl th0)) in
247 INST[n_tm, n_var_num] MEM_NUM_EMPTY;;
251 (* MEM_NUM_PAIR_CONV *)
253 let MEM_NUM_PAIR_EMPTY = prove(`MEM (n:num#num) [] <=> F`, REWRITE_TAC[MEM]) and
254 MEM_NUM_PAIR_HD = UNDISCH_ALL (prove(`(n = h <=> T) ==> (MEM (n:num#num) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
255 MEM_NUM_PAIR_TL = UNDISCH_ALL (prove(`(n = h <=> F) ==> (MEM (n:num#num) (CONS h t) <=> MEM n t)`, SIMP_TAC[MEM]));;
258 let n_var_numnum = `n:num#num` and
259 h_var_numnum = `h:num#num` and
260 t_var_numnumlist = `t:(num#num)list`;;
263 let rec MEM_NUM_PAIR_CONV tm =
264 let ltm, list_tm = dest_comb tm in
265 let n_tm = rand ltm in
266 if (is_comb list_tm) then
267 let h_tm', t_tm = dest_comb list_tm in
268 let h_tm = rand h_tm' in
269 let eq_th = NUM_PAIR_EQ_CONV (mk_eq (n_tm, h_tm)) in
270 if (rand(concl eq_th) = t_const) then
271 let th0' = INST[n_tm, n_var_numnum; h_tm, h_var_numnum; t_tm, t_var_numnumlist] MEM_NUM_PAIR_HD in
272 MY_PROVE_HYP eq_th th0'
274 let th0' = INST[n_tm, n_var_numnum; h_tm, h_var_numnum; t_tm, t_var_numnumlist] MEM_NUM_PAIR_TL in
275 let th0 = MY_PROVE_HYP eq_th th0' in
276 let th1 = MEM_NUM_PAIR_CONV (rand(concl th0)) in
279 INST[n_tm, n_var_numnum] MEM_NUM_PAIR_EMPTY;;
282 let MEM_REWRITE_CONV = REWRITE_CONV[MEM; PAIR_EQ; ARITH_EQ];;
286 test 1000 MEM_NUM_PAIR_CONV `MEM (1,1) [1,2; 3,4; 2,1]`;; (* 0.140 *)
287 test 1000 MEM_REWRITE_CONV `MEM (1,1) [1,2; 3,4; 2,1]`;; (* 1.276 *)
292 (* LIST_PAIRS_CONV *)
294 let LIST_PAIRS_REWRITE_CONV = REWRITE_CONV[list_pairs; shift_left; APPEND; ZIP];;
297 let list_pairs2 = define `list_pairs2 [] (hd:A) = [] /\
298 list_pairs2 (CONS h []) hd = [h,hd] /\
299 list_pairs2 (CONS h1 (CONS h2 t)) hd = CONS (h1,h2) (list_pairs2 (CONS h2 t) hd)`;;
302 let [list_pairs2_0; list_pairs2_1; list_pairs2_2] = map (INST_TYPE [`:num`, aty]) (CONJUNCTS list_pairs2);;
304 let rec list_pairs2_raw_conv tm =
305 let ltm, h = dest_comb tm in
306 let list = rand ltm in
307 if (is_comb list) then
308 let h_list, t_list = dest_comb list in
309 let h_list = rand h_list in
310 if (is_comb t_list) then
311 let h2,t2 = dest_comb t_list in
313 let th0 = INST[h_list, h1_var_num; h2, h2_var_num; t2, t_var; h, hd_var_num] list_pairs2_2 in
314 let ltm, rtm = dest_comb (rand(concl th0)) in
315 let th1 = list_pairs2_raw_conv rtm in
316 TRANS th0 (AP_TERM ltm th1)
318 INST[h_list, h_var_num; h, hd_var_num] list_pairs2_1
320 INST[h, hd_var_num] list_pairs2_0;;
324 list_pairs2_raw_conv `list_pairs2 [1;2;3;4;5;6] 1`;;
325 test 1000 (list_pairs2_raw_conv) `list_pairs2 [1;2;3;4;5;6] 1`;; (* 0.072 *)
328 let EL_EQ_IMP_EQ = prove(`!l1 l2:(A)list. LENGTH l1 = LENGTH l2 /\
329 (!i. i < LENGTH l1 ==> EL i l1 = EL i l2) ==> l1 = l2`,
330 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; NOT_SUC] THEN
331 REWRITE_TAC[SUC_INJ; injectivity "list"] THEN
332 REPEAT STRIP_TAC THENL
334 FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
335 REWRITE_TAC[LT_0; EL; HD];
338 FIRST_X_ASSUM MATCH_MP_TAC THEN
339 ASM_REWRITE_TAC[] THEN
340 REPEAT STRIP_TAC THEN
341 FIRST_X_ASSUM (MP_TAC o SPEC `SUC i`) THEN
342 ASM_REWRITE_TAC[LT_SUC; EL; TL]);;
345 let LENGTH_LIST_PAIRS2 = prove(`!(x:A) list. LENGTH (list_pairs2 list x) = LENGTH list`,
346 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[list_pairs2; LENGTH] THEN
347 DISJ_CASES_TAC (ISPEC `t:(A)list` list_CASES) THENL
349 ASM_REWRITE_TAC[list_pairs2; LENGTH];
352 FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
353 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
354 ASM_REWRITE_TAC[list_pairs2; LENGTH; SUC_INJ]);;
357 let EL_LIST_PAIRS2 = prove(`!(x:A) list i. i < LENGTH list ==>
358 EL i (list_pairs2 list x) =
359 EL i list, if i = LENGTH list - 1 then x else EL (i + 1) list`,
360 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; LT] THEN
361 REPEAT STRIP_TAC THENL
363 ASM_REWRITE_TAC[] THEN
364 DISJ_CASES_TAC (ISPEC `t:(A)list` list_CASES) THENL
366 ASM_REWRITE_TAC[LENGTH; list_pairs2; EL; HD; ARITH_RULE `SUC 0 - 1 = 0`];
369 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
370 ASM_REWRITE_TAC[LENGTH; list_pairs2; EL; TL; ARITH_RULE `SUC (SUC n) - 1 = SUC n`] THEN
371 FIRST_X_ASSUM (MP_TAC o SPEC `LENGTH (t':(A)list)`) THEN
372 ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC n - 1 = n`; ARITH_RULE `n < SUC n`];
376 DISJ_CASES_TAC (ISPEC `t:(A)list` list_CASES) THENL
378 UNDISCH_TAC `i < LENGTH (t:(A)list)` THEN
379 ASM_REWRITE_TAC[LENGTH; LT];
383 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
384 ASM_REWRITE_TAC[list_pairs2; ARITH_RULE `i + 1 = SUC i`; EL; TL] THEN
386 DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
388 ASM_REWRITE_TAC[EL; HD; LENGTH; ARITH_RULE `~(0 = SUC(SUC n) - 1)`];
392 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
393 ASM_REWRITE_TAC[EL; TL] THEN
394 FIRST_X_ASSUM (MP_TAC o SPEC `n:num`) THEN
395 ASM_REWRITE_TAC[LENGTH; ARITH_RULE `n + 1 = SUC n`; EL; TL] THEN
396 REWRITE_TAC[ARITH_RULE `SUC n = SUC (SUC k) - 1 <=> n = SUC k - 1`] THEN
397 DISCH_THEN MATCH_MP_TAC THEN
398 UNDISCH_TAC `i < LENGTH (t:(A)list)` THEN
399 ASM_REWRITE_TAC[LENGTH; LT_SUC] THEN
403 let LIST_PAIRS2 = prove(`!list:(A)list. list_pairs list = list_pairs2 list (HD list)`,
404 GEN_TAC THEN MATCH_MP_TAC EL_EQ_IMP_EQ THEN
405 REWRITE_TAC[LENGTH_LIST_PAIRS; LENGTH_LIST_PAIRS2] THEN
406 ASM_SIMP_TAC[EL_LIST_PAIRS; EL_LIST_PAIRS2] THEN
407 REPEAT STRIP_TAC THEN
408 COND_CASES_TAC THEN ASM_REWRITE_TAC[EL]);;
411 let LIST_PAIRS_NUM_EMPTY = prove(`list_pairs ([]:(num)list) = []`, CONV_TAC LIST_PAIRS_REWRITE_CONV);;
412 let LIST_PAIRS_NUM_CONS = prove(`list_pairs (CONS (h:num) t) = list_pairs2 (CONS h t) h`, REWRITE_TAC[LIST_PAIRS2; HD]);;
415 let LIST_PAIRS_CONV tm =
416 let list_tm = rand tm in
417 if (is_comb list_tm) then
418 let h_tm', t_tm = dest_comb list_tm in
419 let h_tm = rand h_tm' in
420 let th0 = INST[h_tm, h_var_num; t_tm, t_var_numlist] LIST_PAIRS_NUM_CONS in
421 let th1 = list_pairs2_raw_conv (rand(concl th0)) in
424 LIST_PAIRS_NUM_EMPTY;;
429 let z = `list_pairs [1;2;3;4;5;6]`;;
430 LIST_PAIRS_REWRITE_CONV z;;
431 test 1000 LIST_PAIRS_REWRITE_CONV z;; (* 2.484 *)
434 test 1000 LIST_PAIRS_CONV z;; (* 0.08 *)
438 (***********************************************)
440 (* LIST_OF_FACES_CONV *)
442 let LIST_OF_FACES_REWRITE_CONV = REWRITE_CONV[list_of_faces; MAP; LIST_PAIRS2; list_pairs2; HD];;
444 let LIST_OF_FACES_REWRITE_CONV' = REWRITE_CONV[list_of_faces; MAP; list_pairs; shift_left; APPEND; ZIP];;
447 let y = mk_comb(list_of_faces_const, hol_list);;
448 LIST_OF_FACES_CONV y;;
449 test 10 LIST_OF_FACES_CONV y;; (* 0.304 *)
451 LIST_OF_FACES_CONV2 y;;
452 test 10 LIST_OF_FACES_CONV2 y;; (* 0.172 *)
456 LIST_OF_DARTS_CONV' y;;
457 test 10 LIST_OF_DARTS_CONV' y;; (* 0.920 *)
461 (* LIST_OF_DARTS_CONV *)
462 let LIST_OF_DARTS_REWRITE_CONV = REWRITE_CONV[list_of_darts; ITLIST; list_pairs; shift_left; APPEND; ZIP];;
466 let x = create_hol_list pentstring;;
467 let y = mk_comb (list_of_darts_const, hol_list);;
468 test 10 LIST_OF_DARTS_CONV y;; (* 1.168 *)
472 (**************************************)
475 (* ALL_DISTINCT_CONV *)
476 let ALL_DISTINCT_REWRITE_CONV = REWRITE_CONV[ALL_DISTINCT_ALT; MEM; PAIR_EQ; ARITH];;
479 let ALL_DISTINCT_NUM_PAIR_EMPTY = prove(`ALL_DISTINCT ([]:(num#num)list) <=> T`, REWRITE_TAC[ALL_DISTINCT_ALT]) and
480 ALL_DISTINCT_NUM_PAIR_CONS_F = UNDISCH_ALL (prove(`(MEM (h:num#num) t <=> F) ==> (ALL_DISTINCT (CONS h t) <=> ALL_DISTINCT t)`, SIMP_TAC[ALL_DISTINCT_ALT])) and
481 ALL_DISTINCT_NUM_PAIR_CONS_T = UNDISCH_ALL (prove(`(MEM (h:num#num) t <=> T) ==> (ALL_DISTINCT (CONS h t) <=> F)`, SIMP_TAC[ALL_DISTINCT_ALT]));;
483 let mem_numnum_const = `MEM:(num#num)->(num#num)list->bool`;;
485 let rec ALL_DISTINCT_NUM_PAIR_CONV tm =
486 let list_tm = rand tm in
487 if (is_comb list_tm) then
488 let h_tm', t_tm = dest_comb list_tm in
489 let h_tm = rand h_tm' in
490 let inst = INST[h_tm, h_var_numnum; t_tm, t_var_numnumlist] in
491 let mem_th = MEM_NUM_PAIR_CONV (mk_binop mem_numnum_const h_tm t_tm) in
492 if (rand (concl mem_th) = t_const) then
493 MY_PROVE_HYP mem_th (inst ALL_DISTINCT_NUM_PAIR_CONS_T)
495 let th0 = MY_PROVE_HYP mem_th (inst ALL_DISTINCT_NUM_PAIR_CONS_F) in
496 let th1 = ALL_DISTINCT_NUM_PAIR_CONV (rand(concl th0)) in
499 ALL_DISTINCT_NUM_PAIR_EMPTY;;
503 let z = mk_comb(`ALL_DISTINCT:(num#num)list->bool`, rand(concl (LIST_OF_DARTS_CONV y)));;
504 ALL_DISTINCT_REWRITE_CONV z;;
505 ALL_DISTINCT_NUM_PAIR_CONV z;;
506 test 1 ALL_DISTINCT_REWRITE_CONV z;; (* 0.808 *)
507 test 1 ALL_DISTINCT_NUM_PAIR_CONV z;; (* 0.084 *)
510 (*********************************************)
514 let GOOD_LIST_COND3_EMPTY = prove(`ALL (\d:num#num. MEM (SND d,FST d) list) [] <=> T`, REWRITE_TAC[ALL]);;
515 let GOOD_LIST_COND3_CONS_T = UNDISCH_ALL (prove(`(MEM (y,x) list <=> T) ==>
516 (ALL (\d:num#num. MEM (SND d,FST d) list) (CONS (x,y) t) <=>
517 ALL (\d:num#num. MEM (SND d,FST d) list) t)`, SIMP_TAC[ALL]));;
518 let GOOD_LIST_COND3_CONS_F = UNDISCH_ALL (prove(`(MEM (y,x) list <=> F) ==>
519 (ALL (\d:num#num. MEM (SND d,FST d) list) (CONS (x,y) t) <=>
520 F)`, SIMP_TAC[ALL]));;
522 let list_var_numnumlist = `list:(num#num)list`;;
524 let rec GOOD_LIST_COND3_CONV tm =
525 let ltm, list_tm = dest_comb tm in
526 let f_tm = rand ltm in
527 let list2_tm = rand(snd(dest_abs f_tm)) in
528 if (is_comb list_tm) then
529 let h_tm, t_tm = dest_comb list_tm in
530 let x_tm, y_tm = dest_pair (rand h_tm) in
531 let inst = INST[list2_tm, list_var_numnumlist; x_tm, x_var_num; y_tm, y_var_num; t_tm, t_var_numnumlist] in
532 let mem_th = MEM_NUM_PAIR_CONV (mk_binop mem_numnum_const (mk_pair (y_tm,x_tm)) list2_tm) in
533 if (rand(concl mem_th) = t_const) then
534 let th0 = MY_PROVE_HYP mem_th (inst GOOD_LIST_COND3_CONS_T) in
535 let th1 = GOOD_LIST_COND3_CONV (rand(concl th0)) in
538 MY_PROVE_HYP mem_th (inst GOOD_LIST_COND3_CONS_F)
540 INST[list2_tm, list_var_numnumlist] GOOD_LIST_COND3_EMPTY;;
545 let z = mk_comb(`\ll. !d:num#num. MEM d (list_of_darts ll) ==> MEM (SND d,FST d) (list_of_darts ll)`, x);;
546 let s1 = rand(concl(REWRITE_CONV[darts; ALL_MEM] z));;
547 let s2 = REWRITE_CONV[ALL; MEM] s1;;
548 test 1 (REWRITE_CONV[ALL;MEM]) s1;; (* 1.668 *)
551 GOOD_LIST_COND3_CONV s1;;
552 test 1 GOOD_LIST_COND3_CONV s1;; (* 0.108 *)
558 (*****************************************)
562 let FLATTEN_CLAUSES = prove(`!(h:A) t tt.
563 FLATTEN ([]:((A)list)list) = [] /\
564 FLATTEN (CONS [] tt) = FLATTEN tt /\
565 FLATTEN (CONS (CONS h t) tt) = CONS h (FLATTEN (CONS t tt))`,
566 REPEAT STRIP_TAC THEN REWRITE_TAC[FLATTEN; ITLIST; APPEND]);;
569 let FLATTEN_REWRITE_CONV = REWRITE_CONV[FLATTEN_CLAUSES];;
572 let FLATTEN_NUM_CLAUSES = INST_TYPE[`:num`, aty] (SPEC_ALL FLATTEN_CLAUSES);;
574 let [flatten_0; flatten_01; flatten_11] =
575 CONJUNCTS (FLATTEN_NUM_CLAUSES);;
576 let tt_var_numlistlist = `tt:((num)list)list`;;
577 let h_var_num = `h:num`;;
578 let t_var_numlist = `t:(num)list`;;
582 let rec FLATTEN_NUM_CONV tm =
584 if (is_comb arg) then
585 let hh_tm', tt_tm = dest_comb arg in
586 let hh_tm = rand hh_tm' in
587 if (is_comb hh_tm) then
588 let h_tm', t_tm = dest_comb hh_tm in
589 let h_tm = rand h_tm' in
590 let th0 = INST[h_tm, h_var_num; t_tm, t_var_numlist; tt_tm, tt_var_numlistlist] flatten_11 in
591 let ltm, rtm = dest_comb(rand(concl th0)) in
592 let th1 = AP_TERM ltm (FLATTEN_NUM_CONV rtm) in
595 let th0 = INST[tt_tm, tt_var_numlistlist] flatten_01 in
596 let th1 = FLATTEN_NUM_CONV (rand(concl th0)) in
602 let [flattenA_0; flattenA_01; flattenA_11]
603 = CONJUNCTS (SPEC_ALL FLATTEN_CLAUSES);;
606 (* Works for any list of lists *)
607 let FLATTEN_CONV tm =
608 let tm_ty = hd (snd (dest_type (type_of tm))) in
609 let f0_th = INST_TYPE[tm_ty, aty] flattenA_0 in
610 let f01_th = INST_TYPE[tm_ty, aty] flattenA_01 in
611 let f11_th = INST_TYPE[tm_ty, aty] flattenA_11 in
612 let t_var = mk_var("t", mk_type("list", [tm_ty])) in
613 let tt_var = mk_var("tt", mk_type("list", [type_of t_var])) in
614 let h_var = mk_var("h", tm_ty) in
618 if (is_comb arg) then
619 let hh_tm', tt_tm = dest_comb arg in
620 let hh_tm = rand hh_tm' in
621 if (is_comb hh_tm) then
622 let h_tm', t_tm = dest_comb hh_tm in
623 let h_tm = rand h_tm' in
624 let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] f11_th in
625 let ltm, rtm = dest_comb(rand(concl th0)) in
626 let th1 = AP_TERM ltm (f_conv rtm) in
629 let th0 = INST[tt_tm, tt_var] f01_th in
630 let th1 = f_conv (rand(concl th0)) in
639 let tm = `FLATTEN [[1;2;3]; [4;3;2;1]]`;;
641 test 1000 flatten_conv tm;; (* 0.080 *)
644 test 1000 flatten_conv2 tm;; (* 0.112 *)
646 FLATTEN_REWRITE_CONV tm;;
647 test 1000 FLATTEN_REWRITE_CONV2 tm;; (* 1.11 *)
649 let y = mk_comb(`FLATTEN:((num)list)list->(num)list`, x);;
651 test 100 FLATTEN_CONV y;; (* 0.084 *)
652 test 100 FLATTEN_REWRITE_CONV y;; (* 4.524 *)
656 (**********************************)
658 (* REMOVE_DUPLICATES_CONV *)
659 let remove_duplicates2 = define `remove_duplicates2 [] acc = acc /\
660 remove_duplicates2 (CONS (h:A) t) acc = if (MEM h acc) then remove_duplicates2 t acc
661 else remove_duplicates2 t (CONS h acc)`;;
663 let REMOVE_DUPLICATES_REWRITE_CONV = REWRITE_CONV[REMOVE_DUPLICATES; MEM; ARITH_EQ];;
666 let REMOVE_DUPLICATES_NUM_EMPTY = prove(`REMOVE_DUPLICATES ([]:(num)list) = []`, REWRITE_TAC[REMOVE_DUPLICATES]);;
667 let REMOVE_DUPLICATES_MEM_NUM_T = UNDISCH_ALL(prove(`(MEM (h:num) t <=> T) ==>
668 REMOVE_DUPLICATES (CONS h t) = REMOVE_DUPLICATES t`, SIMP_TAC[REMOVE_DUPLICATES]));;
669 let REMOVE_DUPLICATES_MEM_NUM_F = UNDISCH_ALL(prove(`(MEM (h:num) t <=> F) ==>
670 REMOVE_DUPLICATES (CONS h t) = CONS h (REMOVE_DUPLICATES t)`, SIMP_TAC[REMOVE_DUPLICATES]));;
672 let mem_num_const = `MEM:num->(num)list->bool`;;
675 let rec REMOVE_DUPLICATES_NUM_CONV tm =
676 let list_tm = rand tm in
677 if (is_comb list_tm) then
678 let h_tm', t_tm = dest_comb list_tm in
679 let h_tm = rand h_tm' in
680 let inst = INST[h_tm, h_var_num; t_tm, t_var_numlist] in
681 let mem_th = MEM_NUM_CONV (mk_binop mem_num_const h_tm t_tm) in
682 if (rand(concl mem_th) = t_const) then
683 let th0 = MY_PROVE_HYP mem_th (inst REMOVE_DUPLICATES_MEM_NUM_T) in
684 let th1 = REMOVE_DUPLICATES_NUM_CONV (rand(concl th0)) in
687 let th0 = MY_PROVE_HYP mem_th (inst REMOVE_DUPLICATES_MEM_NUM_F) in
688 let ltm, rtm = dest_comb (rand(concl th0)) in
689 let th1 = REMOVE_DUPLICATES_NUM_CONV rtm in
690 TRANS th0 (AP_TERM ltm th1)
692 REMOVE_DUPLICATES_NUM_EMPTY;;
696 let tm = `REMOVE_DUPLICATES [1;2;3;4;2;1;3]`;;
698 REMOVE_DUPLICATES_REWRITE_CONV tm;;
699 test 10 REMOVE_DUPLICATES_CONV tm;; (* 0.776 *)
701 REMOVE_DUPLICATES_NUM_CONV tm;;
702 test 1000 REMOVE_DUPLICATES_NUM_CONV tm;; (* 0.548 *)
707 let y = mk_comb(list_of_elements_const, hol_list);;
710 let xxx =(REWRITE_CONV[list_of_elements] THENC
711 REWRITE_CONV[FLATTEN; ITLIST; APPEND])
714 let zz = `remove_duplicates2 [1;2;3;4;2;1] []`;;
715 REWRITE_CONV[remove_duplicates2; MEM; ARITH] zz;;
717 let zz = rand(concl xxx);;
719 REMOVE_DUPLICATES_REWRITE_CONV zz;; (* infty *)
720 REMOVE_DUPLICATES_NUM_CONV zz;;
721 test 10 REMOVE_DUPLICATES_NUM_CONV zz;; (* 0.176 *)
727 (**************************************)
729 (* LIST_OF_ELEMENTS_CONV *)
731 let LIST_OF_ELEMENTS_CONV =
732 ONCE_REWRITE_CONV[list_of_elements] THENC
733 ONCE_DEPTH_CONV FLATTEN_CONV THENC
734 REMOVE_DUPLICATES_NUM_CONV;;
737 let y = mk_comb(list_of_elements_const, hol_list);;
738 test 10 LIST_OF_ELEMENTS_CONV y;; (* 0.184 *)
742 (**********************************)
744 (* LIST_OF_NODES_CONV *)
747 let FILTER_NODE_EMPTY = prove(`FILTER (\d:num#num. FST d = x) [] = []`, REWRITE_TAC[FILTER]);;
748 let FILTER_NODE_CONS_EQ = UNDISCH_ALL (prove(`(n = x <=> T) ==> FILTER (\d:num#num. FST d = x) (CONS (n,m) t) =
749 CONS (n,m) (FILTER (\d. FST d = x) t)`, SIMP_TAC[FILTER]));;
750 let FILTER_NODE_CONS_NEQ = UNDISCH_ALL (prove(`(n = x <=> F) ==> FILTER (\d:num#num. FST d = x) (CONS (n,m) t) =
751 FILTER (\d. FST d = x) t`, SIMP_TAC[FILTER]));;
755 let rec FILTER_NODE_CONV tm =
756 let ltm, list_tm = dest_comb tm in
757 let x_tm = (rand o snd o dest_abs o rand) ltm in
758 if (is_comb list_tm) then
759 let h_tm, t_tm = dest_comb list_tm in
760 let n_tm, m_tm = dest_pair (rand h_tm) in
761 let inst = INST[n_tm, n_var_num; m_tm, m_var_num; t_tm, t_var_numnumlist; x_tm, x_var_num] in
762 let eq_th = MY_NUM_EQ_CONV (mk_eq (n_tm, x_tm)) in
763 if (rand(concl eq_th) = t_const) then
764 let th0 = MY_PROVE_HYP eq_th (inst FILTER_NODE_CONS_EQ) in
765 let ltm, rtm = dest_comb (rand(concl th0)) in
766 let th1 = FILTER_NODE_CONV rtm in
767 TRANS th0 (AP_TERM ltm th1)
769 let th0 = MY_PROVE_HYP eq_th (inst FILTER_NODE_CONS_NEQ) in
770 let th1 = FILTER_NODE_CONV (rand(concl th0)) in
773 INST[x_tm, x_var_num] FILTER_NODE_EMPTY;;
778 test 10 LIST_OF_NODES_CONV y;; (* 0.992 *)
783 (****************************************************)
785 (* `node (hypermap_of_list L) x` table construction *)
788 let NODE_HYPERMAP_OF_LIST_EXPLICIT = prove(`!(L:((A)list)list) n d. good_list_nodes L /\
789 MEM n (list_of_nodes L) /\ MEM d n
790 ==> node (hypermap_of_list L) d = set_of_list n`,
791 REWRITE_TAC[good_list_nodes] THEN REPEAT STRIP_TAC THEN
792 SUBGOAL_THEN `set_of_list n IN node_set (hypermap_of_list (L:((A)list)list))` ASSUME_TAC THENL
794 ASM_REWRITE_TAC[IN_SET_OF_LIST; nodes_of_list; MEM_MAP] THEN
795 EXISTS_TAC `n:(A#A)list` THEN
799 MP_TAC (ISPECL [`hypermap_of_list L:(A#A)hypermap`; `set_of_list n:A#A->bool`] Hypermap.lemma_node_representation) THEN
800 ASM_REWRITE_TAC[] THEN
802 ASM_REWRITE_TAC[] THEN
803 MATCH_MP_TAC (GSYM Hypermap.lemma_node_identity) THEN
804 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
805 ASM_REWRITE_TAC[IN_SET_OF_LIST]);;
808 let NODES_HYPERMAP_OF_LIST_ALL = prove(`!(L:((A)list)list). good_list_nodes L ==>
809 ALL (\n. ALL(\d. node (hypermap_of_list L) d = set_of_list n) n) (list_of_nodes L)`,
810 REWRITE_TAC[GSYM ALL_MEM] THEN
811 REPEAT STRIP_TAC THEN
812 MATCH_MP_TAC NODE_HYPERMAP_OF_LIST_EXPLICIT THEN
818 let build_table_of_nodes hyp_list nodes_th =
819 let table_of_nodes = Hashtbl.create 100 in
820 let th0 = (UNDISCH_ALL o ISPEC hyp_list) NODES_HYPERMAP_OF_LIST_ALL in
821 let all_tm = rator (concl th0) in
822 let th1 = EQ_MP (AP_TERM all_tm nodes_th) th0 in
823 let th1_list = get_all th1 in
825 let build1 = fun th ->
826 let th = BETA_RULE th in
827 let list_tm = dest_list(rand(concl th)) in
828 let ths = get_all th in
829 let r = CONV_RULE (BETA_CONV THENC RAND_CONV set_of_list_conv) in
830 map (fun tm, th -> Hashtbl.add table_of_nodes tm (r th)) (zip list_tm ths) in
832 let _ = map build1 th1_list in
839 let hol_list, th_table = compute_all pentstring;;
840 let nodes = Hashtbl.find th_table "nodes";;
843 let MEM_h_CONS_h_t = prove(`!(h:A) t. MEM h (CONS h t)`, REWRITE_TAC[MEM]);;
847 let th = ISPEC hol_list NODES_HYPERMAP_OF_LIST_ALL;;
848 let nodes_th = UNDISCH_ALL (REWRITE_RULE[nodes; ALL; set_of_list] th);;
853 (****************************************************)
855 (* `face (hypermap_of_list L) x` table construction *)
858 let FACE_HYPERMAP_OF_LIST_EXPLICIT = prove(`!(L:((A)list)list) f d. good_list L /\
859 MEM f (list_of_faces L) /\ MEM d f
860 ==> face (hypermap_of_list L) d = set_of_list f`,
861 REPEAT STRIP_TAC THEN
862 MP_TAC (SPECL [`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
863 ASM_REWRITE_TAC[] THEN
864 DISCH_THEN (X_CHOOSE_THEN `x:A#A` STRIP_ASSUME_TAC) THEN
866 SUBGOAL_THEN `MEM (d:A#A) (list_of_darts L)` ASSUME_TAC THENL
868 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
869 EXISTS_TAC `x:A#A` THEN
870 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
874 ASM_SIMP_TAC[FACE_OF_LIST] THEN
876 MATCH_MP_TAC MEM_FIND_FACE_IMP_FACES_EQ THEN
879 UNDISCH_TAC `good_list (L:((A)list)list)` THEN
885 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;
889 let FACES_HYPERMAP_OF_LIST_ALL = prove(`!(L:((A)list)list). good_list L ==>
890 ALL (\f. ALL(\d. face (hypermap_of_list L) d = set_of_list f) f) (list_of_faces L)`,
891 REWRITE_TAC[GSYM ALL_MEM] THEN
892 REPEAT STRIP_TAC THEN
893 MATCH_MP_TAC FACE_HYPERMAP_OF_LIST_EXPLICIT THEN
897 let build_table_of_faces hyp_list good_list_th faces_th =
898 let table_of_faces = Hashtbl.create 100 in
899 let th0 = MY_PROVE_HYP good_list_th ((UNDISCH_ALL o ISPEC hyp_list) FACES_HYPERMAP_OF_LIST_ALL) in
900 let all_tm = rator (concl th0) in
901 let th1 = EQ_MP (AP_TERM all_tm faces_th) th0 in
902 let th1_list = get_all th1 in
904 let build1 = fun th ->
905 let th = BETA_RULE th in
906 let list_tm = dest_list(rand(concl th)) in
907 let ths = get_all th in
908 let r = CONV_RULE (BETA_CONV THENC RAND_CONV set_of_list_conv) in
909 map (fun tm, th -> Hashtbl.add table_of_faces tm (r th)) (zip list_tm ths) in
911 let _ = map build1 th1_list in
921 (********************************************)
923 (* face_map H and inverse (face_map H) tables *)
925 let f_list_ext_table = define `(f_list_ext_table L [] (first:A#A) <=> T)
926 /\ (f_list_ext_table L (CONS h1 (CONS h2 t)) first
927 <=> f_list_ext L h1 = h2 /\
928 inverse (f_list_ext L) h2 = h1 /\
929 f_list_ext_table L (CONS h2 t) first)
930 /\ (f_list_ext_table L [h1] first <=> f_list_ext L h1 = first /\
931 inverse (f_list_ext L) first = h1)`;;
934 let list_to_pair list = hd list, hd(tl list);;
937 let F_LIST_EXT_SINGLE, INV_F_LIST_EXT_SINGLE = (list_to_pair o CONJUNCTS o UNDISCH_ALL)
938 (prove(`f_list_ext_table L [h1:num#num] first
939 ==> f_list_ext L h1 = first /\
940 inverse (f_list_ext L) first = h1`, SIMP_TAC[f_list_ext_table])) and
941 F_LIST_EXT_CONS, INV_F_LIST_EXT_CONS = (list_to_pair o CONJUNCTS o UNDISCH_ALL)
942 (prove(`f_list_ext_table L (CONS (h1:num#num) (CONS h2 t)) first
943 ==> f_list_ext L h1 = h2 /\
944 inverse (f_list_ext L) h2 = h1`, SIMP_TAC[f_list_ext_table])) and
945 F_LIST_EXT_TABLE_CONS = UNDISCH_ALL (prove(`f_list_ext_table L (CONS (h1:num#num) t) first
946 ==> f_list_ext_table L t first`,
947 DISJ_CASES_TAC (ISPEC `t:(num#num)list` list_CASES) THENL
949 ASM_REWRITE_TAC[f_list_ext_table];
950 POP_ASSUM STRIP_ASSUME_TAC THEN
951 ASM_SIMP_TAC[f_list_ext_table]
955 let h1_var = `h1:num#num` and
956 h2_var = `h2:num#num` and
957 t_var = `t:(num#num)list` and
958 first_var = `first:num#num` and
959 l_var = `L:((num)list)list`;;
962 let f_list_ext_table_all th =
963 let ltm, first_tm = dest_comb(concl th) in
964 let ltm, list_tm = dest_comb ltm in
965 let l_tm = rand ltm in
966 let inst_t = INST[l_tm, l_var; first_tm, first_var] in
967 let f_single, inv_f_single = inst_t F_LIST_EXT_SINGLE, inst_t INV_F_LIST_EXT_SINGLE in
968 let f_cons, inv_f_cons = inst_t F_LIST_EXT_CONS, inst_t INV_F_LIST_EXT_CONS in
969 let f_table = inst_t F_LIST_EXT_TABLE_CONS in
971 let rec f_list_raw = fun f_table_th h1_tm t1_tm ->
972 if (is_comb t1_tm) then
973 let h2_tm', t2_tm = dest_comb t1_tm in
974 let h2_tm = rand h2_tm' in
975 let inst_t = MY_PROVE_HYP f_table_th o INST[h1_tm, h1_var; h2_tm, h2_var; t2_tm, t_var] in
977 let f_th, inv_f_th = inst_t f_cons, inst_t inv_f_cons in
978 let th0 = (MY_PROVE_HYP f_table_th o INST[h1_tm, h1_var; t1_tm, t_var]) f_table in
979 let f_list, inv_f_list = f_list_raw th0 h2_tm t2_tm in
980 (h1_tm, f_th) :: f_list, (h2_tm, inv_f_th) :: inv_f_list
983 let inst_t = MY_PROVE_HYP f_table_th o INST[h1_tm, h1_var] in
984 let f_th, inv_f_th = inst_t f_single, inst_t inv_f_single in
985 [h1_tm, f_th], [first_tm, inv_f_th] in
987 if (is_comb list_tm) then
988 let h1_tm, t1_tm = dest_comb list_tm in
989 f_list_raw th (rand h1_tm) t1_tm
996 (**********************)
999 let FIND_FACE_LEMMA_EXPLICIT = prove(`!(L:((A)list)list) f d. good_list L /\
1000 MEM f (list_of_faces L) /\ MEM d f
1001 ==> find_face d L = f`,
1002 REPEAT STRIP_TAC THEN
1003 MP_TAC (SPECL[`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
1004 ASM_REWRITE_TAC[] THEN
1006 UNDISCH_TAC `MEM (d:A#A) f` THEN
1007 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1008 MATCH_MP_TAC MEM_FIND_FACE_IMP_FACES_EQ THEN
1009 UNDISCH_TAC `good_list (L:((A)list)list)` THEN
1010 ASM_SIMP_TAC[good_list]);;
1014 let INVERSE_F_LIST_EXT_LEMMA = prove(`!(L:((A)list)list) d. good_list L ==>
1015 inverse (f_list_ext L) (f_list_ext L d) = d`,
1016 REPEAT STRIP_TAC THEN
1017 ABBREV_TAC `H = hypermap_of_list L:(A#A)hypermap` THEN
1018 MP_TAC (ISPECL [`face_map (H:(A#A)hypermap)`; `dart H:A#A->bool`] PERMUTES_INVERSES) THEN
1019 ASM_SIMP_TAC[Hypermap.hypermap_lemma] THEN
1021 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST]);;
1025 let NEXT_EL_APPEND_lemma = prove(`!l t1 (h:A) h' t2. ALL_DISTINCT l /\
1026 l = CONS h (APPEND t1 (CONS h' t2)) ==>
1027 NEXT_EL h' l = if (t2 = []) then h else HD t2`,
1028 REPEAT STRIP_TAC THEN
1029 REWRITE_TAC[NEXT_EL] THEN
1030 ABBREV_TAC `n1 = LENGTH (t1:(A)list)` THEN
1031 SUBGOAL_THEN `INDEX (h':A) l = SUC n1` ASSUME_TAC THENL
1033 SUBGOAL_THEN `h':A = EL (SUC n1) l` (fun th -> REWRITE_TAC[th]) THENL
1035 ASM_REWRITE_TAC[EL; TL; EL_APPEND; LT_REFL; SUB_REFL; HD];
1038 MATCH_MP_TAC INDEX_EL THEN
1039 ASM_REWRITE_TAC[LENGTH; LENGTH_APPEND] THEN
1043 DISJ_CASES_TAC (ISPEC `t2:(A)list` list_CASES) THENL
1045 ASM_REWRITE_TAC[LENGTH; LENGTH_APPEND; HD] THEN
1049 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1050 ASM_REWRITE_TAC[LENGTH; LENGTH_APPEND; NOT_CONS_NIL; HD] THEN
1051 REWRITE_TAC[ARITH_RULE `~(SUC n1 = SUC (n1 + SUC (SUC n)) - 1)`] THEN
1052 REWRITE_TAC[ARITH_RULE `SUC n1 + 1 = SUC (n1 + 1)`; EL; TL] THEN
1053 ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `~(n1 + 1 < n1)`; ARITH_RULE `(n1 + 1) - n1 = 1`] THEN
1054 REWRITE_TAC[ARITH_RULE `1 = SUC 0`; EL; TL; HD]);;
1059 let F_LIST_EXT_TABLE = prove(`!L:((A)list)list. good_list L
1060 ==> ALL (\f. f_list_ext_table L f (HD f)) (list_of_faces L)`,
1061 REPEAT STRIP_TAC THEN
1062 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
1063 REWRITE_TAC[GSYM ALL_MEM] THEN
1064 X_GEN_TAC `f:(A#A)list` THEN DISCH_TAC THEN
1066 DISJ_CASES_TAC (ISPEC `f:(A#A)list` list_CASES) THENL
1068 ASM_REWRITE_TAC[f_list_ext_table];
1072 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1073 ASM_REWRITE_TAC[HD] THEN
1074 SUBGOAL_THEN `(!t2 t1. t = APPEND t1 t2 ==> f_list_ext_table L t2 (h:A#A)) ==> f_list_ext_table L (CONS h t) h` MP_TAC THENL
1076 DISCH_THEN (MP_TAC o SPECL [`t:(A#A)list`; `[]:(A#A)list`]) THEN
1077 REWRITE_TAC[APPEND] THEN
1078 DISJ_CASES_TAC (ISPEC `t:(A#A)list` list_CASES) THENL
1080 ASM_REWRITE_TAC[f_list_ext_table] THEN
1081 SUBGOAL_THEN `f_list_ext L (h:A#A) = h` ASSUME_TAC THENL
1083 REWRITE_TAC[f_list_ext; res; f_list] THEN
1084 SUBGOAL_THEN `find_face (h:A#A) L = f` ASSUME_TAC THENL
1086 MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1087 ASM_REWRITE_TAC[MEM];
1091 SUBGOAL_THEN `h:A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1093 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE; MEM];
1097 ASM_REWRITE_TAC[NEXT_EL; INDEX; LENGTH; ARITH_RULE `SUC 0 - 1 = 0`; HD];
1100 ASM_REWRITE_TAC[] THEN
1101 FIRST_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1102 MP_TAC (SPECL [`L:((A)list)list`; `h:A#A`] INVERSE_F_LIST_EXT_LEMMA) THEN
1107 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1108 ASM_REWRITE_TAC[f_list_ext_table] THEN
1109 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1111 SUBGOAL_THEN `f_list_ext L h = h':A#A` ASSUME_TAC THENL
1113 REWRITE_TAC[f_list_ext; res; f_list] THEN
1114 SUBGOAL_THEN `find_face (h:A#A) L = f` ASSUME_TAC THENL
1116 MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1117 ASM_REWRITE_TAC[MEM];
1121 SUBGOAL_THEN `h:A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1123 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE; MEM];
1127 ASM_REWRITE_TAC[NEXT_EL; INDEX; LENGTH; ARITH_RULE `~(0 = SUC(SUC n) - 1)`] THEN
1128 REWRITE_TAC[ARITH_RULE `0 + 1 = SUC 0`; EL; TL; HD];
1132 ASM_REWRITE_TAC[] THEN
1133 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1134 ASM_SIMP_TAC[INVERSE_F_LIST_EXT_LEMMA];
1138 DISCH_THEN MATCH_MP_TAC THEN
1139 LIST_INDUCT_TAC THENL
1141 REWRITE_TAC[f_list_ext_table];
1145 REPEAT STRIP_TAC THEN
1147 SUBGOAL_THEN `MEM (h':A#A) f` ASSUME_TAC THENL
1149 ASM_REWRITE_TAC[MEM; MEM_APPEND];
1153 SUBGOAL_THEN `ALL_DISTINCT (f:(A#A)list)` ASSUME_TAC THENL
1155 MATCH_MP_TAC ALL_DISTINCT_FACE THEN
1156 EXISTS_TAC `L:((A)list)list` THEN
1161 UNDISCH_TAC `t = APPEND t1 (CONS (h':A#A) t')` THEN
1162 DISJ_CASES_TAC (ISPEC `t':(A#A)list` list_CASES) THENL
1164 ASM_REWRITE_TAC[f_list_ext_table] THEN DISCH_TAC THEN
1165 SUBGOAL_THEN `f_list_ext L (h':A#A) = h` ASSUME_TAC THENL
1167 REWRITE_TAC[f_list_ext; res; f_list] THEN
1168 SUBGOAL_THEN `find_face (h':A#A) L = f` ASSUME_TAC THENL
1170 MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1175 SUBGOAL_THEN `h':A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1177 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE] THEN
1178 REWRITE_TAC[MEM; MEM_APPEND];
1182 ASM_REWRITE_TAC[] THEN
1183 MP_TAC (ISPECL [`f:(A#A)list`; `t1:(A#A)list`; `h:A#A`; `h':A#A`; `t':(A#A)list`] NEXT_EL_APPEND_lemma) THEN
1188 ASM_REWRITE_TAC[] THEN
1189 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1190 ASM_SIMP_TAC[INVERSE_F_LIST_EXT_LEMMA];
1194 POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1195 ASM_REWRITE_TAC[f_list_ext_table] THEN
1198 SUBGOAL_THEN `f_list_ext L (h':A#A) = h''` ASSUME_TAC THENL
1200 REWRITE_TAC[f_list_ext; res; f_list] THEN
1201 SUBGOAL_THEN `find_face (h':A#A) L = f` ASSUME_TAC THENL
1203 MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1208 SUBGOAL_THEN `h':A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1210 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE] THEN
1211 REWRITE_TAC[MEM; MEM_APPEND];
1215 ASM_REWRITE_TAC[] THEN
1216 MP_TAC (ISPECL [`f:(A#A)list`; `t1:(A#A)list`; `h:A#A`; `h':A#A`; `t':(A#A)list`] NEXT_EL_APPEND_lemma) THEN
1217 ASM_REWRITE_TAC[NOT_CONS_NIL; HD];
1221 ASM_REWRITE_TAC[] THEN
1224 POP_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1225 ASM_SIMP_TAC[INVERSE_F_LIST_EXT_LEMMA];
1229 FIRST_X_ASSUM (MP_TAC o SPEC `APPEND t1 [h':A#A]`) THEN
1230 ASM_REWRITE_TAC[] THEN
1231 DISCH_THEN MATCH_MP_TAC THEN
1233 UNDISCH_TAC `t':(A#A)list = CONS h'' t''` THEN
1234 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1235 REPEAT REMOVE_ASSUM THEN
1236 SPEC_TAC (`t1:(A#A)list`, `t1:(A#A)list`) THEN
1237 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND]);;
1242 let build_f_list_ext_table hol_list good_list_th faces_th =
1243 let f_table, inv_f_table = Hashtbl.create 100, Hashtbl.create 100 in
1244 let th0 = (MY_PROVE_HYP good_list_th o UNDISCH_ALL o ISPEC hol_list) F_LIST_EXT_TABLE in
1245 let all_tm = rator(concl th0) in
1246 let th1 = EQ_MP (AP_TERM all_tm faces_th) th0 in
1247 let th1_list = get_all th1 in
1249 let step = fun th ->
1250 let th = BETA_RULE th in
1251 let ltm, rtm = dest_comb(concl th) in
1252 let first_th = hd_conv rtm in
1253 let f_table_th = EQ_MP (AP_TERM ltm first_th) th in
1254 let f_list, inv_f_list = f_list_ext_table_all f_table_th in
1255 let _ = map (fun tm, th -> Hashtbl.add f_table tm th) f_list in
1256 let _ = map (fun tm, th -> Hashtbl.add inv_f_table tm th) inv_f_list in
1259 let _ = map step th1_list in
1260 f_table, inv_f_table;;
1265 (************************************)
1267 (* Final conversion *)
1270 let compute_all hyp_str =
1271 let thm_table = Hashtbl.create 10 in
1272 let fun_table = Hashtbl.create 10 in
1273 let hol_list = create_hol_list hyp_str in
1274 let faces = LIST_OF_FACES_REWRITE_CONV (mk_comb (list_of_faces_const, hol_list)) in
1275 let LIST_OF_DARTS_CONV = REWRITE_CONV[LIST_OF_DARTS; faces; FLATTEN; ITLIST; APPEND] in
1276 let darts = LIST_OF_DARTS_CONV (mk_comb (list_of_darts_const, hol_list)) in
1278 let GOOD_LIST_CONV tm =
1279 let th0 = REWRITE_CONV[good_list; darts] tm in
1280 let [c1;c2;c3] = conjuncts (rand(concl th0)) in
1281 let th1 = ALL_DISTINCT_NUM_PAIR_CONV c1 in
1282 let th2 = REWRITE_CONV[ALL; NOT_CONS_NIL] c2 in
1283 let th3 = (REWRITE_CONV[ALL_MEM] THENC GOOD_LIST_COND3_CONV) c3 in
1284 let th = CONJ (EQT_ELIM th1) (CONJ (EQT_ELIM th2) (EQT_ELIM th3)) in
1285 EQ_MP (SYM th0) th in
1287 let y = mk_comb(good_list_const, hol_list) in
1288 let good_list_th = GOOD_LIST_CONV y in
1291 test 1 GOOD_LIST_CONV y;; (* 2.448; (ALL_DISTINCT_NUM_PAIR_CONV) 1.748; (COND3) 0.244 *)
1294 let components_th = MATCH_MP COMPONENTS_HYPERMAP_OF_LIST good_list_th in
1295 let darts_th = REWRITE_RULE[darts_of_list; darts] (CONJUNCT1 components_th) in
1296 let faces_th = REWRITE_RULE[faces_of_list; faces] (MATCH_MP FACE_SET_EQ_LIST good_list_th) in
1297 (*REWRITE_RULE[MAP; set_of_list] faces_th;; *)
1299 let y = mk_comb(list_of_elements_const, hol_list) in
1300 let elements = LIST_OF_ELEMENTS_CONV y in
1302 let LIST_OF_NODES_CONV = ONCE_REWRITE_CONV[list_of_nodes] THENC
1303 ONCE_REWRITE_CONV[darts] THENC ONCE_REWRITE_CONV[elements] THENC
1304 map_conv_univ (BETA_CONV THENC FILTER_NODE_CONV) in
1306 let y = mk_comb(list_of_nodes_const, hol_list) in
1307 let nodes = LIST_OF_NODES_CONV y in
1309 let good_nodes_th = ASSUME (mk_comb(`good_list_nodes:((num)list)list->bool`, hol_list)) in
1310 let hyp_nodes = REWRITE_RULE[good_list_nodes; nodes_of_list; nodes; MAP; set_of_list] good_nodes_th in
1312 (* Table of node L x *)
1313 let table_of_nodes = build_table_of_nodes hol_list nodes in
1315 (* Table of face L x *)
1316 let table_of_faces = build_table_of_faces hol_list good_list_th faces in
1318 (* Table of face_map and inverses *)
1320 let f_list_th1 = MP (ISPEC hol_list F_LIST_EXT_TABLE) good_list_th in
1321 let f_list_th2 = REWRITE_RULE[faces; ALL] f_list_th1 in
1322 let f_list_ext_table_th = REWRITE_RULE[f_list_ext_table; HD] f_list_th2 in
1324 let f_list_ext_table, inv_f_list_ext_table = build_f_list_ext_table hol_list good_list_th faces in
1327 let y = mk_comb(list_of_edges_const, hol_list) in
1328 let edges = REWRITE_CONV[list_of_edges; darts; MAP] y in
1330 (* faces3, face4, face5, faces6 *)
1331 let faces3_tm = mk_comb(list_of_faces3_const, hol_list) in
1332 let faces4_tm = mk_comb(list_of_faces4_const, hol_list) in
1333 let faces5_tm = mk_comb(list_of_faces5_const, hol_list) in
1334 let faces6_tm = mk_comb(list_of_faces6_const, hol_list) in
1336 let filter = filter_conv_univ (BETA_CONV THENC
1337 LAND_CONV (length_conv_univ NUM_SUC_CONV) THENC
1340 let faces3 = (REWRITE_CONV[list_of_faces3; faces] THENC filter) faces3_tm in
1341 let faces4 = (REWRITE_CONV[list_of_faces4; faces] THENC filter) faces4_tm in
1342 let faces5 = (REWRITE_CONV[list_of_faces5; faces] THENC filter) faces5_tm in
1343 let faces6 = (REWRITE_CONV[list_of_faces6; faces] THENC filter) faces6_tm in
1345 (* darts3, darts4, dartsX *)
1346 let darts3_tm = mk_comb(list_of_darts3_const, hol_list) in
1347 let darts4_tm = mk_comb(list_of_darts4_const, hol_list) in
1349 let darts3 = (REWRITE_CONV[list_of_darts3; faces3] THENC flatten_conv_univ) darts3_tm in
1350 let darts4 = (REWRITE_CONV[list_of_darts4; faces4] THENC flatten_conv_univ) darts4_tm in
1352 let filter = filter_conv_univ (BETA_CONV THENC
1353 RAND_CONV (length_conv_univ NUM_SUC_CONV) THENC
1355 let dartsX_tm = mk_comb(list_of_dartsX_const, hol_list) in
1356 let dartsX = (REWRITE_CONV[list_of_dartsX; list_of_faces456; faces] THENC
1357 RAND_CONV filter THENC flatten_conv_univ) dartsX_tm in
1359 (* add everything to the table *)
1360 let add = fun str thm -> Hashtbl.add thm_table str thm in
1364 add "good_list" good_list_th;
1367 add "elements" elements;
1368 add "darts3" darts3;
1369 add "darts4" darts4;
1370 add "dartsX" dartsX;
1371 add "faces3" faces3;
1372 add "faces4" faces4;
1373 add "faces5" faces5;
1374 add "faces6" faces6 in
1376 let add = fun str table -> Hashtbl.add fun_table str table in
1378 add "face" table_of_faces;
1379 add "node" table_of_nodes;
1380 add "inverse" inv_f_list_ext_table;
1381 add "f_list_ext" f_list_ext_table in
1383 hol_list, thm_table, fun_table;;
1388 let hol_list, thm_table, fun_table = compute_all pentstring;;
1390 let table = Hashtbl.find fun_table "f_list_ext";;
1391 Hashtbl.find table `0,2`;;
1393 (* (1): 0.560; (2): 0.640; (3): 1.424; (4): 1.448; (5): 0.748 *)
1394 test 1 compute_all pentstring;;
1396 Hashtbl.find list_thm "faces_table";;
1397 Hashtbl.find list_thm "darts4";;
1398 Hashtbl.find list_thm "edges";;
1417 let hol_list, list_thm = compute_all pentstring;;
1418 let th1 = MP (ISPEC hol_list FACE_MAP_TABLE) (Hashtbl.find list_thm "good_list");;
1419 let th2 = REWRITE_RULE[Hashtbl.find list_thm "faces"; ALL] th1;;
1420 let th3 = REWRITE_RULE[face_map_table; HD] th2;;
1424 (* Explicit orbit computation *)
1425 (* Orbits for lists *)
1427 let list_orbit = define `list_orbit f x acc = if (MEM x acc) then acc else list_orbit f (f x) (CONS x acc)`;;
1430 (* The same definitions as in "pack_defs.hl" *)
1431 let REVERSE_TABLE = define `(REVERSE_TABLE (f:num->A) 0 = []) /\
1432 (REVERSE_TABLE f (SUC i) = CONS (f i) ( REVERSE_TABLE f i))`;;
1434 let TABLE = new_definition `!(f:num->A) k. TABLE f k = REVERSE (REVERSE_TABLE f k)`;;
1437 let LENGTH_REVERSE = prove(`!l:(A)list. LENGTH (REVERSE l) = LENGTH l`,
1438 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE; LENGTH; LENGTH_APPEND] THEN ARITH_TAC);;
1441 let LENGTH_REVERSE_TABLE = prove(`!(f:num->A) n. LENGTH (REVERSE_TABLE f n) = n`,
1442 GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE_TABLE; LENGTH]);;
1445 let LENGTH_TABLE = prove(`!(f:num->A) n. LENGTH(TABLE f n) = n`,
1446 REWRITE_TAC[TABLE; LENGTH_REVERSE; LENGTH_REVERSE_TABLE]);;
1449 let EL_REVERSE_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (REVERSE_TABLE f n) = f (n - i - 1)`,
1450 GEN_TAC THEN INDUCT_TAC THEN GEN_TAC THEN REWRITE_TAC[ARITH_RULE `~(i < 0)`] THEN
1452 MP_TAC (SPEC `i:num` num_CASES) THEN
1453 DISCH_THEN DISJ_CASES_TAC THENL
1455 ASM_REWRITE_TAC[REVERSE_TABLE; EL; HD; ARITH_RULE `SUC n - 0 - 1 = n`];
1458 POP_ASSUM CHOOSE_TAC THEN
1459 UNDISCH_TAC `i < SUC n` THEN ASM_REWRITE_TAC[LT_SUC; EL] THEN
1460 REWRITE_TAC[REVERSE_TABLE; TL; ARITH_RULE `SUC n - SUC n' = n - n'`] THEN
1462 FIRST_X_ASSUM MATCH_MP_TAC THEN
1463 ASM_REWRITE_TAC[]);;
1466 let EL_REVERSE = prove(`!(l:(A)list) i. i < LENGTH l ==> EL i (REVERSE l) = EL (LENGTH l - i - 1) l`,
1467 LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; REVERSE; LT] THEN
1468 REPEAT STRIP_TAC THENL
1470 ASM_REWRITE_TAC[EL_APPEND; LENGTH_REVERSE; LT_REFL; SUB_REFL] THEN
1471 REWRITE_TAC[ARITH_RULE `SUC n - n - 1 = 0`] THEN
1472 REWRITE_TAC[EL; HD];
1475 ASM_REWRITE_TAC[EL_APPEND; LENGTH_REVERSE] THEN
1476 ASM_SIMP_TAC[ARITH_RULE `i < n ==> SUC n - i - 1 = SUC(n - i - 1)`] THEN
1477 REWRITE_TAC[EL; TL]);;
1480 let EL_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (TABLE f n) = f i`,
1481 REPEAT STRIP_TAC THEN
1482 REWRITE_TAC[TABLE] THEN
1483 MP_TAC (SPECL [`REVERSE_TABLE (f:num->A) n`; `i:num`] EL_REVERSE) THEN
1484 ASM_REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1485 MP_TAC (SPECL [`f:(num->A)`; `n:num`; `n - i - 1`] EL_REVERSE_TABLE) THEN
1486 ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - (n - i - 1) - 1 = i`] THEN
1487 ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - i - 1 < n`]);;
1492 let LIST_ORBIT_LEMMA = prove(`!f (x:A) n. 1 <= n /\ (f POWER n) x = x /\
1493 (!i j. ~(i = j) /\ i < n /\ j < n ==> ~((f POWER i) x = (f POWER j) x))
1494 ==> (!k. k <= n ==> list_orbit f ((f POWER (n - k)) x)
1495 (REVERSE_TABLE (\i. (f POWER i) x) (n - k)) = REVERSE_TABLE (\i. (f POWER i) x) n)`,
1496 REPEAT GEN_TAC THEN STRIP_TAC THEN
1497 INDUCT_TAC THEN DISCH_TAC THENL
1499 REWRITE_TAC[SUB_0] THEN
1500 ONCE_REWRITE_TAC[list_orbit] THEN
1501 ASM_REWRITE_TAC[] THEN
1502 SUBGOAL_THEN `MEM (x:A) (REVERSE_TABLE (\i. (f POWER i) x) n)` ASSUME_TAC THENL
1504 REWRITE_TAC[MEM_EXISTS_EL] THEN
1505 EXISTS_TAC `n - 1` THEN
1506 REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1507 MP_TAC (ARITH_RULE `1 <= n ==> n - 1 < n`) THEN
1508 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1509 ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN
1510 ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> n - (n - 1) - 1 = 0`] THEN
1511 REWRITE_TAC[Hypermap.POWER_0; I_THM];
1518 ONCE_REWRITE_TAC[list_orbit] THEN
1519 COND_CASES_TAC THENL
1521 POP_ASSUM MP_TAC THEN
1522 REWRITE_TAC[MEM_EXISTS_EL] THEN
1523 REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1525 POP_ASSUM MP_TAC THEN
1526 ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN
1527 FIRST_X_ASSUM (MP_TAC o SPECL [`n - SUC k`; `n - SUC k - i - 1`]) THEN
1530 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1531 UNDISCH_TAC `1 <= n` THEN
1540 SUBGOAL_THEN `f ((f POWER (n - SUC k)) (x:A)) = (f POWER (n - k)) x` (fun th -> REWRITE_TAC[th]) THENL
1542 ASM_SIMP_TAC[ARITH_RULE `SUC k <= n ==> n - k = SUC(n - SUC k)`] THEN
1543 REWRITE_TAC[Hypermap.COM_POWER; o_THM];
1547 SUBGOAL_THEN `CONS ((f POWER (n - SUC k)) (x:A)) (REVERSE_TABLE (\i. (f POWER i) x) (n - SUC k)) = REVERSE_TABLE (\i. (f POWER i) x) (n - k)` ASSUME_TAC THENL
1549 ASM_SIMP_TAC[ARITH_RULE `SUC k <= n ==> n - k = SUC(n - SUC k)`] THEN
1550 REWRITE_TAC[REVERSE_TABLE];
1554 ASM_REWRITE_TAC[] THEN
1555 FIRST_X_ASSUM MATCH_MP_TAC THEN
1556 UNDISCH_TAC `SUC k <= n` THEN ARITH_TAC);;
1560 let LIST_ORBIT_EXPLICIT = prove(`!f (x:A) n. 1 <= n /\ (f POWER n) x = x /\
1561 (!i j. ~(i = j) /\ i < n /\ j < n ==> ~((f POWER i) x = (f POWER j) x))
1562 ==> list_orbit f x [] = REVERSE_TABLE (\i. (f POWER i) x) n`,
1563 REPEAT STRIP_TAC THEN
1564 MP_TAC (SPEC_ALL LIST_ORBIT_LEMMA) THEN
1565 ASM_REWRITE_TAC[] THEN
1566 DISCH_THEN (MP_TAC o SPEC `n:num`) THEN
1567 REWRITE_TAC[LE_REFL; SUB_REFL; Hypermap.POWER; I_THM] THEN
1568 REWRITE_TAC[REVERSE_TABLE]);;
1571 let FINITE_ORBIT_MAP_EXPLICIT = prove(`!s f (x:A). f permutes s /\ FINITE s ==>
1573 orbit_map f x = {(f POWER k) x | k < n} /\
1574 (f POWER n) x = x /\
1575 (!i j. ~(i = j) /\ i < n /\ j < n ==> ~((f POWER i) x = (f POWER j) x))`,
1576 REPEAT STRIP_TAC THEN
1577 ABBREV_TAC `n = CARD (orbit_map f (x:A))` THEN
1578 EXISTS_TAC `n:num` THEN
1579 MP_TAC (SPEC_ALL Hypermap_and_fan.FINITE_ORBIT_MAP) THEN
1580 ASM_REWRITE_TAC[] THEN
1581 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1582 REPEAT CONJ_TAC THENL
1584 MP_TAC (SPEC_ALL Hypermap_and_fan.ORBIT_MAP_CARD_POS) THEN
1585 ASM_REWRITE_TAC[] THEN
1588 MATCH_MP_TAC Hypermap.lemma_cycle_orbit THEN
1589 EXISTS_TAC `s:A->bool` THEN ASM_REWRITE_TAC[];
1592 REPEAT STRIP_TAC THEN
1593 MP_TAC (INST[`n:num`, `k:num`] (SPEC_ALL Hypermap_and_fan.ORBIT_MAP_INJ)) THEN
1594 ASM_REWRITE_TAC[]);;
1598 let ORBIT_EQ_LIST_ORBIT = prove(`!f s (x:A). f permutes s /\ FINITE s
1599 ==> orbit_map f x = set_of_list (list_orbit f x [])`,
1601 DISCH_THEN (MP_TAC o MATCH_MP FINITE_ORBIT_MAP_EXPLICIT) THEN
1602 DISCH_THEN (STRIP_ASSUME_TAC o SPEC `x:A`) THEN
1603 ASM_SIMP_TAC[LIST_ORBIT_EXPLICIT] THEN
1605 REWRITE_TAC[EXTENSION] THEN X_GEN_TAC `y:A` THEN
1606 REWRITE_TAC[IN_ELIM_THM; IN_SET_OF_LIST; MEM_EXISTS_EL] THEN
1607 REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1608 EQ_TAC THEN STRIP_TAC THENL
1610 EXISTS_TAC `n - k - 1` THEN
1611 MP_TAC (ARITH_RULE `k < n ==> n - k - 1 < n`) THEN
1612 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1613 ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN
1614 ASM_SIMP_TAC[ARITH_RULE `k < n ==> n - (n - k - 1) - 1 = k`];
1617 POP_ASSUM MP_TAC THEN
1618 ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN DISCH_TAC THEN
1619 EXISTS_TAC `n - i - 1` THEN
1620 ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - i - 1 < n`]);;
1628 let [el_0_th; el_suc_th] = CONJUNCTS (ISPECL[`n:num`; `l:(num#num)list`] (GEN_ALL EL));;
1629 let n_var_num = `n:num`;;
1630 let l_list = `l:(num#num)list`;;
1631 let zero_const = `_0`;;
1633 let rec el_conv tm =
1634 let ltm, l_tm = dest_comb tm in
1635 let el_tm, n_tm = dest_comb ltm in
1636 if (rand n_tm <> zero_const) then
1637 let n_suc_th = num_CONV n_tm in
1638 let m_tm = rand (rand (concl n_suc_th)) in
1639 let th0 = AP_THM (AP_TERM el_tm n_suc_th) l_tm in
1640 let th1' = INST[m_tm, n_var_num; l_tm, l_list] el_suc_th in
1641 let th1 = REWRITE_RULE[TL] th1' in
1642 let th2 = el_conv (rand(concl th1)) in
1643 TRANS th0 (TRANS th1 th2)
1645 let th0' = INST[l_tm, l_list] el_0_th in
1646 REWRITE_RULE[HD] th0';;
1650 let prev_hd_th = prove(`PREV_EL (x:A) (CONS x t) = LAST (CONS x t)`,
1651 REWRITE_TAC[PREV_EL; INDEX]);;
1655 let PREV_EL_CONV = REWRITE_CONV[PREV_EL; INDEX; PAIR_EQ; ARITH; LAST; NOT_CONS_NIL] THENC
1656 TRY_CONV (ONCE_DEPTH_CONV el_conv);;
1660 let N_LIST_CONV = (REWRITE_CONV[n_list] THENC
1661 REWRITE_CONV[find_face; find_list; faces; MEM; PAIR_EQ; ARITH] THENC
1662 ONCE_DEPTH_CONV PREV_EL_CONV THENC
1663 REWRITE_CONV[e_list]);;
1666 let z = mk_comb (`n_list:((num)list)list->num#num->num#num`, x);;
1667 let zz = mk_comb (z, `2,0`);;
1671 test 10 N_LIST_CONV zz;; (* 0.704 *)
1675 let list_orbit_mem = UNDISCH_ALL (prove(`(MEM (x:num#num) acc <=> T) ==> list_orbit f x acc = acc`,
1676 ONCE_REWRITE_TAC[list_orbit] THEN
1678 let list_orbit_not_mem = UNDISCH_ALL (prove(`(MEM (x:num#num) acc <=> F)
1679 ==> list_orbit f x acc = list_orbit f (f x) (CONS x acc)`,
1681 GEN_REWRITE_TAC LAND_CONV[list_orbit] THEN
1682 ASM_REWRITE_TAC[]));;
1686 let rec list_orbit_conv f_conv tm =
1687 let ltm, acc = dest_comb tm in
1688 let ltm, x_arg = dest_comb ltm in
1689 let ltm, f_arg = dest_comb ltm in
1690 let mem_th = REWRITE_CONV[MEM; PAIR_EQ; ARITH] (mk_binop mem_const x_arg acc) in
1691 if (rand(concl mem_th) = f_const) then
1692 let th0' = INST[x_arg, x_var_pair; f_arg, f_var_fun; acc, acc_var] list_orbit_not_mem in
1693 let th0 = PROVE_HYP mem_th th0' in
1694 let tm1 = rand(concl th0) in
1695 let ltm, acc1 = dest_comb tm1 in
1696 let ltm, x_arg1 = dest_comb ltm in
1697 let x_th = f_conv x_arg1 in
1698 let th1 = TRANS th0 (AP_THM (AP_TERM ltm x_th) acc1) in
1699 let th2 = list_orbit_conv f_conv (rand(concl th1)) in
1702 let th0 = INST[x_arg, x_var_pair; f_arg, f_var_fun; acc, acc_var] list_orbit_mem in
1703 PROVE_HYP mem_th th0;;
1708 let t1 = mk_comb (`list_orbit:(num#num->num#num)->(num#num)->(num#num)list->(num#num)list`, z) in
1709 mk_comb(mk_comb(t1, `12,7`), `[]:(num#num)list`);;
1711 list_orbit_conv N_LIST_CONV zzz;;