formal_lp/old/ineqs/list_hypermap.hl

   1 needs "../formal_lp/hypermap/list_hypermap_defs.hl";;
   2
   3
   4 open Sphere;;
   5 (* For IMAGE_LEMMA *)
   6 open Hypermap_and_fan;;
   7
   8 let REMOVE_ASSUM = POP_ASSUM (fun th -> ALL_TAC);;
   9
  10 let IN_TRANS = prove(`!(x:A) s t. t SUBSET s /\ x IN t ==> x IN s`,
  11    SET_TAC[]);;
  12
  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
  16      DISCH_TAC THEN
  17      FIRST_X_ASSUM MATCH_MP_TAC THEN
  18      ASM_REWRITE_TAC[]);;
  19
  20
  21
  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
  28      ASM_SIMP_TAC[]);;
  29
  30
  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
  36      [
  37        ASM_REWRITE_TAC[EL; HD];
  38        ALL_TAC
  39      ] THEN
  40      POP_ASSUM CHOOSE_TAC THEN
  41      ASM_REWRITE_TAC[LT_SUC; EL; TL]);;
  42
  43
  44 (****************************)
  45
  46 (* INDEX *)
  47
  48
  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
  52      [
  53        ASM_REWRITE_TAC[INDEX; EL; HD];
  54        ALL_TAC
  55      ] THEN
  56      ASM_REWRITE_TAC[INDEX; EL; TL]);;
  57
  58
  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]);;
  62
  63
  64
  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);;
  69
  70
  71
  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]);;
  75
  76
  77 (* ALL_DISTINCT *)
  78
  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
  82      STRIP_TAC 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]);;
  86
  87
  88 (* list_sum *)
  89
  90
  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
  94      STRIP_TAC THEN
  95      ASM_SIMP_TAC[SUM_CLAUSES; FINITE_SET_OF_LIST] THEN
  96      ASM_REWRITE_TAC[IN_SET_OF_LIST]);;
  97
  98
  99
 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
 102      STRIP_TAC 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]);;
 108
 109
 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[]);;
 121
 122
 123
 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]);;
 130
 131
 132
 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]);;
 137
 138
 139
 140
 141
 142 (* Shift left/right *)
 143
 144
 145
 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)))`,
 149    REPEAT GEN_TAC THEN
 150      REWRITE_TAC[shift_right; NOT_CONS_NIL; LAST; BUTLAST]);;
 151
 152
 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]);;
 155
 156
 157
 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[]);;
 162
 163
 164
 165
 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
 168      COND_CASES_TAC THENL
 169      [
 170        POP_ASSUM MP_TAC THEN REWRITE_TAC[APPEND_EQ_NIL; NOT_CONS_NIL];
 171        ALL_TAC
 172      ] THEN
 173      ASM_REWRITE_TAC[]);;
 174
 175
 176
 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
 181      COND_CASES_TAC THENL
 182      [
 183        POP_ASSUM (MP_TAC o AP_TERM `LENGTH:(A)list->num`) THEN
 184          REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN ARITH_TAC;
 185        ALL_TAC
 186      ] THEN
 187      REWRITE_TAC[BUTLAST_APPEND_SING; LAST_APPEND; NOT_CONS_NIL; LAST]);;
 188
 189
 190
 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]);;
 193
 194
 195
 196 let MEM_SHIFT_RIGHT = prove(`!(x:A) l. MEM x l <=> MEM x (shift_right l)`,
 197    REPEAT GEN_TAC THEN
 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]);;
 202
 203
 204
 205
 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
 208      STRIP_TAC THENL
 209      [
 210        ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `SUC n - 1 = n`; LT_REFL; SUB_REFL; EL; HD];
 211        ALL_TAC
 212      ] THEN
 213      ASM_SIMP_TAC[ARITH_RULE `i < n ==> ~(i = SUC n - 1)`] THEN
 214      ASM_REWRITE_TAC[EL_APPEND; GSYM ADD1; EL; TL]);;
 215
 216
 217
 218
 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);;
 222
 223
 224 let LENGTH_SHIFT_RIGHT = prove(`!list:(A)list. LENGTH (shift_right list) = LENGTH list`,
 225    GEN_TAC THEN
 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]);;
 229
 230
 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
 234      [
 235        SUBGOAL_THEN `~(list:(A)list = [])` ASSUME_TAC THENL
 236          [
 237            DISCH_TAC THEN UNDISCH_TAC `i < LENGTH (list:(A)list)` THEN
 238              ASM_REWRITE_TAC[LENGTH; LT_REFL];
 239            ALL_TAC
 240          ] THEN
 241          ASM_SIMP_TAC[GSYM LAST_EL] THEN
 242          ASM_REWRITE_TAC[shift_right; EL; HD];
 243        ALL_TAC
 244      ] THEN
 245
 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
 251      ANTS_TAC THENL
 252      [
 253        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 254        ALL_TAC
 255      ] THEN
 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
 258      [
 259        POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN ARITH_TAC;
 260        ALL_TAC
 261      ] THEN
 262      ASM_SIMP_TAC[ARITH_RULE `~(i = 0) ==> i - 1 + 1 = i`]);;
 263
 264
 265 (* NEXT_EL, PREV_EL *)
 266
 267
 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]);;
 274
 275
 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]);;
 286
 287
 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]);;
 295
 296
 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]);;
 304
 305
 306
 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]);;
 309
 310
 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
 315      [
 316        DISCH_TAC THEN UNDISCH_TAC `MEM (x:A) list` THEN
 317          ASM_REWRITE_TAC[MEM];
 318        ALL_TAC
 319      ] THEN
 320      COND_CASES_TAC THENL
 321      [
 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
 325          ASM_REWRITE_TAC[];
 326        ALL_TAC
 327      ] THEN
 328
 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
 332      [
 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];
 337        ALL_TAC
 338      ] THEN
 339
 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
 345      ASM_SIMP_TAC[]);;
 346
 347
 348
 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
 353      [
 354        DISCH_TAC THEN UNDISCH_TAC `MEM (x:A) list` THEN
 355          ASM_REWRITE_TAC[MEM];
 356        ALL_TAC
 357      ] THEN
 358      SUBGOAL_THEN `0 < LENGTH (list:(A)list)` ASSUME_TAC THENL
 359      [
 360        UNDISCH_TAC `~(list = []:(A)list)` THEN
 361          ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN
 362          REWRITE_TAC[NOT_LT; LE; LENGTH_EQ_NIL];
 363        ALL_TAC
 364      ] THEN
 365
 366      COND_CASES_TAC THENL
 367      [
 368        REWRITE_TAC[NEXT_EL] THEN
 369          SUBGOAL_THEN `INDEX (LAST list) (list:(A)list) = LENGTH list - 1` ASSUME_TAC THENL
 370          [
 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`];
 374            ALL_TAC
 375          ] THEN
 376          ASM_REWRITE_TAC[] THEN
 377          MP_TAC (SPECL [`x:A`; `list:(A)list`] EL_INDEX) THEN
 378          ASM_REWRITE_TAC[EL];
 379        ALL_TAC
 380      ] THEN
 381
 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
 385      [
 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];
 390        ALL_TAC
 391      ] THEN
 392
 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
 400      ASM_SIMP_TAC[]);;
 401
 402
 403
 404 (* FLATTEN, REMOVE_DUPLICATES *)
 405
 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[]);;
 410
 411
 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]);;
 416
 417
 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
 421      EQ_TAC THENL
 422      [
 423        STRIP_TAC THENL
 424          [
 425            EXISTS_TAC `h:(A)list` THEN ASM_REWRITE_TAC[];
 426            ALL_TAC
 427          ] THEN
 428          POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
 429          EXISTS_TAC `l:(A)list` THEN
 430          ASM_REWRITE_TAC[];
 431        ALL_TAC
 432      ] THEN
 433      STRIP_TAC THENL
 434      [
 435        UNDISCH_TAC `l = h:(A)list` THEN DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]);
 436        ALL_TAC
 437      ] THEN
 438      DISJ2_TAC THEN ASM_REWRITE_TAC[] THEN
 439      EXISTS_TAC `l:(A)list` THEN ASM_REWRITE_TAC[]);;
 440
 441
 442 (* lists *)
 443
 444
 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]);;
 448
 449
 450
 451
 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]);;
 455
 456
 457 (* Faces *)
 458
 459
 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
 463      [
 464        REWRITE_TAC[MAP; find_list; find_pair_list; list_pairs; shift_left; ZIP];
 465        ALL_TAC
 466      ] THEN
 467      REWRITE_TAC[MAP; find_pair_list; find_list] THEN
 468      COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
 469
 470
 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
 475      STRIP_TAC THENL
 476      [
 477        POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[find_list] THEN DISCH_TAC THEN
 478          ASM_REWRITE_TAC[];
 479        ALL_TAC
 480      ] THEN
 481      ASM_CASES_TAC `MEM (x:A) h` THEN ASM_REWRITE_TAC[find_list] THEN
 482      DISJ2_TAC THEN
 483      FIRST_X_ASSUM MATCH_MP_TAC THEN
 484      EXISTS_TAC `l:(A)list` THEN
 485      ASM_REWRITE_TAC[]);;
 486
 487
 488
 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
 494      ASM_REWRITE_TAC[]);;
 495
 496
 497
 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
 502      EQ_TAC THENL
 503      [
 504        ASM_REWRITE_TAC[MEM_FIND_LIST];
 505        ALL_TAC
 506      ] THEN
 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
 509      DISCH_TAC THEN
 510      FIRST_X_ASSUM (MP_TAC o check(is_imp o concl)) THEN
 511      ANTS_TAC THENL
 512      [
 513        GEN_TAC THEN DISCH_TAC THEN
 514          FIRST_X_ASSUM (MP_TAC o SPEC `x:(A)list`) THEN
 515          ASM_REWRITE_TAC[];
 516        ALL_TAC
 517      ] THEN
 518
 519      DISCH_TAC THEN
 520      REWRITE_TAC[find_list] THEN
 521      SUBGOAL_THEN `!t. find_list x t = h ==> MEM (x:A) h` ASSUME_TAC THENL
 522      [
 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]);
 528        ALL_TAC
 529      ] THEN
 530
 531      ASM_CASES_TAC `MEM (x:A) h` THEN ASM_REWRITE_TAC[] THENL
 532      [
 533        REWRITE_TAC[MEM_FLATTEN; MEM] THEN
 534          EXISTS_TAC `h:(A)list` THEN
 535          ASM_REWRITE_TAC[];
 536        ALL_TAC
 537      ] THEN
 538      STRIP_TAC THENL
 539      [
 540        FIRST_X_ASSUM (MP_TAC o SPEC `t:((A)list)list`) THEN
 541          ASM_REWRITE_TAC[];
 542        ALL_TAC
 543      ] THEN
 544      REWRITE_TAC[FLATTEN; ITLIST; MEM_APPEND] THEN
 545      ASM_REWRITE_TAC[GSYM FLATTEN] THEN
 546      FIRST_X_ASSUM MATCH_MP_TAC THEN
 547      ASM_REWRITE_TAC[]);;
 548
 549
 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]);;
 564
 565
 566
 567 (* Hypermap maps properties *)
 568
 569
 570 (* e_list_ext permutes darts *)
 571
 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
 580      [
 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];
 585        ALL_TAC
 586      ] THEN
 587      ASM_REWRITE_TAC[]);;
 588
 589
 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
 594      SIMP_TAC[]);;
 595
 596
 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
 604      ASM_REWRITE_TAC[]);;
 605
 606
 607
 608
 609
 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
 613      [
 614        REPEAT STRIP_TAC THEN
 615        ASM_REWRITE_TAC[e_list_ext; res];
 616        ALL_TAC
 617      ] THEN
 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]);;
 622
 623
 624
 625 (* f_list_ext permutes darts *)
 626
 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
 630      [
 631        DISJ1_TAC THEN
 632          POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
 633        ALL_TAC
 634      ] THEN
 635      DISJ2_TAC THEN
 636      REWRITE_TAC[GSYM list_of_darts] THEN
 637      FIRST_X_ASSUM MATCH_MP_TAC THEN
 638      ASM_REWRITE_TAC[]);;
 639
 640
 641
 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
 644      [
 645        ASM_REWRITE_TAC[list_of_darts; ITLIST; MEM];
 646        ALL_TAC
 647      ] THEN
 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
 653      ASM_REWRITE_TAC[]);;
 654
 655
 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
 658      [
 659        ASM_REWRITE_TAC[list_of_darts; ITLIST; MEM; find_pair_list; list_pairs; shift_left; ZIP];
 660        ALL_TAC
 661      ] THEN
 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]);;
 665
 666
 667
 668
 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]);;
 671
 672
 673
 674
 675
 676
 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])));;
 687
 688
 689
 690
 691
 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
 695      [
 696        REWRITE_TAC[MEM];
 697        ALL_TAC
 698      ] THEN
 699      REWRITE_TAC[MEM; list_of_darts; ITLIST] THEN
 700      REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 701      [
 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
 704          DISCH_TAC 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
 711          ASM_REWRITE_TAC[];
 712
 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
 715          DISCH_TAC 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
 722          ASM_REWRITE_TAC[];
 723
 724        ALL_TAC
 725      ] THEN
 726
 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]);;
 731
 732
 733
 734
 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
 742      [
 743        MATCH_MP_TAC DART_IN_DARTS THEN
 744          EXISTS_TAC `l:(A)list` THEN
 745          ASM_REWRITE_TAC[];
 746        ALL_TAC
 747      ] THEN
 748      ASM_SIMP_TAC[MEM_FIND_PAIR_LIST] THEN
 749      ASM_REWRITE_TAC[GSYM DART_IN_FIND_PAIR_LIST]);;
 750
 751
 752
 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
 757      STRIP_TAC THEN
 758      COND_CASES_TAC THEN ASM_SIMP_TAC[]);;
 759
 760
 761
 762
 763
 764
 765
 766
 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]);;
 771
 772
 773
 774
 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]);;
 780
 781
 782
 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]);;
 788
 789
 790
 791
 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[]);;
 800
 801
 802
 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
 807      STRIP_TAC 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]);;
 811
 812
 813
 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
 824      [
 825        DISCH_TAC THEN
 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
 842          ASM_SIMP_TAC[]
 843      ]);;
 844
 845
 846
 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
 859      DISCH_TAC THEN
 860      MP_TAC (SPEC_ALL INDEX_EL) THEN
 861      ASM_SIMP_TAC[]);;
 862
 863
 864
 865
 866
 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);;
 878
 879
 880
 881
 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
 890      [
 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];
 894        ALL_TAC
 895      ] THEN
 896
 897      SUBGOAL_THEN `EL i (list_pairs list) = d:A#A` ASSUME_TAC THENL
 898      [
 899        EXPAND_TAC "i" THEN
 900          MATCH_MP_TAC EL_INDEX THEN ASM_REWRITE_TAC[];
 901        ALL_TAC
 902      ] THEN
 903
 904      MP_TAC (SPECL [`i:num`; `d:A#A`; `list:(A)list`] INDEX_FST_SND) THEN
 905      ASM_REWRITE_TAC[] THEN
 906
 907      COND_CASES_TAC THEN ASM_REWRITE_TAC[] THENL
 908      [
 909        STRIP_TAC THEN
 910          ASM_REWRITE_TAC[] THEN
 911          MP_TAC (SPEC_ALL EL_LIST_PAIRS) THEN
 912          ASM_REWRITE_TAC[] THEN
 913          ANTS_TAC THENL
 914          [
 915            MATCH_MP_TAC (ARITH_RULE `i < n ==> n - 1 < n`) THEN
 916              ASM_REWRITE_TAC[];
 917            ALL_TAC
 918          ] 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[];
 926        ALL_TAC
 927      ] THEN
 928
 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
 932      [
 933        REPLICATE_TAC 3 (POP_ASSUM MP_TAC) THEN ARITH_TAC;
 934        ALL_TAC
 935      ] THEN
 936
 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]);;
 944
 945
 946
 947
 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
 953      [
 954        EXPAND_TAC "t" THEN
 955          MATCH_MP_TAC MEM_PREV_EL THEN
 956          ASM_REWRITE_TAC[];
 957        ALL_TAC
 958      ] THEN
 959      MP_TAC (SPECL [`t:A#A`; `list:(A)list`] MEM_LIST_PAIRS_EXPLICIT) THEN
 960      ASM_REWRITE_TAC[] THEN
 961
 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
 965      REWRITE_TAC[] THEN
 966      MP_TAC (SPEC_ALL PREV_NEXT_ID) THEN
 967      ANTS_TAC THENL
 968      [
 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
 972          ASM_SIMP_TAC[];
 973        ALL_TAC
 974      ] THEN
 975      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
 976      SUBGOAL_THEN `y = FST (d:A#A)` ASSUME_TAC THENL
 977      [
 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
 981          ANTS_TAC THENL
 982          [
 983            ASM_REWRITE_TAC[] THEN
 984              MATCH_MP_TAC ALL_DISTINCT_LIST_PAIRS THEN
 985              ASM_REWRITE_TAC[];
 986            ALL_TAC
 987          ] THEN
 988          REWRITE_TAC[] 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]);
 994        ALL_TAC
 995      ] THEN
 996
 997      DISCH_THEN (fun th -> ASM_REWRITE_TAC[SYM th]));;
 998
 999
