1 needs "../formal_lp/hypermap/list_hypermap_defs.hl";;
6 open Hypermap_and_fan;;
8 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
10 let IN_TRANS = prove(`!(x:A) s t. t SUBSET s /\ x IN t ==> x IN s`,
13 let LENGTH_ZIP = prove(`!(l1:(A)list) (l2:(B)list). LENGTH l1 = LENGTH l2 ==> LENGTH (ZIP l1 l2) = LENGTH l1`,
14 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; ZIP; NOT_SUC; GSYM NOT_SUC] THEN
15 REWRITE_TAC[SUC_INJ] THEN
17 FIRST_X_ASSUM MATCH_MP_TAC THEN
22 let MEM_ZIP = prove(`!(i:A) (j:B) l1 l2. LENGTH l1 = LENGTH l2 /\ MEM (i,j) (ZIP l1 l2) ==> MEM i l1 /\ MEM j l2`,
23 GEN_TAC THEN GEN_TAC THEN
24 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; ZIP; MEM; NOT_SUC; GSYM NOT_SUC] THEN
25 REWRITE_TAC[SUC_INJ; PAIR_EQ] THEN
26 STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
27 FIRST_X_ASSUM (MP_TAC o SPEC `t':(B)list`) THEN
31 let EL_ZIP = prove(`!(l1:(A)list) (l2:(B)list) i. LENGTH l1 = LENGTH l2 /\ i < LENGTH l1 ==> EL i (ZIP l1 l2) = (EL i l1, EL i l2)`,
32 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; ZIP; LT; NOT_SUC; SUC_INJ] THEN
33 POP_ASSUM (fun th -> ALL_TAC) THEN GEN_TAC THEN
34 REWRITE_TAC[GSYM LT] THEN
35 DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
37 ASM_REWRITE_TAC[EL; HD];
40 POP_ASSUM CHOOSE_TAC THEN
41 ASM_REWRITE_TAC[LT_SUC; EL; TL]);;
44 (****************************)
49 let EL_INDEX = prove(`!(x:A) list. MEM x list ==> EL (INDEX x list) list = x`,
50 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THEN
51 ASM_CASES_TAC `x = h:A` THEN ASM_REWRITE_TAC[] THENL
53 ASM_REWRITE_TAC[INDEX; EL; HD];
56 ASM_REWRITE_TAC[INDEX; EL; TL]);;
59 let INDEX_LE_LENGTH = prove(`!(x:A) list. INDEX x list <= LENGTH list`,
60 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[INDEX; LENGTH; LE_REFL] THEN
61 ASM_CASES_TAC `x = h:A` THEN ASM_REWRITE_TAC[ARITH_RULE `0 <= SUC n`; LE_SUC]);;
65 let INDEX_EQ_LENGTH = prove(`!(x:A) list. ~(MEM x list) <=> INDEX x list = LENGTH list`,
66 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; INDEX; LENGTH] THEN
67 REWRITE_TAC[DE_MORGAN_THM] THEN
68 ASM_CASES_TAC `x = h:A` THEN ASM_REWRITE_TAC[GSYM NOT_SUC] THEN ARITH_TAC);;
72 let INDEX_LT_LENGTH = prove(`!(x:A) list. MEM x list <=> INDEX x list < LENGTH list`,
73 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[INDEX; LENGTH; MEM; LT_REFL] THEN
74 ASM_CASES_TAC `x = h:A` THEN ASM_REWRITE_TAC[ARITH_RULE `0 < SUC n`; LT_SUC]);;
79 let CARD_SET_OF_LIST_ALL_DISTINCT = prove(`!l:(A)list. ALL_DISTINCT l ==>
80 CARD (set_of_list l) = LENGTH l`,
81 LIST_INDUCT_TAC THEN REWRITE_TAC[ALL_DISTINCT_ALT; LENGTH; set_of_list; CARD_CLAUSES] THEN
83 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
84 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
85 ASM_SIMP_TAC[FINITE_SET_OF_LIST; CARD_CLAUSES; IN_SET_OF_LIST]);;
91 let ALL_DISTINCT_SUM = prove(`!(f:A->real) list. ALL_DISTINCT list ==> sum (set_of_list list) f = list_sum list f`,
92 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[ALL_DISTINCT_ALT; set_of_list; SUM_CLAUSES; list_sum; ITLIST] THEN
93 REWRITE_TAC[GSYM list_sum] THEN
95 ASM_SIMP_TAC[SUM_CLAUSES; FINITE_SET_OF_LIST] THEN
96 ASM_REWRITE_TAC[IN_SET_OF_LIST]);;
100 let ALL_DISTINCT_APPEND = prove(`!l1 l2:(A)list. ALL_DISTINCT (APPEND l1 l2) ==> ALL_DISTINCT l1 /\ ALL_DISTINCT l2`,
101 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[ALL_DISTINCT_ALT; APPEND; APPEND_NIL] THEN
103 FIRST_X_ASSUM (MP_TAC o SPEC `CONS (h':A) t'`) THEN
104 ASM_REWRITE_TAC[ALL_DISTINCT_ALT] THEN
105 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
106 POP_ASSUM MP_TAC THEN
107 SIMP_TAC[MEM_APPEND; DE_MORGAN_THM]);;
110 let ALL_DISTINCT_APPEND_SYM = prove(`!l1 l2:(A)list. ALL_DISTINCT (APPEND l1 l2) <=>
111 ALL_DISTINCT (APPEND l2 l1)`,
112 LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[ALL_DISTINCT_ALT; APPEND; APPEND_NIL] THEN
113 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
114 FIRST_ASSUM (MP_TAC o SPEC `CONS (h':A) t'`) THEN
115 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
116 REWRITE_TAC[APPEND; ALL_DISTINCT_ALT; MEM_APPEND; DE_MORGAN_THM] THEN
117 FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN
118 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
119 REWRITE_TAC[MEM; DE_MORGAN_THM] THEN
120 EQ_TAC THEN SIMP_TAC[]);;
124 let ALL_DISTINCT_IMP_INDEX_UNIQUE = prove(`!(x:A) i l. ALL_DISTINCT l /\ MEM x l /\ i < LENGTH l /\ EL i l = x ==> i = INDEX x l`,
125 REWRITE_TAC[ALL_DISTINCT] THEN
126 REPEAT STRIP_TAC THEN
127 FIRST_X_ASSUM (MP_TAC o SPECL [`i:num`; `INDEX (x:A) l`]) THEN
128 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH] THEN
129 ASM_SIMP_TAC[EL_INDEX]);;
133 let INDEX_EL = prove(`!i (list:(A)list). ALL_DISTINCT list /\ i < LENGTH list ==> INDEX (EL i list) list = i`,
134 REPEAT STRIP_TAC THEN
135 MATCH_MP_TAC (GSYM ALL_DISTINCT_IMP_INDEX_UNIQUE) THEN
136 ASM_SIMP_TAC[MEM_EL]);;
142 (* Shift left/right *)
146 let SHIFT_RIGHT = prove(`!h h' (t:(A)list). shift_right ([]:(A)list) = []
147 /\ shift_right (CONS h []) = [h]
148 /\ shift_right (CONS h (CONS h' t)) = CONS (LAST (CONS h' t)) (BUTLAST (CONS h (CONS h' t)))`,
150 REWRITE_TAC[shift_right; NOT_CONS_NIL; LAST; BUTLAST]);;
153 let SHIFT_RIGHT = prove(`!(h:A) t. shift_right ([]:(A)list) = [] /\ shift_right (CONS h t) = CONS (LAST (CONS h t)) (BUTLAST (CONS h t))`,
154 REWRITE_TAC[shift_right; NOT_CONS_NIL]);;
158 let MEM_SHIFT_LEFT = prove(`!(x:A) l. MEM x l <=> MEM x (shift_left l)`,
159 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; shift_left] THEN
160 REWRITE_TAC[MEM_APPEND; MEM] THEN
161 ASM_CASES_TAC `x = h:A` THEN ASM_REWRITE_TAC[]);;
166 let BUTLAST_APPEND_SING = prove(`!(x:A) t. BUTLAST (APPEND t [x]) = t`,
167 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[APPEND; BUTLAST] THEN
170 POP_ASSUM MP_TAC THEN REWRITE_TAC[APPEND_EQ_NIL; NOT_CONS_NIL];
177 let SHIFT_LEFT_RIGHT = prove(`!list:(A)list. shift_left (shift_right list) = list /\ shift_right (shift_left list) = list`,
178 LIST_INDUCT_TAC THEN REWRITE_TAC[shift_left; SHIFT_RIGHT] THEN
179 SIMP_TAC[NOT_CONS_NIL; APPEND_BUTLAST_LAST] THEN
180 REWRITE_TAC[shift_right] THEN
183 POP_ASSUM (MP_TAC o AP_TERM `LENGTH:(A)list->num`) THEN
184 REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN ARITH_TAC;
187 REWRITE_TAC[BUTLAST_APPEND_SING; LAST_APPEND; NOT_CONS_NIL; LAST]);;
191 let SHIFT_LEFT_RIGHT_o_I = prove(`shift_left o shift_right = (I:(A)list->(A)list) /\ shift_right o shift_left = (I:(A)list->(A)list)`,
192 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; SHIFT_LEFT_RIGHT]);;
196 let MEM_SHIFT_RIGHT = prove(`!(x:A) l. MEM x l <=> MEM x (shift_right l)`,
198 MP_TAC (SPEC `l:(A)list` SHIFT_LEFT_RIGHT) THEN
199 DISCH_THEN (MP_TAC o SYM o CONJUNCT1) THEN
200 DISCH_THEN (fun th -> CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV[th]))) THEN
201 REWRITE_TAC[GSYM MEM_SHIFT_LEFT]);;
206 let EL_SHIFT_LEFT = prove(`!i (list:(A)list). i < LENGTH list ==> EL i (shift_left list) = if (i = LENGTH list - 1) then EL 0 list else EL (i + 1) list`,
207 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[EL; LENGTH; shift_left; LT] THEN
210 ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `SUC n - 1 = n`; LT_REFL; SUB_REFL; EL; HD];
213 ASM_SIMP_TAC[ARITH_RULE `i < n ==> ~(i = SUC n - 1)`] THEN
214 ASM_REWRITE_TAC[EL_APPEND; GSYM ADD1; EL; TL]);;
219 let LENGTH_SHIFT_LEFT = prove(`!list:(A)list. LENGTH (shift_left list) = LENGTH list`,
220 LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; shift_left] THEN
221 REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN ARITH_TAC);;
224 let LENGTH_SHIFT_RIGHT = prove(`!list:(A)list. LENGTH (shift_right list) = LENGTH list`,
226 MP_TAC (CONJUNCT1 (SPEC `list:(A)list` SHIFT_LEFT_RIGHT)) THEN
227 DISCH_THEN (MP_TAC o (fun th -> AP_TERM `LENGTH:(A)list->num` th)) THEN
228 REWRITE_TAC[LENGTH_SHIFT_LEFT]);;
231 let EL_SHIFT_RIGHT = prove(`!i (list:(A)list). i < LENGTH list ==> EL i (shift_right list) = if (i = 0) then EL (LENGTH list - 1) list else EL (i - 1) list`,
232 REPEAT STRIP_TAC THEN
233 ASM_CASES_TAC `i = 0` THEN ASM_REWRITE_TAC[] THENL
235 SUBGOAL_THEN `~(list:(A)list = [])` ASSUME_TAC THENL
237 DISCH_TAC THEN UNDISCH_TAC `i < LENGTH (list:(A)list)` THEN
238 ASM_REWRITE_TAC[LENGTH; LT_REFL];
241 ASM_SIMP_TAC[GSYM LAST_EL] THEN
242 ASM_REWRITE_TAC[shift_right; EL; HD];
246 MP_TAC (CONJUNCT1 (SPEC `list:(A)list` SHIFT_LEFT_RIGHT)) THEN
247 DISCH_THEN (MP_TAC o (fun th -> AP_TERM `(EL:num->(A)list->A) (i - 1)` th)) THEN
248 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
249 MP_TAC (SPECL [`i - 1`; `shift_right (list:(A)list)`] EL_SHIFT_LEFT) THEN
250 REWRITE_TAC[LENGTH_SHIFT_RIGHT; SHIFT_LEFT_RIGHT] THEN
253 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
256 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
257 SUBGOAL_THEN `~(i - 1 = LENGTH (list:(A)list) - 1)` (fun th -> REWRITE_TAC[th]) THENL
259 POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
262 ASM_SIMP_TAC[ARITH_RULE `~(i = 0) ==> i - 1 + 1 = i`]);;
265 (* NEXT_EL, PREV_EL *)
268 let NEXT_EL_ALT = prove(`!(x:A) list. MEM x list ==> NEXT_EL x list = EL (INDEX x list) (shift_left list)`,
269 REWRITE_TAC[INDEX_LT_LENGTH] THEN REPEAT STRIP_TAC THEN
270 MP_TAC (SPECL [`INDEX x (list:(A)list)`; `list:(A)list`] EL_SHIFT_LEFT) THEN
271 ASM_REWRITE_TAC[] THEN
272 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
273 REWRITE_TAC[NEXT_EL; EL]);;
276 let PREV_EL_ALT = prove(`!(x:A) list. MEM x list ==> PREV_EL x list = EL (INDEX x list) (shift_right list)`,
277 REWRITE_TAC[INDEX_LT_LENGTH] THEN REPEAT STRIP_TAC THEN
278 MP_TAC (SPECL [`INDEX x (list:(A)list)`; `list:(A)list`] EL_SHIFT_RIGHT) THEN
279 ASM_REWRITE_TAC[] THEN
280 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
281 REWRITE_TAC[PREV_EL] THEN
282 AP_THM_TAC THEN AP_TERM_TAC THEN
283 MATCH_MP_TAC LAST_EL THEN
284 DISCH_TAC THEN UNDISCH_TAC `INDEX x (list:(A)list) < LENGTH (list:(A)list)` THEN
285 ASM_REWRITE_TAC[LENGTH; LT]);;
288 let MEM_NEXT_EL = prove(`!(x:A) list. MEM x list ==> MEM (NEXT_EL x list) list`,
289 REPEAT STRIP_TAC THEN
290 ASM_SIMP_TAC[NEXT_EL_ALT] THEN
291 ONCE_REWRITE_TAC[MEM_SHIFT_LEFT] THEN
292 REWRITE_TAC[MEM_EXISTS_EL] THEN
293 EXISTS_TAC `INDEX (x:A) list` THEN
294 ASM_REWRITE_TAC[LENGTH_SHIFT_LEFT; GSYM INDEX_LT_LENGTH]);;
297 let MEM_PREV_EL = prove(`!(x:A) list. MEM x list ==> MEM (PREV_EL x list) list`,
298 REPEAT STRIP_TAC THEN
299 ASM_SIMP_TAC[PREV_EL_ALT] THEN
300 ONCE_REWRITE_TAC[MEM_SHIFT_RIGHT] THEN
301 REWRITE_TAC[MEM_EXISTS_EL] THEN
302 EXISTS_TAC `INDEX (x:A) list` THEN
303 ASM_REWRITE_TAC[LENGTH_SHIFT_RIGHT; GSYM INDEX_LT_LENGTH]);;
307 let INDEX_HD = prove(`!list:(A)list. ~(list = []) ==> INDEX (HD list) list = 0`,
308 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[NOT_CONS_NIL; INDEX; HD]);;
311 let PREV_NEXT_ID = prove(`!(x:A) list. ALL_DISTINCT list /\ MEM x list ==> PREV_EL (NEXT_EL x list) list = x`,
312 REPEAT STRIP_TAC THEN
313 REWRITE_TAC[NEXT_EL] THEN
314 SUBGOAL_THEN `~(list = []:(A)list)` ASSUME_TAC THENL
316 DISCH_TAC THEN UNDISCH_TAC `MEM (x:A) list` THEN
317 ASM_REWRITE_TAC[MEM];
322 REWRITE_TAC[PREV_EL] THEN
323 ASM_SIMP_TAC[INDEX_HD; LAST_EL] THEN
324 MP_TAC (SPECL [`x:A`; `list:(A)list`] EL_INDEX) THEN
329 REWRITE_TAC[PREV_EL] THEN
330 ABBREV_TAC `i = INDEX (x:A) list` THEN
331 SUBGOAL_THEN `i + 1 < LENGTH (list:(A)list)` ASSUME_TAC THENL
333 REWRITE_TAC[ARITH_RULE `i + 1 < n <=> i < n /\ ~(i = n - 1)`] THEN
334 ASM_REWRITE_TAC[] THEN
335 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
336 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
340 MP_TAC (SPECL [`i + 1`; `list:(A)list`] INDEX_EL) THEN
341 ASM_REWRITE_TAC[] THEN
342 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
343 REWRITE_TAC[ARITH_RULE `~(i + 1 = 0)`; ARITH_RULE `(i + 1) - 1 = i`] THEN
344 MP_TAC (SPECL [`x:A`; `list:(A)list`] EL_INDEX) THEN
349 let NEXT_PREV_ID = prove(`!(x:A) list. ALL_DISTINCT list /\ MEM x list ==> NEXT_EL (PREV_EL x list) list = x`,
350 REPEAT STRIP_TAC THEN
351 REWRITE_TAC[PREV_EL] THEN
352 SUBGOAL_THEN `~(list = []:(A)list)` ASSUME_TAC THENL
354 DISCH_TAC THEN UNDISCH_TAC `MEM (x:A) list` THEN
355 ASM_REWRITE_TAC[MEM];
358 SUBGOAL_THEN `0 < LENGTH (list:(A)list)` ASSUME_TAC THENL
360 UNDISCH_TAC `~(list = []:(A)list)` THEN
361 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
362 REWRITE_TAC[NOT_LT; LE; LENGTH_EQ_NIL];
368 REWRITE_TAC[NEXT_EL] THEN
369 SUBGOAL_THEN `INDEX (LAST list) (list:(A)list) = LENGTH list - 1` ASSUME_TAC THENL
371 ASM_SIMP_TAC[LAST_EL] THEN
372 MATCH_MP_TAC INDEX_EL THEN
373 ASM_REWRITE_TAC[ARITH_RULE `n - 1 < n <=> 0 < n`];
376 ASM_REWRITE_TAC[] THEN
377 MP_TAC (SPECL [`x:A`; `list:(A)list`] EL_INDEX) THEN
382 REWRITE_TAC[NEXT_EL] THEN
383 ABBREV_TAC `i = INDEX (x:A) list` THEN
384 SUBGOAL_THEN `0 < i /\ i - 1 < LENGTH (list:(A)list)` ASSUME_TAC THENL
386 ASM_REWRITE_TAC[LT_NZ] THEN
387 MATCH_MP_TAC (ARITH_RULE `i < n ==> i - 1 < n`) THEN
388 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
389 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
393 MP_TAC (SPECL [`i - 1`; `list:(A)list`] INDEX_EL) THEN
394 ASM_REWRITE_TAC[] THEN
395 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
396 ASM_SIMP_TAC[ARITH_RULE `0 < i /\ 0 < n ==> (i - 1 = n - 1 <=> i = n)`] THEN
397 ASM_SIMP_TAC[ARITH_RULE `0 < i ==> i - 1 + 1 = i`] THEN
398 EXPAND_TAC "i" THEN ASM_REWRITE_TAC[GSYM INDEX_EQ_LENGTH] THEN
399 MP_TAC (SPECL [`x:A`; `list:(A)list`] EL_INDEX) THEN
404 (* FLATTEN, REMOVE_DUPLICATES *)
406 let MEM_REMOVE_DUPLICATES = prove(`!(x:A) list. MEM x (REMOVE_DUPLICATES list) <=> MEM x list`,
407 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[REMOVE_DUPLICATES; MEM] THEN
408 COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM] THEN
409 EQ_TAC THEN SIMP_TAC[] THEN STRIP_TAC THEN ASM_REWRITE_TAC[]);;
412 let ALL_DISTINCT_REMOVE_DUPLICATES = prove(`!list:(A)list. ALL_DISTINCT (REMOVE_DUPLICATES list)`,
413 LIST_INDUCT_TAC THEN REWRITE_TAC[ALL_DISTINCT_ALT; REMOVE_DUPLICATES] THEN
414 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
415 ASM_REWRITE_TAC[ALL_DISTINCT_ALT; MEM_REMOVE_DUPLICATES]);;
418 let MEM_FLATTEN = prove(`!(x:A) ll. MEM x (FLATTEN ll) <=> ?l. MEM l ll /\ MEM x l`,
419 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM; FLATTEN; ITLIST] THEN
420 REWRITE_TAC[MEM_APPEND; GSYM FLATTEN] THEN
425 EXISTS_TAC `h:(A)list` THEN ASM_REWRITE_TAC[];
428 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
429 EXISTS_TAC `l:(A)list` THEN
435 UNDISCH_TAC `l = h:(A)list` THEN DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);
438 DISJ2_TAC THEN ASM_REWRITE_TAC[] THEN
439 EXISTS_TAC `l:(A)list` THEN ASM_REWRITE_TAC[]);;
445 let LIST_PAIRS_EMPTY = prove(`!list:(A)list. list_pairs list = [] <=> list = []`,
446 REWRITE_TAC[list_pairs; GSYM LENGTH_EQ_NIL] THEN
447 SIMP_TAC[LENGTH_ZIP; LENGTH_SHIFT_LEFT]);;
452 let LIST_OF_DARTS = prove(`!ll:((A)list)list. list_of_darts ll = FLATTEN (list_of_faces ll)`,
453 REWRITE_TAC[list_of_darts; FLATTEN; list_of_faces] THEN
454 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[ITLIST; MAP]);;
460 let FIND_FACE = prove(`!(d:A#A) ll. find_face d ll = list_pairs (find_pair_list d ll)`,
461 REWRITE_TAC[find_face; list_of_faces] THEN
462 GEN_TAC THEN LIST_INDUCT_TAC THENL
464 REWRITE_TAC[MAP; find_list; find_pair_list; list_pairs; shift_left; ZIP];
467 REWRITE_TAC[MAP; find_pair_list; find_list] THEN
468 COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
471 let MEM_FIND_LIST = prove(`!(x:A) ll. MEM x (FLATTEN ll) ==>
472 MEM (find_list x ll) ll`,
473 REWRITE_TAC[MEM_FLATTEN] THEN
474 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THEN
477 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[find_list] THEN DISCH_TAC THEN
481 ASM_CASES_TAC `MEM (x:A) h` THEN ASM_REWRITE_TAC[find_list] THEN
483 FIRST_X_ASSUM MATCH_MP_TAC THEN
484 EXISTS_TAC `l:(A)list` THEN
489 let MEM_FIND_FACE = prove(`!(d:A#A) ll. MEM d (list_of_darts ll)
490 ==> MEM (find_face d ll) (list_of_faces ll)`,
491 REWRITE_TAC[LIST_OF_DARTS] THEN REPEAT STRIP_TAC THEN
492 REWRITE_TAC[find_face] THEN
493 MATCH_MP_TAC MEM_FIND_LIST THEN
498 let MEM_FIND_LIST_NONEMPTY = prove(`!(x:A) ll. ALL (\l. ~(l = [])) ll ==>
499 (MEM x (FLATTEN ll) <=> MEM (find_list x ll) ll)`,
500 REWRITE_TAC[GSYM ALL_MEM] THEN
501 REPEAT STRIP_TAC THEN
504 ASM_REWRITE_TAC[MEM_FIND_LIST];
507 POP_ASSUM MP_TAC THEN SPEC_TAC (`ll:((A)list)list`, `ll:((A)list)list`) THEN
508 LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THEN
510 FIRST_X_ASSUM (MP_TAC o check(is_imp o concl)) THEN
513 GEN_TAC THEN DISCH_TAC THEN
514 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A)list`) THEN
520 REWRITE_TAC[find_list] THEN
521 SUBGOAL_THEN `!t. find_list x t = h ==> MEM (x:A) h` ASSUME_TAC THENL
523 FIRST_X_ASSUM (MP_TAC o SPEC `h:(A)list`) THEN
524 REWRITE_TAC[] THEN DISCH_TAC THEN
525 LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[find_list] THEN
526 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
527 DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);
531 ASM_CASES_TAC `MEM (x:A) h` THEN ASM_REWRITE_TAC[] THENL
533 REWRITE_TAC[MEM_FLATTEN; MEM] THEN
534 EXISTS_TAC `h:(A)list` THEN
540 FIRST_X_ASSUM (MP_TAC o SPEC `t:((A)list)list`) THEN
544 REWRITE_TAC[FLATTEN; ITLIST; MEM_APPEND] THEN
545 ASM_REWRITE_TAC[GSYM FLATTEN] THEN
546 FIRST_X_ASSUM MATCH_MP_TAC THEN
550 let MEM_FIND_FACE_NONEMPTY = prove(`!(d:A#A) ll. ALL (\l. ~(l = [])) ll
551 ==> (MEM d (list_of_darts ll) <=> MEM (find_face d ll) (list_of_faces ll))`,
552 REWRITE_TAC[find_face; LIST_OF_DARTS] THEN REPEAT STRIP_TAC THEN
553 MATCH_MP_TAC MEM_FIND_LIST_NONEMPTY THEN
554 REWRITE_TAC[list_of_faces] THEN
555 REWRITE_TAC[ALL_MAP] THEN
556 POP_ASSUM MP_TAC THEN
557 REWRITE_TAC[GSYM ALL_MEM; o_THM] THEN
558 DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
559 REWRITE_TAC[list_pairs] THEN
560 FIRST_X_ASSUM (MP_TAC o SPEC `x:(A)list`) THEN
561 ASM_REWRITE_TAC[CONTRAPOS_THM] THEN
562 REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
563 SIMP_TAC[LENGTH_ZIP; LENGTH_SHIFT_LEFT]);;
567 (* Hypermap maps properties *)
570 (* e_list_ext permutes darts *)
572 let E_LIST_EXT_INVOLUTION = prove(`!ll:((A)list)list. good_list ll ==> e_list_ext ll o e_list_ext ll = I`,
573 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; e_list_ext; good_list] THEN
574 REPEAT STRIP_TAC THEN
575 MP_TAC (ISPEC `x:A#A` PAIR_SURJECTIVE) THEN
576 DISCH_THEN (X_CHOOSE_THEN `i:A` MP_TAC) THEN
577 DISCH_THEN (X_CHOOSE_THEN `j:A` ASSUME_TAC) THEN
578 ASM_REWRITE_TAC[res; e_list] THEN
579 ASM_CASES_TAC `i,j:A IN darts_of_list ll` THENL
581 ASM_REWRITE_TAC[] THEN
582 FIRST_X_ASSUM (MP_TAC o SPEC (`i:A,j:A`)) THEN
583 POP_ASSUM MP_TAC THEN
584 SIMP_TAC[darts_of_list; IN_SET_OF_LIST];
590 let LEFT_RIGHT_INVERSES_COINSIDE = prove(`!(f:A->B) l r. f o r = I /\ l o f = I ==> r = l`,
591 REPEAT STRIP_TAC THEN
592 POP_ASSUM (MP_TAC o (AP_TERM `\tm:(A->A). tm o (r:B->A)`)) THEN
593 ASM_REWRITE_TAC[I_O_ID; GSYM o_ASSOC] THEN
597 let INVERSE_EXISTS_IMP_BIJECTIVE = prove(`!(f:A->B) g. f o g = I /\ g o f = I ==> (!y. ?!x. f x = y)`,
598 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
599 REPEAT STRIP_TAC THEN REWRITE_TAC[EXISTS_UNIQUE] THEN
600 EXISTS_TAC `(g:B->A) y` THEN
601 ASM_REWRITE_TAC[] THEN
602 REPEAT STRIP_TAC THEN
603 POP_ASSUM (MP_TAC o AP_TERM `g:B->A`) THEN
610 let E_LIST_EXT_PERMUTES_DARTS = prove(`!ll:((A)list)list. good_list ll ==> (e_list_ext ll) permutes (darts_of_list ll)`,
611 REWRITE_TAC[ permutes] THEN
612 GEN_TAC THEN STRIP_TAC THEN STRIP_TAC THENL
614 REPEAT STRIP_TAC THEN
615 ASM_REWRITE_TAC[e_list_ext; res];
618 MATCH_MP_TAC INVERSE_EXISTS_IMP_BIJECTIVE THEN
619 EXISTS_TAC `e_list_ext (ll:((A)list)list)` THEN
620 REWRITE_TAC[ETA_AX] THEN
621 ASM_SIMP_TAC[E_LIST_EXT_INVOLUTION]);;
625 (* f_list_ext permutes darts *)
627 let DART_IN_DARTS = prove(`!(d:A#A) l ll. MEM d (list_pairs l) /\ MEM l ll ==> MEM d (list_of_darts ll)`,
628 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THEN
629 REPEAT STRIP_TAC THEN REWRITE_TAC[list_of_darts; ITLIST; MEM_APPEND] THENL
632 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
636 REWRITE_TAC[GSYM list_of_darts] THEN
637 FIRST_X_ASSUM MATCH_MP_TAC THEN
642 let MEM_FIND_PAIR_LIST = prove(`!(d:A#A) ll. MEM d (list_of_darts ll) ==> MEM (find_pair_list d ll) ll`,
643 GEN_TAC THEN LIST_INDUCT_TAC THENL
645 ASM_REWRITE_TAC[list_of_darts; ITLIST; MEM];
648 REWRITE_TAC[list_of_darts; find_pair_list; ITLIST; MEM] THEN
649 COND_CASES_TAC THEN REWRITE_TAC[] THEN
650 ASM_REWRITE_TAC[MEM_APPEND; GSYM list_of_darts] THEN
651 DISCH_TAC THEN DISJ2_TAC THEN
652 FIRST_X_ASSUM MATCH_MP_TAC THEN
656 let DART_IN_FIND_PAIR_LIST = prove(`!(d:A#A) ll. MEM d (list_of_darts ll) <=> MEM d (list_pairs (find_pair_list d ll))`,
657 GEN_TAC THEN LIST_INDUCT_TAC THENL
659 ASM_REWRITE_TAC[list_of_darts; ITLIST; MEM; find_pair_list; list_pairs; shift_left; ZIP];
662 REWRITE_TAC[list_of_darts; find_pair_list; ITLIST; MEM] THEN
663 COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM_APPEND] THEN
664 ASM_REWRITE_TAC[GSYM list_of_darts]);;
669 let DART_IN_FACE = prove(`!(d:A#A) ll. MEM d (list_of_darts ll) <=> MEM d (find_face d ll)`,
670 REWRITE_TAC[FIND_FACE; DART_IN_FIND_PAIR_LIST]);;
677 let MEM_IMP_NOT_ALL_DISTINCT_APPEND = prove(`!(x:A) l1 l2. MEM x l1 /\ MEM x l2 ==> ~ALL_DISTINCT (APPEND l1 l2)`,
678 REWRITE_TAC[ALL_DISTINCT; NOT_FORALL_THM; LENGTH_APPEND; EL_APPEND] THEN
679 REWRITE_TAC[MEM_EXISTS_EL] THEN
680 REPEAT STRIP_TAC THEN
681 EXISTS_TAC `i:num` THEN EXISTS_TAC `LENGTH (l1:(A)list) + i'` THEN
682 REWRITE_TAC[NOT_IMP] THEN
683 ASM_SIMP_TAC[ARITH_RULE `i < l1 ==> i < l1 + l2:num`; ARITH_RULE `i' < l2 ==> l1 + i' < l1 + l2:num`; ARITH_RULE `i < l1 ==> ~(i = l1 + i':num)`] THEN
684 REWRITE_TAC[ARITH_RULE `(l1 + i') - l1 = i':num`] THEN
685 REWRITE_TAC[ARITH_RULE `~(l1 + i' < l1:num)`] THEN
686 REPEAT (FIRST_X_ASSUM (fun th -> REWRITE_TAC[SYM th])));;
692 let ALL_DISTINCT_IMP_UNIQUE_LIST = prove(`!l1 l2 (d:A#A) ll. ALL_DISTINCT (list_of_darts ll) /\ MEM l1 ll /\ MEM l2 ll
693 /\ MEM d (list_pairs l1) /\ MEM d (list_pairs l2) ==> l1 = l2`,
694 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THENL
699 REWRITE_TAC[MEM; list_of_darts; ITLIST] THEN
700 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
702 FIRST_X_ASSUM (MP_TAC o check (fun th -> (rator o concl) th = `ALL_DISTINCT:(A#A)list->bool`)) THEN
703 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
705 MATCH_MP_TAC MEM_IMP_NOT_ALL_DISTINCT_APPEND THEN
706 EXISTS_TAC `d:A#A` THEN
707 FIRST_X_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
708 REWRITE_TAC[GSYM list_of_darts] THEN
709 MATCH_MP_TAC DART_IN_DARTS THEN
710 EXISTS_TAC `l2:(A)list` THEN
713 FIRST_X_ASSUM (MP_TAC o check (fun th -> (rator o concl) th = `ALL_DISTINCT:(A#A)list->bool`)) THEN
714 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
716 MATCH_MP_TAC MEM_IMP_NOT_ALL_DISTINCT_APPEND THEN
717 EXISTS_TAC `d:A#A` THEN
718 FIRST_X_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
719 REWRITE_TAC[GSYM list_of_darts] THEN
720 MATCH_MP_TAC DART_IN_DARTS THEN
721 EXISTS_TAC `l1:(A)list` THEN
727 FIRST_X_ASSUM MATCH_MP_TAC THEN
728 ASM_REWRITE_TAC[] THEN
729 FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP ALL_DISTINCT_APPEND th)) THEN
730 SIMP_TAC[GSYM list_of_darts]);;
735 let FIND_PAIR_LIST_UNIQUE = prove(`!l d (ll:((A)list)list). ALL_DISTINCT (list_of_darts ll) /\
736 MEM l ll /\ MEM d (list_pairs l) ==> l = find_pair_list d ll`,
737 REPEAT STRIP_TAC THEN
738 MATCH_MP_TAC ALL_DISTINCT_IMP_UNIQUE_LIST THEN
739 MAP_EVERY EXISTS_TAC [`d:A#A`; `ll:((A)list)list`] THEN
740 ASM_REWRITE_TAC[] THEN
741 SUBGOAL_THEN `MEM (d:A#A) (list_of_darts ll)` ASSUME_TAC THENL
743 MATCH_MP_TAC DART_IN_DARTS THEN
744 EXISTS_TAC `l:(A)list` THEN
748 ASM_SIMP_TAC[MEM_FIND_PAIR_LIST] THEN
749 ASM_REWRITE_TAC[GSYM DART_IN_FIND_PAIR_LIST]);;
753 let ALL_DISTINCT_FIND_FACE = prove(`!(d:A#A) ll. ALL_DISTINCT (list_of_darts ll) ==> ALL_DISTINCT (find_face d ll)`,
754 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[list_of_darts; ALL_DISTINCT_ALT; ITLIST; find_face; list_of_faces; find_list; MAP] THEN
755 REWRITE_TAC[GSYM list_of_darts; GSYM find_face; GSYM list_of_faces] THEN
756 DISCH_THEN (MP_TAC o (fun th -> MATCH_MP ALL_DISTINCT_APPEND th)) THEN
758 COND_CASES_TAC THEN ASM_SIMP_TAC[]);;
767 let LENGTH_LIST_PAIRS = prove(`!l:(A)list. LENGTH (list_pairs l) = LENGTH l`,
768 GEN_TAC THEN REWRITE_TAC[list_pairs] THEN
769 MATCH_MP_TAC LENGTH_ZIP THEN
770 REWRITE_TAC[LENGTH_SHIFT_LEFT]);;
775 let MEM_LIST_PAIRS = prove(`!(x:A) y l. MEM (x,y) (list_pairs l) ==> MEM x l /\ MEM y l`,
776 REWRITE_TAC[list_pairs] THEN
777 REPEAT GEN_TAC THEN DISCH_TAC THEN
778 MP_TAC (ISPECL [`x:A`; `y:A`; `l:(A)list`; `shift_left (l:(A)list)`] MEM_ZIP) THEN
779 ASM_REWRITE_TAC[LENGTH_SHIFT_LEFT; GSYM MEM_SHIFT_LEFT]);;
783 let MEM_F_LIST = prove(`!(d:A#A) ll. MEM d (list_of_darts ll) ==> MEM (f_list ll d) (find_face d ll)`,
784 REPEAT STRIP_TAC THEN
785 ASM_REWRITE_TAC[f_list] THEN
786 MATCH_MP_TAC MEM_NEXT_EL THEN
787 ASM_REWRITE_TAC[GSYM DART_IN_FACE]);;
792 let EL_LIST_PAIRS = prove(`!i (list:(A)list). i < LENGTH list ==> EL i (list_pairs list) = (EL i list, EL (if i = LENGTH list - 1 then 0 else i + 1) list)`,
793 REPEAT STRIP_TAC THEN
794 REWRITE_TAC[list_pairs] THEN
795 MP_TAC (ISPECL [`list:(A)list`; `shift_left (list:(A)list)`; `i:num`] EL_ZIP) THEN
796 ASM_REWRITE_TAC[LENGTH_SHIFT_LEFT] THEN
797 DISCH_THEN (fun th -> REWRITE_TAC[th; PAIR_EQ]) THEN
798 ASM_SIMP_TAC[EL_SHIFT_LEFT] THEN
799 COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
803 let ALL_DISTINCT_LIST_PAIRS = prove(`!list:(A)list. ALL_DISTINCT list ==> ALL_DISTINCT (list_pairs list)`,
804 REWRITE_TAC[ALL_DISTINCT; LENGTH_LIST_PAIRS] THEN
805 GEN_TAC THEN ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
806 REWRITE_TAC[NOT_FORALL_THM; NOT_IMP] THEN
808 MAP_EVERY EXISTS_TAC [`i:num`; `j:num`] THEN
809 ASM_REWRITE_TAC[] THEN
810 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC[EL_LIST_PAIRS; PAIR_EQ]);;
814 let ALL_DISTINCT_SHIFT_LEFT = prove(`!list:(A)list. ALL_DISTINCT list ==> ALL_DISTINCT (shift_left list)`,
815 LIST_INDUCT_TAC THEN REWRITE_TAC[shift_left] THEN
816 POP_ASSUM (fun th -> ALL_TAC) THEN
817 ASM_REWRITE_TAC[ALL_DISTINCT] THEN
818 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
819 REWRITE_TAC[NOT_FORALL_THM; NOT_IMP; EL_APPEND; LENGTH_APPEND; LENGTH; ARITH_SUC] THEN
820 STRIP_TAC THEN POP_ASSUM MP_TAC THEN
821 ABBREV_TAC `m = LENGTH (t:(A)list)` THEN
822 ASSUME_TAC (ARITH_RULE `!n. n < m + 1 /\ ~(n < m) ==> n = m`) THEN
823 REPEAT COND_CASES_TAC THENL
826 MAP_EVERY EXISTS_TAC [`SUC i`; `SUC j`] THEN
827 ASM_REWRITE_TAC[LT_SUC; SUC_INJ; EL; TL];
828 FIRST_X_ASSUM (MP_TAC o SPEC `j:num`) THEN
829 ASM_REWRITE_TAC[] THEN
830 DISCH_THEN (fun th -> REWRITE_TAC[th; SUB_REFL]) THEN
831 REWRITE_TAC[EL; HD] THEN DISCH_TAC THEN
832 MAP_EVERY EXISTS_TAC [`SUC i`; `0`] THEN
833 ASM_REWRITE_TAC[LT_SUC; NOT_SUC; LT_0; EL; TL; HD];
834 FIRST_X_ASSUM (MP_TAC o SPEC `i:num`) THEN
835 ASM_REWRITE_TAC[] THEN
836 DISCH_THEN (fun th -> REWRITE_TAC[th; SUB_REFL]) THEN
837 REWRITE_TAC[EL; HD] THEN DISCH_TAC THEN
838 MAP_EVERY EXISTS_TAC [`0`; `SUC j`] THEN
839 ASM_REWRITE_TAC[LT_SUC; NOT_SUC; LT_0; EL; TL; HD];
840 UNDISCH_TAC `~(i = j:num)` THEN
841 FIRST_ASSUM (MP_TAC o SPEC `i:num`) THEN FIRST_X_ASSUM (MP_TAC o SPEC `j:num`) THEN
847 let MEM_LIST_PAIRS_EXPLICIT = prove(`!(d:A#A) list. ALL_DISTINCT list /\ MEM d (list_pairs list)
848 ==> d = (FST d, NEXT_EL (FST d) list)`,
849 REWRITE_TAC[MEM_EXISTS_EL] THEN
850 REWRITE_TAC[LENGTH_LIST_PAIRS] THEN
851 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN
852 REWRITE_TAC[list_pairs] THEN
853 MP_TAC (ISPECL [`list:(A)list`; `shift_left list:(A)list`; `i:num`] EL_ZIP) THEN
854 ASM_REWRITE_TAC[LENGTH_SHIFT_LEFT] THEN
855 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
856 DISCH_THEN (fun th -> REWRITE_TAC[th; PAIR_EQ]) THEN
857 MP_TAC (SPECL [`EL i list:A`; `list:(A)list`] NEXT_EL_ALT) THEN
858 ASM_SIMP_TAC[MEM_EL] THEN
860 MP_TAC (SPEC_ALL INDEX_EL) THEN
867 let INDEX_FST_SND = prove(`!i (d:A#A) list. ALL_DISTINCT list /\ i < LENGTH list /\ EL i (list_pairs list) = d ==>
868 INDEX (FST d) list = i /\ INDEX (SND d) list = if (i = LENGTH list - 1) then 0 else i + 1`,
869 REPEAT GEN_TAC THEN STRIP_TAC THEN
870 POP_ASSUM MP_TAC THEN
871 ASM_SIMP_TAC[EL_LIST_PAIRS] THEN
872 MP_TAC (ISPEC `d:A#A` PAIR_SURJECTIVE) THEN
873 STRIP_TAC THEN ASM_REWRITE_TAC[PAIR_EQ] THEN
874 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
875 CONJ_TAC THEN MATCH_MP_TAC INDEX_EL THEN ASM_REWRITE_TAC[] THEN
876 ABBREV_TAC `n = LENGTH (list:(A)list)` THEN
877 UNDISCH_TAC `i < n:num` THEN COND_CASES_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC);;
882 let NEXT_EL_LIST_PAIRS = prove(`!(d:A#A) list. ALL_DISTINCT list /\ MEM d (list_pairs list) ==> NEXT_EL d (list_pairs list) = (SND d, NEXT_EL (SND d) list)`,
883 REPEAT STRIP_TAC THEN
884 REWRITE_TAC[NEXT_EL; LENGTH_LIST_PAIRS] THEN
885 MP_TAC (SPEC `list:(A)list` ALL_DISTINCT_LIST_PAIRS) THEN
886 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
887 ABBREV_TAC `i = INDEX (d:A#A) (list_pairs list)` THEN
888 ABBREV_TAC `n = LENGTH (list:(A)list)` THEN
889 SUBGOAL_THEN `i < n:num` ASSUME_TAC THENL
891 EXPAND_TAC "n" THEN EXPAND_TAC "i" THEN
892 ONCE_REWRITE_TAC[GSYM LENGTH_LIST_PAIRS] THEN
893 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
897 SUBGOAL_THEN `EL i (list_pairs list) = d:A#A` ASSUME_TAC THENL
900 MATCH_MP_TAC EL_INDEX THEN ASM_REWRITE_TAC[];
904 MP_TAC (SPECL [`i:num`; `d:A#A`; `list:(A)list`] INDEX_FST_SND) THEN
905 ASM_REWRITE_TAC[] THEN
907 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
910 ASM_REWRITE_TAC[] THEN
911 MP_TAC (SPEC_ALL EL_LIST_PAIRS) THEN
912 ASM_REWRITE_TAC[] THEN
915 MATCH_MP_TAC (ARITH_RULE `i < n ==> n - 1 < n`) THEN
919 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
920 ONCE_REWRITE_TAC[GSYM EL] THEN
921 MP_TAC (SPECL [`0`; `list:(A)list`] EL_LIST_PAIRS) THEN
922 ASM_REWRITE_TAC[] THEN
923 ANTS_TAC THENL [ MATCH_MP_TAC (ARITH_RULE `i < n ==> 0 < n`) THEN ASM_REWRITE_TAC[]; ALL_TAC ] THEN
924 DISCH_THEN (fun th -> REWRITE_TAC[th; PAIR_EQ]) THEN
925 COND_CASES_TAC THEN ASM_REWRITE_TAC[];
929 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
930 MP_TAC (SPECL [`i + 1`; `list:(A)list`] EL_LIST_PAIRS) THEN
931 SUBGOAL_THEN `i + 1 < n` ASSUME_TAC THENL
933 REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN ARITH_TAC;
937 ASM_REWRITE_TAC[] THEN
938 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
939 ONCE_REWRITE_TAC[GSYM EL] THEN
940 MP_TAC (SPECL [`i:num`; `list:(A)list`] EL_LIST_PAIRS) THEN
941 ASM_REWRITE_TAC[] THEN
942 DISCH_THEN (fun th -> REWRITE_TAC[th; PAIR_EQ]) THEN
943 COND_CASES_TAC THEN ASM_REWRITE_TAC[PAIR_EQ]);;
948 let PREV_EL_LIST_PAIRS = prove(`!(d:A#A) list. ALL_DISTINCT list /\ MEM d (list_pairs list) ==>
949 PREV_EL d (list_pairs list) = (PREV_EL (FST d) list, FST d)`,
950 REPEAT STRIP_TAC THEN
951 ABBREV_TAC `t = PREV_EL (d:A#A) (list_pairs list)` THEN
952 SUBGOAL_THEN `MEM (t:A#A) (list_pairs list)` ASSUME_TAC THENL
955 MATCH_MP_TAC MEM_PREV_EL THEN
959 MP_TAC (SPECL [`t:A#A`; `list:(A)list`] MEM_LIST_PAIRS_EXPLICIT) THEN
960 ASM_REWRITE_TAC[] THEN
962 MP_TAC (ISPEC `t:A#A` PAIR_SURJECTIVE) THEN
963 STRIP_TAC THEN ASM_REWRITE_TAC[PAIR_EQ] THEN
964 DISCH_THEN (MP_TAC o AP_TERM `(\tm:A. PREV_EL tm list)`) THEN
966 MP_TAC (SPEC_ALL PREV_NEXT_ID) THEN
969 ASM_REWRITE_TAC[] THEN
970 MP_TAC (SPECL [`x:A`; `y:A`; `list:(A)list`] MEM_LIST_PAIRS) THEN
971 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
975 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
976 SUBGOAL_THEN `y = FST (d:A#A)` ASSUME_TAC THENL
978 UNDISCH_TAC `PREV_EL d (list_pairs list) = t:A#A` THEN
979 DISCH_THEN (MP_TAC o AP_TERM `\tm:A#A. NEXT_EL tm (list_pairs list)`) THEN
980 MP_TAC (ISPECL [`d:A#A`; `list_pairs (list:(A)list)`] NEXT_PREV_ID) THEN
983 ASM_REWRITE_TAC[] THEN
984 MATCH_MP_TAC ALL_DISTINCT_LIST_PAIRS THEN
989 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
990 MP_TAC (SPECL [`t:A#A`; `list:(A)list`] NEXT_EL_LIST_PAIRS) THEN
991 ASM_REWRITE_TAC[] THEN
992 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
993 DISCH_THEN (fun th -> REWRITE_TAC[th; PAIR_EQ]);
997 DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]));;
1001 let F_LIST_INVERSE = prove(`!(d:A#A) ll. ALL_DISTINCT (list_of_darts ll) /\ MEM d (list_of_darts ll) ==>
1002 let g = (\x:A#A. PREV_EL x (find_face x ll)) in
1003 f_list ll (g d) = d /\ g (f_list ll d) = d`,
1004 REWRITE_TAC[LET_DEF; LET_END_DEF; f_list] THEN
1005 REPEAT STRIP_TAC THENL
1007 ABBREV_TAC `f = find_face (d:A#A) ll` THEN
1008 SUBGOAL_THEN `find_face (PREV_EL (d:A#A) f) ll = f` ASSUME_TAC THENL
1010 EXPAND_TAC "f" THEN REWRITE_TAC[FIND_FACE] THEN
1012 REWRITE_TAC[GSYM FIND_FACE] THEN
1014 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1015 ASM_REWRITE_TAC[] THEN
1016 MP_TAC (SPEC_ALL MEM_FIND_PAIR_LIST) THEN
1017 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
1018 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1019 ASM_REWRITE_TAC[GSYM FIND_FACE] THEN
1020 MATCH_MP_TAC MEM_PREV_EL THEN
1022 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1026 ASM_REWRITE_TAC[] THEN
1027 MATCH_MP_TAC NEXT_PREV_ID THEN
1028 MP_TAC (SPEC_ALL ALL_DISTINCT_FIND_FACE) THEN
1031 POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
1033 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1037 ABBREV_TAC `f = find_face (d:A#A) ll` THEN
1038 SUBGOAL_THEN `find_face (NEXT_EL (d:A#A) f) ll = f` ASSUME_TAC THENL
1040 EXPAND_TAC "f" THEN REWRITE_TAC[FIND_FACE] THEN
1042 REWRITE_TAC[GSYM FIND_FACE] THEN
1044 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1045 ASM_REWRITE_TAC[] THEN
1046 MP_TAC (SPEC_ALL MEM_FIND_PAIR_LIST) THEN
1047 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
1048 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN
1049 ASM_REWRITE_TAC[GSYM FIND_FACE] THEN
1050 MATCH_MP_TAC MEM_NEXT_EL THEN
1052 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1056 ASM_REWRITE_TAC[] THEN
1057 MATCH_MP_TAC PREV_NEXT_ID THEN
1058 MP_TAC (SPEC_ALL ALL_DISTINCT_FIND_FACE) THEN
1061 POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
1063 ASM_REWRITE_TAC[GSYM DART_IN_FACE]);;
1068 let FIND_FACE_F_LIST = prove(`!(d:A#A) ll. ALL_DISTINCT (list_of_darts ll) /\ MEM d (list_of_darts ll) ==>
1069 find_face (f_list ll d) ll = find_face d ll`,
1070 REPEAT STRIP_TAC THEN
1071 REWRITE_TAC[FIND_FACE] THEN
1073 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1074 ASM_SIMP_TAC[MEM_FIND_PAIR_LIST] THEN
1075 REWRITE_TAC[GSYM FIND_FACE] THEN
1076 ASM_SIMP_TAC[MEM_F_LIST]);;
1081 let F_LIST_EXT_PERMUTES_DARTS = prove(`!ll:((A)list)list. ALL_DISTINCT (list_of_darts ll) ==> (f_list_ext ll) permutes (darts_of_list ll)`,
1082 REWRITE_TAC[f_list_ext; permutes; res] THEN
1083 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
1084 REWRITE_TAC[EXISTS_UNIQUE] THEN
1085 ASM_CASES_TAC `y:A#A IN darts_of_list ll` THENL
1087 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN DISCH_TAC THEN
1088 MP_TAC (SPECL [`y:A#A`; `ll:((A)list)list`] F_LIST_INVERSE) THEN
1089 ASM_REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
1090 ABBREV_TAC `x:A#A = PREV_EL y (find_face y ll)` THEN
1092 EXISTS_TAC `x:A#A` THEN
1095 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts ll)` ASSUME_TAC THENL
1097 REWRITE_TAC[DART_IN_FACE] THEN
1099 SUBGOAL_THEN `find_face (PREV_EL y (find_face y ll)) ll = find_face (y:A#A) ll` (fun th -> REWRITE_TAC[th]) THENL
1101 REWRITE_TAC[FIND_FACE] THEN AP_TERM_TAC THEN
1102 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1103 REWRITE_TAC[GSYM FIND_FACE] THEN
1104 ASM_SIMP_TAC[MEM_FIND_PAIR_LIST] THEN
1106 MATCH_MP_TAC MEM_PREV_EL THEN
1107 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1111 MATCH_MP_TAC MEM_PREV_EL THEN
1112 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1120 X_GEN_TAC `d:A#A` THEN
1121 COND_CASES_TAC THENL
1124 MP_TAC (SPEC_ALL F_LIST_INVERSE) THEN
1125 ASM_REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
1129 DISCH_THEN (fun th -> POP_ASSUM (MP_TAC o REWRITE_RULE[th])) THEN
1134 EXISTS_TAC `y:A#A` THEN
1135 ASM_REWRITE_TAC[] THEN
1136 X_GEN_TAC `z:A#A` THEN
1137 COND_CASES_TAC THENL
1139 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN DISCH_TAC THEN
1140 DISCH_THEN (ASSUME_TAC o SYM) THEN
1141 MP_TAC (SPECL [`z:A#A`; `ll:((A)list)list`] MEM_F_LIST) THEN
1142 ASM_REWRITE_TAC[] THEN
1143 MP_TAC (SPECL [`z:A#A`; `ll:((A)list)list`] FIND_FACE_F_LIST) THEN
1144 ASM_REWRITE_TAC[] THEN
1145 DISCH_THEN (fun th -> REWRITE_TAC[GSYM th]) THEN
1146 REWRITE_TAC[GSYM DART_IN_FACE] THEN
1147 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1148 ASM_REWRITE_TAC[GSYM IN_SET_OF_LIST; GSYM darts_of_list];
1162 let FIND_FACE_EMPTY = prove(`!(d:A#A) ll. find_face d ll = [] <=> ~MEM d (list_of_darts ll)`,
1163 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[find_face; MAP; list_of_faces; find_list; list_of_darts; ITLIST; MEM] THEN
1164 COND_CASES_TAC THENL
1166 ASM_REWRITE_TAC[MEM_APPEND] THEN
1167 DISCH_TAC THEN UNDISCH_TAC `MEM (d:A#A) (list_pairs h)` THEN
1168 ASM_REWRITE_TAC[MEM];
1171 ASM_REWRITE_TAC[GSYM list_of_faces; GSYM find_face; GSYM list_of_darts; MEM_APPEND]);;
1176 let MEM_FIND_FACE_IMP_FACES_EQ = prove(`!(x:A#A) y ll. ALL_DISTINCT (list_of_darts ll) /\ MEM y (find_face x ll)
1177 ==> find_face y ll = find_face x ll`,
1178 REPEAT STRIP_TAC THEN
1179 REWRITE_TAC[FIND_FACE] THEN AP_TERM_TAC THEN
1180 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1181 ASM_REWRITE_TAC[GSYM FIND_FACE] THEN
1182 MATCH_MP_TAC MEM_FIND_PAIR_LIST THEN
1183 POP_ASSUM MP_TAC THEN
1184 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1185 REWRITE_TAC[GSYM FIND_FACE_EMPTY] THEN
1186 DISCH_TAC THEN ASM_REWRITE_TAC[MEM]);;
1190 let MEM_FIND_FACE_IMP_MEM_DARTS = prove(`!(d:A#A) x ll. MEM d (find_face x ll) ==> MEM d (list_of_darts ll)`,
1191 GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THENL
1193 REWRITE_TAC[find_face; list_of_darts; ITLIST; MEM; list_of_faces; MAP; find_list];
1196 REWRITE_TAC[find_face; list_of_darts; ITLIST; MEM_APPEND; list_of_faces; MAP; find_list] THEN
1197 COND_CASES_TAC THENL
1199 DISCH_THEN (fun th -> REWRITE_TAC[th]);
1202 ASM_SIMP_TAC[GSYM list_of_faces; GSYM find_face; GSYM list_of_darts]);;
1209 let F_LIST_EXT_INVERSE = prove(`!ll:((A)list)list. ALL_DISTINCT (list_of_darts ll) ==>
1210 inverse (f_list_ext ll) = res (\d. PREV_EL d (find_face d ll)) (darts_of_list ll)`,
1211 REPEAT STRIP_TAC THEN
1212 MATCH_MP_TAC INVERSE_UNIQUE_o THEN
1213 REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; f_list_ext; res] THEN
1214 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
1215 CONJ_TAC THEN GEN_TAC THENL
1217 ASM_CASES_TAC `MEM (x:A#A) (list_of_darts ll)` THEN ASM_REWRITE_TAC[] THEN
1218 SUBGOAL_THEN `MEM (PREV_EL (x:A#A) (find_face x ll)) (list_of_darts ll)` ASSUME_TAC THENL
1220 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
1221 EXISTS_TAC `x:A#A` THEN
1222 MATCH_MP_TAC MEM_PREV_EL THEN
1223 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1227 ASM_REWRITE_TAC[f_list] THEN
1228 SUBGOAL_THEN `find_face (PREV_EL x (find_face x ll)) ll = find_face (x:A#A) ll` (fun th -> REWRITE_TAC[th]) THENL
1230 REWRITE_TAC[FIND_FACE] THEN AP_TERM_TAC THEN
1231 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1232 REWRITE_TAC[GSYM FIND_FACE] THEN
1233 ASM_SIMP_TAC[MEM_FIND_PAIR_LIST] THEN
1234 MATCH_MP_TAC MEM_PREV_EL THEN
1235 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1239 MATCH_MP_TAC NEXT_PREV_ID THEN
1240 ASM_SIMP_TAC[ALL_DISTINCT_FIND_FACE] THEN
1241 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1245 ASM_CASES_TAC `MEM (x:A#A) (list_of_darts ll)` THEN ASM_REWRITE_TAC[] THEN
1246 REWRITE_TAC[f_list] THEN
1247 SUBGOAL_THEN `MEM (NEXT_EL (x:A#A) (find_face x ll)) (list_of_darts ll)` ASSUME_TAC THENL
1249 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
1250 EXISTS_TAC `x:A#A` THEN
1251 MATCH_MP_TAC MEM_NEXT_EL THEN
1252 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1256 ASM_REWRITE_TAC[] THEN
1257 SUBGOAL_THEN `find_face (NEXT_EL x (find_face x ll)) ll = find_face (x:A#A) ll` (fun th -> REWRITE_TAC[th]) THENL
1259 REWRITE_TAC[FIND_FACE] THEN AP_TERM_TAC THEN
1260 MATCH_MP_TAC (GSYM FIND_PAIR_LIST_UNIQUE) THEN
1261 REWRITE_TAC[GSYM FIND_FACE] THEN
1262 ASM_SIMP_TAC[MEM_FIND_PAIR_LIST] THEN
1263 MATCH_MP_TAC MEM_NEXT_EL THEN
1264 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1268 MATCH_MP_TAC PREV_NEXT_ID THEN
1269 ASM_SIMP_TAC[ALL_DISTINCT_FIND_FACE] THEN
1270 ASM_REWRITE_TAC[GSYM DART_IN_FACE]);;
1273 let F_LIST_EXT_INVERSE_WORKS = prove(`!ll:((A)list)list. ALL_DISTINCT (list_of_darts ll) ==>
1274 f_list_ext ll o inverse (f_list_ext ll) = I /\ inverse (f_list_ext ll) o f_list_ext ll = I`,
1275 GEN_TAC THEN DISCH_TAC THEN
1276 MATCH_MP_TAC PERMUTES_INVERSES_o THEN
1277 EXISTS_TAC `(darts_of_list ll):(A#A)->bool` THEN
1278 MATCH_MP_TAC F_LIST_EXT_PERMUTES_DARTS THEN
1279 ASM_REWRITE_TAC[]);;
1284 let N_EQ_E_FI = prove(`!ll:((A)list)list. ALL_DISTINCT (list_of_darts ll) ==>
1285 n_list_ext ll = e_list_ext ll o (inverse (f_list_ext ll))`,
1286 REPEAT STRIP_TAC THEN
1287 ASM_SIMP_TAC[F_LIST_EXT_INVERSE] THEN
1288 REWRITE_TAC[FUN_EQ_THM; o_THM] THEN GEN_TAC THEN
1289 REWRITE_TAC[n_list_ext; e_list_ext; res] THEN
1290 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
1291 COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
1292 SUBGOAL_THEN `MEM (PREV_EL (x:A#A) (find_face x ll)) (list_of_darts ll)` (fun th -> REWRITE_TAC[th]) THENL
1294 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
1295 EXISTS_TAC `x:A#A` THEN
1296 MATCH_MP_TAC MEM_PREV_EL THEN
1297 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1301 REWRITE_TAC[n_list]);;
1305 let N_LIST_EXT_PERMUTES_DARTS = prove(`!ll:((A)list)list. good_list ll ==>
1306 (n_list_ext ll) permutes (darts_of_list ll)`,
1307 REPEAT STRIP_TAC THEN FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
1308 ASM_SIMP_TAC[N_EQ_E_FI] THEN
1309 MATCH_MP_TAC PERMUTES_COMPOSE THEN
1310 ASM_SIMP_TAC[E_LIST_EXT_PERMUTES_DARTS] THEN
1311 MATCH_MP_TAC PERMUTES_INVERSE THEN
1312 ASM_SIMP_TAC[F_LIST_EXT_PERMUTES_DARTS]);;
1316 let E_N_F_ID = prove(`!ll:((A)list)list. good_list ll ==>
1317 e_list_ext ll o n_list_ext ll o f_list_ext ll = I`,
1318 REPEAT STRIP_TAC THEN FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
1319 ASM_SIMP_TAC[N_EQ_E_FI] THEN
1320 SUBGOAL_THEN `!e (f:A#A->A#A) fi:(A#A)->(A#A). e o (e o fi) o f = (e o e) o (fi o f)` (fun th -> REWRITE_TAC[th]) THENL
1322 REWRITE_TAC[o_ASSOC];
1326 ASM_SIMP_TAC[E_LIST_EXT_INVOLUTION; F_LIST_EXT_INVERSE_WORKS] THEN
1327 REWRITE_TAC[I_O_ID]);;
1331 (* hypermap_of_list is a hypermap *)
1333 let HYPERMAP_OF_LIST = prove(`!ll:((A)list)list. good_list ll ==>
1334 tuple_hypermap (hypermap_of_list ll) =
1335 darts_of_list ll, e_list_ext ll, n_list_ext ll, f_list_ext ll`,
1336 REWRITE_TAC[hypermap_of_list; GSYM Hypermap.hypermap_tybij] THEN
1337 GEN_TAC THEN DISCH_TAC THEN FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
1338 ASM_SIMP_TAC[E_LIST_EXT_PERMUTES_DARTS; N_LIST_EXT_PERMUTES_DARTS; F_LIST_EXT_PERMUTES_DARTS; E_N_F_ID] THEN
1339 REWRITE_TAC[darts_of_list; FINITE_SET_OF_LIST]);;
1347 let NEXT_EL_MOD = prove(`!list (x:A). MEM x list ==>
1348 NEXT_EL x list = EL ((INDEX x list + 1) MOD LENGTH list) list`,
1349 REPEAT STRIP_TAC THEN
1350 REWRITE_TAC[NEXT_EL] THEN
1351 ABBREV_TAC `n = LENGTH (list:(A)list)` THEN
1352 SUBGOAL_THEN `1 <= n` ASSUME_TAC THENL
1354 UNDISCH_TAC `MEM (x:A) list` THEN
1355 ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1356 STRIP_TAC THEN UNDISCH_TAC `i < n:num` THEN
1360 COND_CASES_TAC THENL
1362 ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> n - 1 + 1 = n`] THEN
1363 MP_TAC (SPECL [`n:num`; `1`] MOD_MULT) THEN
1364 ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> ~(n = 0)`; MULT_CLAUSES; EL];
1367 AP_THM_TAC THEN AP_TERM_TAC THEN
1368 MATCH_MP_TAC (GSYM MOD_LT) THEN
1369 MP_TAC (SPEC_ALL INDEX_LT_LENGTH) THEN
1370 ASM_REWRITE_TAC[] THEN
1371 POP_ASSUM MP_TAC THEN ARITH_TAC);;
1376 let NEXT_EL_POWER = prove(`!list (x:A) i. ALL_DISTINCT list /\ MEM x list ==>
1377 ((\t. NEXT_EL t list) POWER i) x = EL ((INDEX x list + i) MOD (LENGTH list)) list`,
1378 GEN_TAC THEN GEN_TAC THEN
1379 ABBREV_TAC `n = LENGTH (list:(A)list)` THEN
1380 ABBREV_TAC `k = INDEX (x:A) list` THEN
1383 REWRITE_TAC[ADD_0; Hypermap.POWER_0; I_THM] THEN
1385 SUBGOAL_THEN `k MOD n = k` (fun th -> REWRITE_TAC[th]) THENL
1387 MATCH_MP_TAC MOD_LT THEN
1388 EXPAND_TAC "k" THEN EXPAND_TAC "n" THEN
1389 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
1394 MATCH_MP_TAC (GSYM EL_INDEX) THEN
1400 SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THENL
1402 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1403 STRIP_TAC THEN UNDISCH_TAC `i' < n:num` THEN
1408 FIRST_X_ASSUM (MP_TAC o check(is_imp o concl)) THEN
1409 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1410 ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
1411 ABBREV_TAC `y:A = EL ((k + i) MOD n) list` THEN
1412 MP_TAC (SPECL [`list:(A)list`; `y:A`] NEXT_EL_MOD) THEN
1415 REWRITE_TAC[MEM_EXISTS_EL] THEN
1416 EXISTS_TAC `(k + i) MOD n` THEN
1417 ASM_REWRITE_TAC[] THEN
1418 ASM_SIMP_TAC[DIVISION];
1422 DISCH_THEN (fun th -> ASM_REWRITE_TAC[th]) THEN
1423 SUBGOAL_THEN `INDEX (y:A) list = (k + i) MOD n` (fun th -> REWRITE_TAC[th]) THENL
1426 MATCH_MP_TAC INDEX_EL THEN
1427 ASM_SIMP_TAC[DIVISION];
1431 AP_THM_TAC THEN AP_TERM_TAC THEN
1432 ASM_CASES_TAC `n = 1` THENL
1434 ASM_REWRITE_TAC[MOD_1];
1437 SUBGOAL_THEN `1 = 1 MOD n` (fun th -> ONCE_REWRITE_TAC[th]) THENL
1439 MATCH_MP_TAC (GSYM MOD_LT) THEN
1440 ASM_REWRITE_TAC[ARITH_RULE `1 < n <=> ~(n = 0) /\ ~(n = 1)`];
1443 ASM_SIMP_TAC[MOD_ADD_MOD] THEN
1444 AP_THM_TAC THEN AP_TERM_TAC THEN
1450 let NEXT_EL_ORBIT = prove(`!(list:(A)list) x. ALL_DISTINCT list /\ MEM x list ==>
1451 orbit_map (\t. NEXT_EL t list) x = set_of_list list`,
1452 REPEAT STRIP_TAC THEN
1453 ABBREV_TAC `n = LENGTH (list:(A)list)` THEN
1454 SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THENL
1456 UNDISCH_TAC `MEM (x:A) list` THEN
1457 ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1458 STRIP_TAC THEN UNDISCH_TAC `i < n:num` THEN ARITH_TAC;
1461 REWRITE_TAC[Hypermap.orbit_map; EXTENSION; IN_SET_OF_LIST; IN_ELIM_THM] THEN
1462 GEN_TAC THEN EQ_TAC THENL
1464 STRIP_TAC THEN POP_ASSUM MP_TAC THEN
1465 ASM_SIMP_TAC[NEXT_EL_POWER] THEN DISCH_TAC THEN
1466 MATCH_MP_TAC MEM_EL THEN
1467 ASM_SIMP_TAC[DIVISION];
1470 ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1472 ASM_SIMP_TAC[NEXT_EL_POWER] THEN
1473 ABBREV_TAC `k = INDEX (x:A) list` THEN
1474 EXISTS_TAC `n - k + i:num` THEN
1475 SUBGOAL_THEN `k < n:num` ASSUME_TAC THENL
1477 EXPAND_TAC "k" THEN EXPAND_TAC "n" THEN
1478 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
1481 REWRITE_TAC[GE; LE_0] THEN
1482 AP_THM_TAC THEN AP_TERM_TAC THEN
1483 ASM_SIMP_TAC[ARITH_RULE `k < n ==> k + n - k + i = n + i:num`] THEN
1484 MP_TAC (SPECL [`1`; `n:num`; `i:num`] MOD_MULT_ADD) THEN
1485 REWRITE_TAC[MULT_CLAUSES] THEN
1486 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1487 MATCH_MP_TAC (GSYM MOD_LT) THEN
1488 ASM_REWRITE_TAC[]);;
1493 let ORBIT_MAP_RES_LEMMA = prove(`!f (x:A) s. orbit_map f x SUBSET s ==>
1494 orbit_map (res f s) x = orbit_map f x`,
1495 REWRITE_TAC[SUBSET; Hypermap.orbit_map; IN_ELIM_THM] THEN REPEAT STRIP_TAC THEN
1496 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
1497 SUBGOAL_THEN `!n. (res f s POWER n) x = (f POWER n) (x:A)` ASSUME_TAC THENL
1499 INDUCT_TAC THEN REWRITE_TAC[Hypermap.POWER_0] THEN
1500 ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
1501 REWRITE_TAC[res] THEN
1502 SUBGOAL_THEN `(f POWER n) (x:A) IN s` (fun th -> REWRITE_TAC[th]) THEN
1503 FIRST_X_ASSUM MATCH_MP_TAC THEN
1504 EXISTS_TAC `n:num` THEN
1505 REWRITE_TAC[GE; LE_0];
1509 ASM_REWRITE_TAC[]);;
1513 let ORBIT_SUBSET_LEMMA = prove(`!f s (x:A). x IN s /\ (!y. y IN s ==> f y IN s)
1514 ==> orbit_map f x SUBSET s`,
1515 REPEAT STRIP_TAC THEN
1516 REWRITE_TAC[Hypermap.orbit_map; SUBSET; IN_ELIM_THM] THEN
1517 GEN_TAC THEN DISCH_THEN CHOOSE_TAC THEN POP_ASSUM MP_TAC THEN
1518 SPEC_TAC (`x':A`, `y:A`) THEN
1519 SPEC_TAC (`n:num`, `n:num`) THEN
1520 INDUCT_TAC THEN ASM_SIMP_TAC[GE; LE_0; Hypermap.POWER_0; I_THM] THEN
1521 GEN_TAC THEN REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
1523 FIRST_X_ASSUM (MP_TAC o SPEC `(f POWER n) (x:A)`) THEN
1524 ASM_REWRITE_TAC[GE; LE_0]);;
1529 let ORBIT_MAP_RES = prove(`!f (x:A) s. x IN s /\ (res f s) permutes s
1530 ==> orbit_map (res f s) x = orbit_map f x`,
1531 REPEAT STRIP_TAC THEN
1532 MATCH_MP_TAC ORBIT_MAP_RES_LEMMA THEN
1533 MATCH_MP_TAC ORBIT_SUBSET_LEMMA THEN
1534 ASM_REWRITE_TAC[] THEN
1535 REPEAT STRIP_TAC THEN
1536 SUBGOAL_THEN `(f:A->A) y = (res f s) y` (fun th -> REWRITE_TAC[th]) THENL
1538 ASM_REWRITE_TAC[res];
1541 MP_TAC (ISPECL [`res (f:A->A) s`; `s:A->bool`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
1547 let F_LIST_EXT_ORBIT = prove(`!ll (x:A#A). MEM x (list_of_darts ll) /\ ALL_DISTINCT (list_of_darts ll) ==>
1548 orbit_map (f_list_ext ll) x = set_of_list (find_face x ll)`,
1549 REPEAT STRIP_TAC THEN
1550 MP_TAC (SPEC_ALL F_LIST_EXT_PERMUTES_DARTS) THEN
1551 ASM_REWRITE_TAC[] THEN
1552 REWRITE_TAC[f_list_ext] THEN
1554 SUBGOAL_THEN `x:A#A IN darts_of_list ll` ASSUME_TAC THENL
1556 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST];
1559 ASM_SIMP_TAC[ORBIT_MAP_RES] THEN
1561 REWRITE_TAC[Hypermap.orbit_map] THEN
1562 SUBGOAL_THEN `!n. (f_list ll POWER n) x = ((\d:A#A. NEXT_EL d (find_face x ll)) POWER n) x` ASSUME_TAC THENL
1566 REWRITE_TAC[Hypermap.POWER_0; I_THM];
1570 ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
1571 REWRITE_TAC[f_list] THEN
1573 MATCH_MP_TAC MEM_FIND_FACE_IMP_FACES_EQ THEN
1574 ASM_REWRITE_TAC[] THEN
1575 MP_TAC (ISPECL [`find_face (x:A#A) ll`; `x:A#A`; `n:num`] NEXT_EL_POWER) THEN
1578 ASM_SIMP_TAC[ALL_DISTINCT_FIND_FACE] THEN
1579 ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1582 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1583 REWRITE_TAC[MEM_EXISTS_EL] THEN
1584 ABBREV_TAC `f:(A#A)list = find_face x ll` THEN
1585 EXISTS_TAC `(INDEX (x:A#A) f + n) MOD LENGTH f` THEN
1587 SUBGOAL_THEN `~(LENGTH (f:(A#A)list) = 0)` ASSUME_TAC THENL
1589 MP_TAC (SPEC_ALL (SPECL [`x:A#A`] DART_IN_FACE)) THEN
1590 ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1591 STRIP_TAC THEN UNDISCH_TAC `i < LENGTH (f:(A#A)list)` THEN
1595 ASM_SIMP_TAC[DIVISION];
1598 ASM_REWRITE_TAC[] THEN
1599 REWRITE_TAC[GSYM Hypermap.orbit_map] THEN
1600 MATCH_MP_TAC NEXT_EL_ORBIT THEN
1601 ASM_SIMP_TAC[ALL_DISTINCT_FIND_FACE; GSYM DART_IN_FACE]);;
1605 let ALL_DISTINCT_FLATTEN = prove(`!ll:((A)list)list.
1606 ALL_DISTINCT (FLATTEN ll) /\ ALL (\l. ~(l = [])) ll ==> ALL_DISTINCT ll`,
1607 LIST_INDUCT_TAC THEN REWRITE_TAC[FLATTEN; ALL_DISTINCT_ALT] THEN
1608 REWRITE_TAC[ITLIST; ALL] THEN
1609 REWRITE_TAC[GSYM FLATTEN; ALL_DISTINCT_APPEND] THEN
1611 MP_TAC (SPECL [`h:(A)list`; `FLATTEN t:(A)list`] ALL_DISTINCT_APPEND) THEN
1612 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1614 REPLICATE_TAC 5 (POP_ASSUM MP_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
1615 SPEC_TAC (`t:((A)list)list`, `t:((A)list)list`) THEN
1616 LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THEN
1617 REWRITE_TAC[ALL; FLATTEN; ITLIST] THEN
1618 REWRITE_TAC[GSYM FLATTEN] THEN
1619 REWRITE_TAC[APPEND_ASSOC; DE_MORGAN_THM] THEN
1620 REPEAT STRIP_TAC THENL
1622 MP_TAC (SPECL [`APPEND h h':(A)list`; `FLATTEN t:(A)list`] ALL_DISTINCT_APPEND) THEN
1623 ASM_REWRITE_TAC[DE_MORGAN_THM] THEN
1624 DISJ1_TAC THEN MATCH_MP_TAC MEM_IMP_NOT_ALL_DISTINCT_APPEND THEN
1625 MP_TAC (ISPEC `h':(A)list` list_CASES) THEN
1626 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1627 EXISTS_TAC `h'':A` THEN
1628 ASM_REWRITE_TAC[MEM];
1631 POP_ASSUM MP_TAC THEN REWRITE_TAC[] THEN
1632 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
1633 REPEAT ANTS_TAC THEN ASM_REWRITE_TAC[] THENL
1635 REPLICATE_TAC 5 REMOVE_ASSUM THEN
1636 POP_ASSUM MP_TAC THEN
1637 ONCE_REWRITE_TAC[ALL_DISTINCT_APPEND_SYM] THEN
1638 REWRITE_TAC[APPEND_ASSOC] THEN
1640 MP_TAC (SPECL [`APPEND (FLATTEN t) h:(A)list`; `h':(A)list`] ALL_DISTINCT_APPEND) THEN
1644 MP_TAC (SPECL [`h':(A)list`; `FLATTEN t:(A)list`] ALL_DISTINCT_APPEND) THEN
1649 let FLATTEN_FILTER_EMPTY = prove(`!ll:((A)list)list.
1650 FLATTEN (FILTER (\l. ~(l = [])) ll) = FLATTEN ll`,
1651 LIST_INDUCT_TAC THEN REWRITE_TAC[FLATTEN; FILTER; ITLIST] THEN
1652 REWRITE_TAC[GSYM FLATTEN] THEN
1653 COND_CASES_TAC THEN ASM_REWRITE_TAC[APPEND] THEN
1654 REWRITE_TAC[FLATTEN; ITLIST] THEN
1655 ASM_REWRITE_TAC[GSYM FLATTEN]);;
1658 let ALL_FILTER = prove(`!P list:(A)list. ALL P (FILTER P list)`,
1659 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[FILTER; ALL] THEN
1660 COND_CASES_TAC THEN ASM_REWRITE_TAC[ALL]);;
1666 let ALL_DISTINCT_SUBLIST_UNIQUE = prove(`!l1 l2 (x:A) ll. ALL_DISTINCT (FLATTEN ll) /\
1667 MEM l1 ll /\ MEM l2 ll /\ MEM x l1 /\ MEM x l2
1669 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
1670 LIST_INDUCT_TAC THEN REWRITE_TAC[MEM] THEN
1671 REWRITE_TAC[FLATTEN; ITLIST] THEN
1672 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
1674 FIRST_X_ASSUM (MP_TAC o check (fun th -> (rator o concl) th = `ALL_DISTINCT:(A)list->bool`)) THEN
1675 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1677 MATCH_MP_TAC MEM_IMP_NOT_ALL_DISTINCT_APPEND THEN
1678 EXISTS_TAC `x:A` THEN
1679 FIRST_X_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
1680 REWRITE_TAC[GSYM FLATTEN] THEN
1681 REWRITE_TAC[MEM_FLATTEN] THEN
1682 EXISTS_TAC `l2:(A)list` THEN
1685 FIRST_X_ASSUM (MP_TAC o check (fun th -> (rator o concl) th = `ALL_DISTINCT:(A)list->bool`)) THEN
1686 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
1688 MATCH_MP_TAC MEM_IMP_NOT_ALL_DISTINCT_APPEND THEN
1689 EXISTS_TAC `x:A` THEN
1690 FIRST_X_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]) THEN
1691 REWRITE_TAC[GSYM FLATTEN] THEN
1692 REWRITE_TAC[MEM_FLATTEN] THEN
1693 EXISTS_TAC `l1:(A)list` THEN
1699 FIRST_X_ASSUM MATCH_MP_TAC THEN
1700 ASM_REWRITE_TAC[] THEN
1701 FIRST_X_ASSUM (MP_TAC o (fun th -> MATCH_MP ALL_DISTINCT_APPEND th)) THEN
1702 SIMP_TAC[GSYM FLATTEN]);;
1708 let ALL_DISTINCT_FACE_UNIQUE = prove(`!f1 f2 d (ll:((A)list)list).
1709 ALL_DISTINCT (list_of_darts ll) /\ MEM f1 (list_of_faces ll) /\
1710 MEM f2 (list_of_faces ll) /\ MEM d f1 /\ MEM d f2 ==> f1 = f2`,
1711 REPEAT STRIP_TAC THEN
1712 MATCH_MP_TAC ALL_DISTINCT_SUBLIST_UNIQUE THEN
1713 EXISTS_TAC `d:A#A` THEN
1714 EXISTS_TAC `list_of_faces ll:((A#A)list)list` THEN
1715 ASM_REWRITE_TAC[GSYM LIST_OF_DARTS]);;
1720 let MEM_FACE_LEMMA = prove(`!f (ll:((A)list)list). good_list ll /\
1721 MEM f (list_of_faces ll) ==>
1722 ?d. MEM d (list_of_darts ll) /\ f = find_face d ll`,
1723 REWRITE_TAC[good_list] THEN REPEAT STRIP_TAC THEN
1724 EXISTS_TAC `HD f:A#A` THEN
1725 POP_ASSUM MP_TAC THEN
1726 MP_TAC (ISPEC `f:(A#A)list` list_CASES) THEN
1729 ASM_REWRITE_TAC[list_of_faces; MEM_MAP] THEN
1730 STRIP_TAC THEN POP_ASSUM (MP_TAC o SYM) THEN
1731 REWRITE_TAC[LIST_PAIRS_EMPTY] THEN DISCH_TAC THEN
1732 UNDISCH_TAC `ALL (\l:(A)list. ~(l = [])) ll` THEN
1733 REWRITE_TAC[GSYM ALL_MEM] THEN
1734 DISCH_THEN (MP_TAC o SPEC `x:(A)list`) THEN
1738 ASM_REWRITE_TAC[HD] THEN DISCH_TAC THEN
1739 SUBGOAL_THEN `MEM (h:A#A) (list_of_darts ll)` ASSUME_TAC THENL
1741 REWRITE_TAC[LIST_OF_DARTS; MEM_FLATTEN] THEN
1742 EXISTS_TAC `f:(A#A)list` THEN
1743 ASM_REWRITE_TAC[MEM];
1746 ASM_REWRITE_TAC[] THEN
1747 MATCH_MP_TAC ALL_DISTINCT_FACE_UNIQUE THEN
1748 EXISTS_TAC `h:A#A` THEN
1749 EXISTS_TAC `ll:((A)list)list` THEN
1750 ASM_REWRITE_TAC[MEM] THEN
1751 ASM_SIMP_TAC[MEM_FIND_FACE] THEN
1752 ASM_REWRITE_TAC[GSYM DART_IN_FACE]);;
1761 let FACE_SET_EQ_LIST = prove(`!ll:((A)list)list. good_list ll ==>
1762 face_set (hypermap_of_list ll) = set_of_list (faces_of_list ll)`,
1763 REPEAT STRIP_TAC THEN FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
1764 ASM_SIMP_TAC[Hypermap.face_set; Hypermap.face_map; Hypermap.dart; HYPERMAP_OF_LIST] THEN
1765 REWRITE_TAC[Hypermap.set_of_orbits] THEN
1766 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SET_OF_LIST] THEN
1768 X_GEN_TAC `f:(A#A->bool)` THEN
1769 REWRITE_TAC[GSYM EXTENSION] THEN
1772 DISCH_THEN (X_CHOOSE_THEN `d:A#A` MP_TAC) THEN
1773 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
1774 STRIP_TAC THEN POP_ASSUM MP_TAC THEN
1775 ASM_SIMP_TAC[F_LIST_EXT_ORBIT] THEN
1777 REWRITE_TAC[faces_of_list; MEM_MAP] THEN
1778 EXISTS_TAC `find_face (d:A#A) ll` THEN
1779 ASM_SIMP_TAC[MEM_FIND_FACE];
1783 REWRITE_TAC[faces_of_list; MEM_MAP] THEN
1784 DISCH_THEN (X_CHOOSE_THEN `ff:(A#A)list` ASSUME_TAC) THEN
1785 MP_TAC (SPECL [`ff:(A#A)list`; `ll:((A)list)list`] MEM_FACE_LEMMA) THEN
1786 ASM_REWRITE_TAC[] THEN
1788 EXISTS_TAC `d:A#A` THEN
1789 ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
1790 ASM_SIMP_TAC[F_LIST_EXT_ORBIT]);;
1793 (* Define nodes of a good hypermap *)
1794 let good_list_nodes = new_definition `good_list_nodes L <=>
1795 node_set (hypermap_of_list L) = set_of_list (nodes_of_list L)`;;
1800 let COMPONENTS_HYPERMAP_OF_LIST = prove(`!L:((A)list)list. good_list L ==>
1801 dart (hypermap_of_list L) = darts_of_list L /\
1802 edge_map (hypermap_of_list L) = e_list_ext L /\
1803 node_map (hypermap_of_list L) = n_list_ext L /\
1804 face_map (hypermap_of_list L) = f_list_ext L`,
1805 GEN_TAC THEN DISCH_TAC THEN
1806 REWRITE_TAC[Hypermap.dart; Hypermap.edge_map; Hypermap.node_map; Hypermap.face_map] THEN
1807 ASM_SIMP_TAC[HYPERMAP_OF_LIST]);;
1812 let SET_OF_LIST_FILTER = prove(`!P list:(A)list.
1813 set_of_list (FILTER P list) = {x | MEM x list /\ P x}`,
1814 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[FILTER; MEM] THENL
1816 REWRITE_TAC[set_of_list] THEN SET_TAC[];
1819 COND_CASES_TAC THENL
1821 ASM_REWRITE_TAC[set_of_list] THEN
1822 POP_ASSUM MP_TAC THEN SET_TAC[];
1825 ASM_REWRITE_TAC[] THEN
1826 POP_ASSUM MP_TAC THEN SET_TAC[]);;
1830 let SET_OF_LIST_REMOVE_DUPLICATES = prove(`!list:(A)list.
1831 set_of_list (REMOVE_DUPLICATES list) = set_of_list list`,
1832 LIST_INDUCT_TAC THEN REWRITE_TAC[REMOVE_DUPLICATES; set_of_list] THEN
1833 COND_CASES_TAC THEN ASM_REWRITE_TAC[set_of_list] THEN
1834 POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM IN_SET_OF_LIST] THEN
1840 let SET_OF_LIST_FLATTEN = prove(`!list:((A)list)list.
1841 set_of_list (FLATTEN list) = UNIONS {set_of_list l | MEM l list}`,
1842 LIST_INDUCT_TAC THEN REWRITE_TAC[FLATTEN; ITLIST; MEM] THENL
1844 SET_TAC[set_of_list];
1847 REWRITE_TAC[GSYM FLATTEN] THEN
1848 ASM_REWRITE_TAC[SET_OF_LIST_APPEND] THEN
1854 let NODE_OF_LIST_LEMMA = prove(`!(x:A) L.
1855 set_of_list (FILTER (\d. FST d = x) (list_of_darts L))
1856 = {(x, y) | y | (x, y) IN darts_of_list L}`,
1857 REWRITE_TAC[SET_OF_LIST_FILTER; darts_of_list; IN_SET_OF_LIST] THEN
1859 REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
1860 X_GEN_TAC `d:A#A` THEN
1861 EQ_TAC THEN STRIP_TAC THENL
1863 EXISTS_TAC `SND (d:A#A)` THEN
1864 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
1871 let NODES_OF_LIST = prove(`!L:((A)list)list. set_of_list (nodes_of_list L)
1872 = {{(x, y) | y | (x, y) IN darts_of_list L} | x | x IN elements_of_list L}`,
1873 REWRITE_TAC[nodes_of_list; list_of_nodes] THEN
1874 REWRITE_TAC[SET_OF_LIST_MAP] THEN
1875 REWRITE_TAC[GSYM IMAGE_LEMMA; IN_ELIM_THM; GSYM elements_of_list] THEN
1877 REWRITE_TAC[EXTENSION] THEN
1878 REWRITE_TAC[IN_ELIM_THM] THEN
1879 X_GEN_TAC `y:A#A->bool` THEN
1880 EQ_TAC THEN STRIP_TAC THENL
1882 POP_ASSUM MP_TAC THEN
1883 ASM_REWRITE_TAC[NODE_OF_LIST_LEMMA] THEN
1885 EXISTS_TAC `x':A` THEN
1889 EXISTS_TAC `FILTER (\d. FST d = x:A) (list_of_darts L)` THEN
1890 ASM_REWRITE_TAC[NODE_OF_LIST_LEMMA] THEN
1891 EXISTS_TAC `x:A` THEN
1892 ASM_REWRITE_TAC[]);;
1896 let GOOD_LIST_NODE = prove(`!L (d:A#A). good_list L /\ good_list_nodes L /\ d IN darts_of_list L
1897 ==> node (hypermap_of_list L) d = {(FST d, x) | x | (FST d, x) IN darts_of_list L}`,
1898 REWRITE_TAC[good_list_nodes; Hypermap.node_set; Hypermap.set_of_orbits] THEN
1899 REWRITE_TAC[GSYM Hypermap.node] THEN
1900 REWRITE_TAC[NODES_OF_LIST] THEN
1902 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [EXTENSION] THEN
1903 REWRITE_TAC[IN_ELIM_THM] THEN
1904 REPEAT STRIP_TAC THEN
1905 FIRST_X_ASSUM (MP_TAC o SPEC `node (hypermap_of_list L) (d:A#A)`) THEN
1906 SUBGOAL_THEN `?x:A#A. x IN dart (hypermap_of_list L) /\ node (hypermap_of_list L) d = node (hypermap_of_list L) x` ASSUME_TAC THENL
1908 EXISTS_TAC `d:A#A` THEN
1909 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST];
1912 ASM_REWRITE_TAC[] THEN
1914 ASM_REWRITE_TAC[] THEN
1915 MP_TAC (ISPECL [`hypermap_of_list (L:((A)list)list)`; `d:A#A`] Hypermap.node_refl) THEN
1916 ASM_REWRITE_TAC[IN_ELIM_THM] THEN
1918 ASM_REWRITE_TAC[]);;
1921 let PREV_EL_LIST_PAIRS_GENERAL = prove(`!x (y:A) list. MEM (x,y) (list_pairs list)
1922 ==> ?z. PREV_EL (x,y) (list_pairs list) = (z, x) /\ MEM (z,x) (list_pairs list)`,
1923 REPEAT STRIP_TAC THEN
1924 ABBREV_TAC `z = FST (PREV_EL (x:A,y) (list_pairs list))` THEN
1925 EXISTS_TAC `z:A` THEN
1926 SUBGOAL_THEN `PREV_EL (x:A,y) (list_pairs list) = z,x` ASSUME_TAC THENL
1928 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1929 REWRITE_TAC[PREV_EL] THEN
1930 ABBREV_TAC `k = INDEX (x:A,y) (list_pairs list)` THEN
1931 ABBREV_TAC `n = LENGTH (list:(A)list)` THEN
1932 SUBGOAL_THEN `k < n:num` ASSUME_TAC THENL
1934 MP_TAC (SPEC `list:(A)list` LENGTH_LIST_PAIRS) THEN
1935 ASM_REWRITE_TAC[] THEN
1936 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1938 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
1942 COND_CASES_TAC THENL
1944 MP_TAC (ISPEC `list_pairs (list:(A)list)` LAST_EL) THEN
1948 UNDISCH_TAC `MEM (x:A,y) (list_pairs list)` THEN
1949 ASM_REWRITE_TAC[MEM];
1952 DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1953 ASM_REWRITE_TAC[LENGTH_LIST_PAIRS] THEN
1954 MP_TAC (SPECL [`n - 1`; `list:(A)list`] EL_LIST_PAIRS) THEN
1955 ASM_REWRITE_TAC[] THEN
1958 MATCH_MP_TAC (ARITH_RULE `k < n ==> n - 1 < n`) THEN
1963 DISCH_THEN (fun th -> REWRITE_TAC[th; PAIR_EQ]) THEN
1964 MP_TAC (ISPECL [`(x:A,y:A)`; `list_pairs (list:(A)list)`] EL_INDEX) THEN
1965 ASM_REWRITE_TAC[] THEN
1966 MP_TAC (SPECL [`0`; `list:(A)list`] EL_LIST_PAIRS) THEN
1969 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
1973 DISCH_THEN (fun th -> SIMP_TAC[th; PAIR_EQ]);
1977 MP_TAC (SPECL [`k - 1`; `list:(A)list`] EL_LIST_PAIRS) THEN
1978 ASM_SIMP_TAC[ARITH_RULE `k < n ==> k - 1 < n`; PAIR_EQ] THEN
1979 DISCH_THEN (fun th -> ALL_TAC) THEN
1980 ASM_SIMP_TAC[ARITH_RULE `k < n /\ ~(k = 0) ==> ~(k - 1 = n - 1)`] THEN
1981 ASM_SIMP_TAC[ARITH_RULE `~(k = 0) ==> k - 1 + 1 = k`] THEN
1983 MP_TAC (ISPECL [`(x:A,y:A)`; `list_pairs (list:(A)list)`] EL_INDEX) THEN
1984 ASM_REWRITE_TAC[] THEN
1985 ASM_SIMP_TAC[EL_LIST_PAIRS; PAIR_EQ];
1989 ASM_REWRITE_TAC[] THEN
1990 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
1991 MATCH_MP_TAC MEM_PREV_EL THEN
1992 ASM_REWRITE_TAC[]);;
1996 let N_LIST_EXT_FST = prove(`!(x:A) y L. good_list L /\ (x,y) IN darts_of_list L
1997 ==> ?z. n_list_ext L (x,y) = (x,z) /\ (x,z) IN darts_of_list L`,
1998 REPEAT STRIP_TAC THEN FIRST_ASSUM MP_TAC THEN
1999 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
2000 GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV)[DART_IN_FACE] THEN
2001 REWRITE_TAC[FIND_FACE] THEN
2003 MP_TAC (SPECL[`x:A`; `y:A`; `find_pair_list (x:A,y) L`] PREV_EL_LIST_PAIRS_GENERAL) THEN
2004 ASM_REWRITE_TAC[] THEN
2007 EXISTS_TAC `z:A` THEN
2008 SUBGOAL_THEN `n_list_ext L (x,y) = x,z:A` ASSUME_TAC THENL
2010 ASM_REWRITE_TAC[n_list_ext; res; n_list; FIND_FACE; e_list];
2014 ASM_REWRITE_TAC[] THEN
2015 REWRITE_TAC[GSYM IN_SET_OF_LIST; GSYM darts_of_list] THEN
2016 MP_TAC (ISPECL[`n_list_ext (L:((A)list)list)`; `darts_of_list (L:((A)list)list)`] PERMUTES_IMP_INSIDE) THEN
2017 ASM_SIMP_TAC[N_LIST_EXT_PERMUTES_DARTS] THEN
2018 DISCH_THEN (MP_TAC o SPEC `x:A,y:A`) THEN
2025 let LIST_EXT_POWER_IN_DARTS = prove(`!(d:A#A) L n. good_list L /\ d IN darts_of_list L
2026 ==> (e_list_ext L POWER n) d IN darts_of_list L /\
2027 (n_list_ext L POWER n) d IN darts_of_list L /\
2028 (f_list_ext L POWER n) d IN darts_of_list L`,
2029 REPEAT GEN_TAC THEN STRIP_TAC THEN
2030 ABBREV_TAC `H = hypermap_of_list (L:((A)list)list)` THEN
2031 MP_TAC (SPEC_ALL COMPONENTS_HYPERMAP_OF_LIST) THEN
2032 ASM_REWRITE_TAC[] THEN
2033 REPEAT STRIP_TAC THENL
2035 MATCH_MP_TAC IN_TRANS THEN
2036 EXISTS_TAC `edge H (d:A#A)` THEN
2037 MP_TAC (ISPECL [`H:(A#A)hypermap`; `d:A#A`] Hypermap.lemma_edge_subset) THEN
2038 ASM_SIMP_TAC[Hypermap.edge; Hypermap.orbit_map] THEN
2039 REWRITE_TAC[IN_ELIM_THM] THEN
2041 EXISTS_TAC `n:num` THEN
2042 REWRITE_TAC[GE; LE_0];
2044 MATCH_MP_TAC IN_TRANS THEN
2045 EXISTS_TAC `node H (d:A#A)` THEN
2046 MP_TAC (ISPECL [`H:(A#A)hypermap`; `d:A#A`] Hypermap.lemma_node_subset) THEN
2047 ASM_SIMP_TAC[Hypermap.node; Hypermap.orbit_map] THEN
2048 REWRITE_TAC[IN_ELIM_THM] THEN
2050 EXISTS_TAC `n:num` THEN
2051 REWRITE_TAC[GE; LE_0];
2053 MATCH_MP_TAC IN_TRANS THEN
2054 EXISTS_TAC `face H (d:A#A)` THEN
2055 MP_TAC (ISPECL [`H:(A#A)hypermap`; `d:A#A`] Hypermap.lemma_face_subset) THEN
2056 ASM_SIMP_TAC[Hypermap.face; Hypermap.orbit_map] THEN
2057 REWRITE_TAC[IN_ELIM_THM] THEN
2059 EXISTS_TAC `n:num` THEN
2060 REWRITE_TAC[GE; LE_0];
2065 let FST_N_LIST_EXT_POWER = prove(`!x (y:A) L n. good_list L /\ x,y IN darts_of_list L
2066 ==> FST ((n_list_ext L POWER n) (x,y)) = x`,
2067 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN
2068 INDUCT_TAC THEN REWRITE_TAC[Hypermap.POWER_0; I_THM] THEN
2070 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
2071 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2072 ABBREV_TAC `d = (n_list_ext L POWER n) (x:A,y)` THEN
2073 ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
2074 MP_TAC (SPECL [`FST (d:A#A)`; `SND (d:A#A)`; `L:((A)list)list`] N_LIST_EXT_FST) THEN
2075 ASM_REWRITE_TAC[PAIR] THEN
2079 ASM_SIMP_TAC[LIST_EXT_POWER_IN_DARTS];
2083 ASM_REWRITE_TAC[]);;
2088 let MEM_LIST_PAIRS_EXISTS = prove(`!x l. MEM x l <=> ?y:A. MEM (x,y) (list_pairs l)`,
2093 EXISTS_TAC `NEXT_EL (x:A) l` THEN
2094 REWRITE_TAC[MEM_EXISTS_EL] THEN
2095 EXISTS_TAC `INDEX (x:A) l` THEN
2096 REWRITE_TAC[LENGTH_LIST_PAIRS] THEN
2097 ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH] THEN
2098 ASM_SIMP_TAC[GSYM INDEX_LT_LENGTH; EL_LIST_PAIRS] THEN
2099 ASM_SIMP_TAC[EL_INDEX; PAIR_EQ; NEXT_EL] THEN
2100 COND_CASES_TAC THEN ASM_REWRITE_TAC[EL];
2103 ASM_SIMP_TAC[MEM_LIST_PAIRS]);;
2108 let MEM_LIST_OF_DARTS = prove(`!d L. MEM d (list_of_darts L) <=>
2109 ?l:(A)list. MEM l L /\ MEM d (list_pairs l)`,
2110 REPEAT GEN_TAC THEN EQ_TAC THENL
2112 SPEC_TAC (`L:((A)list)list`, `L:((A)list)list`) THEN
2113 LIST_INDUCT_TAC THEN REWRITE_TAC[list_of_darts; ITLIST; MEM] THEN
2114 REWRITE_TAC[GSYM list_of_darts; MEM_APPEND] THEN
2117 EXISTS_TAC `h:(A)list` THEN
2121 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
2122 ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
2123 EXISTS_TAC `l:(A)list` THEN
2128 MATCH_MP_TAC DART_IN_DARTS THEN
2129 EXISTS_TAC `l:(A)list` THEN ASM_REWRITE_TAC[]);;
2134 let MEM_LIST_OF_ELEMENTS = prove(`!x L. MEM x (list_of_elements L) <=>
2135 ?y:A. MEM (x,y) (list_of_darts L)`,
2136 REWRITE_TAC[list_of_elements; MEM_REMOVE_DUPLICATES; MEM_FLATTEN] THEN
2137 REWRITE_TAC[MEM_LIST_OF_DARTS] THEN
2138 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
2139 REWRITE_TAC[RIGHT_EXISTS_AND_THM] THEN
2140 REWRITE_TAC[GSYM MEM_LIST_PAIRS_EXISTS]);;
2146 let ALL_DISTINCT_FILTER = prove(`!(P:A->bool) l. ALL_DISTINCT l ==> ALL_DISTINCT (FILTER P l)`,
2147 GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[ALL_DISTINCT_ALT; FILTER] THEN
2149 FIRST_X_ASSUM (MP_TAC o check (is_imp o concl)) THEN
2150 ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
2151 COND_CASES_TAC THEN ASM_REWRITE_TAC[ALL_DISTINCT_ALT; MEM_FILTER]);;
2156 let ALL_DISTINCT_NODE = prove(`!L (n:(A#A)list). good_list L /\ MEM n (list_of_nodes L)
2157 ==> ALL_DISTINCT n`,
2158 REWRITE_TAC[good_list; list_of_nodes; MEM_MAP] THEN
2159 REPEAT STRIP_TAC THEN
2160 ASM_REWRITE_TAC[] THEN
2161 MATCH_MP_TAC ALL_DISTINCT_FILTER THEN
2162 ASM_REWRITE_TAC[]);;
2167 let ALL_DISTINCT_FACE = prove(`!L (f:(A#A)list). good_list L /\ MEM f (list_of_faces L)
2168 ==> ALL_DISTINCT f`,
2169 REPEAT STRIP_TAC THEN
2170 MP_TAC (SPECL [`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2171 ASM_REWRITE_TAC[] THEN
2173 ASM_REWRITE_TAC[] THEN
2174 MATCH_MP_TAC ALL_DISTINCT_FIND_FACE THEN
2175 UNDISCH_TAC `good_list (L:((A)list)list)` THEN
2176 SIMP_TAC[good_list]);;
2182 let LIST_OF_EDGES = prove(`!L:((A)list)list. good_list L ==>
2183 hyp_edge_pairs (hypermap_of_list L) = set_of_list (list_of_edges L)`,
2184 REWRITE_TAC[hyp_edge_pairs; list_of_edges] THEN
2185 REPEAT STRIP_TAC THEN
2186 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST] THEN
2187 REWRITE_TAC[darts_of_list; e_list_ext; e_list; res; IN_SET_OF_LIST] THEN
2188 REWRITE_TAC[EXTENSION; IN_SET_OF_LIST; IN_ELIM_THM; MEM_MAP] THEN
2189 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
2191 POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
2193 EXISTS_TAC `x':A#A` THEN
2195 EXISTS_TAC `x':A#A` THEN
2200 (* Theorems for special lists *)
2202 let FACE_OF_LIST = prove(`!L (x:A#A). good_list L /\ MEM x (list_of_darts L) ==>
2203 face (hypermap_of_list L) x = set_of_list (find_face x L)`,
2204 REPEAT STRIP_TAC THEN
2205 MP_TAC (SPEC `L:((A)list)list` FACE_SET_EQ_LIST) THEN
2206 ASM_REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
2207 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST; darts_of_list; IN_SET_OF_LIST] THEN
2208 GEN_REWRITE_TAC LAND_CONV [EXTENSION] THEN
2209 DISCH_THEN (MP_TAC o SPEC `face (hypermap_of_list L) (x:A#A)`) THEN
2210 REWRITE_TAC[IN_ELIM_THM] THEN
2211 DISCH_THEN (MP_TAC o MATCH_MP (TAUT `(A <=> B) ==> (A ==> B)`)) THEN
2214 EXISTS_TAC `x:A#A` THEN
2218 REWRITE_TAC[IN_SET_OF_LIST; faces_of_list; MEM_MAP] THEN
2219 DISCH_THEN (X_CHOOSE_THEN `f:(A#A)list` STRIP_ASSUME_TAC) THEN
2221 MP_TAC (SPECL [`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2222 ASM_REWRITE_TAC[] THEN
2224 ASM_REWRITE_TAC[] THEN
2226 MATCH_MP_TAC (GSYM MEM_FIND_FACE_IMP_FACES_EQ) THEN
2229 UNDISCH_TAC `good_list (L:((A)list)list)` THEN
2230 SIMP_TAC[good_list];
2234 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2236 REWRITE_TAC[GSYM IN_SET_OF_LIST] THEN
2237 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2238 REWRITE_TAC[Hypermap.face_refl]);;
2242 let CARD_FACE_OF_LIST = prove(`!L (x:A#A). good_list L /\ MEM x (list_of_darts L) ==>
2243 CARD (face (hypermap_of_list L) x) = LENGTH (find_face x L)`,
2244 REPEAT STRIP_TAC THEN
2245 ASM_SIMP_TAC[FACE_OF_LIST] THEN
2246 MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
2247 MATCH_MP_TAC ALL_DISTINCT_FIND_FACE THEN
2248 REMOVE_ASSUM THEN POP_ASSUM MP_TAC THEN
2249 SIMP_TAC[good_list]);;
2252 let LIST_OF_FACES_n = prove(`!(L:((A)list)list) n. good_list L ==>
2253 {f | f IN face_set (hypermap_of_list L) /\ CARD f = n} =
2254 set_of_list (MAP set_of_list (FILTER (\f. LENGTH f = n) (list_of_faces L)))`,
2255 REPEAT STRIP_TAC THEN
2256 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
2257 REWRITE_TAC[Hypermap.face_set; Hypermap.set_of_orbits; GSYM Hypermap.face] THEN
2258 REWRITE_TAC[IN_ELIM_THM] THEN
2259 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST] THEN
2260 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST] THEN
2261 REWRITE_TAC[EXTENSION] THEN
2262 X_GEN_TAC `f:A#A->bool` THEN
2263 REWRITE_TAC[GSYM EXTENSION] THEN
2264 REWRITE_TAC[IN_ELIM_THM; IN_SET_OF_LIST; MEM_MAP; MEM_FILTER] THEN
2268 EXISTS_TAC `find_face (x:A#A) L` THEN
2269 ASM_SIMP_TAC[MEM_FIND_FACE; FACE_OF_LIST] THEN
2270 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2271 ASM_SIMP_TAC[CARD_FACE_OF_LIST];
2272 DISCH_THEN (X_CHOOSE_THEN `l:(A#A)list` STRIP_ASSUME_TAC) THEN
2273 MP_TAC (SPECL[`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2274 ASM_REWRITE_TAC[] THEN
2278 EXISTS_TAC `d:A#A` THEN
2279 ASM_REWRITE_TAC[] THEN
2280 ASM_SIMP_TAC[FACE_OF_LIST];
2284 UNDISCH_TAC `LENGTH (l:(A#A)list) = n` THEN
2285 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
2286 ASM_REWRITE_TAC[] THEN
2287 MATCH_MP_TAC CARD_SET_OF_LIST_ALL_DISTINCT THEN
2288 MATCH_MP_TAC ALL_DISTINCT_FIND_FACE THEN
2295 let LIST_OF_FACES3 = prove(`!L:((A)list)list. good_list L ==>
2296 hyp_face3 (hypermap_of_list L) =
2297 set_of_list (MAP set_of_list (list_of_faces3 L))`,
2298 REWRITE_TAC[hyp_face3; list_of_faces3] THEN
2299 REWRITE_TAC[LIST_OF_FACES_n]);;
2303 let LIST_OF_FACES4 = prove(`!L:((A)list)list. good_list L ==>
2304 hyp_face4 (hypermap_of_list L) =
2305 set_of_list (MAP set_of_list (list_of_faces4 L))`,
2306 REWRITE_TAC[hyp_face4; list_of_faces4] THEN
2307 REWRITE_TAC[LIST_OF_FACES_n]);;
2311 let LIST_OF_FACES5 = prove(`!L:((A)list)list. good_list L ==>
2312 hyp_face5 (hypermap_of_list L) =
2313 set_of_list (MAP set_of_list (list_of_faces5 L))`,
2314 REWRITE_TAC[hyp_face5; list_of_faces5] THEN
2315 REWRITE_TAC[LIST_OF_FACES_n]);;
2319 let LIST_OF_FACES6 = prove(`!L:((A)list)list. good_list L ==>
2320 hyp_face6 (hypermap_of_list L) =
2321 set_of_list (MAP set_of_list (list_of_faces6 L))`,
2322 REWRITE_TAC[hyp_face6; list_of_faces6] THEN
2323 REWRITE_TAC[LIST_OF_FACES_n]);;
2328 let LIST_OF_DARTS3 = prove(`!L:((A)list)list. good_list L ==>
2329 hyp_dart3 (hypermap_of_list L) = set_of_list (list_of_darts3 L)`,
2330 REWRITE_TAC[hyp_dart3; list_of_darts3; list_of_faces3] THEN
2331 REPEAT STRIP_TAC THEN
2332 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
2333 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST] THEN
2334 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; LIST_OF_DARTS] THEN
2335 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SET_OF_LIST] THEN
2336 REWRITE_TAC[MEM_FLATTEN; MEM_FILTER] THEN
2337 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
2339 EXISTS_TAC `l:(A#A)list` THEN
2340 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2341 ASM_REWRITE_TAC[] THEN
2342 MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2343 ASM_REWRITE_TAC[] THEN
2345 ASM_REWRITE_TAC[] THEN
2346 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2348 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
2349 EXISTS_TAC `d:A#A` THEN
2350 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2353 ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2355 MATCH_MP_TAC (GSYM MEM_FIND_FACE_IMP_FACES_EQ) THEN
2356 ASM_REWRITE_TAC[] THEN
2357 REMOVE_ASSUM THEN POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2363 EXISTS_TAC `l:(A#A)list` THEN
2368 MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2369 ASM_REWRITE_TAC[] THEN
2372 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2374 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
2375 EXISTS_TAC `d:A#A` THEN
2376 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2380 ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2381 UNDISCH_TAC `LENGTH (l:(A#A)list) = 3` THEN
2382 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
2384 ASM_REWRITE_TAC[] THEN
2385 MATCH_MP_TAC (MEM_FIND_FACE_IMP_FACES_EQ) THEN
2386 ASM_REWRITE_TAC[] THEN
2387 REMOVE_ASSUM THEN POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;
2391 let LIST_OF_DARTS4 = prove(`!L:((A)list)list. good_list L ==>
2392 hyp_dart4 (hypermap_of_list L) = set_of_list (list_of_darts4 L)`,
2393 REWRITE_TAC[hyp_dart4; list_of_darts4; list_of_faces4] THEN
2394 REPEAT STRIP_TAC THEN
2395 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
2396 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST] THEN
2397 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; LIST_OF_DARTS] THEN
2398 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SET_OF_LIST] THEN
2399 REWRITE_TAC[MEM_FLATTEN; MEM_FILTER] THEN
2400 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
2402 EXISTS_TAC `l:(A#A)list` THEN
2403 POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2404 ASM_REWRITE_TAC[] THEN
2405 MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2406 ASM_REWRITE_TAC[] THEN
2408 ASM_REWRITE_TAC[] THEN
2409 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2411 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
2412 EXISTS_TAC `d:A#A` THEN
2413 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2416 ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2418 MATCH_MP_TAC (GSYM MEM_FIND_FACE_IMP_FACES_EQ) THEN
2419 ASM_REWRITE_TAC[] THEN
2420 REMOVE_ASSUM THEN POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2426 EXISTS_TAC `l:(A#A)list` THEN
2431 MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2432 ASM_REWRITE_TAC[] THEN
2435 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2437 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
2438 EXISTS_TAC `d:A#A` THEN
2439 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2443 ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2444 UNDISCH_TAC `LENGTH (l:(A#A)list) = 4` THEN
2445 DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
2447 ASM_REWRITE_TAC[] THEN
2448 MATCH_MP_TAC (MEM_FIND_FACE_IMP_FACES_EQ) THEN
2449 ASM_REWRITE_TAC[] THEN
2450 REMOVE_ASSUM THEN POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;
2454 let LIST_OF_DARTS_X = prove(`!L:((A)list)list. good_list L ==>
2455 hyp_dartX (hypermap_of_list L) = set_of_list (list_of_dartsX L)`,
2456 REWRITE_TAC[hyp_dartX; list_of_dartsX; list_of_faces456] THEN
2457 REPEAT STRIP_TAC THEN
2458 FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
2459 ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST] THEN
2460 REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; LIST_OF_DARTS] THEN
2461 REWRITE_TAC[EXTENSION; IN_ELIM_THM; IN_SET_OF_LIST] THEN
2462 REWRITE_TAC[MEM_FLATTEN; MEM_FILTER] THEN
2463 GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL
2465 EXISTS_TAC `l:(A#A)list` THEN
2466 ASM_REWRITE_TAC[] THEN
2467 POP_ASSUM MP_TAC THEN
2468 MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2469 ASM_REWRITE_TAC[] THEN
2471 ASM_REWRITE_TAC[] THEN
2472 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2474 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
2475 EXISTS_TAC `d:A#A` THEN
2476 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2479 ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2480 SUBGOAL_THEN `find_face (x:A#A) L = find_face d L` (fun th -> SIMP_TAC[th]) THEN
2481 MATCH_MP_TAC MEM_FIND_FACE_IMP_FACES_EQ THEN
2482 ASM_REWRITE_TAC[] THEN
2483 REMOVE_ASSUM THEN POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2489 EXISTS_TAC `l:(A#A)list` THEN
2494 MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2495 ASM_REWRITE_TAC[] THEN
2498 SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2500 MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
2501 EXISTS_TAC `d:A#A` THEN
2502 POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
2506 ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2507 UNDISCH_TAC `4 <= LENGTH (l:(A#A)list)` THEN
2508 ASM_REWRITE_TAC[] THEN
2509 SUBGOAL_THEN `find_face (x:A#A) L = find_face d L` (fun th -> SIMP_TAC[th]) THEN
2510 MATCH_MP_TAC (MEM_FIND_FACE_IMP_FACES_EQ) THEN
2511 ASM_REWRITE_TAC[] THEN
2512 REMOVE_ASSUM THEN POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;