formal_lp/old/list/list_conversions.hl

   1 needs "../formal_lp/arith/nat.hl";;
   2
   3 open Arith_nat;;
   4 open Arith_misc;;
   5
   6 let t_const = `T` and
   7     f_const = `F`;;
   8
   9
  10 let MY_PROVE_HYP hyp th = EQ_MP (DEDUCT_ANTISYM_RULE hyp th) hyp;;
  11 let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  12 let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  13
  14
  15
  16
  17 (******************************)
  18
  19 (* HD conversions *)
  20
  21 let HD_A_CONS = prove(`HD (CONS (h:A) t) = h`, REWRITE_TAC[HD]);;
  22
  23 (* Takes a term `[a;...]` and returns the theorem |- HD [a;...] = a *)
  24 let eval_hd list_tm =
  25   let ltm, t_tm = dest_comb list_tm in
  26   let h_tm = rand ltm in
  27   let list_ty = type_of t_tm and
  28       ty = type_of h_tm in
  29   let h_var = mk_var("h", ty) and
  30       t_var = mk_var("t", list_ty) in
  31     (INST[h_tm, h_var; t_tm, t_var] o INST_TYPE[ty, aty]) HD_A_CONS;;
  32
  33 (* Takes a term `HD [a;...]` and returns the theorem |- HD [a;...] = a *)
  34 let hd_conv hd_tm =
  35   if (fst o dest_const o rator) hd_tm <> "HD" then failwith "hd_conv"
  36   else eval_hd (rand hd_tm);;
  37
  38
  39 (*
  40 let tm = `HD [1;2;3;4]`;;
  41 hd_conv tm;;
  42 (* 0.072 *)
  43 test 1000 (REWRITE_CONV[HD]) tm;;
  44 (* 0.016 *)
  45 test 1000 hd_conv tm;;
  46 let tm = `[1;2;3;4]`;;
  47 eval_hd tm;;
  48 test 1000 eval_hd tm;;
  49 *)
  50
  51
  52 (*********************************)
  53 (* EL conversion *)
  54
  55 let EL_0' = (MY_RULE_NUM o prove)(`EL 0 (CONS (h:A) t) = h`, REWRITE_TAC[EL; HD]);;
  56 let EL_n' = (MY_RULE_NUM o prove)(`0 < n /\ PRE n = m ==> EL n (CONS (h:A) t) = EL m t`,
  57    STRIP_TAC THEN SUBGOAL_THEN `n = SUC m` ASSUME_TAC THENL
  58      [ REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC ] THEN ASM_REWRITE_TAC[EL; TL]);;
  59
  60
  61 let zero_const = `_0` and
  62     pre_const = `PRE`;;
  63
  64 let m_var_num = `m:num` and
  65     n_var_num = `n:num`;;
  66
  67
  68 (* Takes a raw numeral term and a list term and returns the theorem |- EL n [...] = x *)
  69 let eval_el n_tm list_tm =
  70   let list_ty = type_of list_tm in
  71   let ty = (hd o snd o dest_type) list_ty in
  72   let inst_t = INST_TYPE[ty, aty] in
  73   let el_0, el_n = inst_t EL_0', inst_t EL_n' in
  74   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
  75
  76   let rec el_conv_raw = fun n_tm list_tm ->
  77     let h_tm, t_tm = dest_cons list_tm in
  78     let inst0 = INST[h_tm, h_var; t_tm, t_var] in
  79     if n_tm = zero_const then
  80       inst0 el_0
  81     else
  82       let n_gt0 = (EQT_ELIM o raw_gt0_hash_conv) n_tm in
  83       let pre_n = raw_pre_hash_conv (mk_comb (pre_const, n_tm)) in
  84       let m_tm = (rand o concl) pre_n in
  85       let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o
  86                    INST[n_tm, n_var_num; m_tm, m_var_num] o inst0) el_n in
  87       let th1 = el_conv_raw m_tm t_tm in
  88         TRANS th0 th1 in
  89     el_conv_raw n_tm list_tm;;
  90
  91
  92
  93 (* Takes a term `EL n [...]` and returns the theorem |- EL n [...] = x *)
  94 (* Note: n must be a raw numeral term Dx (Dy ... _0) *)
  95 let el_conv el_tm =
  96   let ltm, list_tm = dest_comb el_tm in
  97   let el, n_tm = dest_comb ltm in
  98   if (fst o dest_const) el <> "EL" then failwith "el_conv"
  99   else eval_el n_tm list_tm;;
 100
 101 (*
 102 let n0_tm = `_0` and
 103     n_tm = `D3 _0` and
 104     list_tm = `[1; 2; 3; 4; 5]`;;
 105
 106 eval_el n0_tm list_tm;;
 107 (* 0.24 *)
 108 test 10000 (eval_el n0_tm) list_tm;;
 109
 110 eval_el n_tm list_tm;;
 111 (* 1.22 *)
 112 test 10000 (eval_el n_tm) list_tm;;
 113
 114 let tm = mk_icomb (mk_comb (`EL`, n_tm), list_tm);;
 115 el_conv tm;;
 116 *)
 117
 118
 119
 120 (*******************************)
 121
 122 (* FST, SND conversions *)
 123
 124 let FST' = ISPECL[`x:A`; `y:B`] FST;;
 125 let SND' = ISPECL[`x:A`; `y:B`] SND;;
 126
 127
 128 let fst_conv tm =
 129   let x_tm, y_tm = dest_pair (rand tm) in
 130   let x_ty, y_ty = type_of x_tm, type_of y_tm in
 131   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
 132     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';;
 133
 134 let snd_conv tm =
 135   let x_tm, y_tm = dest_pair (rand tm) in
 136   let x_ty, y_ty = type_of x_tm, type_of y_tm in
 137   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
 138     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';;
 139
 140
 141 (*
 142 let tm = `FST (1,2)`;;
 143 fst_conv tm;;
 144
 145 (* 0.688 *)
 146 test 10000 (REWRITE_CONV[]) tm;;
 147 (* 0.100 *)
 148 test 10000 fst_conv tm;;
 149 *)
 150
 151
 152 (******************************)
 153
 154 (* LENGTH conversions *)
 155
 156 let LENGTH_0' = (MY_RULE_NUM o prove) (`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and
 157     LENGTH_CONS' = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);;
 158
 159 let suc_const = `SUC`;;
 160
 161 (* Takes a term `[...]` and returns the theorem |- LENGTH [...] = n *)
 162 let eval_length list_tm =
 163   let list_ty = type_of list_tm in
 164   let ty = (hd o snd o dest_type) list_ty in
 165   let inst_t = INST_TYPE[ty, aty] in
 166   let length_empty, length_cons = inst_t LENGTH_0', inst_t LENGTH_CONS' in
 167   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
 168
 169   let rec length_conv_raw = fun list_tm ->
 170     if (is_comb list_tm) then
 171       let ltm, t_tm = dest_comb list_tm in
 172       let h_tm = rand ltm in
 173       let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in
 174       let th1' = length_conv_raw t_tm in
 175       let th1 = AP_TERM suc_const th1' in
 176       let th2 = raw_suc_conv_hash (rand(concl th1)) in
 177         TRANS (TRANS th0 th1) th2
 178     else
 179       length_empty in
 180     length_conv_raw list_tm;;
 181
 182
 183 (* Takes a term `LENGTH [...]` and returns the theorem |- LENGTH [...] = n *)
 184 let length_conv length_tm =
 185   if (fst o dest_const o rator) length_tm <> "LENGTH" then failwith "length_conv"
 186   else eval_length (rand length_tm);;
 187
 188
 189 (*
 190 let tm = `LENGTH [&1;&4;&4;&6;&7 * &8]`;;
 191 length_conv tm;;
 192 test 1000 (REWRITE_CONV[LENGTH; ARITH_SUC]) tm;; (* 0.792 *)
 193 test 1000 length_conv tm;; (* 0.076 *)
 194 *)
 195
 196
 197 (***************)
 198 (* eval_zip *)
 199
 200 let ZIP_0' = prove(`ZIP ([]:(A)list) ([]:(B)list) = []`, REWRITE_TAC[ZIP]) and
 201     ZIP_CONS' = prove(`ZIP (CONS (h1:A) t1) (CONS (h2:B) t2) = CONS (h1, h2) (ZIP t1 t2)`,
 202                       REWRITE_TAC[ZIP]);;
 203
 204 let eval_zip list1_tm list2_tm =
 205   let list1_ty = type_of list1_tm and
 206       list2_ty = type_of list2_tm in
 207   let ty1 = (hd o snd o dest_type) list1_ty and
 208       ty2 = (hd o snd o dest_type) list2_ty in
 209   let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 210   let zip0, zip_cons = inst_t ZIP_0', inst_t ZIP_CONS' in
 211   let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
 212       h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) in
 213
 214   let rec zip_conv_rec = fun list1_tm list2_tm ->
 215     if (is_comb list1_tm) then
 216       let ltm1, t1_tm = dest_comb list1_tm and
 217           ltm2, t2_tm = dest_comb list2_tm in
 218       let h1_tm, h2_tm = rand ltm1, rand ltm2 in
 219       let th0 = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var] zip_cons in
 220       let cons_tm = (rator o rand o concl) th0 in
 221       let th1' = zip_conv_rec t1_tm t2_tm in
 222       let th1 = AP_TERM cons_tm th1' in
 223         TRANS th0 th1
 224     else
 225       zip0 in
 226     zip_conv_rec list1_tm list2_tm;;
 227
 228
 229 (******************)
 230 (* ALL conversion *)
 231 (******************)
 232
 233 let ALL_0' = prove(`ALL P ([]:(A)list) <=> T`, REWRITE_TAC[ALL]) and
 234     ALL_CONS_T' = (MY_RULE o prove)(`(P h <=> T) /\ (ALL P t <=> T) ==> (ALL P (CONS (h:A) t) <=> T)`,
 235                                     REWRITE_TAC[ALL]) and
 236     ALL_CONS_F2' = (MY_RULE o prove)(`(ALL P t <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
 237                                      SIMP_TAC[ALL]) and
 238     ALL_CONS_F1' = (MY_RULE o prove)(`(P h <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
 239                                      SIMP_TAC[ALL]);;
 240
 241
 242 (* Note: p_conv should return theorems of the form |- P a b <=> T *)
 243 let all_conv_univ p_conv tm =
 244   let ltm, list_tm = dest_comb tm in
 245   let p_tm = rand ltm in
 246
 247   let list_ty = type_of list_tm and
 248       p_ty = type_of p_tm in
 249   let ty = (hd o snd o dest_type) list_ty in
 250   let inst_t = INST_TYPE[ty, aty] in
 251
 252   let all_0, all_t, all_f1, all_f2 = inst_t ALL_0', inst_t ALL_CONS_T',
 253     inst_t ALL_CONS_F1', inst_t ALL_CONS_F2' in
 254   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) and
 255       p_var = mk_var("P", p_ty) in
 256
 257   let rec all_conv_rec = fun list_tm ->
 258     if is_comb list_tm then
 259       let ltm, t_tm = dest_comb list_tm in
 260       let h_tm = rand ltm in
 261       let p_th = p_conv (mk_comb (p_tm, h_tm)) in
 262       let inst = INST[h_tm, h_var; t_tm, t_var; p_tm, p_var] in
 263         if (rand o concl) p_th = t_const then
 264           let all_th = all_conv_rec t_tm in
 265             if (rand o concl) all_th = t_const then
 266               (MY_PROVE_HYP all_th o MY_PROVE_HYP p_th o inst) all_t
 267             else
 268               (MY_PROVE_HYP all_th o inst) all_f2
 269         else
 270           (MY_PROVE_HYP p_th o inst) all_f1
 271     else
 272       INST[p_tm, p_var] all_0 in
 273     all_conv_rec list_tm;;
 274
 275
 276 (*
 277 let tm = `ALL ((<) 0) [1;3;4;2;4]`;;
 278 all_conv_univ NUM_LT_CONV tm;;
 279 let test_conv = REWRITE_CONV[ALL] THENC ONCE_DEPTH_CONV NUM_LT_CONV;;
 280 test_conv tm;;
 281 (* 0.504 *)
 282 test 1000 (all_conv_univ NUM_LT_CONV) tm;;
 283 (* 1.056 *)
 284 test 1000 test_conv test_tm;;
 285 *)
 286
 287
 288
 289 (*******************)
 290 (* ALL2 conversion *)
 291 (*******************)
 292
 293 let ALL2_0' = prove(`ALL2 P ([]:(A)list) ([]:(B)list) <=> T`, REWRITE_TAC[ALL2]) and
 294     ALL2_CONS_T' = (MY_RULE o prove)(`(P h1 h2 <=> T) /\ (ALL2 P t1 t2 <=> T) ==>
 295                                        (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> T)`,
 296                                      REWRITE_TAC[ALL2]) and
 297     ALL2_CONS_F2' = (MY_RULE o prove)(`(ALL2 P t1 t2 <=> F) ==>
 298                                         (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
 299                                       SIMP_TAC[ALL2]) and
 300     ALL2_CONS_F1' = (MY_RULE o prove)(`(P h1 h2 <=> F) ==>
 301                                         (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
 302                                       SIMP_TAC[ALL2]);;
 303
 304
 305 (* Note: p_conv should return theorems of the form |- P a b <=> T *)
 306 let all2_conv_univ p_conv tm =
 307   let ltm, list2_tm = dest_comb tm in
 308   let ltm2, list1_tm = dest_comb ltm in
 309   let p_tm = rand ltm2 in
 310
 311   let list1_ty = type_of list1_tm and
 312       list2_ty = type_of list2_tm and
 313       p_ty = type_of p_tm in
 314   let ty1 = (hd o snd o dest_type) list1_ty and
 315       ty2 = (hd o snd o dest_type) list2_ty in
 316   let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 317
 318   let all2_0, all2_t, all2_f1, all2_f2 = inst_t ALL2_0', inst_t ALL2_CONS_T',
 319     inst_t ALL2_CONS_F1', inst_t ALL2_CONS_F2' in
 320   let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
 321       h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) and
 322       p_var = mk_var("P", p_ty) in
 323
 324   let rec all2_conv_rec = fun list1_tm list2_tm ->
 325     if is_comb list1_tm then
 326       let ltm1, t1_tm = dest_comb list1_tm and
 327           ltm2, t2_tm = dest_comb list2_tm in
 328       let h1_tm, h2_tm = rand ltm1, rand ltm2 in
 329       let p_th = p_conv (mk_binop p_tm h1_tm h2_tm) in
 330       let inst = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var; p_tm, p_var] in
 331         if (rand o concl) p_th = t_const then
 332           let all2_th = all2_conv_rec t1_tm t2_tm in
 333             if (rand o concl) all2_th = t_const then
 334               (MY_PROVE_HYP all2_th o MY_PROVE_HYP p_th o inst) all2_t
 335             else
 336               (MY_PROVE_HYP all2_th o inst) all2_f2
 337         else
 338           (MY_PROVE_HYP p_th o inst) all2_f1
 339     else
 340       if is_comb list2_tm then failwith ("all2_conv_univ: l1 = []; l2 = "^string_of_term list2_tm) else
 341         INST[p_tm, p_var] all2_0 in
 342     all2_conv_rec list1_tm list2_tm;;
 343
 344
 345 (*
 346 let tm = `ALL2 (<) [1;3;4;2;4] [3;343;454;454;5]`;;
 347 all2_conv_univ NUM_LT_CONV tm;;
 348 let test_conv = REWRITE_CONV[ALL2] THENC ONCE_DEPTH_CONV NUM_LT_CONV;;
 349 test_conv tm;;
 350 (* 0.744 *)
 351 test 1000 (all2_conv_univ NUM_LT_CONV) tm;;
 352 (* 2.280 *)
 353 test 1000 test_conv test_tm;;
 354 *)
 355
 356
 357
 358 (******************************)
 359
 360 (* MEM conversions *)
 361
 362 let MEM_A_EMPTY = prove(`MEM (x:A) [] <=> F`, REWRITE_TAC[MEM]) and
 363     MEM_A_HD = MY_RULE (prove(`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
 364     MEM_A_TL = MY_RULE (prove(`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]));;
 365
 366
 367 let rec eval_mem_univ eq_conv x_tm list_tm =
 368   let ty = type_of x_tm in
 369   let inst_t = INST_TYPE[ty, aty] in
 370   let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in
 371   let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and
 372       t_var = mk_var("t", mk_type("list", [ty])) in
 373
 374   let rec mem_conv_raw list_tm =
 375     if (is_comb list_tm) then
 376       let h_tm', t_tm = dest_comb list_tm in
 377       let h_tm = rand h_tm' in
 378       let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
 379         if (rand(concl eq_th) = t_const) then
 380           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in
 381             MY_PROVE_HYP eq_th th0'
 382         else
 383           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in
 384           let th0 = MY_PROVE_HYP eq_th th0' in
 385           let th1 = mem_conv_raw t_tm in
 386             TRANS th0 th1
 387     else
 388       INST[x_tm, x_var] mem_empty in
 389
 390     mem_conv_raw list_tm;;
 391
 392
 393 let mem_conv_univ eq_conv mem_tm =
 394   let ltm, list_tm = dest_comb mem_tm in
 395   let c_tm, x_tm = dest_comb ltm in
 396     if (fst o dest_const) c_tm <> "MEM" then failwith "mem_conv_univ" else
 397       eval_mem_univ eq_conv x_tm list_tm;;
 398
 399
 400 (*
 401 let tm = `MEM 11 [1;2;3;4;5;6;4;5;6;7;3;4;4;6;8;9;10]`;;
 402 mem_conv_univ (PURE_REWRITE_CONV[ARITH_EQ]) tm;;
 403
 404 test 100 (mem_conv_univ (REWRITE_CONV[ARITH_EQ])) tm;; (* 0.176 *)
 405 test 100 (REWRITE_CONV[MEM; ARITH_EQ]) tm;; (* 0.352 *)
 406 *)
 407
 408
 409 (**********************************)
 410
 411 (* FILTER conversions *)
 412
 413 let FILTER_A_EMPTY = prove(`FILTER (P:A->bool) [] = []`, REWRITE_TAC[FILTER]) and
 414     FILTER_A_HD = (MY_RULE o prove)(`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`,
 415                                     SIMP_TAC[FILTER]) and
 416     FILTER_A_TL = (MY_RULE o prove)(`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`,
 417                                     SIMP_TAC[FILTER]);;
 418
 419
 420
 421 let filter_conv_univ p_conv tm =
 422   let ltm, list_tm = dest_comb tm in
 423   let p_tm = rand ltm in
 424   let p_ty = type_of p_tm in
 425   let ty = (hd o snd o dest_type) p_ty in
 426   let inst_t = INST_TYPE[ty, aty] in
 427   let filter_empty, filter_hd, filter_tl =
 428     inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in
 429   let p_var = mk_var("P", p_ty) in
 430   let h_var = mk_var("h", ty) in
 431   let t_var = mk_var("t", mk_type("list",[ty])) in
 432
 433   let rec filter_conv_raw = fun list_tm ->
 434     if (is_comb list_tm) then
 435       let ltm, t_tm = dest_comb list_tm in
 436       let h_tm = rand ltm in
 437       let p_th = p_conv (mk_comb(p_tm, h_tm)) in
 438         if (rand(concl p_th) = t_const) then
 439           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in
 440           let th0 = MY_PROVE_HYP p_th th0' in
 441           let ltm = rator(rand(concl th0)) in
 442           let th1 = filter_conv_raw t_tm in
 443             TRANS th0 (AP_TERM ltm th1)
 444         else
 445           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in
 446           let th0 = MY_PROVE_HYP p_th th0' in
 447           let th1 = filter_conv_raw t_tm in
 448             TRANS th0 th1
 449     else
 450       INST[p_tm, p_var] filter_empty in
 451
 452     filter_conv_raw list_tm;;
 453
 454
 455
 456
 457 (*
 458 let tm = `FILTER (\n. n = 2 \/ n = 3) [1;2;3;4;2;3;1]`;;
 459
 460 REWRITE_CONV[FILTER; ARITH_EQ] tm;;
 461 filter_conv_univ (REWRITE_CONV[ARITH_EQ]) tm;;
 462
 463 test 100 (REWRITE_CONV[FILTER; ARITH_EQ]) tm;; (* 7.596 *)
 464 test 100 (filter_conv_univ (REWRITE_CONV[ARITH_EQ])) tm;; (* 0.236 *)
 465 *)
 466
 467 (***************************)
 468
 469 (* MAP conversions *)
 470
 471
 472 let MAP_AB_EMPTY = prove(`MAP (f:A->B) [] = []`, REWRITE_TAC[MAP]) and
 473     MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
 474
 475
 476 let map_conv_univ f_conv tm =
 477   let ltm, list_tm = dest_comb tm in
 478   let ftm = rand ltm in
 479   let ftm_ty = type_of ftm in
 480   let f_var = mk_var("f", ftm_ty) in
 481   let [a_type; b_type] = snd(dest_type ftm_ty) in
 482   let h_var = mk_var("h", a_type) in
 483   let t_var = mk_var("t", mk_type("list", [a_type])) in
 484   let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in
 485   let map_empty, map_cons =
 486     inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in
 487
 488   let rec map_conv_raw list_tm =
 489     if (is_comb list_tm) then
 490       let h_tm', t_tm = dest_comb list_tm in
 491       let h_tm = rand h_tm' in
 492       let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in
 493       let ltm, rtm = dest_comb (rand(concl th0)) in
 494       let cons_tm, f_h_tm = dest_comb ltm in
 495       let f_h_th = f_conv f_h_tm in
 496       let map_t_th = map_conv_raw t_tm in
 497         TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th))
 498     else
 499       map_empty in
 500
 501     map_conv_raw list_tm;;
 502
 503
 504 (*
 505 let tm = `MAP (\x. x + 1) [1;2;3;4;5;6;7;8;9;10;11]`;;
 506
 507 REWRITE_CONV[MAP] tm;;
 508 map_conv_univ BETA_CONV tm;;
 509 map_conv_univ (BETA_CONV THENC NUM_ADD_CONV) tm;;
 510
 511 test 100 (REWRITE_CONV[MAP]) tm;; (* 0.464 *)
 512 test 100 (map_conv_univ BETA_CONV) tm;; (* 0.04 *)
 513
 514 test 100 (map_conv_univ (BETA_CONV THENC NUM_ADD_CONV)) tm;; (* 0.096 *)
 515 *)
 516
 517
 518 (*****************************************)
 519
 520 (* ALL rules *)
 521
 522
 523 let ALL_A_HD = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL])) and
 524     ALL_A_TL = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]));;
 525
 526
 527 (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *)
 528 let get_all th =
 529   let ltm, list_tm = dest_comb (concl th) in
 530   let p_tm = rand ltm in
 531   let list_ty = type_of list_tm in
 532   let p_ty = type_of p_tm in
 533   let ty = (hd o snd o dest_type) list_ty in
 534   let p_var = mk_var("P", p_ty) in
 535   let h_var = mk_var("h", ty) in
 536   let t_var = mk_var("t", list_ty) in
 537
 538   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 539   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 540
 541   let rec get_all_raw all_th list_tm =
 542     if (is_comb list_tm) then
 543       let h_tm', t_tm = dest_comb list_tm in
 544       let h_tm = rand h_tm' in
 545       let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 546       let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 547       let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 548         th_hd :: get_all_raw th_tl t_tm
 549     else
 550       [] in
 551
 552     get_all_raw th list_tm;;
 553
 554
 555
 556 (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in)
 557    where i1,...,in are given indices.
 558    The list of indices should be sorted *)
 559 let select_all th indices =
 560   let ltm, list_tm = dest_comb (concl th) in
 561   let p_tm = rand ltm in
 562   let list_ty = type_of list_tm in
 563   let p_ty = type_of p_tm in
 564   let ty = (hd o snd o dest_type) list_ty in
 565   let p_var = mk_var("P", p_ty) in
 566   let h_var = mk_var("h", ty) in
 567   let t_var = mk_var("t", list_ty) in
 568
 569   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 570   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 571
 572   let rec get_all_raw all_th list_tm indices n =
 573     match indices with
 574         [] -> []
 575       | i::is ->
 576           let h_tm', t_tm = dest_comb list_tm in
 577           let h_tm = rand h_tm' in
 578           let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 579           let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 580
 581           if (i - n = 0) then
 582             let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 583               th_hd :: get_all_raw th_tl t_tm is (n + 1)
 584           else
 585             get_all_raw th_tl t_tm (i::is) (n + 1) in
 586
 587     get_all_raw th list_tm indices 0;;
 588
 589
 590 (*
 591 let tm = `ALL (\x. x > 3) [4; 5; 8; 10; 5; 4]`;;
 592 let th = (EQT_ELIM o REWRITE_CONV[ALL; ARITH]) tm;;
 593 get_all th;;
 594 select_all th [2;3;4];;
 595
 596 (* 0.192 *)
 597 test 100 (CONJUNCTS o REWRITE_RULE[ALL]) th;;
 598 (* 0.016 *)
 599 test 100 (get_all) th;;
 600 (* 0.012 *)
 601 test 100 (select_all th) [2;3;4];;
 602 *)
 603
 604
 605 (*****************************************)
 606
 607 (* set_of_list conversions *)
 608
 609 let SET_OF_LIST_A_EMPTY = prove(`set_of_list ([]:(A)list) = {}`, REWRITE_TAC[set_of_list]) and
 610     SET_OF_LIST_A_H = prove(`set_of_list [h:A] = {h}`, REWRITE_TAC[set_of_list]) and
 611     SET_OF_LIST_A_CONS = prove(`set_of_list (CONS (h:A) t) = h INSERT set_of_list t`, REWRITE_TAC[set_of_list]);;
 612
 613
 614
 615 let set_of_list_conv tm =
 616   let list_tm = rand tm in
 617   let list_ty = type_of list_tm in
 618   let ty = (hd o snd o dest_type) list_ty in
 619   let h_var = mk_var("h", ty) in
 620   let t_var = mk_var("t", list_ty) in
 621   let inst_t = INST_TYPE[ty, aty] in
 622   let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in
 623
 624   let rec set_of_list_conv_raw = fun h_tm t_tm ->
 625     if (is_comb t_tm) then
 626       let h_tm', t_tm' = dest_comb t_tm in
 627       let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in
 628       let ltm, rtm = dest_comb(rand(concl th0)) in
 629         TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm'))
 630     else
 631       INST[h_tm, h_var] set_of_list_h in
 632
 633     if (is_comb list_tm) then
 634       let h_tm, t_tm = dest_comb list_tm in
 635         set_of_list_conv_raw (rand h_tm) t_tm
 636     else
 637       inst_t SET_OF_LIST_A_EMPTY;;
 638
 639
 640
 641 (*
 642 let tm = `set_of_list [&1; &5; &6; &3; &5; &8; &9]`;;
 643 set_of_list_conv tm;;
 644 (* 0.872 *)
 645 test 1000 (REWRITE_CONV[set_of_list]) tm;;
 646 (* 0.076 *)
 647 test 1000 set_of_list_conv tm;;
 648 *)
 649
 650
 651
 652
 653 (*************************************)
 654
 655 (* list_sum conversions *)
 656
 657 let list_sum = new_definition `list_sum list f = ITLIST (\t1 t2. f t1 + t2) list (&0)`;;
 658
 659 let LIST_SUM_A_EMPTY = prove(`list_sum [] (f:A->real) = &0`, REWRITE_TAC[list_sum; ITLIST]) and
 660     LIST_SUM_A_H = prove(`list_sum [h:A] f = f h`, REWRITE_TAC[list_sum; ITLIST; REAL_ADD_RID]) and
 661     LIST_SUM_A_CONS = prove(`list_sum (CONS (h:A) t) f = f h + list_sum t f`, REWRITE_TAC[list_sum; ITLIST]);;
 662
 663
 664 let list_sum_conv f_conv tm =
 665   let ltm, f_tm = dest_comb tm in
 666   let list_tm = rand ltm in
 667   let list_ty = type_of list_tm in
 668   let f_ty = type_of f_tm in
 669   let ty = (hd o snd o dest_type) list_ty in
 670   let f_var = mk_var("f", f_ty) and
 671       h_var = mk_var("h", ty) and
 672       t_var = mk_var("t", list_ty) in
 673   let inst_t = INST[f_tm, f_var] o INST_TYPE[ty, aty] in
 674   let list_sum_h = inst_t LIST_SUM_A_H and
 675       list_sum_cons = inst_t LIST_SUM_A_CONS in
 676
 677   let rec list_sum_conv_raw = fun h_tm t_tm ->
 678     if (is_comb t_tm) then
 679       let h_tm', t_tm' = dest_comb t_tm in
 680       let th0 = INST[h_tm, h_var; t_tm, t_var] list_sum_cons in
 681       let ltm, rtm = dest_comb(rand(concl th0)) in
 682       let plus_op, fh_tm = dest_comb ltm in
 683       let f_th = f_conv fh_tm in
 684       let th1 = list_sum_conv_raw (rand h_tm') t_tm' in
 685       let th2 = MK_COMB(AP_TERM plus_op f_th, th1) in
 686         TRANS th0 th2
 687     else
 688       let th0 = INST[h_tm, h_var] list_sum_h in
 689       let f_th = f_conv (rand(concl th0)) in
 690         TRANS th0 f_th in
 691
 692     if (is_comb list_tm) then
 693       let h_tm, t_tm = dest_comb list_tm in
 694         list_sum_conv_raw (rand h_tm) t_tm
 695     else
 696       inst_t LIST_SUM_A_EMPTY;;
 697
 698
 699
 700
 701 (*
 702 let tm = `list_sum [&1; &3; &4; pi; #0.1] cos`;;
 703
 704 list_sum_conv ALL_CONV tm;;
 705
 706 (* 2.812 *)
 707 test 1000 (REWRITE_CONV[list_sum; ITLIST; REAL_ADD_RID]) tm;;
 708 (* 0.076 *)
 709 test 1000 (list_sum_conv ALL_CONV) tm;;
 710
 711
 712 let tm = `list_sum [&1; &3; &4; pi; #0.1] (\x. cos x)`;;
 713 (* 0.104 *)
 714 test 1000 (list_sum_conv BETA_CONV) tm;;
 715 *)
 716
 717
 718