formal_lp/old/hypermap/list_hypermap_defs.hl

   1 (* Sets *)
   2
   3 let hyp_edge_pairs = new_definition `hyp_edge_pairs H = {x, edge_map H x | x | x IN dart H}`;;
   4
   5 let hyp_dart3 = new_definition `hyp_dart3 H = {x | x IN dart H /\ CARD (face H x) = 3}`;;
   6 let hyp_dart4 = new_definition `hyp_dart4 H = {x | x IN dart H /\ CARD (face H x) = 4}`;;
   7 let hyp_dartX = new_definition `hyp_dartX H = {x | x IN dart H /\ 4 <= CARD (face H x)}`;;
   8
   9 let hyp_face3 = new_definition `hyp_face3 H = {f | f IN face_set H /\ CARD f = 3}`;;
  10 let hyp_face4 = new_definition `hyp_face4 H = {f | f IN face_set H /\ CARD f = 4}`;;
  11 let hyp_face5 = new_definition `hyp_face5 H = {f | f IN face_set H /\ CARD f = 5}`;;
  12 let hyp_face6 = new_definition `hyp_face6 H = {f | f IN face_set H /\ CARD f = 6}`;;
  13
  14
  15 (* List operations *)
  16
  17 let FLATTEN = new_definition `FLATTEN ll = ITLIST (\list all. APPEND list all) ll []`;;
  18
  19 let REMOVE_DUPLICATES = define `REMOVE_DUPLICATES [] = [] /\
  20   REMOVE_DUPLICATES (CONS h t) = if (MEM h t) then REMOVE_DUPLICATES t else CONS h (REMOVE_DUPLICATES t)`;;
  21
  22
  23 (* INDEX 2 [1;3;4;2] = 3 *)
  24 let INDEX = define `INDEX i [] = 0 /\ INDEX i (CONS h t) = if (i = h) then 0 else SUC (INDEX i t)`;;
  25
  26 let ALL_DISTINCT = new_definition `ALL_DISTINCT list = (!i j. i < LENGTH list /\ j < LENGTH list /\ ~(i = j) ==> ~(EL i list = EL j list))`;;
  27
  28
  29 (* Sum of the list elements *)
  30 let list_sum = new_definition `list_sum list f = ITLIST (\t1 t2. f t1 + t2) list (&0)`;;
  31
  32
  33
  34 (* shift_left [1;2;3] = [2;3;1] *)
  35 let shift_left = define `shift_left [] = [] /\ shift_left (CONS h t) = APPEND t [h]`;;
  36
  37 let shift_right = new_definition `shift_right list = if (list = []) then [] else CONS (LAST list) (BUTLAST list)`;;
  38
  39
  40 (* Returns the next element in the cyclic order:
  41  NEXT_EL [1;3;2] 3 = 2
  42  NEXT_EL [1;3;2] 2 = 1 *)
  43
  44 let NEXT_EL = new_definition `NEXT_EL x list =
  45   if (INDEX x list = LENGTH list - 1) then HD list else EL (INDEX x list + 1) list`;;
  46
  47 let PREV_EL = new_definition `PREV_EL x list =
  48   if (INDEX x list = 0) then LAST list else EL (INDEX x list - 1) list`;;
  49
  50
  51
  52 (* list_pairs [1;2;3] = {(1,2), (2,3), (3,1)} *)
  53 let list_pairs = new_definition `list_pairs list = ZIP list (shift_left list)`;;
  54
  55
  56 let list_of_darts = new_definition `list_of_darts ll = ITLIST (\list all. APPEND (list_pairs list) all) ll []`;;
  57
  58 let darts_of_list = new_definition `darts_of_list ll = set_of_list (list_of_darts ll)`;;
  59
  60 let list_of_edges = new_definition `list_of_edges L = MAP (\d:A#A. d, (SND d,FST d)) (list_of_darts L)`;;
  61
  62 let list_of_faces = new_definition `list_of_faces ll = MAP list_pairs ll`;;
  63
  64 let faces_of_list = new_definition `faces_of_list ll = MAP set_of_list (list_of_faces ll)`;;
  65
  66 let list_of_elements = new_definition `list_of_elements ll = REMOVE_DUPLICATES (FLATTEN ll)`;;
  67
  68 let elements_of_list = new_definition `elements_of_list ll = set_of_list (list_of_elements ll)`;;
  69
  70 let list_of_nodes = new_definition `list_of_nodes ll = MAP (\x. FILTER (\d. FST d = x) (list_of_darts ll)) (list_of_elements ll)`;;
  71
  72 let nodes_of_list = new_definition `nodes_of_list ll = MAP set_of_list (list_of_nodes ll)`;;
  73
  74
  75 (* Special lists *)
  76
  77 let list_of_faces3 = new_definition `list_of_faces3 (L:((A)list)list) =
  78   FILTER (\f. LENGTH f = 3) (list_of_faces L)`;;
  79
  80 let list_of_faces4 = new_definition `list_of_faces4 (L:((A)list)list) =
  81   FILTER (\f. LENGTH f = 4) (list_of_faces L)`;;
  82
  83 let list_of_faces5 = new_definition `list_of_faces5 (L:((A)list)list) =
  84   FILTER (\f. LENGTH f = 5) (list_of_faces L)`;;
  85
  86 let list_of_faces6 = new_definition `list_of_faces6 (L:((A)list)list) =
  87   FILTER (\f. LENGTH f = 6) (list_of_faces L)`;;
  88
  89 let list_of_faces456 = new_definition `list_of_faces456 (L:((A)list)list) =
  90   FILTER (\f. 4 <= LENGTH f) (list_of_faces L)`;;
  91
  92
  93 let list_of_darts3 = new_definition `list_of_darts3 (L:((A)list)list) =
  94   FLATTEN (list_of_faces3 L)`;;
  95
  96 let list_of_darts4 = new_definition `list_of_darts4 (L:((A)list)list) =
  97   FLATTEN (list_of_faces4 L)`;;
  98
  99 let list_of_dartsX = new_definition `list_of_dartsX (L:((A)list)list) =
 100   FLATTEN (list_of_faces456 L)`;;
 101
 102
 103 (* Faces *)
 104
 105 let find_list = define `find_list x [] = [] /\ find_list x (CONS h t) = if (MEM x h) then h else find_list x t`;;
 106
 107 let find_pair_list = define `find_pair_list d [] = [] /\ find_pair_list d (CONS h t) = if (MEM d (list_pairs h)) then h else find_pair_list d t`;;
 108
 109 let find_face = new_definition `find_face d ll = find_list d (list_of_faces ll)`;;
 110
 111
 112 (* Hypermap maps *)
 113
 114 let f_list = new_definition `f_list ll d = NEXT_EL d (find_face d ll)`;;
 115
 116 let e_list = new_definition `e_list ll d = (SND d, FST d)`;;
 117
 118 (* let n_list = new_definition `n_list ll d = (FST d, PREV_EL (FST d) (find_pair_list d ll))`;; *)
 119 let n_list = new_definition `n_list ll d = e_list ll (PREV_EL d (find_face d ll))`;;
 120
 121
 122
 123
 124 (* Hypermap definition *)
 125
 126 let f_list_ext = new_definition `f_list_ext ll = res (f_list ll) (darts_of_list ll)`;;
 127 let e_list_ext = new_definition `e_list_ext ll = res (e_list ll) (darts_of_list ll)`;;
 128 let n_list_ext = new_definition `n_list_ext ll = res (n_list ll) (darts_of_list ll)`;;
 129
 130
 131 let hypermap_of_list = new_definition `hypermap_of_list (ll:((A)list)list) = hypermap (darts_of_list ll, e_list_ext ll, n_list_ext ll, f_list_ext ll)`;;
 132
 133
 134
 135 (* Define "good" lists *)
 136 let good_list = new_definition `good_list ll <=> ALL_DISTINCT (list_of_darts ll) /\
 137                                                  ALL (\l. ~(l = [])) ll /\
 138                                                  (!d. MEM d (list_of_darts ll) ==> MEM (SND d, FST d) (list_of_darts ll))`;;
 139
 140
 141
 142
 143
 144
 145
 146 (* Some general theorems *)
 147
 148 let ALL_DISTINCT_ALT = prove(`!(h:A) t. (ALL_DISTINCT ([]:(A)list) <=> T) /\ (ALL_DISTINCT (CONS h t) <=> ALL_DISTINCT t /\ ~(MEM h t))`,
 149    REPEAT STRIP_TAC THENL
 150      [
 151        REWRITE_TAC[ALL_DISTINCT; LENGTH] THEN
 152          REWRITE_TAC[ARITH_RULE `~(i < 0)`];
 153        ALL_TAC
 154      ] THEN
 155
 156      REWRITE_TAC[ALL_DISTINCT] THEN
 157      EQ_TAC THENL
 158      [
 159        REPEAT STRIP_TAC THENL
 160          [
 161            FIRST_X_ASSUM (MP_TAC o SPECL [`SUC i`; `SUC j`]) THEN
 162              ASM_REWRITE_TAC[LENGTH; LT_SUC; SUC_INJ] THEN
 163              ASM_REWRITE_TAC[EL; TL];
 164            ALL_TAC
 165          ] THEN
 166
 167          POP_ASSUM MP_TAC THEN REWRITE_TAC[MEM_EXISTS_EL] THEN
 168          STRIP_TAC THEN
 169          FIRST_X_ASSUM (MP_TAC o SPECL [`0`; `SUC i`]) THEN
 170          ASM_REWRITE_TAC[LENGTH; LT_SUC; LT_0; GSYM NOT_SUC] THEN
 171          REWRITE_TAC[EL; HD; TL];
 172        ALL_TAC
 173      ] THEN
 174
 175      REPEAT STRIP_TAC THEN
 176      POP_ASSUM MP_TAC THEN
 177      DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
 178      [
 179        DISJ_CASES_TAC (SPEC `j:num` num_CASES) THENL
 180          [
 181            UNDISCH_TAC `~(i = j:num)` THEN ASM_REWRITE_TAC[];
 182            ALL_TAC
 183          ] THEN
 184
 185          POP_ASSUM CHOOSE_TAC THEN
 186          ASM_REWRITE_TAC[EL; HD; TL] THEN
 187          DISCH_TAC THEN UNDISCH_TAC `~MEM (h:A) t` THEN
 188          REWRITE_TAC[MEM_EXISTS_EL] THEN
 189          EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 190          UNDISCH_TAC `j < LENGTH (CONS (h:A) t)` THEN
 191          ASM_REWRITE_TAC[LENGTH; LT_SUC];
 192        ALL_TAC
 193      ] THEN
 194
 195      POP_ASSUM CHOOSE_TAC THEN
 196      DISJ_CASES_TAC (SPEC `j:num` num_CASES) THENL
 197      [
 198        ASM_REWRITE_TAC[EL; HD; TL] THEN
 199          DISCH_TAC THEN UNDISCH_TAC `~MEM (h:A) t` THEN
 200          REWRITE_TAC[MEM_EXISTS_EL] THEN
 201          EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[] THEN
 202          UNDISCH_TAC `i < LENGTH (CONS (h:A) t)` THEN
 203          ASM_REWRITE_TAC[LENGTH; LT_SUC];
 204        ALL_TAC
 205      ] THEN
 206
 207      POP_ASSUM CHOOSE_TAC THEN
 208      ASM_REWRITE_TAC[EL; TL] THEN
 209      DISCH_TAC THEN
 210      FIRST_X_ASSUM (MP_TAC o SPECL [`n:num`; `n':num`]) THEN
 211      ANTS_TAC THENL
 212      [
 213        UNDISCH_TAC `i < LENGTH (CONS (h:A) t)` THEN UNDISCH_TAC `j < LENGTH (CONS (h:A) t)` THEN
 214          UNDISCH_TAC `~(i = j:num)` THEN
 215          ASM_SIMP_TAC[LENGTH; LT_SUC; SUC_INJ];
 216        ALL_TAC
 217      ] THEN
 218
 219      ASM_REWRITE_TAC[]);;