1000
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
1006      [
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
1009          [
1010            EXPAND_TAC "f" THEN REWRITE_TAC[FIND_FACE] THEN
1011              AP_TERM_TAC THEN
1012              REWRITE_TAC[GSYM FIND_FACE] THEN
1013
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
1021              EXPAND_TAC "f" THEN
1022              ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1023            ALL_TAC
1024          ] THEN
1025
1026          ASM_REWRITE_TAC[] THEN
1027          MATCH_MP_TAC NEXT_PREV_ID THEN
1028          MP_TAC (SPEC_ALL ALL_DISTINCT_FIND_FACE) THEN
1029          ASM_SIMP_TAC[] THEN
1030          DISCH_TAC THEN
1031          POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
1032          EXPAND_TAC "f" THEN
1033          ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1034        ALL_TAC
1035      ] THEN
1036
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
1039      [
1040        EXPAND_TAC "f" THEN REWRITE_TAC[FIND_FACE] THEN
1041          AP_TERM_TAC THEN
1042          REWRITE_TAC[GSYM FIND_FACE] THEN
1043
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
1051          EXPAND_TAC "f" THEN
1052          ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1053        ALL_TAC
1054      ] THEN
1055
1056      ASM_REWRITE_TAC[] THEN
1057      MATCH_MP_TAC PREV_NEXT_ID THEN
1058      MP_TAC (SPEC_ALL ALL_DISTINCT_FIND_FACE) THEN
1059      ASM_SIMP_TAC[] THEN
1060      DISCH_TAC THEN
1061      POP_ASSUM (fun th -> ALL_TAC) THEN POP_ASSUM (fun th -> ALL_TAC) THEN
1062      EXPAND_TAC "f" THEN
1063      ASM_REWRITE_TAC[GSYM DART_IN_FACE]);;
1064
1065
1066
1067
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
1072      AP_TERM_TAC 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]);;
1077
1078
1079
1080
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
1086      [
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
1091          STRIP_TAC THEN
1092          EXISTS_TAC `x:A#A` THEN
1093          CONJ_TAC THENL
1094          [
1095            SUBGOAL_THEN `MEM (x:A#A) (list_of_darts ll)` ASSUME_TAC THENL
1096              [
1097                REWRITE_TAC[DART_IN_FACE] THEN
1098                  EXPAND_TAC "x" 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
1100                  [
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
1105                      EXPAND_TAC "x" THEN
1106                      MATCH_MP_TAC MEM_PREV_EL THEN
1107                      ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1108                    ALL_TAC
1109                  ] THEN
1110
1111                  MATCH_MP_TAC MEM_PREV_EL THEN
1112                  ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1113                ALL_TAC
1114              ] THEN
1115
1116              ASM_REWRITE_TAC[];
1117            ALL_TAC
1118          ] THEN
1119
1120          X_GEN_TAC `d:A#A` THEN
1121          COND_CASES_TAC THENL
1122          [
1123            DISCH_TAC THEN
1124              MP_TAC (SPEC_ALL F_LIST_INVERSE) THEN
1125              ASM_REWRITE_TAC[LET_DEF; LET_END_DEF] THEN
1126              SIMP_TAC[];
1127            ALL_TAC
1128          ] THEN
1129          DISCH_THEN (fun th -> POP_ASSUM (MP_TAC o REWRITE_RULE[th])) THEN
1130          ASM_REWRITE_TAC[];
1131        ALL_TAC
1132      ] THEN
1133
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
1138      [
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];
1149        ALL_TAC
1150      ] THEN
1151
1152      REWRITE_TAC[]);;
1153
1154
1155
1156
1157
1158
1159 (* e o n o f = I *)
1160
1161
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
1165      [
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];
1169        ALL_TAC
1170      ] THEN
1171      ASM_REWRITE_TAC[GSYM list_of_faces; GSYM find_face; GSYM list_of_darts; MEM_APPEND]);;
1172
1173
1174
1175
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]);;
1187
1188
1189
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
1192      [
1193        REWRITE_TAC[find_face; list_of_darts; ITLIST; MEM; list_of_faces; MAP; find_list];
1194        ALL_TAC
1195      ] THEN
1196      REWRITE_TAC[find_face; list_of_darts; ITLIST; MEM_APPEND; list_of_faces; MAP; find_list] THEN
1197      COND_CASES_TAC THENL
1198      [
1199        DISCH_THEN (fun th -> REWRITE_TAC[th]);
1200        ALL_TAC
1201      ] THEN
1202      ASM_SIMP_TAC[GSYM list_of_faces; GSYM find_face; GSYM list_of_darts]);;
1203
1204
1205
1206
1207
1208
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
1216      [
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
1219          [
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];
1224            ALL_TAC
1225          ] THEN
1226
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
1229          [
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];
1236            ALL_TAC
1237          ] THEN
1238
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];
1242        ALL_TAC
1243      ] THEN
1244
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
1248      [
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];
1253        ALL_TAC
1254      ] THEN
1255
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
1258      [
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];
1265        ALL_TAC
1266      ] THEN
1267
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]);;
1271
1272
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[]);;
1280
1281
1282
1283
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
1293      [
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];
1298        ALL_TAC
1299      ] THEN
1300
1301      REWRITE_TAC[n_list]);;
1302
1303
1304
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]);;
1313
1314
1315
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
1321      [
1322        REWRITE_TAC[o_ASSOC];
1323        ALL_TAC
1324      ] THEN
1325
1326      ASM_SIMP_TAC[E_LIST_EXT_INVOLUTION; F_LIST_EXT_INVERSE_WORKS] THEN
1327      REWRITE_TAC[I_O_ID]);;
1328
1329
1330
1331 (* hypermap_of_list is a hypermap *)
1332
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]);;
1340
1341
1342 (* Set of faces *)
1343
1344
1345
1346
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
1353      [
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
1357          ARITH_TAC;
1358        ALL_TAC
1359      ] THEN
1360      COND_CASES_TAC THENL
1361      [
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];
1365        ALL_TAC
1366      ] THEN
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);;
1372
1373
1374
1375
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
1381      INDUCT_TAC THENL
1382      [
1383        REWRITE_TAC[ADD_0; Hypermap.POWER_0; I_THM] THEN
1384          STRIP_TAC THEN
1385          SUBGOAL_THEN `k MOD n = k` (fun th -> REWRITE_TAC[th]) THENL
1386          [
1387            MATCH_MP_TAC MOD_LT THEN
1388              EXPAND_TAC "k" THEN EXPAND_TAC "n" THEN
1389              ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
1390            ALL_TAC
1391          ] THEN
1392
1393          EXPAND_TAC "k" THEN
1394          MATCH_MP_TAC (GSYM EL_INDEX) THEN
1395          ASM_REWRITE_TAC[];
1396        ALL_TAC
1397      ] THEN
1398
1399      STRIP_TAC THEN
1400      SUBGOAL_THEN `~(n = 0)` ASSUME_TAC THENL
1401      [
1402        POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1403          STRIP_TAC THEN UNDISCH_TAC `i' < n:num` THEN
1404          ARITH_TAC;
1405        ALL_TAC
1406      ] THEN
1407
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
1413      ANTS_TAC THENL
1414      [
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];
1419        ALL_TAC
1420      ] THEN
1421
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
1424      [
1425        EXPAND_TAC "y" THEN
1426          MATCH_MP_TAC INDEX_EL THEN
1427          ASM_SIMP_TAC[DIVISION];
1428        ALL_TAC
1429      ] THEN
1430
1431      AP_THM_TAC THEN AP_TERM_TAC THEN
1432      ASM_CASES_TAC `n = 1` THENL
1433      [
1434        ASM_REWRITE_TAC[MOD_1];
1435        ALL_TAC
1436      ] THEN
1437      SUBGOAL_THEN `1 = 1 MOD n` (fun th -> ONCE_REWRITE_TAC[th]) THENL
1438      [
1439        MATCH_MP_TAC (GSYM MOD_LT) THEN
1440          ASM_REWRITE_TAC[ARITH_RULE `1 < n <=> ~(n = 0) /\ ~(n = 1)`];
1441        ALL_TAC
1442      ] THEN
1443      ASM_SIMP_TAC[MOD_ADD_MOD] THEN
1444      AP_THM_TAC THEN AP_TERM_TAC THEN
1445      ARITH_TAC);;
1446
1447
1448
1449
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
1455      [
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;
1459        ALL_TAC
1460      ] THEN
1461      REWRITE_TAC[Hypermap.orbit_map; EXTENSION; IN_SET_OF_LIST; IN_ELIM_THM] THEN
1462      GEN_TAC THEN EQ_TAC THENL
1463      [
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];
1468        ALL_TAC
1469      ] THEN
1470      ASM_REWRITE_TAC[MEM_EXISTS_EL] THEN
1471      STRIP_TAC 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
1476      [
1477        EXPAND_TAC "k" THEN EXPAND_TAC "n" THEN
1478          ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
1479        ALL_TAC
1480      ] THEN
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[]);;
1489
1490
1491
1492
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
1498      [
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];
1506        ALL_TAC
1507      ] THEN
1508
1509      ASM_REWRITE_TAC[]);;
1510
1511
1512
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
1522      DISCH_TAC THEN
1523      FIRST_X_ASSUM (MP_TAC o SPEC `(f POWER n) (x:A)`) THEN
1524      ASM_REWRITE_TAC[GE; LE_0]);;
1525
1526
1527
1528
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
1537      [
1538        ASM_REWRITE_TAC[res];
1539        ALL_TAC
1540      ] THEN
1541      MP_TAC (ISPECL [`res (f:A->A) s`; `s:A->bool`] Hypermap_and_fan.PERMUTES_IMP_INSIDE) THEN
1542      ASM_SIMP_TAC[]);;
1543
1544
1545
1546
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
1553      DISCH_TAC THEN
1554      SUBGOAL_THEN `x:A#A IN darts_of_list ll` ASSUME_TAC THENL
1555      [
1556        ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST];
1557        ALL_TAC
1558      ] THEN
1559      ASM_SIMP_TAC[ORBIT_MAP_RES] THEN
1560
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
1563      [
1564        INDUCT_TAC THENL
1565          [
1566            REWRITE_TAC[Hypermap.POWER_0; I_THM];
1567            ALL_TAC
1568          ] THEN
1569
1570          ASM_REWRITE_TAC[Hypermap.COM_POWER; o_THM] THEN
1571          REWRITE_TAC[f_list] THEN
1572          AP_TERM_TAC 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
1576          ANTS_TAC THENL
1577          [
1578            ASM_SIMP_TAC[ALL_DISTINCT_FIND_FACE] THEN
1579              ASM_REWRITE_TAC[GSYM DART_IN_FACE];
1580            ALL_TAC
1581          ] THEN
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
1586          REWRITE_TAC[] THEN
1587          SUBGOAL_THEN `~(LENGTH (f:(A#A)list) = 0)` ASSUME_TAC THENL
1588          [
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
1592              ARITH_TAC;
1593            ALL_TAC
1594          ] THEN
1595          ASM_SIMP_TAC[DIVISION];
1596        ALL_TAC
1597      ] THEN
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]);;
1602
1603
1604
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
1610      STRIP_TAC THEN
1611      MP_TAC (SPECL [`h:(A)list`; `FLATTEN t:(A)list`] ALL_DISTINCT_APPEND) THEN
1612      ASM_REWRITE_TAC[] THEN STRIP_TAC THEN
1613      ASM_SIMP_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
1621      [
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];
1629        ALL_TAC
1630      ] THEN
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
1634      [
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
1639          DISCH_TAC THEN
1640          MP_TAC (SPECL [`APPEND (FLATTEN t) h:(A)list`; `h':(A)list`] ALL_DISTINCT_APPEND) THEN
1641          ASM_SIMP_TAC[];
1642        ALL_TAC
1643      ] THEN
1644      MP_TAC (SPECL [`h':(A)list`; `FLATTEN t:(A)list`] ALL_DISTINCT_APPEND) THEN
1645      ASM_SIMP_TAC[]);;
1646
1647
1648
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]);;
1656
1657
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]);;
1661
1662
1663
1664
1665
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
1668                                         ==> l1 = 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
1673      [
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
1676          DISCH_TAC 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
1683          ASM_REWRITE_TAC[];
1684
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
1687          DISCH_TAC 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
1694          ASM_REWRITE_TAC[];
1695
1696        ALL_TAC
1697      ] THEN
1698
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]);;
1703
1704
1705
1706
1707
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]);;
1716
1717
1718
1719
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
1727      STRIP_TAC THENL
1728      [
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
1735          ASM_REWRITE_TAC[];
1736        ALL_TAC
1737      ] THEN
1738      ASM_REWRITE_TAC[HD] THEN DISCH_TAC THEN
1739      SUBGOAL_THEN `MEM (h:A#A) (list_of_darts ll)` ASSUME_TAC THENL
1740      [
1741        REWRITE_TAC[LIST_OF_DARTS; MEM_FLATTEN] THEN
1742          EXISTS_TAC `f:(A#A)list` THEN
1743          ASM_REWRITE_TAC[MEM];
1744        ALL_TAC
1745      ] THEN
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]);;
1753
1754
1755
1756
1757
1758
1759
1760
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
1767
1768      X_GEN_TAC `f:(A#A->bool)` THEN
1769      REWRITE_TAC[GSYM EXTENSION] THEN
1770      EQ_TAC THENL
1771      [
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
1776          DISCH_TAC 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];
1780        ALL_TAC
1781      ] THEN
1782
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
1787      STRIP_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]);;
1791
1792
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)`;;
1796
1797
1798
1799
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]);;
1808
1809
1810
1811
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
1815      [
1816        REWRITE_TAC[set_of_list] THEN SET_TAC[];
1817        ALL_TAC
1818      ] THEN
1819      COND_CASES_TAC THENL
1820      [
1821        ASM_REWRITE_TAC[set_of_list] THEN
1822          POP_ASSUM MP_TAC THEN SET_TAC[];
1823        ALL_TAC
1824      ] THEN
1825      ASM_REWRITE_TAC[] THEN
1826      POP_ASSUM MP_TAC THEN SET_TAC[]);;
1827
1828
1829
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
1835      SET_TAC[]);;
1836
1837
1838
1839
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
1843      [
1844        SET_TAC[set_of_list];
1845        ALL_TAC
1846      ] THEN
1847      REWRITE_TAC[GSYM FLATTEN] THEN
1848      ASM_REWRITE_TAC[SET_OF_LIST_APPEND] THEN
1849      SET_TAC[]);;
1850
1851
1852
1853
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
1858      REPEAT GEN_TAC THEN
1859      REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
1860      X_GEN_TAC `d:A#A` THEN
1861      EQ_TAC THEN STRIP_TAC THENL
1862      [
1863        EXISTS_TAC `SND (d:A#A)` THEN
1864          POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
1865        ASM_REWRITE_TAC[]
1866      ]);;
1867
1868
1869
1870
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
1876      GEN_TAC 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
1881      [
1882        POP_ASSUM MP_TAC THEN
1883          ASM_REWRITE_TAC[NODE_OF_LIST_LEMMA] THEN
1884          DISCH_TAC THEN
1885          EXISTS_TAC `x':A` THEN
1886          ASM_REWRITE_TAC[];
1887        ALL_TAC
1888      ] 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[]);;
1893
1894
1895
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
1901      REPEAT GEN_TAC 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
1907      [
1908        EXISTS_TAC `d:A#A` THEN
1909          ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST];
1910        ALL_TAC
1911      ] THEN
1912      ASM_REWRITE_TAC[] THEN
1913      STRIP_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
1917      STRIP_TAC THEN
1918      ASM_REWRITE_TAC[]);;
1919
1920
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
1927      [
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
1933          [
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
1937              EXPAND_TAC "k" THEN
1938              ASM_REWRITE_TAC[GSYM INDEX_LT_LENGTH];
1939            ALL_TAC
1940          ] THEN
1941
1942          COND_CASES_TAC THENL
1943          [
1944            MP_TAC (ISPEC `list_pairs (list:(A)list)` LAST_EL) THEN
1945              ANTS_TAC THENL
1946              [
1947                DISCH_TAC THEN
1948                  UNDISCH_TAC `MEM (x:A,y) (list_pairs list)` THEN
1949                  ASM_REWRITE_TAC[MEM];
1950                ALL_TAC
1951              ] THEN
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
1956              ANTS_TAC THENL
1957              [
1958                MATCH_MP_TAC (ARITH_RULE `k < n ==> n - 1 < n`) THEN
1959                  ASM_REWRITE_TAC[];
1960                ALL_TAC
1961              ] THEN
1962
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
1967              ANTS_TAC THENL
1968              [
1969                POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
1970                ALL_TAC
1971              ] THEN
1972
1973              DISCH_THEN (fun th -> SIMP_TAC[th; PAIR_EQ]);
1974            ALL_TAC
1975          ] THEN
1976
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
1982          EXPAND_TAC "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];
1986        ALL_TAC
1987      ] THEN
1988
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[]);;
1993
1994
1995
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
2002      STRIP_TAC 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
2005
2006      STRIP_TAC THEN
2007      EXISTS_TAC `z:A` THEN
2008      SUBGOAL_THEN `n_list_ext L (x,y) = x,z:A` ASSUME_TAC THENL
2009      [
2010        ASM_REWRITE_TAC[n_list_ext; res; n_list; FIND_FACE; e_list];
2011        ALL_TAC
2012      ] THEN
2013
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
2019      ASM_SIMP_TAC[]);;
2020
2021
2022
2023
2024
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
2034       [
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
2040           DISCH_TAC THEN
2041           EXISTS_TAC `n:num` THEN
2042           REWRITE_TAC[GE; LE_0];
2043
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
2049           DISCH_TAC THEN
2050           EXISTS_TAC `n:num` THEN
2051           REWRITE_TAC[GE; LE_0];
2052
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
2058           DISCH_TAC THEN
2059           EXISTS_TAC `n:num` THEN
2060           REWRITE_TAC[GE; LE_0];
2061      ]);;
2062
2063
2064
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
2069      STRIP_TAC 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
2076      ANTS_TAC THENL
2077      [
2078        EXPAND_TAC "d" THEN
2079          ASM_SIMP_TAC[LIST_EXT_POWER_IN_DARTS];
2080        ALL_TAC
2081      ] THEN
2082      STRIP_TAC THEN
2083      ASM_REWRITE_TAC[]);;
2084
2085
2086
2087
2088 let MEM_LIST_PAIRS_EXISTS = prove(`!x l. MEM x l <=> ?y:A. MEM (x,y) (list_pairs l)`,
2089    REPEAT GEN_TAC THEN
2090      EQ_TAC THENL
2091      [
2092        DISCH_TAC THEN
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];
2101        ALL_TAC
2102      ] THEN
2103      ASM_SIMP_TAC[MEM_LIST_PAIRS]);;
2104
2105
2106
2107
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
2111      [
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
2115          STRIP_TAC THENL
2116          [
2117            EXISTS_TAC `h:(A)list` THEN
2118              ASM_REWRITE_TAC[];
2119            ALL_TAC
2120          ] 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
2124          ASM_REWRITE_TAC[];
2125        ALL_TAC
2126      ] THEN
2127      STRIP_TAC THEN
2128      MATCH_MP_TAC DART_IN_DARTS THEN
2129      EXISTS_TAC `l:(A)list` THEN ASM_REWRITE_TAC[]);;
2130
2131
2132
2133
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]);;
2141
2142
2143
2144
2145
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
2148      STRIP_TAC 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]);;
2152
2153
2154
2155
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[]);;
2163
2164
2165
2166
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
2172      STRIP_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]);;
2177
2178
2179
2180
2181
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
2190      [
2191        POP_ASSUM MP_TAC THEN ASM_REWRITE_TAC[] THEN
2192          DISCH_TAC THEN
2193          EXISTS_TAC `x':A#A` THEN
2194          ASM_REWRITE_TAC[];
2195        EXISTS_TAC `x':A#A` THEN
2196          ASM_REWRITE_TAC[]
2197      ]);;
2198
2199
2200 (* Theorems for special lists *)
2201
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
2212      ANTS_TAC THENL
2213      [
2214        EXISTS_TAC `x:A#A` THEN
2215          ASM_REWRITE_TAC[];
2216        ALL_TAC
2217      ] 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
2220
2221      MP_TAC (SPECL [`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2222      ASM_REWRITE_TAC[] THEN
2223      STRIP_TAC THEN
2224      ASM_REWRITE_TAC[] THEN
2225      AP_TERM_TAC THEN
2226      MATCH_MP_TAC (GSYM MEM_FIND_FACE_IMP_FACES_EQ) THEN
2227      CONJ_TAC THENL
2228      [
2229        UNDISCH_TAC `good_list (L:((A)list)list)` THEN
2230          SIMP_TAC[good_list];
2231        ALL_TAC
2232      ] THEN
2233
2234      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
2235      REMOVE_ASSUM 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]);;
2239
2240
2241
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]);;
2250
2251
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
2265      EQ_TAC THENL
2266      [
2267        STRIP_TAC 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
2275          STRIP_TAC THEN
2276          CONJ_TAC THENL
2277          [
2278            EXISTS_TAC `d:A#A` THEN
2279              ASM_REWRITE_TAC[] THEN
2280              ASM_SIMP_TAC[FACE_OF_LIST];
2281            ALL_TAC
2282          ] THEN
2283
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
2289          ASM_REWRITE_TAC[]
2290      ]);;
2291
2292
2293
2294
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]);;
2300
2301
2302
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]);;
2308
2309
2310
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]);;
2316
2317
2318
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]);;
2324
2325
2326
2327
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
2338      [
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
2344          STRIP_TAC THEN
2345          ASM_REWRITE_TAC[] THEN
2346          SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2347          [
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]);
2351            ALL_TAC
2352          ] THEN
2353          ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2354          AP_TERM_TAC 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]);
2358        ALL_TAC
2359      ] THEN
2360
2361      CONJ_TAC THENL
2362      [
2363        EXISTS_TAC `l:(A#A)list` THEN
2364          ASM_REWRITE_TAC[];
2365        ALL_TAC
2366      ] THEN
2367
2368      MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2369      ASM_REWRITE_TAC[] THEN
2370      STRIP_TAC THEN
2371
2372      SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2373      [
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]);
2377        ALL_TAC
2378      ] THEN
2379
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
2383      AP_TERM_TAC 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]));;
2388
2389
2390
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
2401      [
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
2407          STRIP_TAC THEN
2408          ASM_REWRITE_TAC[] THEN
2409          SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2410          [
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]);
2414            ALL_TAC
2415          ] THEN
2416          ASM_SIMP_TAC[CARD_FACE_OF_LIST] THEN
2417          AP_TERM_TAC 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]);
2421        ALL_TAC
2422      ] THEN
2423
2424      CONJ_TAC THENL
2425      [
2426        EXISTS_TAC `l:(A#A)list` THEN
2427          ASM_REWRITE_TAC[];
2428        ALL_TAC
2429      ] THEN
2430
2431      MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2432      ASM_REWRITE_TAC[] THEN
2433      STRIP_TAC THEN
2434
2435      SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2436      [
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]);
2440        ALL_TAC
2441      ] THEN
2442
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
2446      AP_TERM_TAC 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]));;
2451
2452
2453
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
2464      [
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
2470          STRIP_TAC THEN
2471          ASM_REWRITE_TAC[] THEN
2472          SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2473          [
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]);
2477            ALL_TAC
2478          ] THEN
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]);
2484        ALL_TAC
2485      ] THEN
2486
2487      CONJ_TAC THENL
2488      [
2489        EXISTS_TAC `l:(A#A)list` THEN
2490          ASM_REWRITE_TAC[];
2491        ALL_TAC
2492      ] THEN
2493
2494      MP_TAC (SPECL [`l:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
2495      ASM_REWRITE_TAC[] THEN
2496      STRIP_TAC THEN
2497
2498      SUBGOAL_THEN `MEM (x:A#A) (list_of_darts L)` ASSUME_TAC THENL
2499      [
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]);
2503        ALL_TAC
2504      ] THEN
2505
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]));;
2513
2514