formal_lp/old/hypermap/list_hypermap_computations.hl

   1 (* Explicit computations for hypermap_of_list *)
   2
   3 #load "str.cma";;
   4
   5 needs "../formal_lp/hypermap/list_hypermap.hl";;
   6 needs "../formal_lp/hypermap/list_conversions.hl";;
   7
   8 open Str;;
   9 open List;;
  10
  11
  12
  13 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;
  14
  15
  16 let test n f x =
  17   let start = Sys.time() in
  18     for i = 1 to n do
  19       let _ = f x in ()
  20     done;
  21     Sys.time() -. start;;
  22
  23
  24 (* Constants and variables *)
  25 let hd_var_num = `hd:num` and
  26     h_var_num = `h:num` and
  27     h1_var_num = `h1:num` and
  28     h2_var_num = `h2:num` and
  29     t_var = `t:(num)list` and
  30     x_var_pair = `x:num#num` and
  31     acc_var = `acc:(num#num)list` and
  32     f_var_fun = `f:num#num->num#num`;;
  33
  34 let num_type = `:num`;;
  35 let num_list_type = `:(num)list`;;
  36 let num_list_list_type = `:((num)list)list`;;
  37
  38 let mem_const = `MEM:(num#num)->(num#num)list->bool` and
  39     f_const = `F`;;
  40
  41
  42 let hypermap_of_list_const = `hypermap_of_list:((num)list)list->(num#num)hypermap` and
  43     list_of_darts_const = `list_of_darts:((num)list)list->(num#num)list` and
  44     list_of_edges_const = `list_of_edges:((num)list)list->((num#num)#(num#num))list` and
  45     list_of_faces_const = `list_of_faces:((num)list)list->((num#num)list)list` and
  46     list_of_nodes_const = `list_of_nodes:((num)list)list->((num#num)list)list` and
  47     list_of_elements_const = `list_of_elements:((num)list)list->(num)list` and
  48     list_of_faces3_const = `list_of_faces3:((num)list)list->((num#num)list)list` and
  49     list_of_faces4_const = `list_of_faces4:((num)list)list->((num#num)list)list` and
  50     list_of_faces5_const = `list_of_faces5:((num)list)list->((num#num)list)list` and
  51     list_of_faces6_const = `list_of_faces6:((num)list)list->((num#num)list)list` and
  52     list_of_darts3_const = `list_of_darts3:((num)list)list->(num#num)list` and
  53     list_of_darts4_const = `list_of_darts4:((num)list)list->(num#num)list` and
  54     list_of_dartsX_const = `list_of_dartsX:((num)list)list->(num#num)list` and
  55     good_list_const = `good_list:((num)list)list->bool` and
  56     good_list_nodes_const = `good_list_nodes:((num)list)list->bool`;;
  57
  58
  59
  60 (* example of java style string from hypermap generator. *)
  61 let pentstring = "13_150834109178 18 3 0 1 2 3 3 2 7 3 3 0 2 4 5 4 0 3 4 6 1 0 4 3 7 2 8 3 8 2 1 4 8 1 6 9 3 9 6 10 3 10 6 4 3 10 4 5 4 5 3 7 11 3 10 5 11 3 11 7 12 3 12 7 8 3 12 8 9 3 9 10 11 3 11 12 9 ";;
  62 let test_string = "149438122187 18 6 0 1 2 3 4 5 4 0 5 6 7 3 6 5 4 3 6 4 8 3 8 4 3 3 8 3 9 3 9 3 2 3 9 2 10 3 10 2 11 3 11 2 1 3 11 1 0 3 11 0 7 3 10 11 7 3 10 7 12 3 12 7 6 3 12 6 8 3 12 8 9 3 9 10 12 ";;
  63
  64 (* conversion to list.  e.g. convert_to_list pentstring *)
  65
  66 let convert_to_list  =
  67   let split_sp=  Str.split (regexp " +") in
  68   let strip_ = global_replace (regexp "_") "" in
  69   let rec movelist n (x,a) =
  70     if n=0 then (x,a) else match x with y::ys -> movelist (n-1) (ys, y::a) in
  71   let getone (x,a) = match x with
  72     | [] -> ([],a)
  73     | y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in
  74   let rec getall (x,a) =
  75     if (x=[]) then (x,a) else getall (getone (x,a)) in
  76   fun s ->
  77     let h::ss = (split_sp (strip_ s)) in
  78     let _::ns = map int_of_string ss in
  79     let (_,a) = getall (ns,[]) in
  80      (h,rev (map rev a));;
  81
  82
  83
  84 let create_hol_list str =
  85   let ll = snd (convert_to_list str) in
  86   let s1 = map (map mk_small_numeral) ll in
  87   let s2 = map (fun l -> mk_list (l, num_type)) s1 in
  88     mk_list (s2, num_list_type);;
  89
  90
  91
  92 (********************************************)
  93
  94 (* MEM_CONV and related conversions *)
  95
  96
  97 (* MY_NUM_EQ_CONV *)
  98
  99 let NUMERAL_EQ = prove(`NUMERAL m = NUMERAL n <=> m = n`, REWRITE_TAC[NUMERAL]) and
 100     NUM_EQ_00 = prove(`BIT0 m = BIT0 n <=> m = n`, REWRITE_TAC[BIT0] THEN ARITH_TAC) and
 101     NUM_EQ_10 = prove(`BIT1 m = BIT0 n <=> F`, REWRITE_TAC[ARITH]) and
 102     NUM_EQ_01 = prove(`BIT0 m = BIT1 n <=> F`, REWRITE_TAC[ARITH]) and
 103     NUM_EQ_11 = prove(`BIT1 m = BIT1 n <=> m = n`, REWRITE_TAC[ARITH]) and
 104     NUM_EQ_ZERO_B0 = prove(`_0 = BIT0 n <=> _0 = n`, REWRITE_TAC[ARITH]) and
 105     NUM_EQ_B0_ZERO = prove(`BIT0 n = _0 <=> n = _0`, REWRITE_TAC[ARITH]) and
 106     NUM_EQ_ZERO_B1 = prove(`_0 = BIT1 n <=> F`, REWRITE_TAC[ARITH]) and
 107     NUM_EQ_B1_ZERO = prove(`BIT1 n = _0 <=> F`, REWRITE_TAC[ARITH]) and
 108     NUM_EQ_ZERO_ZERO = prove(`_0 = _0 <=> T`, REWRITE_TAC[ARITH]);;
 109
 110
 111 let zero_const = `_0` and
 112     numeral_const = `NUMERAL` and
 113     n_var_num = `n:num` and
 114     m_var_num = `m:num`;;
 115
 116 let rec raw_num_eq_conv tm =
 117   let lhs, rhs = dest_eq tm in
 118   if (is_comb lhs) then
 119     let bm, m_tm = dest_comb lhs in
 120     let bm_c = fst(dest_const bm) in
 121       if (is_comb rhs) then
 122         let bn, n_tm = dest_comb rhs in
 123         let bn_c = fst(dest_const bn) in
 124           if (bm_c = bn_c) then
 125             let th0 = INST[m_tm, m_var_num; n_tm, n_var_num]
 126               (if (bm_c = "BIT0") then NUM_EQ_00 else NUM_EQ_11) in
 127             let th1 = raw_num_eq_conv (mk_eq (m_tm, n_tm)) in
 128               TRANS th0 th1
 129           else
 130             INST[m_tm, m_var_num; n_tm, n_var_num]
 131               (if (bm_c = "BIT0") then NUM_EQ_01 else NUM_EQ_10)
 132       else
 133         if bm_c = "BIT0" then
 134           let th0 = INST[m_tm, n_var_num] NUM_EQ_B0_ZERO in
 135           let th1 = raw_num_eq_conv (mk_eq (m_tm, zero_const)) in
 136             TRANS th0 th1
 137         else
 138           INST[m_tm, n_var_num] NUM_EQ_B1_ZERO
 139   else
 140     if (is_comb rhs) then
 141       let bn, n_tm = dest_comb rhs in
 142       let bn_c = fst(dest_const bn) in
 143         if (bn_c = "BIT0") then
 144           let th0 = INST[n_tm, n_var_num] NUM_EQ_ZERO_B0 in
 145           let th1 = raw_num_eq_conv (mk_eq (zero_const, n_tm)) in
 146             TRANS th0 th1
 147         else
 148           INST[n_tm, n_var_num] NUM_EQ_ZERO_B1
 149     else
 150       NUM_EQ_ZERO_ZERO;;
 151
 152
 153 let MY_NUM_EQ_CONV tm =
 154   let lhs, rhs = dest_eq tm in
 155     if lhs = rhs then EQT_INTRO (REFL lhs) else
 156       let th0 = INST[rand lhs, m_var_num; rand rhs, n_var_num] NUMERAL_EQ in
 157       let ltm, rtm = dest_eq (concl th0) in
 158         if ltm <> tm then
 159           failwith "MY_NUM_EQ_CONV"
 160         else
 161           TRANS th0 (raw_num_eq_conv rtm);;
 162
 163 (*
 164 let tm1 = `65535 = 32767`;;
 165 let tm2 = `65535 = 65535`;;
 166
 167 test 1000 NUM_EQ_CONV tm1;; (* 0.448 *)
 168 test 1000 NUM_EQ_CONV tm2;; (* 0.488 *)
 169
 170 test 1000 MY_NUM_EQ_CONV tm1;; (* 0.144 *)
 171 test 1000 MY_NUM_EQ_CONV tm2;; (* 0.136 *)
 172 *)
 173
 174 (* NUM_PAIR_EQ_CONV *)
 175
 176 let NUM_PAIR_EQ = UNDISCH_ALL (prove(`(n:num = x <=> T) ==> (m:num = y <=> T) ==> (n, m = x, y <=> T)`, SIMP_TAC[PAIR_EQ])) and
 177     NUM_PAIR_NOT_EQ1 = UNDISCH_ALL (prove(`(n = x <=> F) ==> (n:num,m:num = x,y <=> F)`, SIMP_TAC[PAIR_EQ])) and
 178     NUM_PAIR_NOT_EQ2 = UNDISCH_ALL (prove(`(m = y <=> F) ==> (n:num,m:num = x,y <=> F)`, SIMP_TAC[PAIR_EQ]));;
 179
 180
 181 let t_const = `T` and f_const = `F` and
 182     x_var_num = `x:num` and y_var_num = `y:num`;;
 183
 184
 185 let NUM_PAIR_EQ_CONV tm =
 186   let lhs, rhs = dest_eq tm in
 187     if (lhs = rhs) then
 188       EQT_INTRO (REFL lhs)
 189     else
 190       let n_tm, m_tm = dest_pair lhs in
 191       let x_tm, y_tm = dest_pair rhs in
 192       let inst = INST[n_tm, n_var_num; m_tm, m_var_num; x_tm, x_var_num; y_tm, y_var_num] in
 193       let fst_th = MY_NUM_EQ_CONV (mk_eq (n_tm, x_tm)) in
 194         if (rand(concl fst_th) = t_const) then
 195           let snd_th = MY_NUM_EQ_CONV (mk_eq (m_tm, y_tm)) in
 196             if (rand(concl snd_th) = t_const) then
 197               let th0 = inst NUM_PAIR_EQ in
 198                 MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0)
 199             else
 200               let th0 = inst NUM_PAIR_NOT_EQ2 in
 201                 MY_PROVE_HYP snd_th th0
 202         else
 203           let th0 = inst NUM_PAIR_NOT_EQ1 in
 204             MY_PROVE_HYP fst_th th0;;
 205
 206
 207
 208
 209 (*
 210 let tm1 = `(12,4) = (12,4)` and
 211     tm2 = `(12,4) = (12,5)`;;
 212
 213 NUM_PAIR_EQ_CONV tm1;;
 214 NUM_PAIR_EQ_CONV tm2;;
 215 test 1000 NUM_PAIR_EQ_CONV tm1;; (* 0.016 *)
 216 test 1000 NUM_PAIR_EQ_CONV tm2;; (* 0.040 *)
 217 *)
 218
 219
 220 (* MEM_NUM_CONV *)
 221
 222 let MEM_NUM_EMPTY = prove(`MEM (n:num) [] <=> F`, REWRITE_TAC[MEM]) and
 223     MEM_NUM_HD = UNDISCH_ALL (prove(`(n = h <=> T) ==> (MEM (n:num) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
 224     MEM_NUM_TL = UNDISCH_ALL (prove(`(n = h <=> F) ==> (MEM (n:num) (CONS h t) <=> MEM n t)`, SIMP_TAC[MEM]));;
 225
 226
 227 let h_var_num = `h:num` and
 228     t_var_numlist = `t:(num)list`;;
 229
 230
 231 let rec MEM_NUM_CONV tm =
 232   let ltm, list_tm = dest_comb tm in
 233   let n_tm = rand ltm in
 234     if (is_comb list_tm) then
 235       let h_tm', t_tm = dest_comb list_tm in
 236       let h_tm = rand h_tm' in
 237       let eq_th = MY_NUM_EQ_CONV (mk_eq (n_tm, h_tm)) in
 238         if (rand(concl eq_th) = t_const) then
 239           let th0' = INST[n_tm, n_var_num; h_tm, h_var_num; t_tm, t_var_numlist] MEM_NUM_HD in
 240             MY_PROVE_HYP eq_th th0'
 241         else
 242           let th0' = INST[n_tm, n_var_num; h_tm, h_var_num; t_tm, t_var_numlist] MEM_NUM_TL in
 243           let th0 = MY_PROVE_HYP eq_th th0' in
 244           let th1 = MEM_NUM_CONV (rand(concl th0)) in
 245             TRANS th0 th1
 246     else
 247       INST[n_tm, n_var_num] MEM_NUM_EMPTY;;
 248
 249
 250
 251 (* MEM_NUM_PAIR_CONV *)
 252
 253 let MEM_NUM_PAIR_EMPTY = prove(`MEM (n:num#num) [] <=> F`, REWRITE_TAC[MEM]) and
 254     MEM_NUM_PAIR_HD = UNDISCH_ALL (prove(`(n = h <=> T) ==> (MEM (n:num#num) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
 255     MEM_NUM_PAIR_TL = UNDISCH_ALL (prove(`(n = h <=> F) ==> (MEM (n:num#num) (CONS h t) <=> MEM n t)`, SIMP_TAC[MEM]));;
 256
 257
 258 let n_var_numnum = `n:num#num` and
 259     h_var_numnum = `h:num#num` and
 260     t_var_numnumlist = `t:(num#num)list`;;
 261
 262
 263 let rec MEM_NUM_PAIR_CONV tm =
 264   let ltm, list_tm = dest_comb tm in
 265   let n_tm = rand ltm in
 266     if (is_comb list_tm) then
 267       let h_tm', t_tm = dest_comb list_tm in
 268       let h_tm = rand h_tm' in
 269       let eq_th = NUM_PAIR_EQ_CONV (mk_eq (n_tm, h_tm)) in
 270         if (rand(concl eq_th) = t_const) then
 271           let th0' = INST[n_tm, n_var_numnum; h_tm, h_var_numnum; t_tm, t_var_numnumlist] MEM_NUM_PAIR_HD in
 272             MY_PROVE_HYP eq_th th0'
 273         else
 274           let th0' = INST[n_tm, n_var_numnum; h_tm, h_var_numnum; t_tm, t_var_numnumlist] MEM_NUM_PAIR_TL in
 275           let th0 = MY_PROVE_HYP eq_th th0' in
 276           let th1 = MEM_NUM_PAIR_CONV (rand(concl th0)) in
 277             TRANS th0 th1
 278     else
 279       INST[n_tm, n_var_numnum] MEM_NUM_PAIR_EMPTY;;
 280
 281
 282 let MEM_REWRITE_CONV = REWRITE_CONV[MEM; PAIR_EQ; ARITH_EQ];;
 283
 284
 285 (*
 286 test 1000 MEM_NUM_PAIR_CONV `MEM (1,1) [1,2; 3,4; 2,1]`;; (* 0.140 *)
 287 test 1000 MEM_REWRITE_CONV `MEM (1,1) [1,2; 3,4; 2,1]`;; (* 1.276 *)
 288 *)
 289
 290
 291
 292 (* LIST_PAIRS_CONV *)
 293
 294 let LIST_PAIRS_REWRITE_CONV = REWRITE_CONV[list_pairs; shift_left; APPEND; ZIP];;
 295
 296
 297 let list_pairs2 = define `list_pairs2 [] (hd:A) = [] /\
 298                    list_pairs2 (CONS h []) hd = [h,hd] /\
 299                    list_pairs2 (CONS h1 (CONS h2 t)) hd = CONS (h1,h2) (list_pairs2 (CONS h2 t) hd)`;;
 300
 301
 302 let [list_pairs2_0; list_pairs2_1; list_pairs2_2] = map (INST_TYPE [`:num`, aty]) (CONJUNCTS list_pairs2);;
 303
 304 let rec list_pairs2_raw_conv tm =
 305   let ltm, h = dest_comb tm in
 306   let list = rand ltm in
 307     if (is_comb list) then
 308       let h_list, t_list = dest_comb list in
 309       let h_list = rand h_list in
 310         if (is_comb t_list) then
 311           let h2,t2 = dest_comb t_list in
 312           let h2 = rand h2 in
 313           let th0 = INST[h_list, h1_var_num; h2, h2_var_num; t2, t_var; h, hd_var_num] list_pairs2_2 in
 314           let ltm, rtm = dest_comb (rand(concl th0)) in
 315           let th1 = list_pairs2_raw_conv rtm in
 316             TRANS th0 (AP_TERM ltm th1)
 317         else
 318           INST[h_list, h_var_num; h, hd_var_num] list_pairs2_1
 319     else
 320       INST[h, hd_var_num] list_pairs2_0;;
 321
 322
 323 (*
 324 list_pairs2_raw_conv `list_pairs2 [1;2;3;4;5;6] 1`;;
 325 test 1000 (list_pairs2_raw_conv) `list_pairs2 [1;2;3;4;5;6] 1`;; (* 0.072 *)
 326 *)
 327
 328 let EL_EQ_IMP_EQ = prove(`!l1 l2:(A)list. LENGTH l1 = LENGTH l2 /\
 329     (!i. i < LENGTH l1 ==> EL i l1 = EL i l2) ==> l1 = l2`,
 330    LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; NOT_SUC] THEN
 331      REWRITE_TAC[SUC_INJ; injectivity "list"] THEN
 332      REPEAT STRIP_TAC THENL
 333      [
 334        FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
 335          REWRITE_TAC[LT_0; EL; HD];
 336        ALL_TAC
 337      ] THEN
 338      FIRST_X_ASSUM MATCH_MP_TAC THEN
 339      ASM_REWRITE_TAC[] THEN
 340      REPEAT STRIP_TAC THEN
 341      FIRST_X_ASSUM (MP_TAC o SPEC `SUC i`) THEN
 342      ASM_REWRITE_TAC[LT_SUC; EL; TL]);;
 343
 344
 345 let LENGTH_LIST_PAIRS2 = prove(`!(x:A) list. LENGTH (list_pairs2 list x) = LENGTH list`,
 346    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[list_pairs2; LENGTH] THEN
 347      DISJ_CASES_TAC (ISPEC `t:(A)list` list_CASES) THENL
 348      [
 349        ASM_REWRITE_TAC[list_pairs2; LENGTH];
 350        ALL_TAC
 351      ] THEN
 352      FIRST_X_ASSUM (MP_TAC o check (is_eq o concl)) THEN
 353      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 354      ASM_REWRITE_TAC[list_pairs2; LENGTH; SUC_INJ]);;
 355
 356
 357 let EL_LIST_PAIRS2 = prove(`!(x:A) list i. i < LENGTH list ==>
 358                              EL i (list_pairs2 list x) =
 359                                EL i list, if i = LENGTH list - 1 then x else EL (i + 1) list`,
 360    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; LT] THEN
 361      REPEAT STRIP_TAC THENL
 362      [
 363        ASM_REWRITE_TAC[] THEN
 364          DISJ_CASES_TAC (ISPEC `t:(A)list` list_CASES) THENL
 365          [
 366            ASM_REWRITE_TAC[LENGTH; list_pairs2; EL; HD; ARITH_RULE `SUC 0 - 1 = 0`];
 367            ALL_TAC
 368          ] THEN
 369          POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 370          ASM_REWRITE_TAC[LENGTH; list_pairs2; EL; TL; ARITH_RULE `SUC (SUC n) - 1 = SUC n`] THEN
 371          FIRST_X_ASSUM (MP_TAC o SPEC `LENGTH (t':(A)list)`) THEN
 372          ASM_REWRITE_TAC[LENGTH; ARITH_RULE `SUC n - 1 = n`; ARITH_RULE `n < SUC n`];
 373        ALL_TAC
 374      ] THEN
 375
 376      DISJ_CASES_TAC (ISPEC `t:(A)list` list_CASES) THENL
 377      [
 378        UNDISCH_TAC `i < LENGTH (t:(A)list)` THEN
 379          ASM_REWRITE_TAC[LENGTH; LT];
 380        ALL_TAC
 381      ] THEN
 382
 383      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 384      ASM_REWRITE_TAC[list_pairs2; ARITH_RULE `i + 1 = SUC i`; EL; TL] THEN
 385
 386      DISJ_CASES_TAC (SPEC `i:num` num_CASES) THENL
 387      [
 388        ASM_REWRITE_TAC[EL; HD; LENGTH; ARITH_RULE `~(0 = SUC(SUC n) - 1)`];
 389        ALL_TAC
 390      ] THEN
 391
 392      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
 393      ASM_REWRITE_TAC[EL; TL] THEN
 394      FIRST_X_ASSUM (MP_TAC o SPEC `n:num`) THEN
 395      ASM_REWRITE_TAC[LENGTH; ARITH_RULE `n + 1 = SUC n`; EL; TL] THEN
 396      REWRITE_TAC[ARITH_RULE `SUC n = SUC (SUC k) - 1 <=> n = SUC k - 1`] THEN
 397      DISCH_THEN MATCH_MP_TAC THEN
 398      UNDISCH_TAC `i < LENGTH (t:(A)list)` THEN
 399      ASM_REWRITE_TAC[LENGTH; LT_SUC] THEN
 400      ARITH_TAC);;
 401
 402
 403 let LIST_PAIRS2 = prove(`!list:(A)list. list_pairs list = list_pairs2 list (HD list)`,
 404    GEN_TAC THEN MATCH_MP_TAC EL_EQ_IMP_EQ THEN
 405      REWRITE_TAC[LENGTH_LIST_PAIRS; LENGTH_LIST_PAIRS2] THEN
 406      ASM_SIMP_TAC[EL_LIST_PAIRS; EL_LIST_PAIRS2] THEN
 407      REPEAT STRIP_TAC THEN
 408      COND_CASES_TAC THEN ASM_REWRITE_TAC[EL]);;
 409
 410
 411 let LIST_PAIRS_NUM_EMPTY = prove(`list_pairs ([]:(num)list) = []`, CONV_TAC LIST_PAIRS_REWRITE_CONV);;
 412 let LIST_PAIRS_NUM_CONS = prove(`list_pairs (CONS (h:num) t) = list_pairs2 (CONS h t) h`, REWRITE_TAC[LIST_PAIRS2; HD]);;
 413
 414
 415 let LIST_PAIRS_CONV tm =
 416   let list_tm = rand tm in
 417     if (is_comb list_tm) then
 418       let h_tm', t_tm = dest_comb list_tm in
 419       let h_tm = rand h_tm' in
 420       let th0 = INST[h_tm, h_var_num; t_tm, t_var_numlist] LIST_PAIRS_NUM_CONS in
 421       let th1 = list_pairs2_raw_conv (rand(concl th0)) in
 422         TRANS th0 th1
 423     else
 424       LIST_PAIRS_NUM_EMPTY;;
 425
 426
 427
 428 (*
 429 let z = `list_pairs [1;2;3;4;5;6]`;;
 430 LIST_PAIRS_REWRITE_CONV z;;
 431 test 1000 LIST_PAIRS_REWRITE_CONV z;; (* 2.484 *)
 432
 433 LIST_PAIRS_CONV z;;
 434 test 1000 LIST_PAIRS_CONV z;; (* 0.08 *)
 435 *)
 436
 437
 438 (***********************************************)
 439
 440 (* LIST_OF_FACES_CONV *)
 441
 442 let LIST_OF_FACES_REWRITE_CONV = REWRITE_CONV[list_of_faces; MAP; LIST_PAIRS2; list_pairs2; HD];;
 443
 444 let LIST_OF_FACES_REWRITE_CONV' = REWRITE_CONV[list_of_faces; MAP; list_pairs; shift_left; APPEND; ZIP];;
 445
 446 (*
 447 let y = mk_comb(list_of_faces_const, hol_list);;
 448 LIST_OF_FACES_CONV y;;
 449 test 10 LIST_OF_FACES_CONV y;; (* 0.304 *)
 450
 451 LIST_OF_FACES_CONV2 y;;
 452 test 10 LIST_OF_FACES_CONV2 y;; (* 0.172 *)
 453 *)
 454
 455 (*
 456 LIST_OF_DARTS_CONV' y;;
 457 test 10 LIST_OF_DARTS_CONV' y;; (* 0.920 *)
 458 *)
 459
 460
 461 (* LIST_OF_DARTS_CONV *)
 462 let LIST_OF_DARTS_REWRITE_CONV = REWRITE_CONV[list_of_darts; ITLIST; list_pairs; shift_left; APPEND; ZIP];;
 463
 464
 465 (*
 466 let x = create_hol_list pentstring;;
 467 let y = mk_comb (list_of_darts_const, hol_list);;
 468 test 10 LIST_OF_DARTS_CONV y;; (* 1.168 *)
 469 *)
 470
 471
 472 (**************************************)
 473
 474
 475 (* ALL_DISTINCT_CONV *)
 476 let ALL_DISTINCT_REWRITE_CONV = REWRITE_CONV[ALL_DISTINCT_ALT; MEM; PAIR_EQ; ARITH];;
 477
 478
 479 let ALL_DISTINCT_NUM_PAIR_EMPTY = prove(`ALL_DISTINCT ([]:(num#num)list) <=> T`, REWRITE_TAC[ALL_DISTINCT_ALT]) and
 480     ALL_DISTINCT_NUM_PAIR_CONS_F = UNDISCH_ALL (prove(`(MEM (h:num#num) t <=> F) ==> (ALL_DISTINCT (CONS h t) <=> ALL_DISTINCT t)`, SIMP_TAC[ALL_DISTINCT_ALT])) and
 481     ALL_DISTINCT_NUM_PAIR_CONS_T = UNDISCH_ALL (prove(`(MEM (h:num#num) t <=> T) ==> (ALL_DISTINCT (CONS h t) <=> F)`, SIMP_TAC[ALL_DISTINCT_ALT]));;
 482
 483 let mem_numnum_const = `MEM:(num#num)->(num#num)list->bool`;;
 484
 485 let rec ALL_DISTINCT_NUM_PAIR_CONV tm =
 486   let list_tm = rand tm in
 487     if (is_comb list_tm) then
 488       let h_tm', t_tm = dest_comb list_tm in
 489       let h_tm = rand h_tm' in
 490       let inst = INST[h_tm, h_var_numnum; t_tm, t_var_numnumlist] in
 491       let mem_th = MEM_NUM_PAIR_CONV (mk_binop mem_numnum_const h_tm t_tm) in
 492         if (rand (concl mem_th) = t_const) then
 493           MY_PROVE_HYP mem_th (inst ALL_DISTINCT_NUM_PAIR_CONS_T)
 494         else
 495           let th0 = MY_PROVE_HYP mem_th (inst ALL_DISTINCT_NUM_PAIR_CONS_F) in
 496           let th1 = ALL_DISTINCT_NUM_PAIR_CONV (rand(concl th0)) in
 497             TRANS th0 th1
 498     else
 499       ALL_DISTINCT_NUM_PAIR_EMPTY;;
 500
 501
 502 (*
 503 let z = mk_comb(`ALL_DISTINCT:(num#num)list->bool`, rand(concl (LIST_OF_DARTS_CONV y)));;
 504 ALL_DISTINCT_REWRITE_CONV z;;
 505 ALL_DISTINCT_NUM_PAIR_CONV z;;
 506 test 1 ALL_DISTINCT_REWRITE_CONV z;; (* 0.808 *)
 507 test 1 ALL_DISTINCT_NUM_PAIR_CONV z;; (* 0.084 *)
 508 *)
 509
 510 (*********************************************)
 511
 512 (* GOOD_LIST_CONV *)
 513
 514 let GOOD_LIST_COND3_EMPTY = prove(`ALL (\d:num#num. MEM (SND d,FST d) list) [] <=> T`, REWRITE_TAC[ALL]);;
 515 let GOOD_LIST_COND3_CONS_T = UNDISCH_ALL (prove(`(MEM (y,x) list <=> T) ==>
 516                                                   (ALL (\d:num#num. MEM (SND d,FST d) list) (CONS (x,y) t) <=>
 517                                                      ALL (\d:num#num. MEM (SND d,FST d) list) t)`, SIMP_TAC[ALL]));;
 518 let GOOD_LIST_COND3_CONS_F = UNDISCH_ALL (prove(`(MEM (y,x) list <=> F) ==>
 519                                                   (ALL (\d:num#num. MEM (SND d,FST d) list) (CONS (x,y) t) <=>
 520                                                      F)`, SIMP_TAC[ALL]));;
 521
 522 let list_var_numnumlist = `list:(num#num)list`;;
 523
 524 let rec GOOD_LIST_COND3_CONV tm =
 525   let ltm, list_tm = dest_comb tm in
 526   let f_tm = rand ltm in
 527   let list2_tm = rand(snd(dest_abs f_tm)) in
 528     if (is_comb list_tm) then
 529       let h_tm, t_tm = dest_comb list_tm in
 530       let x_tm, y_tm = dest_pair (rand h_tm) in
 531       let inst = INST[list2_tm, list_var_numnumlist; x_tm, x_var_num; y_tm, y_var_num; t_tm, t_var_numnumlist] in
 532       let mem_th = MEM_NUM_PAIR_CONV (mk_binop mem_numnum_const (mk_pair (y_tm,x_tm)) list2_tm) in
 533         if (rand(concl mem_th) = t_const) then
 534           let th0 = MY_PROVE_HYP mem_th (inst GOOD_LIST_COND3_CONS_T) in
 535           let th1 = GOOD_LIST_COND3_CONV (rand(concl th0)) in
 536             TRANS th0 th1
 537         else
 538           MY_PROVE_HYP mem_th (inst GOOD_LIST_COND3_CONS_F)
 539     else
 540       INST[list2_tm, list_var_numnumlist] GOOD_LIST_COND3_EMPTY;;
 541
 542
 543 (*
 544 good_list;;
 545 let z = mk_comb(`\ll. !d:num#num. MEM d (list_of_darts ll) ==> MEM (SND d,FST d) (list_of_darts ll)`, x);;
 546 let s1 = rand(concl(REWRITE_CONV[darts; ALL_MEM] z));;
 547 let s2 = REWRITE_CONV[ALL; MEM] s1;;
 548 test 1 (REWRITE_CONV[ALL;MEM]) s1;; (* 1.668 *)
 549
 550
 551 GOOD_LIST_COND3_CONV s1;;
 552 test 1 GOOD_LIST_COND3_CONV s1;; (* 0.108 *)
 553 *)
 554
 555
 556
 557
 558 (*****************************************)
 559
 560 (* FLATTEN_CONV *)
 561
 562 let FLATTEN_CLAUSES = prove(`!(h:A) t tt.
 563                                FLATTEN ([]:((A)list)list) = [] /\
 564                                FLATTEN (CONS [] tt) = FLATTEN tt /\
 565                                FLATTEN (CONS (CONS h t) tt) = CONS h (FLATTEN (CONS t tt))`,
 566    REPEAT STRIP_TAC THEN REWRITE_TAC[FLATTEN; ITLIST; APPEND]);;
 567
 568
 569 let FLATTEN_REWRITE_CONV = REWRITE_CONV[FLATTEN_CLAUSES];;
 570
 571
 572 let FLATTEN_NUM_CLAUSES = INST_TYPE[`:num`, aty] (SPEC_ALL FLATTEN_CLAUSES);;
 573
 574 let [flatten_0; flatten_01; flatten_11] =
 575   CONJUNCTS (FLATTEN_NUM_CLAUSES);;
 576 let tt_var_numlistlist = `tt:((num)list)list`;;
 577 let h_var_num = `h:num`;;
 578 let t_var_numlist = `t:(num)list`;;
 579
 580
 581
 582 let rec FLATTEN_NUM_CONV tm =
 583   let arg = rand tm in
 584     if (is_comb arg) then
 585       let hh_tm', tt_tm = dest_comb arg in
 586       let hh_tm = rand hh_tm' in
 587         if (is_comb hh_tm) then
 588           let h_tm', t_tm = dest_comb hh_tm in
 589           let h_tm = rand h_tm' in
 590           let th0 = INST[h_tm, h_var_num; t_tm, t_var_numlist; tt_tm, tt_var_numlistlist] flatten_11 in
 591           let ltm, rtm = dest_comb(rand(concl th0)) in
 592           let th1 = AP_TERM ltm (FLATTEN_NUM_CONV rtm) in
 593             TRANS th0 th1
 594         else
 595           let th0 = INST[tt_tm, tt_var_numlistlist] flatten_01 in
 596           let th1 = FLATTEN_NUM_CONV (rand(concl th0)) in
 597             TRANS th0 th1
 598     else
 599       flatten_0;;
 600
 601
 602 let [flattenA_0; flattenA_01; flattenA_11]
 603     = CONJUNCTS (SPEC_ALL FLATTEN_CLAUSES);;
 604
 605
 606 (* Works for any list of lists *)
 607 let FLATTEN_CONV tm =
 608   let tm_ty = hd (snd (dest_type (type_of tm))) in
 609   let f0_th = INST_TYPE[tm_ty, aty] flattenA_0 in
 610   let f01_th = INST_TYPE[tm_ty, aty] flattenA_01 in
 611   let f11_th = INST_TYPE[tm_ty, aty] flattenA_11 in
 612   let t_var = mk_var("t", mk_type("list", [tm_ty])) in
 613   let tt_var = mk_var("tt", mk_type("list", [type_of t_var])) in
 614   let h_var = mk_var("h", tm_ty) in
 615
 616   let rec f_conv tm =
 617       let arg = rand tm in
 618         if (is_comb arg) then
 619           let hh_tm', tt_tm = dest_comb arg in
 620           let hh_tm = rand hh_tm' in
 621             if (is_comb hh_tm) then
 622               let h_tm', t_tm = dest_comb hh_tm in
 623               let h_tm = rand h_tm' in
 624               let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] f11_th in
 625               let ltm, rtm = dest_comb(rand(concl th0)) in
 626               let th1 = AP_TERM ltm (f_conv rtm) in
 627                 TRANS th0 th1
 628             else
 629               let th0 = INST[tt_tm, tt_var] f01_th in
 630               let th1 = f_conv (rand(concl th0)) in
 631                 TRANS th0 th1
 632         else
 633           f0_th in
 634
 635     f_conv tm;;
 636
 637
 638 (*
 639 let tm = `FLATTEN [[1;2;3]; [4;3;2;1]]`;;
 640 flatten_conv tm;;
 641 test 1000 flatten_conv tm;; (* 0.080 *)
 642
 643 flatten_conv2 tm;;
 644 test 1000 flatten_conv2 tm;; (* 0.112 *)
 645
 646 FLATTEN_REWRITE_CONV tm;;
 647 test 1000 FLATTEN_REWRITE_CONV2 tm;; (* 1.11 *)
 648
 649 let y = mk_comb(`FLATTEN:((num)list)list->(num)list`, x);;
 650 FLATTEN_CONV y;;
 651 test 100 FLATTEN_CONV y;; (* 0.084 *)
 652 test 100 FLATTEN_REWRITE_CONV y;; (* 4.524 *)
 653 *)
 654
 655
 656 (**********************************)
 657
 658 (* REMOVE_DUPLICATES_CONV *)
 659 let remove_duplicates2 = define `remove_duplicates2 [] acc = acc /\
 660     remove_duplicates2 (CONS (h:A) t) acc = if (MEM h acc) then remove_duplicates2 t acc
 661                                            else remove_duplicates2 t (CONS h acc)`;;
 662
 663 let REMOVE_DUPLICATES_REWRITE_CONV = REWRITE_CONV[REMOVE_DUPLICATES; MEM; ARITH_EQ];;
 664
 665
 666 let REMOVE_DUPLICATES_NUM_EMPTY = prove(`REMOVE_DUPLICATES ([]:(num)list) = []`, REWRITE_TAC[REMOVE_DUPLICATES]);;
 667 let REMOVE_DUPLICATES_MEM_NUM_T = UNDISCH_ALL(prove(`(MEM (h:num) t <=> T) ==>
 668                                       REMOVE_DUPLICATES (CONS h t) = REMOVE_DUPLICATES t`, SIMP_TAC[REMOVE_DUPLICATES]));;
 669 let REMOVE_DUPLICATES_MEM_NUM_F = UNDISCH_ALL(prove(`(MEM (h:num) t <=> F) ==>
 670                                       REMOVE_DUPLICATES (CONS h t) = CONS h (REMOVE_DUPLICATES t)`, SIMP_TAC[REMOVE_DUPLICATES]));;
 671
 672 let mem_num_const = `MEM:num->(num)list->bool`;;
 673
 674
 675 let rec REMOVE_DUPLICATES_NUM_CONV tm =
 676   let list_tm = rand tm in
 677     if (is_comb list_tm) then
 678       let h_tm', t_tm = dest_comb list_tm in
 679       let h_tm = rand h_tm' in
 680       let inst = INST[h_tm, h_var_num; t_tm, t_var_numlist] in
 681       let mem_th = MEM_NUM_CONV (mk_binop mem_num_const h_tm t_tm) in
 682         if (rand(concl mem_th) = t_const) then
 683           let th0 = MY_PROVE_HYP mem_th (inst REMOVE_DUPLICATES_MEM_NUM_T) in
 684           let th1 = REMOVE_DUPLICATES_NUM_CONV (rand(concl th0)) in
 685             TRANS th0 th1
 686         else
 687           let th0 = MY_PROVE_HYP mem_th (inst REMOVE_DUPLICATES_MEM_NUM_F) in
 688           let ltm, rtm = dest_comb (rand(concl th0)) in
 689           let th1 = REMOVE_DUPLICATES_NUM_CONV rtm in
 690             TRANS th0 (AP_TERM ltm th1)
 691     else
 692       REMOVE_DUPLICATES_NUM_EMPTY;;
 693
 694
 695 (*
 696 let tm = `REMOVE_DUPLICATES [1;2;3;4;2;1;3]`;;
 697
 698 REMOVE_DUPLICATES_REWRITE_CONV tm;;
 699 test 10 REMOVE_DUPLICATES_CONV tm;; (* 0.776 *)
 700
 701 REMOVE_DUPLICATES_NUM_CONV tm;;
 702 test 1000 REMOVE_DUPLICATES_NUM_CONV tm;; (* 0.548 *)
 703 *)
 704
 705
 706 (*
 707 let y = mk_comb(list_of_elements_const, hol_list);;
 708
 709
 710 let xxx =(REWRITE_CONV[list_of_elements] THENC
 711    REWRITE_CONV[FLATTEN; ITLIST; APPEND])
 712 y;;
 713
 714 let zz = `remove_duplicates2 [1;2;3;4;2;1] []`;;
 715 REWRITE_CONV[remove_duplicates2; MEM; ARITH] zz;;
 716
 717 let zz = rand(concl xxx);;
 718
 719 REMOVE_DUPLICATES_REWRITE_CONV zz;; (* infty *)
 720 REMOVE_DUPLICATES_NUM_CONV zz;;
 721 test 10 REMOVE_DUPLICATES_NUM_CONV zz;; (* 0.176 *)
 722
 723 *)
 724
 725
 726
 727 (**************************************)
 728
 729 (* LIST_OF_ELEMENTS_CONV *)
 730
 731 let LIST_OF_ELEMENTS_CONV =
 732   ONCE_REWRITE_CONV[list_of_elements] THENC
 733     ONCE_DEPTH_CONV FLATTEN_CONV THENC
 734     REMOVE_DUPLICATES_NUM_CONV;;
 735
 736 (*
 737 let y = mk_comb(list_of_elements_const, hol_list);;
 738 test 10 LIST_OF_ELEMENTS_CONV y;; (* 0.184 *)
 739 *)
 740
 741
 742 (**********************************)
 743
 744 (* LIST_OF_NODES_CONV *)
 745
 746
 747 let FILTER_NODE_EMPTY = prove(`FILTER (\d:num#num. FST d = x) [] = []`, REWRITE_TAC[FILTER]);;
 748 let FILTER_NODE_CONS_EQ = UNDISCH_ALL (prove(`(n = x <=> T) ==> FILTER (\d:num#num. FST d = x) (CONS (n,m) t) =
 749                                                  CONS (n,m) (FILTER (\d. FST d = x) t)`, SIMP_TAC[FILTER]));;
 750 let FILTER_NODE_CONS_NEQ = UNDISCH_ALL (prove(`(n = x <=> F) ==> FILTER (\d:num#num. FST d = x) (CONS (n,m) t) =
 751                                                   FILTER (\d. FST d = x) t`, SIMP_TAC[FILTER]));;
 752
 753
 754
 755 let rec FILTER_NODE_CONV tm =
 756   let ltm, list_tm = dest_comb tm in
 757   let x_tm = (rand o snd o dest_abs o rand) ltm in
 758     if (is_comb list_tm) then
 759       let h_tm, t_tm = dest_comb list_tm in
 760       let n_tm, m_tm = dest_pair (rand h_tm) in
 761       let inst = INST[n_tm, n_var_num; m_tm, m_var_num; t_tm, t_var_numnumlist; x_tm, x_var_num] in
 762       let eq_th = MY_NUM_EQ_CONV (mk_eq (n_tm, x_tm)) in
 763         if (rand(concl eq_th) = t_const) then
 764           let th0 = MY_PROVE_HYP eq_th (inst FILTER_NODE_CONS_EQ) in
 765           let ltm, rtm = dest_comb (rand(concl th0)) in
 766           let th1 = FILTER_NODE_CONV rtm in
 767             TRANS th0 (AP_TERM ltm th1)
 768         else
 769           let th0 = MY_PROVE_HYP eq_th (inst FILTER_NODE_CONS_NEQ) in
 770           let th1 = FILTER_NODE_CONV (rand(concl th0)) in
 771             TRANS th0 th1
 772     else
 773       INST[x_tm, x_var_num] FILTER_NODE_EMPTY;;
 774
 775
 776
 777 (*
 778 test 10 LIST_OF_NODES_CONV y;; (* 0.992 *)
 779 *)
 780
 781
 782
 783 (****************************************************)
 784
 785 (* `node (hypermap_of_list L) x` table construction *)
 786
 787
 788 let NODE_HYPERMAP_OF_LIST_EXPLICIT = prove(`!(L:((A)list)list) n d. good_list_nodes L /\
 789                                              MEM n (list_of_nodes L) /\ MEM d n
 790                                            ==> node (hypermap_of_list L) d = set_of_list n`,
 791    REWRITE_TAC[good_list_nodes] THEN REPEAT STRIP_TAC THEN
 792      SUBGOAL_THEN `set_of_list n IN node_set (hypermap_of_list (L:((A)list)list))` ASSUME_TAC THENL
 793      [
 794        ASM_REWRITE_TAC[IN_SET_OF_LIST; nodes_of_list; MEM_MAP] THEN
 795          EXISTS_TAC `n:(A#A)list` THEN
 796          ASM_REWRITE_TAC[];
 797        ALL_TAC
 798      ] THEN
 799      MP_TAC (ISPECL [`hypermap_of_list L:(A#A)hypermap`; `set_of_list n:A#A->bool`] Hypermap.lemma_node_representation) THEN
 800      ASM_REWRITE_TAC[] THEN
 801      STRIP_TAC THEN
 802      ASM_REWRITE_TAC[] THEN
 803      MATCH_MP_TAC (GSYM Hypermap.lemma_node_identity) THEN
 804      POP_ASSUM (fun th -> REWRITE_TAC[SYM th]) THEN
 805      ASM_REWRITE_TAC[IN_SET_OF_LIST]);;
 806
 807
 808 let NODES_HYPERMAP_OF_LIST_ALL = prove(`!(L:((A)list)list). good_list_nodes L ==>
 809                 ALL (\n. ALL(\d. node (hypermap_of_list L) d = set_of_list n) n) (list_of_nodes L)`,
 810    REWRITE_TAC[GSYM ALL_MEM] THEN
 811      REPEAT STRIP_TAC THEN
 812      MATCH_MP_TAC NODE_HYPERMAP_OF_LIST_EXPLICIT THEN
 813      ASM_REWRITE_TAC[]);;
 814
 815
 816
 817
 818 let build_table_of_nodes hyp_list nodes_th =
 819   let table_of_nodes = Hashtbl.create 100 in
 820   let th0 = (UNDISCH_ALL o ISPEC hyp_list) NODES_HYPERMAP_OF_LIST_ALL in
 821   let all_tm = rator (concl th0) in
 822   let th1 = EQ_MP (AP_TERM all_tm nodes_th) th0 in
 823   let th1_list = get_all th1 in
 824
 825   let build1 = fun th ->
 826     let th = BETA_RULE th in
 827     let list_tm = dest_list(rand(concl th)) in
 828     let ths = get_all th in
 829     let r = CONV_RULE (BETA_CONV THENC RAND_CONV set_of_list_conv) in
 830       map (fun tm, th -> Hashtbl.add table_of_nodes tm (r th)) (zip list_tm ths) in
 831
 832   let _ = map build1 th1_list in
 833     table_of_nodes;;
 834
 835
 836
 837
 838 (*
 839 let hol_list, th_table = compute_all pentstring;;
 840 let nodes = Hashtbl.find th_table "nodes";;
 841
 842
 843 let MEM_h_CONS_h_t = prove(`!(h:A) t. MEM h (CONS h t)`, REWRITE_TAC[MEM]);;
 844
 845
 846
 847 let th = ISPEC hol_list NODES_HYPERMAP_OF_LIST_ALL;;
 848 let nodes_th = UNDISCH_ALL (REWRITE_RULE[nodes; ALL; set_of_list] th);;
 849 CONJUNCTS nodes_th;;
 850 *)
 851
 852
 853 (****************************************************)
 854
 855 (* `face (hypermap_of_list L) x` table construction *)
 856
 857
 858 let FACE_HYPERMAP_OF_LIST_EXPLICIT = prove(`!(L:((A)list)list) f d. good_list L /\
 859                                              MEM f (list_of_faces L) /\ MEM d f
 860                                            ==> face (hypermap_of_list L) d = set_of_list f`,
 861    REPEAT STRIP_TAC THEN
 862      MP_TAC (SPECL [`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
 863      ASM_REWRITE_TAC[] THEN
 864      DISCH_THEN (X_CHOOSE_THEN `x:A#A` STRIP_ASSUME_TAC) THEN
 865
 866      SUBGOAL_THEN `MEM (d:A#A) (list_of_darts L)` ASSUME_TAC THENL
 867      [
 868        MATCH_MP_TAC MEM_FIND_FACE_IMP_MEM_DARTS THEN
 869          EXISTS_TAC `x:A#A` THEN
 870          POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]);
 871        ALL_TAC
 872      ] THEN
 873
 874      ASM_SIMP_TAC[FACE_OF_LIST] THEN
 875      AP_TERM_TAC THEN
 876      MATCH_MP_TAC MEM_FIND_FACE_IMP_FACES_EQ THEN
 877      CONJ_TAC THENL
 878      [
 879        UNDISCH_TAC `good_list (L:((A)list)list)` THEN
 880          SIMP_TAC[good_list];
 881        ALL_TAC
 882      ] THEN
 883
 884      REMOVE_ASSUM THEN
 885      POP_ASSUM (fun th -> ASM_REWRITE_TAC[SYM th]));;
 886
 887
 888
 889 let FACES_HYPERMAP_OF_LIST_ALL = prove(`!(L:((A)list)list). good_list L ==>
 890                 ALL (\f. ALL(\d. face (hypermap_of_list L) d = set_of_list f) f) (list_of_faces L)`,
 891    REWRITE_TAC[GSYM ALL_MEM] THEN
 892      REPEAT STRIP_TAC THEN
 893      MATCH_MP_TAC FACE_HYPERMAP_OF_LIST_EXPLICIT THEN
 894      ASM_REWRITE_TAC[]);;
 895
 896
 897 let build_table_of_faces hyp_list good_list_th faces_th =
 898   let table_of_faces = Hashtbl.create 100 in
 899   let th0 = MY_PROVE_HYP good_list_th ((UNDISCH_ALL o ISPEC hyp_list) FACES_HYPERMAP_OF_LIST_ALL) in
 900   let all_tm = rator (concl th0) in
 901   let th1 = EQ_MP (AP_TERM all_tm faces_th) th0 in
 902   let th1_list = get_all th1 in
 903
 904   let build1 = fun th ->
 905     let th = BETA_RULE th in
 906     let list_tm = dest_list(rand(concl th)) in
 907     let ths = get_all th in
 908     let r = CONV_RULE (BETA_CONV THENC RAND_CONV set_of_list_conv) in
 909       map (fun tm, th -> Hashtbl.add table_of_faces tm (r th)) (zip list_tm ths) in
 910
 911   let _ = map build1 th1_list in
 912     table_of_faces;;
 913
 914
 915
 916
 917
 918
 919
 920
 921 (********************************************)
 922
 923 (* face_map H and inverse (face_map H) tables *)
 924
 925 let f_list_ext_table = define `(f_list_ext_table L [] (first:A#A) <=> T)
 926   /\ (f_list_ext_table L (CONS h1 (CONS h2 t)) first
 927                                   <=> f_list_ext L h1 = h2 /\
 928                                       inverse (f_list_ext L) h2 = h1 /\
 929                                       f_list_ext_table L (CONS h2 t) first)
 930   /\ (f_list_ext_table L [h1] first <=> f_list_ext L h1 = first /\
 931                                      inverse (f_list_ext L) first = h1)`;;
 932
 933
 934 let list_to_pair list = hd list, hd(tl list);;
 935
 936
 937 let F_LIST_EXT_SINGLE, INV_F_LIST_EXT_SINGLE = (list_to_pair o CONJUNCTS o UNDISCH_ALL)
 938   (prove(`f_list_ext_table L [h1:num#num] first
 939          ==> f_list_ext L h1 = first /\
 940              inverse (f_list_ext L) first = h1`, SIMP_TAC[f_list_ext_table])) and
 941 F_LIST_EXT_CONS, INV_F_LIST_EXT_CONS = (list_to_pair o CONJUNCTS o UNDISCH_ALL)
 942   (prove(`f_list_ext_table L (CONS (h1:num#num) (CONS h2 t)) first
 943          ==> f_list_ext L h1 = h2 /\
 944              inverse (f_list_ext L) h2 = h1`, SIMP_TAC[f_list_ext_table])) and
 945 F_LIST_EXT_TABLE_CONS = UNDISCH_ALL (prove(`f_list_ext_table L (CONS (h1:num#num) t) first
 946                                                ==> f_list_ext_table L t first`,
 947    DISJ_CASES_TAC (ISPEC `t:(num#num)list` list_CASES) THENL
 948      [
 949        ASM_REWRITE_TAC[f_list_ext_table];
 950        POP_ASSUM STRIP_ASSUME_TAC THEN
 951          ASM_SIMP_TAC[f_list_ext_table]
 952      ]));;
 953
 954
 955 let h1_var = `h1:num#num` and
 956     h2_var = `h2:num#num` and
 957     t_var = `t:(num#num)list` and
 958     first_var = `first:num#num` and
 959     l_var = `L:((num)list)list`;;
 960
 961
 962 let f_list_ext_table_all th =
 963   let ltm, first_tm = dest_comb(concl th) in
 964   let ltm, list_tm = dest_comb ltm in
 965   let l_tm = rand ltm in
 966   let inst_t = INST[l_tm, l_var; first_tm, first_var] in
 967   let f_single, inv_f_single = inst_t F_LIST_EXT_SINGLE, inst_t INV_F_LIST_EXT_SINGLE in
 968   let f_cons, inv_f_cons = inst_t F_LIST_EXT_CONS, inst_t INV_F_LIST_EXT_CONS in
 969   let f_table = inst_t F_LIST_EXT_TABLE_CONS in
 970
 971   let rec f_list_raw = fun f_table_th h1_tm t1_tm ->
 972     if (is_comb t1_tm) then
 973       let h2_tm', t2_tm = dest_comb t1_tm in
 974       let h2_tm = rand h2_tm' in
 975       let inst_t = MY_PROVE_HYP f_table_th o INST[h1_tm, h1_var; h2_tm, h2_var; t2_tm, t_var] in
 976
 977       let f_th, inv_f_th = inst_t f_cons, inst_t inv_f_cons in
 978       let th0 = (MY_PROVE_HYP f_table_th o INST[h1_tm, h1_var; t1_tm, t_var]) f_table in
 979       let f_list, inv_f_list = f_list_raw th0 h2_tm t2_tm in
 980         (h1_tm, f_th) :: f_list, (h2_tm, inv_f_th) :: inv_f_list
 981
 982     else
 983       let inst_t = MY_PROVE_HYP f_table_th o INST[h1_tm, h1_var] in
 984       let f_th, inv_f_th = inst_t f_single, inst_t inv_f_single in
 985         [h1_tm, f_th], [first_tm, inv_f_th] in
 986
 987     if (is_comb list_tm) then
 988       let h1_tm, t1_tm = dest_comb list_tm in
 989         f_list_raw th (rand h1_tm) t1_tm
 990     else
 991       [], [];;
 992
 993
 994
 995
 996 (**********************)
 997
 998
 999 let FIND_FACE_LEMMA_EXPLICIT = prove(`!(L:((A)list)list) f d. good_list L /\
1000                                        MEM f (list_of_faces L) /\ MEM d f
1001                                      ==> find_face d L = f`,
1002    REPEAT STRIP_TAC THEN
1003      MP_TAC (SPECL[`f:(A#A)list`; `L:((A)list)list`] MEM_FACE_LEMMA) THEN
1004      ASM_REWRITE_TAC[] THEN
1005      STRIP_TAC THEN
1006      UNDISCH_TAC `MEM (d:A#A) f` THEN
1007      ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1008      MATCH_MP_TAC MEM_FIND_FACE_IMP_FACES_EQ THEN
1009      UNDISCH_TAC `good_list (L:((A)list)list)` THEN
1010      ASM_SIMP_TAC[good_list]);;
1011
1012
1013
1014 let INVERSE_F_LIST_EXT_LEMMA = prove(`!(L:((A)list)list) d. good_list L ==>
1015         inverse (f_list_ext L) (f_list_ext L d) = d`,
1016    REPEAT STRIP_TAC THEN
1017      ABBREV_TAC `H = hypermap_of_list L:(A#A)hypermap` THEN
1018      MP_TAC (ISPECL [`face_map (H:(A#A)hypermap)`; `dart H:A#A->bool`] PERMUTES_INVERSES) THEN
1019      ASM_SIMP_TAC[Hypermap.hypermap_lemma] THEN
1020      EXPAND_TAC "H" THEN
1021      ASM_SIMP_TAC[COMPONENTS_HYPERMAP_OF_LIST]);;
1022
1023
1024
1025 let NEXT_EL_APPEND_lemma = prove(`!l t1 (h:A) h' t2. ALL_DISTINCT l /\
1026                                    l = CONS h (APPEND t1 (CONS h' t2)) ==>
1027                                    NEXT_EL h' l = if (t2 = []) then h else HD t2`,
1028    REPEAT STRIP_TAC THEN
1029      REWRITE_TAC[NEXT_EL] THEN
1030      ABBREV_TAC `n1 = LENGTH (t1:(A)list)` THEN
1031      SUBGOAL_THEN `INDEX (h':A) l = SUC n1` ASSUME_TAC THENL
1032      [
1033        SUBGOAL_THEN `h':A = EL (SUC n1) l` (fun th -> REWRITE_TAC[th]) THENL
1034          [
1035            ASM_REWRITE_TAC[EL; TL; EL_APPEND; LT_REFL; SUB_REFL; HD];
1036            ALL_TAC
1037          ] THEN
1038          MATCH_MP_TAC INDEX_EL THEN
1039          ASM_REWRITE_TAC[LENGTH; LENGTH_APPEND] THEN
1040          ARITH_TAC;
1041        ALL_TAC
1042      ] THEN
1043      DISJ_CASES_TAC (ISPEC `t2:(A)list` list_CASES) THENL
1044      [
1045        ASM_REWRITE_TAC[LENGTH; LENGTH_APPEND; HD] THEN
1046          ARITH_TAC;
1047        ALL_TAC
1048      ] THEN
1049      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1050      ASM_REWRITE_TAC[LENGTH; LENGTH_APPEND; NOT_CONS_NIL; HD] THEN
1051      REWRITE_TAC[ARITH_RULE `~(SUC n1 = SUC (n1 + SUC (SUC n)) - 1)`] THEN
1052      REWRITE_TAC[ARITH_RULE `SUC n1 + 1 = SUC (n1 + 1)`; EL; TL] THEN
1053      ASM_REWRITE_TAC[EL_APPEND; ARITH_RULE `~(n1 + 1 < n1)`; ARITH_RULE `(n1 + 1) - n1 = 1`] THEN
1054      REWRITE_TAC[ARITH_RULE `1 = SUC 0`; EL; TL; HD]);;
1055
1056
1057
1058
1059 let F_LIST_EXT_TABLE = prove(`!L:((A)list)list. good_list L
1060                              ==> ALL (\f. f_list_ext_table L f (HD f)) (list_of_faces L)`,
1061    REPEAT STRIP_TAC THEN
1062      FIRST_ASSUM MP_TAC THEN REWRITE_TAC[good_list] THEN STRIP_TAC THEN
1063      REWRITE_TAC[GSYM ALL_MEM] THEN
1064      X_GEN_TAC `f:(A#A)list` THEN DISCH_TAC THEN
1065
1066      DISJ_CASES_TAC (ISPEC `f:(A#A)list` list_CASES) THENL
1067      [
1068        ASM_REWRITE_TAC[f_list_ext_table];
1069        ALL_TAC
1070      ] THEN
1071
1072      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1073      ASM_REWRITE_TAC[HD] THEN
1074      SUBGOAL_THEN `(!t2 t1. t = APPEND t1 t2 ==> f_list_ext_table L t2 (h:A#A)) ==> f_list_ext_table L (CONS h t) h` MP_TAC THENL
1075      [
1076        DISCH_THEN (MP_TAC o SPECL [`t:(A#A)list`; `[]:(A#A)list`]) THEN
1077          REWRITE_TAC[APPEND] THEN
1078          DISJ_CASES_TAC (ISPEC `t:(A#A)list` list_CASES) THENL
1079          [
1080            ASM_REWRITE_TAC[f_list_ext_table] THEN
1081              SUBGOAL_THEN `f_list_ext L (h:A#A) = h` ASSUME_TAC THENL
1082              [
1083                REWRITE_TAC[f_list_ext; res; f_list] THEN
1084                  SUBGOAL_THEN `find_face (h:A#A) L = f` ASSUME_TAC THENL
1085                  [
1086                    MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1087                      ASM_REWRITE_TAC[MEM];
1088                    ALL_TAC
1089                  ] THEN
1090
1091                  SUBGOAL_THEN `h:A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1092                  [
1093                    ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE; MEM];
1094                    ALL_TAC
1095                  ] THEN
1096
1097                  ASM_REWRITE_TAC[NEXT_EL; INDEX; LENGTH; ARITH_RULE `SUC 0 - 1 = 0`; HD];
1098                ALL_TAC
1099              ] THEN
1100              ASM_REWRITE_TAC[] THEN
1101              FIRST_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1102              MP_TAC (SPECL [`L:((A)list)list`; `h:A#A`] INVERSE_F_LIST_EXT_LEMMA) THEN
1103              ASM_REWRITE_TAC[];
1104            ALL_TAC
1105          ] THEN
1106
1107          POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1108          ASM_REWRITE_TAC[f_list_ext_table] THEN
1109          DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1110
1111          SUBGOAL_THEN `f_list_ext L h = h':A#A` ASSUME_TAC THENL
1112          [
1113            REWRITE_TAC[f_list_ext; res; f_list] THEN
1114              SUBGOAL_THEN `find_face (h:A#A) L = f` ASSUME_TAC THENL
1115              [
1116                MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1117                  ASM_REWRITE_TAC[MEM];
1118                ALL_TAC
1119              ] THEN
1120
1121              SUBGOAL_THEN `h:A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1122              [
1123                ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE; MEM];
1124                ALL_TAC
1125              ] THEN
1126
1127              ASM_REWRITE_TAC[NEXT_EL; INDEX; LENGTH; ARITH_RULE `~(0 = SUC(SUC n) - 1)`] THEN
1128              REWRITE_TAC[ARITH_RULE `0 + 1 = SUC 0`; EL; TL; HD];
1129            ALL_TAC
1130          ] THEN
1131
1132          ASM_REWRITE_TAC[] THEN
1133          POP_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1134          ASM_SIMP_TAC[INVERSE_F_LIST_EXT_LEMMA];
1135        ALL_TAC
1136      ] THEN
1137
1138      DISCH_THEN MATCH_MP_TAC THEN
1139      LIST_INDUCT_TAC THENL
1140      [
1141        REWRITE_TAC[f_list_ext_table];
1142        ALL_TAC
1143      ] THEN
1144
1145      REPEAT STRIP_TAC THEN
1146
1147      SUBGOAL_THEN `MEM (h':A#A) f` ASSUME_TAC THENL
1148      [
1149        ASM_REWRITE_TAC[MEM; MEM_APPEND];
1150        ALL_TAC
1151      ] THEN
1152
1153      SUBGOAL_THEN `ALL_DISTINCT (f:(A#A)list)` ASSUME_TAC THENL
1154      [
1155        MATCH_MP_TAC ALL_DISTINCT_FACE THEN
1156          EXISTS_TAC `L:((A)list)list` THEN
1157          ASM_REWRITE_TAC[];
1158        ALL_TAC
1159      ] THEN
1160
1161      UNDISCH_TAC `t = APPEND t1 (CONS (h':A#A) t')` THEN
1162      DISJ_CASES_TAC (ISPEC `t':(A#A)list` list_CASES) THENL
1163      [
1164        ASM_REWRITE_TAC[f_list_ext_table] THEN DISCH_TAC THEN
1165          SUBGOAL_THEN `f_list_ext L (h':A#A) = h` ASSUME_TAC THENL
1166          [
1167            REWRITE_TAC[f_list_ext; res; f_list] THEN
1168              SUBGOAL_THEN `find_face (h':A#A) L = f` ASSUME_TAC THENL
1169              [
1170                MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1171                  ASM_REWRITE_TAC[];
1172                ALL_TAC
1173              ] THEN
1174
1175              SUBGOAL_THEN `h':A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1176              [
1177                ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE] THEN
1178                  REWRITE_TAC[MEM; MEM_APPEND];
1179                ALL_TAC
1180              ] THEN
1181
1182              ASM_REWRITE_TAC[] THEN
1183              MP_TAC (ISPECL [`f:(A#A)list`; `t1:(A#A)list`; `h:A#A`; `h':A#A`; `t':(A#A)list`] NEXT_EL_APPEND_lemma) THEN
1184              ASM_REWRITE_TAC[];
1185            ALL_TAC
1186          ] THEN
1187
1188          ASM_REWRITE_TAC[] THEN
1189          POP_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1190          ASM_SIMP_TAC[INVERSE_F_LIST_EXT_LEMMA];
1191        ALL_TAC
1192      ] THEN
1193
1194      POP_ASSUM MP_TAC THEN STRIP_TAC THEN
1195      ASM_REWRITE_TAC[f_list_ext_table] THEN
1196      DISCH_TAC THEN
1197
1198      SUBGOAL_THEN `f_list_ext L (h':A#A) = h''` ASSUME_TAC THENL
1199      [
1200        REWRITE_TAC[f_list_ext; res; f_list] THEN
1201          SUBGOAL_THEN `find_face (h':A#A) L = f` ASSUME_TAC THENL
1202          [
1203            MATCH_MP_TAC FIND_FACE_LEMMA_EXPLICIT THEN
1204              ASM_REWRITE_TAC[];
1205            ALL_TAC
1206          ] THEN
1207
1208          SUBGOAL_THEN `h':A#A IN darts_of_list L` (fun th -> REWRITE_TAC[th]) THENL
1209          [
1210            ASM_REWRITE_TAC[darts_of_list; IN_SET_OF_LIST; DART_IN_FACE] THEN
1211              REWRITE_TAC[MEM; MEM_APPEND];
1212            ALL_TAC
1213          ] THEN
1214
1215          ASM_REWRITE_TAC[] THEN
1216          MP_TAC (ISPECL [`f:(A#A)list`; `t1:(A#A)list`; `h:A#A`; `h':A#A`; `t':(A#A)list`] NEXT_EL_APPEND_lemma) THEN
1217          ASM_REWRITE_TAC[NOT_CONS_NIL; HD];
1218        ALL_TAC
1219      ] THEN
1220
1221      ASM_REWRITE_TAC[] THEN
1222      CONJ_TAC THENL
1223      [
1224        POP_ASSUM (fun th -> ONCE_REWRITE_TAC[SYM th]) THEN
1225          ASM_SIMP_TAC[INVERSE_F_LIST_EXT_LEMMA];
1226        ALL_TAC
1227      ] THEN
1228
1229      FIRST_X_ASSUM (MP_TAC o SPEC `APPEND t1 [h':A#A]`) THEN
1230      ASM_REWRITE_TAC[] THEN
1231      DISCH_THEN MATCH_MP_TAC THEN
1232
1233      UNDISCH_TAC `t':(A#A)list = CONS h'' t''` THEN
1234      DISCH_THEN (fun th -> REWRITE_TAC[SYM th]) THEN
1235      REPEAT REMOVE_ASSUM THEN
1236      SPEC_TAC (`t1:(A#A)list`, `t1:(A#A)list`) THEN
1237      LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND]);;
1238
1239
1240
1241
1242 let build_f_list_ext_table hol_list good_list_th faces_th =
1243   let f_table, inv_f_table = Hashtbl.create 100, Hashtbl.create 100 in
1244   let th0 = (MY_PROVE_HYP good_list_th o UNDISCH_ALL o ISPEC hol_list) F_LIST_EXT_TABLE in
1245   let all_tm = rator(concl th0) in
1246   let th1 = EQ_MP (AP_TERM all_tm faces_th) th0 in
1247   let th1_list = get_all th1 in
1248
1249   let step = fun th ->
1250     let th = BETA_RULE th in
1251     let ltm, rtm = dest_comb(concl th) in
1252     let first_th = hd_conv rtm in
1253     let f_table_th = EQ_MP (AP_TERM ltm first_th) th in
1254     let f_list, inv_f_list = f_list_ext_table_all f_table_th in
1255     let _ = map (fun tm, th -> Hashtbl.add f_table tm th) f_list in
1256     let _ = map (fun tm, th -> Hashtbl.add inv_f_table tm th) inv_f_list in
1257       () in
1258
1259   let _ = map step th1_list in
1260     f_table, inv_f_table;;
1261
1262
1263
1264
1265 (************************************)
1266
1267 (* Final conversion *)
1268
1269
1270 let compute_all hyp_str =
1271   let thm_table = Hashtbl.create 10 in
1272   let fun_table = Hashtbl.create 10 in
1273   let hol_list = create_hol_list hyp_str in
1274   let faces = LIST_OF_FACES_REWRITE_CONV (mk_comb (list_of_faces_const, hol_list)) in
1275   let LIST_OF_DARTS_CONV = REWRITE_CONV[LIST_OF_DARTS; faces; FLATTEN; ITLIST; APPEND] in
1276   let darts = LIST_OF_DARTS_CONV (mk_comb (list_of_darts_const, hol_list)) in
1277
1278   let GOOD_LIST_CONV tm =
1279     let th0 = REWRITE_CONV[good_list; darts] tm in
1280     let [c1;c2;c3] = conjuncts (rand(concl th0)) in
1281     let th1 = ALL_DISTINCT_NUM_PAIR_CONV c1 in
1282     let th2 = REWRITE_CONV[ALL; NOT_CONS_NIL] c2 in
1283     let th3 = (REWRITE_CONV[ALL_MEM] THENC GOOD_LIST_COND3_CONV) c3 in
1284     let th = CONJ (EQT_ELIM th1) (CONJ (EQT_ELIM th2) (EQT_ELIM th3)) in
1285       EQ_MP (SYM th0) th in
1286
1287   let y = mk_comb(good_list_const, hol_list) in
1288   let good_list_th = GOOD_LIST_CONV y in
1289
1290 (*
1291 test 1 GOOD_LIST_CONV y;; (* 2.448; (ALL_DISTINCT_NUM_PAIR_CONV) 1.748; (COND3) 0.244 *)
1292 *)
1293
1294   let components_th = MATCH_MP COMPONENTS_HYPERMAP_OF_LIST good_list_th in
1295   let darts_th = REWRITE_RULE[darts_of_list; darts] (CONJUNCT1 components_th) in
1296   let faces_th = REWRITE_RULE[faces_of_list; faces] (MATCH_MP FACE_SET_EQ_LIST good_list_th) in
1297     (*REWRITE_RULE[MAP; set_of_list] faces_th;; *)
1298
1299   let y = mk_comb(list_of_elements_const, hol_list) in
1300   let elements = LIST_OF_ELEMENTS_CONV y in
1301
1302   let LIST_OF_NODES_CONV = ONCE_REWRITE_CONV[list_of_nodes] THENC
1303     ONCE_REWRITE_CONV[darts] THENC ONCE_REWRITE_CONV[elements] THENC
1304     map_conv_univ (BETA_CONV THENC FILTER_NODE_CONV) in
1305
1306   let y = mk_comb(list_of_nodes_const, hol_list) in
1307   let nodes = LIST_OF_NODES_CONV y in
1308
1309   let good_nodes_th = ASSUME (mk_comb(`good_list_nodes:((num)list)list->bool`, hol_list)) in
1310   let hyp_nodes = REWRITE_RULE[good_list_nodes; nodes_of_list; nodes; MAP; set_of_list] good_nodes_th in
1311
1312   (* Table of node L x *)
1313   let table_of_nodes = build_table_of_nodes hol_list nodes in
1314
1315   (* Table of face L x *)
1316   let table_of_faces = build_table_of_faces hol_list good_list_th faces in
1317
1318   (* Table of face_map and inverses *)
1319 (*
1320   let f_list_th1 = MP (ISPEC hol_list F_LIST_EXT_TABLE) good_list_th in
1321   let f_list_th2 = REWRITE_RULE[faces; ALL] f_list_th1 in
1322   let f_list_ext_table_th = REWRITE_RULE[f_list_ext_table; HD] f_list_th2 in
1323 *)
1324   let f_list_ext_table, inv_f_list_ext_table = build_f_list_ext_table hol_list good_list_th faces in
1325
1326   (* List of edges *)
1327   let y = mk_comb(list_of_edges_const, hol_list) in
1328   let edges = REWRITE_CONV[list_of_edges; darts; MAP] y in
1329
1330   (* faces3, face4, face5, faces6 *)
1331   let faces3_tm = mk_comb(list_of_faces3_const, hol_list) in
1332   let faces4_tm = mk_comb(list_of_faces4_const, hol_list) in
1333   let faces5_tm = mk_comb(list_of_faces5_const, hol_list) in
1334   let faces6_tm = mk_comb(list_of_faces6_const, hol_list) in
1335
1336   let filter = filter_conv_univ (BETA_CONV THENC
1337                                    LAND_CONV (length_conv_univ NUM_SUC_CONV) THENC
1338                                    MY_NUM_EQ_CONV) in
1339
1340   let faces3 = (REWRITE_CONV[list_of_faces3; faces] THENC filter) faces3_tm in
1341   let faces4 = (REWRITE_CONV[list_of_faces4; faces] THENC filter) faces4_tm in
1342   let faces5 = (REWRITE_CONV[list_of_faces5; faces] THENC filter) faces5_tm in
1343   let faces6 = (REWRITE_CONV[list_of_faces6; faces] THENC filter) faces6_tm in
1344
1345   (* darts3, darts4, dartsX *)
1346   let darts3_tm = mk_comb(list_of_darts3_const, hol_list) in
1347   let darts4_tm = mk_comb(list_of_darts4_const, hol_list) in
1348
1349   let darts3 = (REWRITE_CONV[list_of_darts3; faces3] THENC flatten_conv_univ) darts3_tm in
1350   let darts4 = (REWRITE_CONV[list_of_darts4; faces4] THENC flatten_conv_univ) darts4_tm in
1351
1352   let filter = filter_conv_univ (BETA_CONV THENC
1353                                    RAND_CONV (length_conv_univ NUM_SUC_CONV) THENC
1354                                    NUM_LE_CONV) in
1355   let dartsX_tm = mk_comb(list_of_dartsX_const, hol_list) in
1356   let dartsX = (REWRITE_CONV[list_of_dartsX; list_of_faces456; faces] THENC
1357                   RAND_CONV filter THENC flatten_conv_univ) dartsX_tm in
1358
1359   (* add everything to the table *)
1360   let add = fun str thm -> Hashtbl.add thm_table str thm in
1361   let _ =
1362     add "faces" faces;
1363     add "darts" darts;
1364     add "good_list" good_list_th;
1365     add "edges" edges;
1366     add "nodes" nodes;
1367     add "elements" elements;
1368     add "darts3" darts3;
1369     add "darts4" darts4;
1370     add "dartsX" dartsX;
1371     add "faces3" faces3;
1372     add "faces4" faces4;
1373     add "faces5" faces5;
1374     add "faces6" faces6 in
1375
1376   let add = fun str table -> Hashtbl.add fun_table str table in
1377   let _ =
1378     add "face" table_of_faces;
1379     add "node" table_of_nodes;
1380     add "inverse" inv_f_list_ext_table;
1381     add "f_list_ext" f_list_ext_table in
1382
1383     hol_list, thm_table, fun_table;;
1384
1385
1386
1387 (*
1388 let hol_list, thm_table, fun_table = compute_all pentstring;;
1389
1390 let table = Hashtbl.find fun_table "f_list_ext";;
1391 Hashtbl.find table `0,2`;;
1392
1393 (* (1): 0.560; (2): 0.640; (3): 1.424; (4): 1.448; (5): 0.748 *)
1394 test 1 compute_all pentstring;;
1395
1396 Hashtbl.find list_thm "faces_table";;
1397 Hashtbl.find list_thm "darts4";;
1398 Hashtbl.find list_thm "edges";;
1399 *)
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416 (*
1417 let hol_list, list_thm = compute_all pentstring;;
1418 let th1 = MP (ISPEC hol_list FACE_MAP_TABLE) (Hashtbl.find list_thm "good_list");;
1419 let th2 = REWRITE_RULE[Hashtbl.find list_thm "faces"; ALL] th1;;
1420 let th3 = REWRITE_RULE[face_map_table; HD] th2;;
1421 *)
1422
1423
1424 (* Explicit orbit computation *)
1425 (* Orbits for lists *)
1426
1427 let list_orbit = define `list_orbit f x acc = if (MEM x acc) then acc else list_orbit f (f x) (CONS x acc)`;;
1428
1429
1430 (* The same definitions as in "pack_defs.hl" *)
1431 let REVERSE_TABLE  = define `(REVERSE_TABLE (f:num->A) 0 = []) /\
1432    (REVERSE_TABLE f (SUC i) = CONS (f i)  ( REVERSE_TABLE f i))`;;
1433
1434 let TABLE = new_definition `!(f:num->A) k. TABLE f k = REVERSE (REVERSE_TABLE f k)`;;
1435
1436
1437 let LENGTH_REVERSE = prove(`!l:(A)list. LENGTH (REVERSE l) = LENGTH l`,
1438    LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE; LENGTH; LENGTH_APPEND] THEN ARITH_TAC);;
1439
1440
1441 let LENGTH_REVERSE_TABLE = prove(`!(f:num->A) n. LENGTH (REVERSE_TABLE f n) = n`,
1442    GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE_TABLE; LENGTH]);;
1443
1444
1445 let LENGTH_TABLE = prove(`!(f:num->A) n. LENGTH(TABLE f n) = n`,
1446    REWRITE_TAC[TABLE; LENGTH_REVERSE; LENGTH_REVERSE_TABLE]);;
1447
1448
1449 let EL_REVERSE_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (REVERSE_TABLE f n) = f (n - i - 1)`,
1450    GEN_TAC THEN INDUCT_TAC THEN GEN_TAC THEN REWRITE_TAC[ARITH_RULE `~(i < 0)`] THEN
1451      DISCH_TAC THEN
1452      MP_TAC (SPEC `i:num` num_CASES) THEN
1453      DISCH_THEN DISJ_CASES_TAC THENL
1454      [
1455        ASM_REWRITE_TAC[REVERSE_TABLE; EL; HD; ARITH_RULE `SUC n - 0 - 1 = n`];
1456        ALL_TAC
1457      ] THEN
1458      POP_ASSUM CHOOSE_TAC THEN
1459      UNDISCH_TAC `i < SUC n` THEN ASM_REWRITE_TAC[LT_SUC; EL] THEN
1460      REWRITE_TAC[REVERSE_TABLE; TL; ARITH_RULE `SUC n - SUC n' = n - n'`] THEN
1461      DISCH_TAC THEN
1462      FIRST_X_ASSUM MATCH_MP_TAC THEN
1463      ASM_REWRITE_TAC[]);;
1464
1465
1466 let EL_REVERSE = prove(`!(l:(A)list) i. i < LENGTH l ==> EL i (REVERSE l) = EL (LENGTH l - i - 1) l`,
1467    LIST_INDUCT_TAC THEN REWRITE_TAC[LENGTH; REVERSE; LT] THEN
1468      REPEAT STRIP_TAC THENL
1469      [
1470        ASM_REWRITE_TAC[EL_APPEND; LENGTH_REVERSE; LT_REFL; SUB_REFL] THEN
1471          REWRITE_TAC[ARITH_RULE `SUC n - n - 1 = 0`] THEN
1472          REWRITE_TAC[EL; HD];
1473        ALL_TAC
1474      ] THEN
1475      ASM_REWRITE_TAC[EL_APPEND; LENGTH_REVERSE] THEN
1476      ASM_SIMP_TAC[ARITH_RULE `i < n ==> SUC n - i - 1 = SUC(n - i - 1)`] THEN
1477      REWRITE_TAC[EL; TL]);;
1478
1479
1480 let EL_TABLE = prove(`!(f:num->A) n i. i < n ==> EL i (TABLE f n) = f i`,
1481    REPEAT STRIP_TAC THEN
1482      REWRITE_TAC[TABLE] THEN
1483      MP_TAC (SPECL [`REVERSE_TABLE (f:num->A) n`; `i:num`] EL_REVERSE) THEN
1484      ASM_REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1485      MP_TAC (SPECL [`f:(num->A)`; `n:num`; `n - i - 1`] EL_REVERSE_TABLE) THEN
1486      ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - (n - i - 1) - 1 = i`] THEN
1487      ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - i - 1 < n`]);;
1488
1489
1490
1491
1492 let LIST_ORBIT_LEMMA = prove(`!f (x:A) n. 1 <= n /\ (f POWER n) x = x /\
1493     (!i j. ~(i = j) /\ i < n /\ j < n ==> ~((f POWER i) x = (f POWER j) x))
1494     ==> (!k. k <= n ==> list_orbit f ((f POWER (n - k)) x)
1495            (REVERSE_TABLE (\i. (f POWER i) x) (n - k)) = REVERSE_TABLE (\i. (f POWER i) x) n)`,
1496    REPEAT GEN_TAC THEN STRIP_TAC THEN
1497      INDUCT_TAC THEN DISCH_TAC THENL
1498      [
1499        REWRITE_TAC[SUB_0] THEN
1500          ONCE_REWRITE_TAC[list_orbit] THEN
1501          ASM_REWRITE_TAC[] THEN
1502          SUBGOAL_THEN `MEM (x:A) (REVERSE_TABLE (\i. (f POWER i) x) n)` ASSUME_TAC THENL
1503          [
1504            REWRITE_TAC[MEM_EXISTS_EL] THEN
1505              EXISTS_TAC `n - 1` THEN
1506              REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1507              MP_TAC (ARITH_RULE `1 <= n ==> n - 1 < n`) THEN
1508              ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1509              ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN
1510              ASM_SIMP_TAC[ARITH_RULE `1 <= n ==> n - (n - 1) - 1 = 0`] THEN
1511              REWRITE_TAC[Hypermap.POWER_0; I_THM];
1512            ALL_TAC
1513          ] THEN
1514          ASM_REWRITE_TAC[];
1515        ALL_TAC
1516      ] THEN
1517
1518      ONCE_REWRITE_TAC[list_orbit] THEN
1519      COND_CASES_TAC THENL
1520      [
1521        POP_ASSUM MP_TAC THEN
1522          REWRITE_TAC[MEM_EXISTS_EL] THEN
1523          REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1524          STRIP_TAC THEN
1525          POP_ASSUM MP_TAC THEN
1526          ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN
1527          FIRST_X_ASSUM (MP_TAC o SPECL [`n - SUC k`; `n - SUC k - i - 1`]) THEN
1528          ANTS_TAC THENL
1529          [
1530            POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
1531              UNDISCH_TAC `1 <= n` THEN
1532              ARITH_TAC;
1533            ALL_TAC
1534          ] THEN
1535
1536          SIMP_TAC[];
1537        ALL_TAC
1538      ] THEN
1539
1540      SUBGOAL_THEN `f ((f POWER (n - SUC k)) (x:A)) = (f POWER (n - k)) x` (fun th -> REWRITE_TAC[th]) THENL
1541      [
1542        ASM_SIMP_TAC[ARITH_RULE `SUC k <= n ==> n - k = SUC(n - SUC k)`] THEN
1543          REWRITE_TAC[Hypermap.COM_POWER; o_THM];
1544        ALL_TAC
1545      ] THEN
1546
1547      SUBGOAL_THEN `CONS ((f POWER (n - SUC k)) (x:A)) (REVERSE_TABLE (\i. (f POWER i) x) (n - SUC k)) = REVERSE_TABLE (\i. (f POWER i) x) (n - k)` ASSUME_TAC THENL
1548      [
1549        ASM_SIMP_TAC[ARITH_RULE `SUC k <= n ==> n - k = SUC(n - SUC k)`] THEN
1550          REWRITE_TAC[REVERSE_TABLE];
1551        ALL_TAC
1552      ] THEN
1553
1554      ASM_REWRITE_TAC[] THEN
1555      FIRST_X_ASSUM MATCH_MP_TAC THEN
1556      UNDISCH_TAC `SUC k <= n` THEN ARITH_TAC);;
1557
1558
1559
1560 let LIST_ORBIT_EXPLICIT = prove(`!f (x:A) n. 1 <= n /\ (f POWER n) x = x /\
1561             (!i j. ~(i = j) /\ i < n /\ j < n ==> ~((f POWER i) x = (f POWER j) x))
1562             ==> list_orbit f x [] = REVERSE_TABLE (\i. (f POWER i) x) n`,
1563    REPEAT STRIP_TAC THEN
1564      MP_TAC (SPEC_ALL LIST_ORBIT_LEMMA) THEN
1565      ASM_REWRITE_TAC[] THEN
1566      DISCH_THEN (MP_TAC o SPEC `n:num`) THEN
1567      REWRITE_TAC[LE_REFL; SUB_REFL; Hypermap.POWER; I_THM] THEN
1568      REWRITE_TAC[REVERSE_TABLE]);;
1569
1570
1571 let FINITE_ORBIT_MAP_EXPLICIT = prove(`!s f (x:A). f permutes s /\ FINITE s ==>
1572                 ?n. 1 <= n /\
1573                     orbit_map f x = {(f POWER k) x | k < n} /\
1574                     (f POWER n) x = x /\
1575                     (!i j. ~(i = j) /\ i < n /\ j < n ==> ~((f POWER i) x = (f POWER j) x))`,
1576    REPEAT STRIP_TAC THEN
1577      ABBREV_TAC `n = CARD (orbit_map f (x:A))` THEN
1578      EXISTS_TAC `n:num` THEN
1579      MP_TAC (SPEC_ALL Hypermap_and_fan.FINITE_ORBIT_MAP) THEN
1580      ASM_REWRITE_TAC[] THEN
1581      DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN
1582      REPEAT CONJ_TAC THENL
1583      [
1584        MP_TAC (SPEC_ALL Hypermap_and_fan.ORBIT_MAP_CARD_POS) THEN
1585          ASM_REWRITE_TAC[] THEN
1586          ARITH_TAC;
1587        EXPAND_TAC "n" THEN
1588          MATCH_MP_TAC Hypermap.lemma_cycle_orbit THEN
1589          EXISTS_TAC `s:A->bool` THEN ASM_REWRITE_TAC[];
1590        ALL_TAC
1591      ] THEN
1592      REPEAT STRIP_TAC THEN
1593      MP_TAC (INST[`n:num`, `k:num`] (SPEC_ALL Hypermap_and_fan.ORBIT_MAP_INJ)) THEN
1594      ASM_REWRITE_TAC[]);;
1595
1596
1597
1598 let ORBIT_EQ_LIST_ORBIT = prove(`!f s (x:A). f permutes s /\ FINITE s
1599                                   ==> orbit_map f x = set_of_list (list_orbit f x [])`,
1600    REPEAT GEN_TAC THEN
1601      DISCH_THEN (MP_TAC o MATCH_MP FINITE_ORBIT_MAP_EXPLICIT) THEN
1602      DISCH_THEN (STRIP_ASSUME_TAC o SPEC `x:A`) THEN
1603      ASM_SIMP_TAC[LIST_ORBIT_EXPLICIT] THEN
1604
1605      REWRITE_TAC[EXTENSION] THEN X_GEN_TAC `y:A` THEN
1606      REWRITE_TAC[IN_ELIM_THM; IN_SET_OF_LIST; MEM_EXISTS_EL] THEN
1607      REWRITE_TAC[LENGTH_REVERSE_TABLE] THEN
1608      EQ_TAC THEN STRIP_TAC THENL
1609      [
1610        EXISTS_TAC `n - k - 1` THEN
1611          MP_TAC (ARITH_RULE `k < n ==> n - k - 1 < n`) THEN
1612          ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
1613          ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN
1614          ASM_SIMP_TAC[ARITH_RULE `k < n ==> n - (n - k - 1) - 1 = k`];
1615        ALL_TAC
1616      ] THEN
1617      POP_ASSUM MP_TAC THEN
1618      ASM_SIMP_TAC[EL_REVERSE_TABLE] THEN DISCH_TAC THEN
1619      EXISTS_TAC `n - i - 1` THEN
1620      ASM_SIMP_TAC[ARITH_RULE `i < n ==> n - i - 1 < n`]);;
1621
1622
1623 (**************)
1624
1625
1626 (* PREV_EL_CONV *)
1627
1628 let [el_0_th; el_suc_th] = CONJUNCTS (ISPECL[`n:num`; `l:(num#num)list`] (GEN_ALL EL));;
1629 let n_var_num = `n:num`;;
1630 let l_list = `l:(num#num)list`;;
1631 let zero_const = `_0`;;
1632
1633 let rec el_conv tm =
1634   let ltm, l_tm = dest_comb tm in
1635   let el_tm, n_tm = dest_comb ltm in
1636     if (rand n_tm <> zero_const) then
1637       let n_suc_th = num_CONV n_tm in
1638       let m_tm = rand (rand (concl n_suc_th)) in
1639       let th0 = AP_THM (AP_TERM el_tm n_suc_th) l_tm in
1640       let th1' = INST[m_tm, n_var_num; l_tm, l_list] el_suc_th in
1641       let th1 = REWRITE_RULE[TL] th1' in
1642       let th2 = el_conv (rand(concl th1)) in
1643         TRANS th0 (TRANS th1 th2)
1644     else
1645       let th0' = INST[l_tm, l_list] el_0_th in
1646         REWRITE_RULE[HD] th0';;
1647
1648
1649
1650 let prev_hd_th = prove(`PREV_EL (x:A) (CONS x t) = LAST (CONS x t)`,
1651                        REWRITE_TAC[PREV_EL; INDEX]);;
1652
1653
1654
1655 let PREV_EL_CONV = REWRITE_CONV[PREV_EL; INDEX; PAIR_EQ; ARITH; LAST; NOT_CONS_NIL] THENC
1656   TRY_CONV (ONCE_DEPTH_CONV el_conv);;
1657
1658
1659 (*
1660 let N_LIST_CONV = (REWRITE_CONV[n_list] THENC
1661                      REWRITE_CONV[find_face; find_list; faces; MEM; PAIR_EQ; ARITH] THENC
1662                      ONCE_DEPTH_CONV PREV_EL_CONV THENC
1663                      REWRITE_CONV[e_list]);;
1664 *)
1665 (*
1666 let z = mk_comb (`n_list:((num)list)list->num#num->num#num`, x);;
1667 let zz = mk_comb (z, `2,0`);;
1668
1669
1670 N_LIST_CONV zz;;
1671 test 10 N_LIST_CONV zz;; (* 0.704 *)
1672 *)
1673
1674
1675 let list_orbit_mem = UNDISCH_ALL (prove(`(MEM (x:num#num) acc <=> T) ==> list_orbit f x acc = acc`,
1676                                         ONCE_REWRITE_TAC[list_orbit] THEN
1677                                           SIMP_TAC[]));;
1678 let list_orbit_not_mem = UNDISCH_ALL (prove(`(MEM (x:num#num) acc <=> F)
1679                                             ==> list_orbit f x acc = list_orbit f (f x) (CONS x acc)`,
1680                                             DISCH_TAC THEN
1681                                               GEN_REWRITE_TAC LAND_CONV[list_orbit] THEN
1682                                               ASM_REWRITE_TAC[]));;
1683
1684
1685
1686 let rec list_orbit_conv f_conv tm =
1687   let ltm, acc = dest_comb tm in
1688   let ltm, x_arg = dest_comb ltm in
1689   let ltm, f_arg = dest_comb ltm in
1690   let mem_th = REWRITE_CONV[MEM; PAIR_EQ; ARITH] (mk_binop mem_const x_arg acc) in
1691     if (rand(concl mem_th) = f_const) then
1692       let th0' = INST[x_arg, x_var_pair; f_arg, f_var_fun; acc, acc_var] list_orbit_not_mem in
1693       let th0 = PROVE_HYP mem_th th0' in
1694       let tm1 = rand(concl th0) in
1695       let ltm, acc1 = dest_comb tm1 in
1696       let ltm, x_arg1 = dest_comb ltm in
1697       let x_th = f_conv x_arg1 in
1698       let th1 = TRANS th0 (AP_THM (AP_TERM ltm x_th) acc1) in
1699       let th2 = list_orbit_conv f_conv (rand(concl th1)) in
1700         TRANS th1 th2
1701     else
1702       let th0 = INST[x_arg, x_var_pair; f_arg, f_var_fun; acc, acc_var] list_orbit_mem in
1703         PROVE_HYP mem_th th0;;
1704
1705
1706 (*
1707 let zzz =
1708   let t1 = mk_comb (`list_orbit:(num#num->num#num)->(num#num)->(num#num)list->(num#num)list`, z) in
1709     mk_comb(mk_comb(t1, `12,7`), `[]:(num#num)list`);;
1710
1711 list_orbit_conv N_LIST_CONV zzz;;
1712 *)