3 let hyp_edge_pairs = new_definition `hyp_edge_pairs H = {x, edge_map H x | x | x IN dart H}`;;
5 let hyp_dart3 = new_definition `hyp_dart3 H = {x | x IN dart H /\ CARD (face H x) = 3}`;;
6 let hyp_dart4 = new_definition `hyp_dart4 H = {x | x IN dart H /\ CARD (face H x) = 4}`;;
7 let hyp_dartX = new_definition `hyp_dartX H = {x | x IN dart H /\ 4 <= CARD (face H x)}`;;
9 let hyp_face3 = new_definition `hyp_face3 H = {f | f IN face_set H /\ CARD f = 3}`;;
10 let hyp_face4 = new_definition `hyp_face4 H = {f | f IN face_set H /\ CARD f = 4}`;;
11 let hyp_face5 = new_definition `hyp_face5 H = {f | f IN face_set H /\ CARD f = 5}`;;
12 let hyp_face6 = new_definition `hyp_face6 H = {f | f IN face_set H /\ CARD f = 6}`;;
17 let FLATTEN = new_definition `FLATTEN ll = ITLIST (\list all. APPEND list all) ll []`;;
19 let REMOVE_DUPLICATES = define `REMOVE_DUPLICATES [] = [] /\
20 REMOVE_DUPLICATES (CONS h t) = if (MEM h t) then REMOVE_DUPLICATES t else CONS h (REMOVE_DUPLICATES t)`;;
23 (* INDEX 2 [1;3;4;2] = 3 *)
24 let INDEX = define `INDEX i [] = 0 /\ INDEX i (CONS h t) = if (i = h) then 0 else SUC (INDEX i t)`;;
26 let ALL_DISTINCT = new_definition `ALL_DISTINCT list = (!i j. i < LENGTH list /\ j < LENGTH list /\ ~(i = j) ==> ~(EL i list = EL j list))`;;
29 (* Sum of the list elements *)
30 let list_sum = new_definition `list_sum list f = ITLIST (\t1 t2. f t1 + t2) list (&0)`;;
34 (* shift_left [1;2;3] = [2;3;1] *)
35 let shift_left = define `shift_left [] = [] /\ shift_left (CONS h t) = APPEND t [h]`;;
37 let shift_right = new_definition `shift_right list = if (list = []) then [] else CONS (LAST list) (BUTLAST list)`;;
40 (* Returns the next element in the cyclic order:
42 NEXT_EL [1;3;2] 2 = 1 *)
44 let NEXT_EL = new_definition `NEXT_EL x list =
45 if (INDEX x list = LENGTH list - 1) then HD list else EL (INDEX x list + 1) list`;;
47 let PREV_EL = new_definition `PREV_EL x list =
48 if (INDEX x list = 0) then LAST list else EL (INDEX x list - 1) list`;;
52 (* list_pairs [1;2;3] = {(1,2), (2,3), (3,1)} *)
53 let list_pairs = new_definition `list_pairs list = ZIP list (shift_left list)`;;
56 let list_of_darts = new_definition `list_of_darts ll = ITLIST (\list all. APPEND (list_pairs list) all) ll []`;;
58 let darts_of_list = new_definition `darts_of_list ll = set_of_list (list_of_darts ll)`;;
60 let list_of_edges = new_definition `list_of_edges L = MAP (\d:A#A. d, (SND d,FST d)) (list_of_darts L)`;;
62 let list_of_faces = new_definition `list_of_faces ll = MAP list_pairs ll`;;
64 let faces_of_list = new_definition `faces_of_list ll = MAP set_of_list (list_of_faces ll)`;;
66 let list_of_elements = new_definition `list_of_elements ll = REMOVE_DUPLICATES (FLATTEN ll)`;;
68 let elements_of_list = new_definition `elements_of_list ll = set_of_list (list_of_elements ll)`;;
70 let list_of_nodes = new_definition `list_of_nodes ll = MAP (\x. FILTER (\d. FST d = x) (list_of_darts ll)) (list_of_elements ll)`;;
72 let nodes_of_list = new_definition `nodes_of_list ll = MAP set_of_list (list_of_nodes ll)`;;
77 let list_of_faces3 = new_definition `list_of_faces3 (L:((A)list)list) =
78 FILTER (\f. LENGTH f = 3) (list_of_faces L)`;;
80 let list_of_faces4 = new_definition `list_of_faces4 (L:((A)list)list) =
81 FILTER (\f. LENGTH f = 4) (list_of_faces L)`;;
83 let list_of_faces5 = new_definition `list_of_faces5 (L:((A)list)list) =
84 FILTER (\f. LENGTH f = 5) (list_of_faces L)`;;
86 let list_of_faces6 = new_definition `list_of_faces6 (L:((A)list)list) =
87 FILTER (\f. LENGTH f = 6) (list_of_faces L)`;;
89 let list_of_faces456 = new_definition `list_of_faces456 (L:((A)list)list) =
90 FILTER (\f. 4 <= LENGTH f) (list_of_faces L)`;;
93 let list_of_darts3 = new_definition `list_of_darts3 (L:((A)list)list) =
94 FLATTEN (list_of_faces3 L)`;;
96 let list_of_darts4 = new_definition `list_of_darts4 (L:((A)list)list) =
97 FLATTEN (list_of_faces4 L)`;;
99 let list_of_dartsX = new_definition `list_of_dartsX (L:((A)list)list) =
100 FLATTEN (list_of_faces456 L)`;;
105 let find_list = define `find_list x [] = [] /\ find_list x (CONS h t) = if (MEM x h) then h else find_list x t`;;
107 let find_pair_list = define `find_pair_list d [] = [] /\ find_pair_list d (CONS h t) = if (MEM d (list_pairs h)) then h else find_pair_list d t`;;
109 let find_face = new_definition `find_face d ll = find_list d (list_of_faces ll)`;;
114 let f_list = new_definition `f_list ll d = NEXT_EL d (find_face d ll)`;;
116 let e_list = new_definition `e_list ll d = (SND d, FST d)`;;
118 (* let n_list = new_definition `n_list ll d = (FST d, PREV_EL (FST d) (find_pair_list d ll))`;; *)
119 let n_list = new_definition `n_list ll d = e_list ll (PREV_EL d (find_face d ll))`;;
124 (* Hypermap definition *)
126 let f_list_ext = new_definition `f_list_ext ll = res (f_list ll) (darts_of_list ll)`;;
127 let e_list_ext = new_definition `e_list_ext ll = res (e_list ll) (darts_of_list ll)`;;
128 let n_list_ext = new_definition `n_list_ext ll = res (n_list ll) (darts_of_list ll)`;;
131 let hypermap_of_list = new_definition `hypermap_of_list (ll:((A)list)list) = hypermap (darts_of_list ll, e_list_ext ll, n_list_ext ll, f_list_ext ll)`;;
135 (* Define "good" lists *)
136 let good_list = new_definition `good_list ll <=> ALL_DISTINCT (list_of_darts ll) /\
137 ALL (\l. ~(l = [])) ll /\
138 (!d. MEM d (list_of_darts ll) ==> MEM (SND d, FST d) (list_of_darts ll))`;;
146 (* Some general theorems *)
148 let ALL_DISTINCT_ALT = prove(`!(h:A) t. (ALL_DISTINCT ([]:(A)list) <=> T) /\ (ALL_DISTINCT (CONS h t) <=> ALL_DISTINCT t /\ ~(MEM h t))`,
149 REPEAT STRIP_TAC THENL
151 REWRITE_TAC[ALL_DISTINCT; LENGTH] THEN
152 REWRITE_TAC[ARITH_RULE `~(i < 0)`];
156 REWRITE_TAC[ALL_DISTINCT] THEN
159 REPEAT STRIP_TAC THENL
161 FIRST_X_ASSUM (MP_TAC o SPECL [`SUC i`; `SUC j`]) THEN
162 ASM_REWRITE_TAC[LENGTH; LT_SUC; SUC_INJ] THEN
163 ASM_REWRITE_TAC[EL; TL];
167 POP_ASSUM MP_TAC THEN REWRITE_TAC[MEM_EXISTS_EL] THEN
169 FIRST_X_ASSUM (MP_TAC o SPECL [`0`; `SUC i`]) THEN
170 ASM_REWRITE_TAC[LENGTH; LT_SUC; LT_0; GSYM NOT_SUC] THEN
171 REWRITE_TAC[EL; HD; TL];
175 REPEAT STRIP_TAC THEN
176 POP_ASSUM MP_TAC THEN
177 DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
179 DISJ_CASES_TAC (SPEC `j:num` num_CASES) THENL
181 UNDISCH_TAC `~(i = j:num)` THEN ASM_REWRITE_TAC[];
185 POP_ASSUM CHOOSE_TAC THEN
186 ASM_REWRITE_TAC[EL; HD; TL] THEN
187 DISCH_TAC THEN UNDISCH_TAC `~MEM (h:A) t` THEN
188 REWRITE_TAC[MEM_EXISTS_EL] THEN
189 EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
190 UNDISCH_TAC `j < LENGTH (CONS (h:A) t)` THEN
191 ASM_REWRITE_TAC[LENGTH; LT_SUC];
195 POP_ASSUM CHOOSE_TAC THEN
196 DISJ_CASES_TAC (SPEC `j:num` num_CASES) THENL
198 ASM_REWRITE_TAC[EL; HD; TL] THEN
199 DISCH_TAC THEN UNDISCH_TAC `~MEM (h:A) t` THEN
200 REWRITE_TAC[MEM_EXISTS_EL] THEN
201 EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
202 UNDISCH_TAC `i < LENGTH (CONS (h:A) t)` THEN
203 ASM_REWRITE_TAC[LENGTH; LT_SUC];
207 POP_ASSUM CHOOSE_TAC THEN
208 ASM_REWRITE_TAC[EL; TL] THEN
210 FIRST_X_ASSUM (MP_TAC o SPECL [`n:num`; `n':num`]) THEN
213 UNDISCH_TAC `i < LENGTH (CONS (h:A) t)` THEN UNDISCH_TAC `j < LENGTH (CONS (h:A) t)` THEN
214 UNDISCH_TAC `~(i = j:num)` THEN
215 ASM_SIMP_TAC[LENGTH; LT_SUC; SUC_INJ];