formal_ineqs/list/list_conversions.hl

   1 (* =========================================================== *)
   2 (* Efficient formal list conversions                           *)
   3 (* Author: Alexey Solovyev                                     *)
   4 (* Date: 2012-10-27                                            *)
   5 (* =========================================================== *)
   6
   7 needs "arith/nat.hl";;
   8 needs "misc/vars.hl";;
   9
  10 module type List_conversions_sig =
  11   sig
  12     val eval_hd : term -> thm
  13     val hd_conv : term -> thm
  14     val eval_el : term -> term -> thm
  15     val el_conv : term -> thm
  16     val fst_conv : term -> thm
  17     val snd_conv : term -> thm
  18     val eval_length : term -> thm
  19     val length_conv : term -> thm
  20     val eval_zip : term -> term -> thm
  21     val all_conv_univ : (term -> thm) -> term -> thm
  22     val all2_conv_univ : (term -> thm) -> term -> thm
  23     val eval_mem_univ : (term -> thm) -> term -> term -> thm
  24     val mem_conv_univ : (term -> thm) -> term -> thm
  25     val filter_conv_univ : (term -> thm) -> term -> thm
  26     val map_conv_univ : (term -> thm) -> term -> thm
  27     val get_all : thm -> thm list
  28     val select_all : thm -> int list -> thm list
  29     val set_of_list_conv : term -> thm
  30   end;;
  31
  32
  33 module List_conversions : List_conversions_sig = struct
  34
  35 open Arith_nat;;
  36 open Arith_misc;;
  37 open Misc_vars;;
  38
  39
  40 let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  41 let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  42
  43 (******************************)
  44
  45 (* HD conversions *)
  46
  47 let HD_A_CONS = prove(`HD (CONS (h:A) t) = h`, REWRITE_TAC[HD]);;
  48
  49 (* Takes a term `[a;...]` and returns the theorem |- HD [a;...] = a *)
  50 let eval_hd list_tm =
  51   let ltm, t_tm = dest_comb list_tm in
  52   let h_tm = rand ltm in
  53   let list_ty = type_of t_tm and
  54       ty = type_of h_tm in
  55   let h_var = mk_var("h", ty) and
  56       t_var = mk_var("t", list_ty) in
  57     (INST[h_tm, h_var; t_tm, t_var] o INST_TYPE[ty, aty]) HD_A_CONS;;
  58
  59 (* Takes a term `HD [a;...]` and returns the theorem |- HD [a;...] = a *)
  60 let hd_conv hd_tm =
  61   if (fst o dest_const o rator) hd_tm <> "HD" then failwith "hd_conv"
  62   else eval_hd (rand hd_tm);;
  63
  64
  65 (*********************************)
  66 (* EL conversion *)
  67
  68 let EL_0' = (MY_RULE_NUM o prove)(`EL 0 (CONS (h:A) t) = h`, REWRITE_TAC[EL; HD]);;
  69 let EL_n' = (MY_RULE_NUM o prove)(`0 < n /\ PRE n = m ==> EL n (CONS (h:A) t) = EL m t`,
  70    STRIP_TAC THEN SUBGOAL_THEN `n = SUC m` ASSUME_TAC THENL
  71      [ REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC ] THEN ASM_REWRITE_TAC[EL; TL]);;
  72
  73
  74 (* Takes a raw numeral term and a list term and returns the theorem |- EL n [...] = x *)
  75 let eval_el n_tm list_tm =
  76   let list_ty = type_of list_tm in
  77   let ty = (hd o snd o dest_type) list_ty in
  78   let inst_t = INST_TYPE[ty, aty] in
  79   let el_0, el_n = inst_t EL_0', inst_t EL_n' in
  80   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
  81
  82   let rec el_conv_raw = fun n_tm list_tm ->
  83     let h_tm, t_tm = dest_cons list_tm in
  84     let inst0 = INST[h_tm, h_var; t_tm, t_var] in
  85     if n_tm = zero_const then
  86       inst0 el_0
  87     else
  88       let n_gt0 = (EQT_ELIM o raw_gt0_hash_conv) n_tm in
  89       let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
  90       let m_tm = (rand o concl) pre_n in
  91       let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o
  92                    INST[n_tm, n_var_num; m_tm, m_var_num] o inst0) el_n in
  93       let th1 = el_conv_raw m_tm t_tm in
  94         TRANS th0 th1 in
  95     el_conv_raw n_tm list_tm;;
  96
  97
  98
  99 (* Takes a term `EL n [...]` and returns the theorem |- EL n [...] = x *)
 100 (* Note: n must be a raw numeral term Dx (Dy ... _0) *)
 101 let el_conv el_tm =
 102   let ltm, list_tm = dest_comb el_tm in
 103   let el, n_tm = dest_comb ltm in
 104   if (fst o dest_const) el <> "EL" then failwith "el_conv"
 105   else eval_el n_tm list_tm;;
 106
 107
 108
 109 (*******************************)
 110 (* FST, SND conversions *)
 111
 112 let FST' = ISPECL[`x:A`; `y:B`] FST;;
 113 let SND' = ISPECL[`x:A`; `y:B`] SND;;
 114
 115 let fst_conv tm =
 116   let x_tm, y_tm = dest_pair (rand tm) in
 117   let x_ty, y_ty = type_of x_tm, type_of y_tm in
 118   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
 119     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';;
 120
 121 let snd_conv tm =
 122   let x_tm, y_tm = dest_pair (rand tm) in
 123   let x_ty, y_ty = type_of x_tm, type_of y_tm in
 124   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
 125     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';;
 126
 127
 128
 129 (******************************)
 130 (* LENGTH conversions *)
 131
 132 let LENGTH_0' = (MY_RULE_NUM o prove) (`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and
 133     LENGTH_CONS' = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);;
 134
 135 (* Takes a term `[...]` and returns the theorem |- LENGTH [...] = n *)
 136 let eval_length list_tm =
 137   let list_ty = type_of list_tm in
 138   let ty = (hd o snd o dest_type) list_ty in
 139   let inst_t = INST_TYPE[ty, aty] in
 140   let length_empty, length_cons = inst_t LENGTH_0', inst_t LENGTH_CONS' in
 141   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
 142
 143   let rec length_conv_raw = fun list_tm ->
 144     if (is_comb list_tm) then
 145       let ltm, t_tm = dest_comb list_tm in
 146       let h_tm = rand ltm in
 147       let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in
 148       let th1' = length_conv_raw t_tm in
 149       let th1 = AP_TERM suc_op_num th1' in
 150       let th2 = raw_suc_conv_hash (rand(concl th1)) in
 151         TRANS (TRANS th0 th1) th2
 152     else
 153       length_empty in
 154     length_conv_raw list_tm;;
 155
 156
 157 (* Takes a term `LENGTH [...]` and returns the theorem |- LENGTH [...] = n *)
 158 let length_conv length_tm =
 159   if (fst o dest_const o rator) length_tm <> "LENGTH" then failwith "length_conv"
 160   else eval_length (rand length_tm);;
 161
 162
 163
 164 (************************)
 165 (* eval_zip *)
 166
 167 let ZIP_0' = prove(`ZIP ([]:(A)list) ([]:(B)list) = []`, REWRITE_TAC[ZIP]) and
 168     ZIP_CONS' = prove(`ZIP (CONS (h1:A) t1) (CONS (h2:B) t2) = CONS (h1, h2) (ZIP t1 t2)`,
 169                       REWRITE_TAC[ZIP]);;
 170
 171 let eval_zip list1_tm list2_tm =
 172   let list1_ty = type_of list1_tm and
 173       list2_ty = type_of list2_tm in
 174   let ty1 = (hd o snd o dest_type) list1_ty and
 175       ty2 = (hd o snd o dest_type) list2_ty in
 176   let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 177   let zip0, zip_cons = inst_t ZIP_0', inst_t ZIP_CONS' in
 178   let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
 179       h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) in
 180
 181   let rec zip_conv_rec = fun list1_tm list2_tm ->
 182     if (is_comb list1_tm) then
 183       let ltm1, t1_tm = dest_comb list1_tm and
 184           ltm2, t2_tm = dest_comb list2_tm in
 185       let h1_tm, h2_tm = rand ltm1, rand ltm2 in
 186       let th0 = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var] zip_cons in
 187       let cons_tm = (rator o rand o concl) th0 in
 188       let th1' = zip_conv_rec t1_tm t2_tm in
 189       let th1 = AP_TERM cons_tm th1' in
 190         TRANS th0 th1
 191     else
 192       zip0 in
 193     zip_conv_rec list1_tm list2_tm;;
 194
 195
 196 (******************)
 197 (* ALL conversion *)
 198 (******************)
 199
 200 let ALL_0' = prove(`ALL P ([]:(A)list) <=> T`, REWRITE_TAC[ALL]) and
 201     ALL_CONS_T' = (MY_RULE o prove)(`(P h <=> T) /\ (ALL P t <=> T) ==> (ALL P (CONS (h:A) t) <=> T)`,
 202                                     REWRITE_TAC[ALL]) and
 203     ALL_CONS_F2' = (MY_RULE o prove)(`(ALL P t <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
 204                                      SIMP_TAC[ALL]) and
 205     ALL_CONS_F1' = (MY_RULE o prove)(`(P h <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
 206                                      SIMP_TAC[ALL]);;
 207
 208
 209 (* Note: p_conv should return theorems of the form |- P a <=> T *)
 210 let all_conv_univ p_conv tm =
 211   let ltm, list_tm = dest_comb tm in
 212   let p_tm = rand ltm in
 213
 214   let list_ty = type_of list_tm and
 215       p_ty = type_of p_tm in
 216   let ty = (hd o snd o dest_type) list_ty in
 217   let inst_t = INST_TYPE[ty, aty] in
 218
 219   let all_0, all_t, all_f1, all_f2 = inst_t ALL_0', inst_t ALL_CONS_T',
 220     inst_t ALL_CONS_F1', inst_t ALL_CONS_F2' in
 221   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) and
 222       p_var = mk_var("P", p_ty) in
 223
 224   let rec all_conv_rec = fun list_tm ->
 225     if is_comb list_tm then
 226       let ltm, t_tm = dest_comb list_tm in
 227       let h_tm = rand ltm in
 228       let p_th = p_conv (mk_comb (p_tm, h_tm)) in
 229       let inst = INST[h_tm, h_var; t_tm, t_var; p_tm, p_var] in
 230         if (rand o concl) p_th = t_const then
 231           let all_th = all_conv_rec t_tm in
 232             if (rand o concl) all_th = t_const then
 233               (MY_PROVE_HYP all_th o MY_PROVE_HYP p_th o inst) all_t
 234             else
 235               (MY_PROVE_HYP all_th o inst) all_f2
 236         else
 237           (MY_PROVE_HYP p_th o inst) all_f1
 238     else
 239       INST[p_tm, p_var] all_0 in
 240     all_conv_rec list_tm;;
 241
 242
 243
 244 (*******************)
 245 (* ALL2 conversion *)
 246 (*******************)
 247
 248 let ALL2_0' = prove(`ALL2 P ([]:(A)list) ([]:(B)list) <=> T`, REWRITE_TAC[ALL2]) and
 249     ALL2_CONS_T' = (MY_RULE o prove)(`(P h1 h2 <=> T) /\ (ALL2 P t1 t2 <=> T) ==>
 250                                        (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> T)`,
 251                                      REWRITE_TAC[ALL2]) and
 252     ALL2_CONS_F2' = (MY_RULE o prove)(`(ALL2 P t1 t2 <=> F) ==>
 253                                         (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
 254                                       SIMP_TAC[ALL2]) and
 255     ALL2_CONS_F1' = (MY_RULE o prove)(`(P h1 h2 <=> F) ==>
 256                                         (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
 257                                       SIMP_TAC[ALL2]);;
 258
 259
 260 (* Note: p_conv should return theorems of the form |- P a b <=> T *)
 261 let all2_conv_univ p_conv tm =
 262   let ltm, list2_tm = dest_comb tm in
 263   let ltm2, list1_tm = dest_comb ltm in
 264   let p_tm = rand ltm2 in
 265
 266   let list1_ty = type_of list1_tm and
 267       list2_ty = type_of list2_tm and
 268       p_ty = type_of p_tm in
 269   let ty1 = (hd o snd o dest_type) list1_ty and
 270       ty2 = (hd o snd o dest_type) list2_ty in
 271   let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 272
 273   let all2_0, all2_t, all2_f1, all2_f2 = inst_t ALL2_0', inst_t ALL2_CONS_T',
 274     inst_t ALL2_CONS_F1', inst_t ALL2_CONS_F2' in
 275   let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
 276       h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) and
 277       p_var = mk_var("P", p_ty) in
 278
 279   let rec all2_conv_rec = fun list1_tm list2_tm ->
 280     if is_comb list1_tm then
 281       let ltm1, t1_tm = dest_comb list1_tm and
 282           ltm2, t2_tm = dest_comb list2_tm in
 283       let h1_tm, h2_tm = rand ltm1, rand ltm2 in
 284       let p_th = p_conv (mk_binop p_tm h1_tm h2_tm) in
 285       let inst = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var; p_tm, p_var] in
 286         if (rand o concl) p_th = t_const then
 287           let all2_th = all2_conv_rec t1_tm t2_tm in
 288             if (rand o concl) all2_th = t_const then
 289               (MY_PROVE_HYP all2_th o MY_PROVE_HYP p_th o inst) all2_t
 290             else
 291               (MY_PROVE_HYP all2_th o inst) all2_f2
 292         else
 293           (MY_PROVE_HYP p_th o inst) all2_f1
 294     else
 295       if is_comb list2_tm then failwith ("all2_conv_univ: l1 = []; l2 = "^string_of_term list2_tm) else
 296         INST[p_tm, p_var] all2_0 in
 297     all2_conv_rec list1_tm list2_tm;;
 298
 299
 300
 301 (******************************)
 302 (* MEM conversions *)
 303
 304 let MEM_A_EMPTY = prove(`MEM (x:A) [] <=> F`, REWRITE_TAC[MEM]) and
 305     MEM_A_HD = MY_RULE (prove(`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`,SIMP_TAC[MEM])) and
 306     MEM_A_TL = MY_RULE (prove(`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]));;
 307
 308
 309 let rec eval_mem_univ eq_conv x_tm list_tm =
 310   let ty = type_of x_tm in
 311   let inst_t = INST_TYPE[ty, aty] in
 312   let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in
 313   let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and
 314       t_var = mk_var("t", mk_type("list", [ty])) in
 315
 316   let rec mem_conv_raw list_tm =
 317     if (is_comb list_tm) then
 318       let h_tm', t_tm = dest_comb list_tm in
 319       let h_tm = rand h_tm' in
 320       let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
 321         if (rand(concl eq_th) = t_const) then
 322           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in
 323             MY_PROVE_HYP eq_th th0'
 324         else
 325           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in
 326           let th0 = MY_PROVE_HYP eq_th th0' in
 327           let th1 = mem_conv_raw t_tm in
 328             TRANS th0 th1
 329     else
 330       INST[x_tm, x_var] mem_empty in
 331
 332     mem_conv_raw list_tm;;
 333
 334
 335 let mem_conv_univ eq_conv mem_tm =
 336   let ltm, list_tm = dest_comb mem_tm in
 337   let c_tm, x_tm = dest_comb ltm in
 338     if (fst o dest_const) c_tm <> "MEM" then failwith "mem_conv_univ" else
 339       eval_mem_univ eq_conv x_tm list_tm;;
 340
 341
 342
 343 (**********************************)
 344 (* FILTER conversions *)
 345
 346 let FILTER_A_EMPTY = prove(`FILTER (P:A->bool) [] = []`, REWRITE_TAC[FILTER]) and
 347     FILTER_A_HD = (MY_RULE o prove)(`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`,
 348                                     SIMP_TAC[FILTER]) and
 349     FILTER_A_TL = (MY_RULE o prove)(`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`,
 350                                     SIMP_TAC[FILTER]);;
 351
 352
 353 let filter_conv_univ p_conv tm =
 354   let ltm, list_tm = dest_comb tm in
 355   let p_tm = rand ltm in
 356   let p_ty = type_of p_tm in
 357   let ty = (hd o snd o dest_type) p_ty in
 358   let inst_t = INST_TYPE[ty, aty] in
 359   let filter_empty, filter_hd, filter_tl =
 360     inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in
 361   let p_var = mk_var("P", p_ty) in
 362   let h_var = mk_var("h", ty) in
 363   let t_var = mk_var("t", mk_type("list",[ty])) in
 364
 365   let rec filter_conv_raw = fun list_tm ->
 366     if (is_comb list_tm) then
 367       let ltm, t_tm = dest_comb list_tm in
 368       let h_tm = rand ltm in
 369       let p_th = p_conv (mk_comb(p_tm, h_tm)) in
 370         if (rand(concl p_th) = t_const) then
 371           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in
 372           let th0 = MY_PROVE_HYP p_th th0' in
 373           let ltm = rator(rand(concl th0)) in
 374           let th1 = filter_conv_raw t_tm in
 375             TRANS th0 (AP_TERM ltm th1)
 376         else
 377           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in
 378           let th0 = MY_PROVE_HYP p_th th0' in
 379           let th1 = filter_conv_raw t_tm in
 380             TRANS th0 th1
 381     else
 382       INST[p_tm, p_var] filter_empty in
 383     filter_conv_raw list_tm;;
 384
 385
 386
 387 (***************************)
 388 (* MAP conversions *)
 389
 390 let MAP_AB_EMPTY = prove(`MAP (f:A->B) [] = []`, REWRITE_TAC[MAP]) and
 391     MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
 392
 393
 394 let map_conv_univ f_conv tm =
 395   let ltm, list_tm = dest_comb tm in
 396   let ftm = rand ltm in
 397   let ftm_ty = type_of ftm in
 398   let f_var = mk_var("f", ftm_ty) in
 399   let [a_type; b_type] = snd(dest_type ftm_ty) in
 400   let h_var = mk_var("h", a_type) in
 401   let t_var = mk_var("t", mk_type("list", [a_type])) in
 402   let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in
 403   let map_empty, map_cons =
 404     inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in
 405
 406   let rec map_conv_raw list_tm =
 407     if (is_comb list_tm) then
 408       let h_tm', t_tm = dest_comb list_tm in
 409       let h_tm = rand h_tm' in
 410       let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in
 411       let ltm, rtm = dest_comb (rand(concl th0)) in
 412       let cons_tm, f_h_tm = dest_comb ltm in
 413       let f_h_th = f_conv f_h_tm in
 414       let map_t_th = map_conv_raw t_tm in
 415         TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th))
 416     else
 417       map_empty in
 418
 419     map_conv_raw list_tm;;
 420
 421
 422 (*****************************************)
 423 (* ALL rules *)
 424
 425 let ALL_A_HD = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL])) and
 426     ALL_A_TL = UNDISCH_ALL(prove(`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]));;
 427
 428
 429 (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *)
 430 let get_all th =
 431   let ltm, list_tm = dest_comb (concl th) in
 432   let p_tm = rand ltm in
 433   let list_ty = type_of list_tm in
 434   let p_ty = type_of p_tm in
 435   let ty = (hd o snd o dest_type) list_ty in
 436   let p_var = mk_var("P", p_ty) in
 437   let h_var = mk_var("h", ty) in
 438   let t_var = mk_var("t", list_ty) in
 439
 440   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 441   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 442
 443   let rec get_all_raw all_th list_tm =
 444     if (is_comb list_tm) then
 445       let h_tm', t_tm = dest_comb list_tm in
 446       let h_tm = rand h_tm' in
 447       let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 448       let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 449       let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 450         th_hd :: get_all_raw th_tl t_tm
 451     else
 452       [] in
 453     get_all_raw th list_tm;;
 454
 455
 456
 457 (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in)
 458    where i1,...,in are given indices.
 459    The list of indices should be sorted *)
 460 let select_all th indices =
 461   let ltm, list_tm = dest_comb (concl th) in
 462   let p_tm = rand ltm in
 463   let list_ty = type_of list_tm in
 464   let p_ty = type_of p_tm in
 465   let ty = (hd o snd o dest_type) list_ty in
 466   let p_var = mk_var("P", p_ty) in
 467   let h_var = mk_var("h", ty) in
 468   let t_var = mk_var("t", list_ty) in
 469
 470   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 471   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 472
 473   let rec get_all_raw all_th list_tm indices n =
 474     match indices with
 475         [] -> []
 476       | i::is ->
 477           let h_tm', t_tm = dest_comb list_tm in
 478           let h_tm = rand h_tm' in
 479           let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 480           let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 481
 482           if (i - n = 0) then
 483             let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 484               th_hd :: get_all_raw th_tl t_tm is (n + 1)
 485           else
 486             get_all_raw th_tl t_tm (i::is) (n + 1) in
 487     get_all_raw th list_tm indices 0;;
 488
 489
 490 (*****************************************)
 491 (* set_of_list conversions *)
 492
 493 let SET_OF_LIST_A_EMPTY = prove(`set_of_list ([]:(A)list) = {}`, REWRITE_TAC[set_of_list]) and
 494     SET_OF_LIST_A_H = prove(`set_of_list [h:A] = {h}`, REWRITE_TAC[set_of_list]) and
 495     SET_OF_LIST_A_CONS = prove(`set_of_list (CONS (h:A) t) = h INSERT set_of_list t`, REWRITE_TAC[set_of_list]);;
 496
 497
 498 let set_of_list_conv tm =
 499   let list_tm = rand tm in
 500   let list_ty = type_of list_tm in
 501   let ty = (hd o snd o dest_type) list_ty in
 502   let h_var = mk_var("h", ty) in
 503   let t_var = mk_var("t", list_ty) in
 504   let inst_t = INST_TYPE[ty, aty] in
 505   let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in
 506
 507   let rec set_of_list_conv_raw = fun h_tm t_tm ->
 508     if (is_comb t_tm) then
 509       let h_tm', t_tm' = dest_comb t_tm in
 510       let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in
 511       let ltm, rtm = dest_comb(rand(concl th0)) in
 512         TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm'))
 513     else
 514       INST[h_tm, h_var] set_of_list_h in
 515
 516     if (is_comb list_tm) then
 517       let h_tm, t_tm = dest_comb list_tm in
 518         set_of_list_conv_raw (rand h_tm) t_tm
 519     else
 520       inst_t SET_OF_LIST_A_EMPTY;;
 521
 522
 523 end;;