formal_lp/hypermap/computations/list_hypermap_computations.hl

   1 (* Explicit computations for hypermap_of_list *)
   2
   3 #load "str.cma";;
   4
   5 needs "../formal_lp/hypermap/ssreflect/list_hypermap_iso-compiled.hl";;
   6 needs "../formal_lp/hypermap/computations/list_conversions2.hl";;
   7 needs "../formal_lp/hypermap/computations/more_theory-compiled.hl";;
   8
   9 module List_hypermap_computations = struct
  10
  11 open Str;;
  12 open List;;
  13 open Misc_vars;;
  14 open Arith_misc;;
  15 open Arith_nat;;
  16 open More_list_hypermap;;
  17 open List_hypermap;;
  18 open List_conversions;;
  19 open List_hypermap_iso;;
  20
  21
  22 let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  23 let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  24 let TO_NUM = REWRITE_RULE[Arith_hash.NUM_THM] o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
  25 let to_num = rand o concl o TO_NUM;;
  26
  27
  28 (* Constants and variables *)
  29 let hd_var_num = `hd:num` and
  30     h_var_num = `h:num` and
  31     h1_var_num = `h1:num` and
  32     h2_var_num = `h2:num` and
  33     t_var = `t:(num)list` and
  34     x_var_pair = `x:num#num` and
  35     d_var_pair = `d:num#num` and
  36     h1_var_pair = `h1:num#num` and
  37     h2_var_pair = `h2:num#num` and
  38     acc_var = `acc:(num#num)list` and
  39     f_var_fun = `f:num#num->num#num` and
  40     l_cap_var = `L:((num)list)list` and
  41     ll_var = `ll:((num)list)list` and
  42     list_var = `list:(num#num)list` and
  43     t_var_numnum_list = `t:(num#num)list` and
  44     t_var_num_list = `t:(num)list` and
  45     t_var_list_list = `t:((num)list)list` and
  46     h_var_list = `h:(num)list` and
  47     r_var_list = `r:(num)list` and
  48     s1_var_list = `s1:(num)list` and
  49     s2_var_list = `s2:(num)list`;;
  50
  51 let num_list_type = `:(num)list`;;
  52 let num_list_list_type = `:((num)list)list`;;
  53
  54 let mem_const = `MEM:(num#num)->(num#num)list->bool` and
  55     flatten_const = `flatten:((num#num)list)list -> (num#num)list`;;
  56
  57
  58 let hypermap_of_list_const = `hypermap_of_list:((num)list)list->(num#num)hypermap` and
  59     list_of_darts_const = `list_of_darts:((num)list)list->(num#num)list` and
  60     list_of_edges_const = `list_of_edges:((num)list)list->((num#num)#(num#num))list` and
  61     list_of_faces_const = `list_of_faces:((num)list)list->((num#num)list)list` and
  62     list_of_nodes_const = `list_of_nodes:((num)list)list->((num#num)list)list` and
  63     list_of_elements_const = `list_of_elements:((num)list)list->(num)list` and
  64     good_list_const = `good_list:((num)list)list->bool` and
  65     good_list_nodes_const = `good_list_nodes:((num)list)list->bool`;;
  66
  67
  68 let num_pair_hash tm =
  69   let ltm, rtm = dest_pair tm in
  70     Arith_cache.num_tm_hash ltm ^ "," ^ Arith_cache.num_tm_hash rtm;;
  71
  72
  73
  74 let build_term_rewrite tm lhs =
  75   let rec build_rewrite tm =
  76     if tm = lhs then
  77       (fun th -> th), true
  78     else
  79       match tm with
  80         | Comb (l_tm, r_tm) ->
  81             let l_f, l_flag = build_rewrite l_tm and
  82                 r_f, r_flag = build_rewrite r_tm in
  83               if l_flag then
  84                 if r_flag then
  85                   (fun th -> MK_COMB (l_f th, r_f th)), true
  86                 else
  87                   (fun th -> AP_THM (l_f th) r_tm), true
  88               else
  89                 if r_flag then
  90                   (fun th -> AP_TERM l_tm (r_f th)), true
  91                 else
  92                   I, false
  93         | Abs (var_tm, b_tm) ->
  94             let b_f, b_flag = build_rewrite b_tm in
  95               if b_flag then
  96                 (fun th -> ABS var_tm (b_f th)), true
  97               else
  98                 I, false
  99         | _ -> I, false in
 100   let f, flag = build_rewrite tm in
 101     if flag then f else (fun th -> REFL tm);;
 102
 103
 104 (* eq_th = |- lhs = rhs; rewrites exact occurrences of lhs in tm and returns |- tm = tm[lhs/rhs] *)
 105 let term_rewrite tm eq_th =
 106   let lhs, _ = dest_eq (concl eq_th) in
 107     build_term_rewrite tm lhs eq_th;;
 108
 109
 110 (*
 111 let tm = `(x + 2) * 2 = 0 /\ (\y. (x + 2) * y) 3 = 2` and
 112     th = ARITH_RULE `x + 2 = 1 * 2 + x`;;
 113
 114 let f = build_term_rewrite tm `x + 2`;;
 115
 116 term_rewrite tm th;;
 117 f th;;
 118 PURE_REWRITE_CONV[th] tm;;
 119
 120 (* 0.304 *)
 121 test 10000 (term_rewrite tm) th;;
 122 (* 0.216 *)
 123 test 10000 f th;;
 124 (* 2.808 *)
 125 test 10000 (PURE_REWRITE_CONV[th]) tm;;
 126 *)
 127
 128
 129
 130 (* example of java style string from hypermap generator. *)
 131 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 ";;
 132 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 ";;
 133
 134 (* conversion to list.  e.g. convert_to_list pentstring *)
 135
 136 let convert_to_list  =
 137   let split_sp=  Str.split (regexp " +") in
 138   let strip_ = global_replace (regexp "_") "" in
 139   let rec movelist n (x,a) =
 140     if n = 0 then (x,a) else
 141       match x with
 142         | [] -> failwith "convert_to_list"
 143         | y::ys -> movelist (n-1) (ys, y::a) in
 144   let getone (x,a) = match x with
 145     | [] -> ([],a)
 146     | y::ys -> let (u,v) = movelist y (ys,[]) in (u,v::a) in
 147   let rec getall (x,a) =
 148     if (x=[]) then (x,a) else getall (getone (x,a)) in
 149   fun s ->
 150     let h::ss = (split_sp (strip_ s)) in
 151     let _::ns = map int_of_string ss in
 152     let (_,a) = getall (ns,[]) in
 153      (h,rev (map rev a));;
 154
 155
 156 let create_hol_list ll =
 157   let s1 = map (map mk_small_numeral) ll in
 158   let s2 = map (fun l -> mk_list (l, num_type)) s1 in
 159     mk_list (s2, num_list_type);;
 160
 161 let create_hol_list_str =
 162   create_hol_list o snd o convert_to_list;;
 163
 164 let test_list0 = create_hol_list_str test_string;;
 165 let test_list = to_num test_list0;;
 166
 167
 168 let print_num tm =
 169   try
 170     let n = raw_dest_hash tm in
 171     let str = "'" ^ Num.string_of_num n in
 172       Format.print_string str
 173   with _ -> failwith "print_num";;
 174
 175 install_user_printer ("num", print_num);;
 176
 177
 178 (********************************************)
 179
 180 let eval_mem_num_pair = eval_mem_univ pair_eq_conv_num;;
 181 let mem_num_pair_conv = mem_conv_univ pair_eq_conv_num;;
 182
 183
 184 (*************************************)
 185 (* list_sum conversions *)
 186
 187 let LIST_SUM_A_EMPTY = prove(`list_sum [] (f:A->real) = &0`, REWRITE_TAC[Seq2.list_sum_nil]) and
 188     LIST_SUM_A_H = prove(`list_sum [h:A] f = f h`, REWRITE_TAC[Seq2.list_sum_cons; Seq2.list_sum_nil; REAL_ADD_RID]) and
 189     LIST_SUM_A_CONS = prove(`list_sum (CONS (h:A) t) f = f h + list_sum t f`, REWRITE_TAC[Seq2.list_sum_cons]);;
 190
 191
 192 let list_sum_conv f_conv tm =
 193   let ltm, f_tm = dest_comb tm in
 194   let list_tm = rand ltm in
 195   let list_ty = type_of list_tm in
 196   let f_ty = type_of f_tm in
 197   let ty = (hd o snd o dest_type) list_ty in
 198   let f_var = mk_var("f", f_ty) and
 199       h_var = mk_var("h", ty) and
 200       t_var = mk_var("t", list_ty) in
 201   let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in
 202   let list_sum_h = inst_t LIST_SUM_A_H and
 203       list_sum_cons = inst_t LIST_SUM_A_CONS in
 204
 205   let rec list_sum_conv_raw = fun h_tm t_tm ->
 206     if (is_comb t_tm) then
 207       let h_tm', t_tm' = dest_comb t_tm in
 208       let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in
 209       let ltm, rtm = dest_comb(rand(concl th0)) in
 210       let plus_op, fh_tm = dest_comb ltm in
 211       let f_th = f_conv fh_tm in
 212       let th1 = list_sum_conv_raw (rand h_tm') t_tm' in
 213       let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in
 214         TRANS th0 th2
 215     else
 216       let th0 = INST[h_tm, h_var] list_sum_h in
 217       let f_th = f_conv (rand(concl th0)) in
 218         TRANS th0 f_th in
 219
 220     if (is_comb list_tm) then
 221       let h_tm, t_tm = dest_comb list_tm in
 222         list_sum_conv_raw (rand h_tm) t_tm
 223     else
 224       inst_t LIST_SUM_A_EMPTY;;
 225
 226
 227 (*********************************)
 228 (* e_list conversions *)
 229
 230 let eval_e_list_num =
 231   let th0 = prove(`e_list (x:num,y:num) = y,x`, REWRITE_TAC[e_list]) in
 232     fun d_tm ->
 233       let ltm, y_tm = dest_comb d_tm in
 234       let x_tm = rand ltm in
 235         INST[x_tm, x_var_num; y_tm, y_var_num] th0;;
 236
 237
 238 let e_list_conv_num tm =
 239   let ltm, d_tm = dest_comb tm in
 240     if ((fst o dest_const) ltm <> "e_list") then
 241       failwith "e_list_conv_num: e_list expected"
 242     else
 243       eval_e_list_num d_tm;;
 244
 245
 246 (*********************************)
 247 (* list_pairs_conv *)
 248 let RULE tm = prove(tm, REWRITE_TAC[list_pairs2]);;
 249 let list_pairs2_0 = RULE `list_pairs2 [] (hd:num) = []` and
 250     list_pairs2_1 = RULE `list_pairs2 [h1] (hd:num) = [h1,hd]` and
 251     list_pairs2_2 = RULE `list_pairs2 (h1 :: h2 :: t) (hd:num) = (h1,h2) :: list_pairs2 (h2 :: t) hd`;;
 252
 253 let RULE tm = prove(tm, REWRITE_TAC[list_pairs_eq_list_pairs2; list_pairs2_0; HD]);;
 254 let list_pairs_empty = RULE `list_pairs ([]:(num)list) = []` and
 255     list_pairs_cons = RULE `list_pairs ((h:num) :: t) = list_pairs2 (h :: t) h`;;
 256
 257
 258 let list_pairs2_conv tm =
 259   let ltm, hd_tm = dest_comb tm in
 260   let rec list_pairs2_rec list =
 261     if (is_comb list) then
 262       let h_tm', t1_tm = dest_comb list in
 263       let h1_tm = rand h_tm' in
 264         if (is_comb t1_tm) then
 265           let h_tm', t2_tm = dest_comb t1_tm in
 266           let h2_tm = rand h_tm' in
 267           let th0 = INST[h1_tm, h1_var_num; h2_tm, h2_var_num; t2_tm, t_var; hd_tm, hd_var_num] list_pairs2_2 in
 268           let ltm = rator (rand (concl th0)) in
 269           let th1 = list_pairs2_rec t1_tm in
 270             TRANS th0 (AP_TERM ltm th1)
 271         else
 272           INST[h1_tm, h1_var_num; hd_tm, hd_var_num] list_pairs2_1
 273     else
 274       INST[hd_tm, hd_var_num] list_pairs2_0 in
 275     list_pairs2_rec (rand ltm);;
 276
 277
 278 let eval_list_pairs list_tm =
 279   if (is_comb list_tm) then
 280     let h_tm', t_tm = dest_comb list_tm in
 281     let h_tm = rand h_tm' in
 282     let th0 = INST[h_tm, h_var_num; t_tm, t_var] list_pairs_cons in
 283     let th1 = list_pairs2_conv (rand (concl th0)) in
 284       TRANS th0 th1
 285   else
 286     list_pairs_empty;;
 287
 288
 289 let list_pairs_conv = eval_list_pairs o rand;;
 290
 291
 292
 293 (***********************************************)
 294 (* list_of_faces_conv *)
 295
 296 let LIST_OF_FACES_REWRITE_CONV = REWRITE_CONV[list_of_faces; MAP; list_pairs_eq_list_pairs2; list_pairs2; HD];;
 297
 298 (* applies the given operation to the rhs of eq_th and returns op (lhs) = op (rhs) *)
 299 let apply_op eq_th op =
 300   let op_rhs = op (rand (concl eq_th)) in
 301   let op_tm = (rator o lhand o concl) op_rhs in
 302     TRANS (AP_TERM op_tm eq_th) op_rhs;;
 303
 304
 305 let eval_list_of_faces =
 306   let eq_th = prove(`list_of_faces (L:((num)list)list) = MAP list_pairs L`, REWRITE_TAC[list_of_faces]) in
 307     fun tm ->
 308       let th0 = INST[tm, l_cap_var] eq_th in
 309       let rtm = (rand o concl) th0 in
 310       let th1 = map_conv_univ list_pairs_conv rtm in
 311         TRANS th0 th1;;
 312
 313
 314 let filter_FILTER = prove(`filter = FILTER`,
 315                           REWRITE_TAC[FUN_EQ_THM] THEN GEN_TAC THEN
 316                             LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[Seq.filter; FILTER]);;
 317
 318 let eval_list_of_faces3, eval_list_of_faces4, eval_list_of_faces5, eval_list_of_faces6 =
 319   let eq3_th = (MY_RULE_NUM o prove)
 320     (`list_of_faces3 (L:((num)list)list) = FILTER (\f. LENGTH f = 3) (list_of_faces L)`,
 321      REWRITE_TAC[list_of_faces3; filter_FILTER]) in
 322   let eq4_th = (MY_RULE_NUM o prove)
 323     (`list_of_faces4 (L:((num)list)list) = FILTER (\f. LENGTH f = 4) (list_of_faces L)`,
 324      REWRITE_TAC[list_of_faces4; filter_FILTER]) in
 325   let eq5_th = (MY_RULE_NUM o prove)
 326     (`list_of_faces5 (L:((num)list)list) = FILTER (\f. LENGTH f = 5) (list_of_faces L)`,
 327      REWRITE_TAC[list_of_faces5; filter_FILTER]) in
 328   let eq6_th = (MY_RULE_NUM o prove)
 329     (`list_of_faces6 (L:((num)list)list) = FILTER (\f. LENGTH f = 6) (list_of_faces L)`,
 330      REWRITE_TAC[list_of_faces6; filter_FILTER]) in
 331   let op3_tm = (rator o rand o concl) eq3_th in
 332   let op4_tm = (rator o rand o concl) eq4_th in
 333   let op5_tm = (rator o rand o concl) eq5_th in
 334   let op6_tm = (rator o rand o concl) eq6_th in
 335   let eval eq_th op_tm list_tm faces_th =
 336     let th0 = INST[list_tm, l_cap_var] eq_th in
 337     let th1 = AP_TERM op_tm faces_th in
 338     let th2 = filter_conv_univ (BETA_CONV THENC LAND_CONV length_conv THENC raw_eq_hash_conv) (rand (concl th1)) in
 339       TRANS th0 (TRANS th1 th2) in
 340     (eval eq3_th op3_tm),
 341   (eval eq4_th op4_tm),
 342   (eval eq5_th op5_tm),
 343   (eval eq6_th op6_tm);;
 344
 345
 346 let eval_faces_of_list0 =
 347   let th0 = ISPEC l_cap_var faces_of_list in
 348   let op_tm = `MAP set_of_list : ((num#num)list)list->(num#num->bool)list` in
 349     fun list_tm faces_th ->
 350       let th1 = INST[list_tm, l_cap_var] th0 in
 351       let th2 = AP_TERM op_tm faces_th in
 352       let th3 = map_conv_univ set_of_list_conv ((rand o concl) th2) in
 353         TRANS th1 (TRANS th2 th3);;
 354
 355
 356 (*
 357 let y = mk_comb (list_of_darts_const, test_list);;
 358 test 100 LIST_OF_FACES_REWRITE_CONV y;; (* 0.224 *)
 359 test 100 eval_list_of_faces test_list;; (* 0.104 *)
 360 *)
 361
 362 (*********************************)
 363 (* list_of_darts *)
 364
 365 let eval_list_of_darts0, eval_list_of_darts3, eval_list_of_darts4,
 366         eval_list_of_darts5, eval_list_of_darts6 =
 367   let eq0_th = prove(`list_of_darts (L:((num)list)list) = flatten (list_of_faces L)`, REWRITE_TAC[list_of_darts_alt]) in
 368   let eq3_th = prove(`list_of_darts3 (L:((num)list)list) = flatten (list_of_faces3 L)`, REWRITE_TAC[list_of_darts3]) in
 369   let eq4_th = prove(`list_of_darts4 (L:((num)list)list) = flatten (list_of_faces4 L)`, REWRITE_TAC[list_of_darts4]) in
 370   let eq5_th = prove(`list_of_darts5 (L:((num)list)list) = flatten (list_of_faces5 L)`, REWRITE_TAC[list_of_darts5]) in
 371   let eq6_th = prove(`list_of_darts6 (L:((num)list)list) = flatten (list_of_faces6 L)`, REWRITE_TAC[list_of_darts6]) in
 372   let eval eq_th list_tm faces_th =
 373     let th0 = INST[list_tm, l_cap_var] eq_th in
 374       TRANS th0 (apply_op faces_th eval_flatten) in
 375     (eval eq0_th), (eval eq3_th), (eval eq4_th), (eval eq5_th), (eval eq6_th);;
 376
 377
 378 let eval_list_of_darts tm =
 379   eval_list_of_darts0 tm (eval_list_of_faces tm);;
 380
 381
 382 (*
 383 test 100 eval_list_of_darts test_list;; (* 0.204 *)
 384 *)
 385
 386
 387 (************************************)
 388 (* list_of_elements *)
 389 let eval_list_of_elements =
 390   let eq_th = prove(`list_of_elements (L:((num)list)list) = undup (flatten L)`, REWRITE_TAC[list_of_elements]) in
 391     fun tm ->
 392       let th0 = INST[tm, l_cap_var] eq_th in
 393         TRANS th0 (apply_op (eval_flatten tm) (eval_undup_univ raw_eq_hash_conv));;
 394
 395
 396 (*
 397 test 100 eval_list_of_elements test_list;; (* 1.432 *)
 398 *)
 399
 400
 401 (******************************)
 402 (* GOOD_LIST_CONV *)
 403
 404 let GOOD_LIST_COND3_EMPTY = prove(`ALL (\d:num#num. MEM (SND d,FST d) list) [] <=> T`, REWRITE_TAC[ALL]) and
 405     GOOD_LIST_COND3_CONS_T = (UNDISCH_ALL o prove)(`(MEM (y,x) list <=> T) ==>
 406                                                      (ALL (\d:num#num. MEM (SND d,FST d) list) (CONS (x,y) t) <=>
 407                                                         ALL (\d:num#num. MEM (SND d,FST d) list) t)`, SIMP_TAC[ALL]) and
 408     GOOD_LIST_COND3_CONS_F = (UNDISCH_ALL o prove)(`(MEM (y,x) list <=> F) ==>
 409                                                      (ALL (\d:num#num. MEM (SND d,FST d) list) (CONS (x,y) t) <=> F)`,
 410                                                    SIMP_TAC[ALL]);;
 411
 412
 413
 414 let rec good_list_cond3_conv tm =
 415   let ltm, list_tm = dest_comb tm in
 416   let f_tm = rand ltm in
 417   let list2_tm = (rand o snd o dest_abs) f_tm in
 418     if (is_comb list_tm) then
 419       let h_tm, t_tm = dest_comb list_tm in
 420       let x_tm, y_tm = dest_pair (rand h_tm) in
 421       let inst = INST[list2_tm, list_var; x_tm, x_var_num; y_tm, y_var_num; t_tm, t_var_numnum_list] in
 422       let mem_th = mem_num_pair_conv (mk_binop mem_const (mk_pair (y_tm, x_tm)) list2_tm) in
 423         if (rand(concl mem_th) = t_const) then
 424           let th0 = MY_PROVE_HYP mem_th (inst GOOD_LIST_COND3_CONS_T) in
 425           let th1 = good_list_cond3_conv (rand (concl th0)) in
 426             TRANS th0 th1
 427         else
 428           MY_PROVE_HYP mem_th (inst GOOD_LIST_COND3_CONS_F)
 429     else
 430       INST[list2_tm, list_var] GOOD_LIST_COND3_EMPTY;;
 431
 432
 433 let good_list_cond2_conv =
 434   let th_T = prove(`(\l. ~(l = [])) ((h:num) :: t) <=> T`, REWRITE_TAC[NOT_CONS_NIL]) and
 435       th_F = prove(`(\l. ~(l = [])) ([]:(num)list) <=> F`, REWRITE_TAC[]) in
 436   let test_f tm =
 437     let list_tm = rand tm in
 438       if is_comb list_tm then
 439         let h_tm', t_tm = dest_comb list_tm in
 440           INST[rand h_tm', h_var_num; t_tm, t_var_num_list] th_T
 441       else
 442         th_F in
 443     fun tm ->
 444       all_conv_univ test_f tm;;
 445
 446
 447
 448 let eval_good_list0 =
 449   let good_th = (MY_RULE o prove)(`list_of_darts L = (list:(num#num)list)
 450       /\ (uniq list <=> T)
 451       /\ (ALL (\l. ~(l = [])) L <=> T)
 452       /\ (ALL (\d. MEM (SND d,FST d) list) list <=> T)
 453       ==> good_list L`,
 454                                   SIMP_TAC[good_list; ALL_MEM; Seq2.ALL_all]) in
 455   let cond2_tm = `ALL (\l:(num)list. ~(l = []))` in
 456   let cond3_tm = `ALL (\d:num#num. MEM (SND d, FST d) list) list` in
 457     fun tm darts_th ->
 458       let darts_tm = (rand o concl) darts_th in
 459       let th0 = INST[tm, l_cap_var; darts_tm, list_var] good_th in
 460       let uniq_th = (eval_uniq_univ pair_eq_conv_num) darts_tm in
 461       let cond2_th = good_list_cond2_conv (mk_comb (cond2_tm, tm)) in
 462       let cond3_th = good_list_cond3_conv (subst[darts_tm, list_var] cond3_tm) in
 463         (MY_PROVE_HYP darts_th o MY_PROVE_HYP uniq_th o MY_PROVE_HYP cond2_th o MY_PROVE_HYP cond3_th) th0;;
 464
 465
 466 (*
 467 let darts = eval_list_of_darts test_list;;
 468 test 10 (eval_good_list0 test_list) darts;; (* 1.376 *)
 469 *)
 470
 471
 472 (*********************************)
 473 (* split_list_hyp *)
 474
 475 let one_eq = TO_NUM `1` and
 476     two_tm = to_num `2` and
 477     three_tm = to_num `3` and
 478     three_lt_tm = to_num `(<) 3`;;
 479
 480
 481 let split_list_hyp_empty = prove(`split_list_hyp [] (d:num#num) = []`, REWRITE_TAC[split_list_hyp]);;
 482 let split_list_hyp_cons_F = (MY_RULE o prove)(`list_pairs h = list /\ (MEM d list <=> F)
 483         ==> split_list_hyp (h :: t) d = h :: split_list_hyp t (d:num#num)`, SIMP_TAC[split_list_hyp]);;
 484 let split_list_hyp_cons_T = (UNDISCH_ALL o PURE_ONCE_REWRITE_RULE[GSYM one_eq] o DISCH_ALL o MY_RULE_NUM o prove)
 485   (`list_pairs h = list /\ (MEM (d:num#num) list <=> T) /\ (3 < LENGTH h <=> T)
 486       /\ indexl d list = i /\ rotr 1 (rot i h) = r /\ take 3 r = s1 /\ dropl 2 r = s2 /\ HD r = h1
 487       ==> split_list_hyp (h :: t) d = s1 :: (h1 :: s2) :: t`,
 488    SIMP_TAC[split_list_hyp; split_list_face] THEN
 489      STRIP_TAC THEN REPLICATE_TAC 3 (POP_ASSUM (fun th -> ALL_TAC)) THEN
 490      POP_ASSUM (fun th -> REWRITE_TAC[GSYM th]) THEN
 491      REWRITE_TAC[Seq.size_rotr; Seq.size_rot; Seq.size] THEN
 492      ASM_REWRITE_TAC[ARITH_RULE `a <= 3 <=> ~(3 < a)`] THEN
 493      REWRITE_TAC[Seq.cat]);;
 494
 495
 496 let rec eval_split_list_hyp tm d_tm =
 497   if not (is_comb tm) then
 498     INST[d_tm, d_var_pair] split_list_hyp_empty
 499   else
 500     let h_tm', t_tm = dest_comb tm in
 501     let h_tm = rand h_tm' in
 502     let pairs_th = eval_list_pairs h_tm in
 503     let list_tm = (rand o concl) pairs_th in
 504     let mem_th = eval_mem_num_pair d_tm list_tm in
 505       if (rand (concl mem_th) = f_const) then
 506         let th0 = (MY_PROVE_HYP pairs_th o MY_PROVE_HYP mem_th o
 507                      INST[d_tm, d_var_pair; t_tm, t_var_list_list; h_tm, h_var_list; list_tm, list_var])
 508           split_list_hyp_cons_F in
 509         let ltm = (rator o rand o concl) th0 in
 510         let th1 = eval_split_list_hyp t_tm d_tm in
 511           TRANS th0 (AP_TERM ltm th1)
 512       else
 513         let size_th = eval_length h_tm in
 514         let size_lt0 = AP_TERM three_lt_tm size_th in
 515         let size_lt1 = raw_lt_hash_conv ((rand o concl) size_lt0) in
 516           if (rand (concl size_lt1) = f_const) then
 517             failwith "eval_split_list_hyp: size (face) <= 3"
 518           else
 519             let size_lt_th = TRANS size_lt0 size_lt1 in
 520             let i_th = eval_index_univ pair_eq_conv_num d_tm list_tm in
 521             let i_tm = (rand o concl) i_th in
 522             let r_th = apply_op (eval_rot i_tm h_tm) eval_rotr1 in
 523             let r_tm = (rand o concl) r_th in
 524             let hd_th = eval_hd r_tm in
 525             let h1_tm = (rand o concl) hd_th in
 526             let take_th = eval_take three_tm r_tm in
 527             let s1_tm = (rand o concl) take_th in
 528             let drop_th = eval_drop two_tm r_tm in
 529             let s2_tm = (rand o concl) drop_th in
 530               (MY_PROVE_HYP i_th o MY_PROVE_HYP hd_th o MY_PROVE_HYP pairs_th o
 531                  MY_PROVE_HYP take_th o MY_PROVE_HYP r_th o MY_PROVE_HYP drop_th o
 532                  MY_PROVE_HYP mem_th o MY_PROVE_HYP size_lt_th o
 533                  INST[h_tm, h_var_list; list_tm, list_var; h1_tm, h1_var_num;
 534                       d_tm, d_var_pair; r_tm, r_var_list; i_tm, i_var_num; t_tm, t_var_list_list;
 535                       s1_tm, s1_var_list; s2_tm, s2_var_list])
 536                 split_list_hyp_cons_T;;
 537
 538
 539 (*
 540 let tm = test_list;;
 541 let d_tm = to_num `7,0`;;
 542
 543 (* 0.152 *)
 544 test 100 (eval_split_list_hyp tm) d_tm;;
 545 *)
 546
 547
 548 (*********************************)
 549 (* list_of_nodes *)
 550
 551 let filter_nodes_empty = prove(`filter (\d:num#num. FST d = x) [] = []`, REWRITE_TAC[Seq.filter]);;
 552 let filter_nodes_cons_eq = (MY_RULE o prove)(`(n = x <=> T) ==> filter (\d:num#num. FST d = x) (CONS (n,m) t) =
 553                                                  CONS (n,m) (filter (\d. FST d = x) t)`, SIMP_TAC[Seq.filter]);;
 554 let filter_nodes_cons_neq = (MY_RULE o prove)(`(n = x <=> F) ==> filter (\d:num#num. FST d = x) (CONS (n,m) t) =
 555                                                   filter (\d. FST d = x) t`, SIMP_TAC[Seq.filter]);;
 556
 557 let rec eval_filter_nodes x_tm list_tm =
 558   if (is_comb list_tm) then
 559     let h_tm', t_tm = dest_comb list_tm in
 560     let h_tm = rand h_tm' in
 561     let n_tm, m_tm = dest_pair h_tm in
 562     let inst = INST[n_tm, n_var_num; m_tm, m_var_num; t_tm, t_var_numnum_list; x_tm, x_var_num] in
 563     let eq_th = raw_eq_hash_conv (mk_eq (n_tm, x_tm)) in
 564       if (rand (concl eq_th) = t_const) then
 565         let th0 = MY_PROVE_HYP eq_th (inst filter_nodes_cons_eq) in
 566         let ltm = (rator o rand o concl) th0 in
 567         let th1 = eval_filter_nodes x_tm t_tm in
 568           TRANS th0 (AP_TERM ltm th1)
 569       else
 570         let th0 = MY_PROVE_HYP eq_th (inst filter_nodes_cons_neq) in
 571         let th1 = eval_filter_nodes x_tm t_tm in
 572           TRANS th0 th1
 573   else
 574     INST[x_tm, x_var_num] filter_nodes_empty;;
 575
 576
 577 let filter_nodes_conv filter_tm =
 578   let ltm, list_tm = dest_comb filter_tm in
 579   let x_tm = (rand o snd o dest_abs o rand) ltm in
 580     eval_filter_nodes x_tm list_tm;;
 581
 582
 583 (*
 584 let x_tm = to_num `11`;;
 585 let list_tm = (rand o concl o eval_list_of_darts) test_list;;
 586
 587 (* 10: 0.396 *)
 588 test 100 (eval_filter_nodes x_tm) list_tm;;
 589 *)
 590
 591
 592 let eval_list_of_nodes0 =
 593   let th0 = (MY_RULE o prove)(`list_of_darts L = list /\ list_of_elements L = (s1:(num)list)
 594       ==> list_of_nodes L = MAP (\x. filter (\d. FST d = x) list) s1`, SIMP_TAC[list_of_nodes]) in
 595     fun tm darts_th elements_th ->
 596       let list_tm = (rand o concl) darts_th in
 597       let s1_tm = (rand o concl) elements_th in
 598       let th1 = (MY_PROVE_HYP darts_th o MY_PROVE_HYP elements_th o
 599                    INST[list_tm, list_var; s1_tm, s1_var_list; tm, l_cap_var]) th0 in
 600       let rtm = rand (concl th1) in
 601       let map_th = map_conv_univ (BETA_CONV THENC filter_nodes_conv) rtm in
 602         TRANS th1 map_th;;
 603
 604
 605 let eval_nodes_of_list0 =
 606   let th0 = ISPEC l_cap_var nodes_of_list in
 607   let op_tm = `MAP set_of_list : ((num#num)list)list->(num#num->bool)list` in
 608     fun list_tm nodes_th ->
 609       let th1 = INST[list_tm, l_cap_var] th0 in
 610       let th2 = AP_TERM op_tm nodes_th in
 611       let th3 = map_conv_univ set_of_list_conv ((rand o concl) th2) in
 612         TRANS th1 (TRANS th2 th3);;
 613
 614
 615
 616 let eval_list_of_nodes tm =
 617   eval_list_of_nodes0 tm (eval_list_of_darts tm) (eval_list_of_elements tm);;
 618
 619
 620 (*
 621 let darts_th = eval_list_of_darts test_list;;
 622 let elements_th = eval_list_of_elements test_list;;
 623 (* 10: 0.528 *)
 624 test 10 (eval_list_of_nodes0 test_list darts_th) elements_th;;
 625 *)
 626
 627
 628 let build_table_of_nodes hyp_list nodes_th =
 629   let table_of_nodes = Hashtbl.create 100 in
 630   let th0 = (UNDISCH_ALL o ISPEC hyp_list) nodes_hypermap_of_list_all in
 631   let all_tm = rator (concl th0) in
 632   let th1 = EQ_MP (AP_TERM all_tm nodes_th) th0 in
 633   let th1_list = get_all th1 in
 634   let build1 th =
 635     let th = MY_BETA_RULE th in
 636     let list_tm = dest_list(rand(concl th)) in
 637     let ths = get_all th in
 638     let r = CONV_RULE (BETA_CONV THENC RAND_CONV set_of_list_conv) in
 639       map (fun tm, th -> Hashtbl.add table_of_nodes (num_pair_hash tm) (r th)) (zip list_tm ths) in
 640   let _ = map build1 th1_list in
 641     table_of_nodes;;
 642
 643
 644 (*
 645 let nodes_th = eval_list_of_nodes test_list;;
 646 (* 10: 0.156 *)
 647 test 10 (build_table_of_nodes test_list) nodes_th;;
 648 *)
 649
 650 (***************************)
 651 (* table of faces *)
 652
 653 let build_table_of_faces hyp_list good_list_th faces_th =
 654   let table_of_faces = Hashtbl.create 100 and
 655       table_of_find_face = Hashtbl.create 100 in
 656   let th0 = (MY_PROVE_HYP good_list_th o UNDISCH_ALL o ISPEC hyp_list) faces_hypermap_of_list_all in
 657   let all_tm = rator (concl th0) in
 658   let th1 = EQ_MP (AP_TERM all_tm faces_th) th0 in
 659   let th1_list = get_all th1 in
 660   let build1 th =
 661     let th = MY_BETA_RULE th in
 662     let list_tm = dest_list(rand(concl th)) in
 663     let ths = get_all th in
 664       map (fun tm, th ->
 665              let th1, th2 = (CONJ_PAIR o CONV_RULE BETA_CONV) th in
 666              let th1_2 = CONV_RULE (RAND_CONV set_of_list_conv) th1 in
 667              let hash = num_pair_hash tm in
 668                Hashtbl.add table_of_faces hash th1_2;
 669                Hashtbl.add table_of_find_face hash th2) (zip list_tm ths) in
 670   let _ = map build1 th1_list in
 671     table_of_faces, table_of_find_face;;
 672
 673 (*
 674 let faces_th = eval_list_of_faces test_list;;
 675 let darts_th = eval_list_of_darts0 test_list faces_th;;
 676 let good_list_th = eval_good_list0 test_list darts_th;;
 677 let table1, table2 = build_table_of_faces test_list good_th faces_th;;
 678 Hashtbl.find table1 "D7,D2D1";;
 679 Hashtbl.find table2 "D7,D2D1";;
 680 (* 10: 0.241 *)
 681 test 10 (build_table_of_faces test_list good_th) faces_th;;
 682 *)
 683
 684
 685 (*****************************)
 686 (* f_list_ext tables *)
 687
 688 let list_to_pair list = hd list, hd(tl list);;
 689
 690 let F_LIST_EXT_SINGLE, INV_F_LIST_EXT_SINGLE = (list_to_pair o CONJUNCTS o MY_RULE o prove)
 691   (`f_list_ext_table L [h1] (x:num#num)
 692    ==> f_list_ext L h1 = x /\
 693        inverse (f_list_ext L) x = h1`, SIMP_TAC[f_list_ext_table]);;
 694
 695 let F_LIST_EXT_CONS, INV_F_LIST_EXT_CONS = (list_to_pair o CONJUNCTS o MY_RULE o prove)
 696   (`f_list_ext_table L (h1 :: h2 :: t) (x:num#num)
 697   ==> f_list_ext L h1 = h2 /\
 698       inverse (f_list_ext L) h2 = h1`, SIMP_TAC[f_list_ext_table]);;
 699
 700 let F_LIST_EXT_TABLE_CONS = (MY_RULE o prove)
 701   (`f_list_ext_table L (h1 :: t) (x:num#num) ==> f_list_ext_table L t x`,
 702    DISJ_CASES_TAC (ISPEC `t:(num#num)list` list_CASES) THENL
 703      [
 704        ASM_REWRITE_TAC[f_list_ext_table];
 705        POP_ASSUM STRIP_ASSUME_TAC THEN
 706          ASM_SIMP_TAC[f_list_ext_table]
 707      ]);;
 708
 709
 710 let f_list_ext_table_all th =
 711   let ltm, x_tm = dest_comb(concl th) in
 712   let ltm, list_tm = dest_comb ltm in
 713   let l_tm = rand ltm in
 714   let inst_t = INST[x_tm, x_var_pair] in
 715   let f_single, inv_f_single = inst_t F_LIST_EXT_SINGLE, inst_t INV_F_LIST_EXT_SINGLE in
 716   let f_cons, inv_f_cons = inst_t F_LIST_EXT_CONS, inst_t INV_F_LIST_EXT_CONS in
 717   let f_table = inst_t F_LIST_EXT_TABLE_CONS in
 718
 719   let rec f_list_raw f_table_th h1_tm t1_tm =
 720     if (is_comb t1_tm) then
 721       let h2_tm', t2_tm = dest_comb t1_tm in
 722       let h2_tm = rand h2_tm' in
 723       let inst_t = MY_PROVE_HYP f_table_th o
 724         INST[l_tm, l_cap_var; h1_tm, h1_var_pair; h2_tm, h2_var_pair; t2_tm, t_var_numnum_list] in
 725
 726       let f_th, inv_f_th = inst_t f_cons, inst_t inv_f_cons in
 727       let th0 = (MY_PROVE_HYP f_table_th o INST[l_tm, l_cap_var; h1_tm, h1_var_pair; t1_tm, t_var_numnum_list]) f_table in
 728       let f_list, inv_f_list = f_list_raw th0 h2_tm t2_tm in
 729         (h1_tm, f_th) :: f_list, (h2_tm, inv_f_th) :: inv_f_list
 730
 731     else
 732       let inst_t = MY_PROVE_HYP f_table_th o INST[l_tm, l_cap_var; h1_tm, h1_var_pair] in
 733       let f_th, inv_f_th = inst_t f_single, inst_t inv_f_single in
 734         [h1_tm, f_th], [x_tm, inv_f_th] in
 735
 736     if (is_comb list_tm) then
 737       let h1_tm, t1_tm = dest_comb list_tm in
 738         f_list_raw th (rand h1_tm) t1_tm
 739     else
 740       [], [];;
 741
 742
 743 let build_f_list_ext_table =
 744   let th0' = (UNDISCH_ALL o ISPEC l_cap_var) f_list_ext_table_list_of_faces in
 745     fun hol_list good_list_th faces_th ->
 746       let f_table, inv_f_table = Hashtbl.create 100, Hashtbl.create 100 in
 747       let th0 = (MY_PROVE_HYP good_list_th o INST[hol_list, l_cap_var]) th0' in
 748       let all_tm = rator (concl th0) in
 749       let th1 = EQ_MP (AP_TERM all_tm faces_th) th0 in
 750       let th1_list = get_all th1 in
 751
 752       let step th =
 753         let th = MY_BETA_RULE th in
 754         let ltm, rtm = dest_comb(concl th) in
 755         let first_th = hd_conv rtm in
 756         let f_table_th = EQ_MP (AP_TERM ltm first_th) th in
 757         let f_list, inv_f_list = f_list_ext_table_all f_table_th in
 758         let _ = map (fun tm, th -> Hashtbl.add f_table (num_pair_hash tm) th) f_list in
 759         let _ = map (fun tm, th -> Hashtbl.add inv_f_table (num_pair_hash tm) th) inv_f_list in
 760           () in
 761
 762       let _ = map step th1_list in
 763         f_table, inv_f_table;;
 764
 765
 766 (*
 767 let faces_th = eval_list_of_faces test_list;;
 768 let darts_th = eval_list_of_darts0 test_list faces_th;;
 769 let good_th = eval_good_list0 test_list darts_th;;
 770 let ft, ift = build_f_list_ext_table test_list good_th faces_th;;
 771 Hashtbl.find ft "D7,D2D1";;
 772 Hashtbl.find ift "D7,D2D1";;
 773 (* 10: 0.056 *)
 774 test 10 (build_f_list_ext_table test_list good_th) faces_th;;
 775 *)
 776
 777
 778 (**************************************)
 779 (* compute_all *)
 780
 781 let compute_all hyp_list good_th_opt =
 782   let thm_table = Hashtbl.create 10 in
 783   let fun_table = Hashtbl.create 10 in
 784   let faces_th = eval_list_of_faces hyp_list in
 785   let darts_th = eval_list_of_darts0 hyp_list faces_th in
 786   let good_th =
 787     match good_th_opt with
 788       | Some th -> th
 789       | None -> eval_good_list0 hyp_list darts_th in
 790   let add = fun str thm -> Hashtbl.add thm_table str thm in
 791   let add_fun = fun str table -> Hashtbl.add fun_table str table in
 792   let _ =
 793     add "good_list" good_th;
 794     add "list_of_darts" darts_th;
 795     add "list_of_faces" faces_th in
 796
 797   let rec hyp_set name =
 798     try Hashtbl.find thm_table name
 799     with Not_found ->
 800       (match name with
 801          | "list_of_darts3" ->
 802              let faces3_th = eval_list_of_faces3 hyp_list faces_th in
 803              let darts3_th = eval_list_of_darts3 hyp_list faces3_th in
 804              let _ = add "list_of_darts3" darts3_th in
 805                darts3_th
 806          | "list_of_darts4" ->
 807              let faces4_th = eval_list_of_faces4 hyp_list faces_th in
 808              let darts4_th = eval_list_of_darts4 hyp_list faces4_th in
 809              let _ = add "list_of_darts4" darts4_th in
 810                darts4_th
 811          | "list_of_darts5" ->
 812              let faces5_th = eval_list_of_faces5 hyp_list faces_th in
 813              let darts5_th = eval_list_of_darts5 hyp_list faces5_th in
 814              let _ = add "list_of_darts5" darts5_th in
 815                darts5_th
 816          | "list_of_darts6" ->
 817              let faces6_th = eval_list_of_faces6 hyp_list faces_th in
 818              let darts6_th = eval_list_of_darts6 hyp_list faces6_th in
 819              let _ = add "list_of_darts6" darts6_th in
 820                darts6_th
 821          | "list_of_elements" ->
 822              let elements_th = eval_list_of_elements hyp_list in
 823              let _ = add "list_of_elements" elements_th in
 824                elements_th
 825          | "list_of_nodes" ->
 826              let nodes_th = eval_list_of_nodes0 hyp_list darts_th (hyp_set "list_of_elements") in
 827              let _ = add "list_of_nodes" nodes_th in
 828                nodes_th
 829          | "nodes_of_list" ->
 830              let set_nodes_th = eval_nodes_of_list0 hyp_list (hyp_set "list_of_nodes") in
 831              let _ = add "nodes_of_list" set_nodes_th in
 832                set_nodes_th
 833          | "faces_of_list" ->
 834              let set_faces_th = eval_faces_of_list0 hyp_list (hyp_set "list_of_faces") in
 835              let _ = add "faces_of_list" set_faces_th in
 836                set_faces_th
 837          | _ -> failwith ("Bad hypermap set: " ^ name)) in
 838
 839   let hyp_fun name dart_tm =
 840     let table =
 841       try Hashtbl.find fun_table name
 842       with Not_found ->
 843         (match name with
 844            | "face" ->
 845                let table_of_faces, table_of_find_face = build_table_of_faces hyp_list good_th faces_th in
 846                let _ = add_fun "face" table_of_faces in
 847                let _ = add_fun "find_face" table_of_find_face in
 848                  table_of_faces
 849            | "find_face" ->
 850                let table_of_faces, table_of_find_face = build_table_of_faces hyp_list good_th faces_th in
 851                let _ = add_fun "face" table_of_faces in
 852                let _ = add_fun "find_face" table_of_find_face in
 853                  table_of_find_face
 854            | "node" ->
 855                let table_of_nodes = build_table_of_nodes hyp_list (hyp_set "list_of_nodes") in
 856                let _ = add_fun "node" table_of_nodes in
 857                  table_of_nodes
 858            | "f_list_ext" | "inverse" ->
 859                let f_table, inv_f_table = build_f_list_ext_table hyp_list good_th faces_th in
 860                let _ = add_fun "f_list_ext" f_table in
 861                let _ = add_fun "inverse" inv_f_table in
 862                  if name = "inverse" then inv_f_table else f_table
 863            | _ -> failwith ("Bad hypermap function: " ^ name)) in
 864       try Hashtbl.find table (num_pair_hash dart_tm)
 865       with Not_found -> failwith ("Bad dart index: " ^ num_pair_hash dart_tm) in
 866
 867     hyp_set, hyp_fun;;
 868
 869
 870 let add_eq eq1_th eq2_th =
 871   let th0 = MK_COMB (AP_TERM add_op_num eq1_th, eq2_th) in
 872   let r_th = raw_add_conv_hash (rand (concl th0)) in
 873     TRANS th0 r_th;;
 874
 875 let mul_eq eq1_th eq2_th =
 876   let th0 = MK_COMB (AP_TERM mul_op_num eq1_th, eq2_th) in
 877   let r_th = raw_mul_conv_hash (rand (concl th0)) in
 878     TRANS th0 r_th;;
 879
 880 let eq_eq eq1_th eq2_th =
 881   let th0 = MK_COMB (AP_TERM eq_op_num eq1_th, eq2_th) in
 882   let r_th = raw_eq_hash_conv (rand (concl th0)) in
 883     TRANS th0 r_th;;
 884
 885
 886 let eval_good_list_nodes_condition0 =
 887   let two = to_num `2` and
 888       four = to_num `4` in
 889     fun elements_th darts_th faces_th ->
 890       let length_darts = apply_op darts_th eval_length and
 891           length_faces = apply_op faces_th eval_length and
 892           length_elements = apply_op elements_th eval_length in
 893         (* 2 * (sizel (list_of_elements L) + sizel (list_of_faces L)) = sizel (list_of_darts L) + 4 *)
 894       let (+), ( * ), (!), (==) = add_eq, mul_eq, REFL, eq_eq in
 895         (!two * (length_elements + length_faces)) == (length_darts + !four);;
 896
 897 let eval_good_list_nodes_condition hyp_set =
 898   eval_good_list_nodes_condition0 (hyp_set "list_of_elements") (hyp_set "list_of_darts") (hyp_set "list_of_faces");;
 899
 900
 901 end;;
 902
 903 (*
 904 open List_hypermap_computations;;
 905
 906 let t1, t2 = compute_all test_list None;;
 907 (* 10: 2.635 *)
 908 test 10 (compute_all test_list) None;;
 909
 910 num_pair_hash (to_num `1,0`);;
 911 t2 "node" (to_num `0,1`);;
 912 *)