formal_lp/hypermap/computations/list_conversions2.hl

   1 (* =========================================================== *)
   2 (* Efficient formal list conversions                           *)
   3 (* Author: Alexey Solovyev                                     *)
   4 (* Date: 2012-10-27                                            *)
   5 (* =========================================================== *)
   6
   7 needs "../formal_lp/hypermap/arith_link.hl";;
   8 needs "misc/vars.hl";;
   9 needs "Examples/seq-compiled.hl";;
  10
  11 module type List_conversions_sig =
  12   sig
  13     (* pair *)
  14     val eval_pair_eq_univ : (term -> thm) * (term -> thm) -> term -> term -> thm
  15     val pair_eq_conv_univ : (term -> thm) * (term -> thm) -> term -> thm
  16     val eval_pair_eq_num : term -> term -> thm
  17     val pair_eq_conv_num : term -> thm
  18     (* HD *)
  19     val eval_hd : term -> thm
  20     val hd_conv : term -> thm
  21       (* EL *)
  22     val eval_el : term -> term -> thm
  23     val el_conv : term -> thm
  24       (* FST, SND *)
  25     val fst_conv : term -> thm
  26     val snd_conv : term -> thm
  27       (* LENGTH *)
  28     val eval_length : term -> thm
  29     val length_conv : term -> thm
  30       (* ZIP *)
  31     val eval_zip : term -> term -> thm
  32       (* ALL *)
  33     val all_conv_univ : (term -> thm) -> term -> thm
  34       (* ALL2 *)
  35     val all2_conv_univ : (term -> thm) -> term -> thm
  36       (* MEM *)
  37     val eval_mem_univ : (term -> thm) -> term -> term -> thm
  38     val mem_conv_univ : (term -> thm) -> term -> thm
  39       (* FILTER *)
  40     val filter_conv_univ : (term -> thm) -> term -> thm
  41       (* MAP *)
  42     val map_conv_univ : (term -> thm) -> term -> thm
  43       (* ALL theorems *)
  44     val get_all : thm -> thm list
  45     val select_all : thm -> int list -> thm list
  46       (* set_of_list *)
  47     val eval_set_of_list : term -> thm
  48     val set_of_list_conv : term -> thm
  49       (* flatten *)
  50     val eval_flatten : term -> thm
  51     val flatten_conv : term -> thm
  52       (* uniq *)
  53     val eval_uniq_univ : (term -> thm) -> term -> thm
  54     val uniq_conv_univ : (term -> thm) -> term -> thm
  55       (* undup *)
  56     val eval_undup_univ : (term -> thm) -> term -> thm
  57     val undup_conv_univ : (term -> thm) -> term -> thm
  58       (* cat *)
  59     val eval_cat : term -> term -> thm
  60     val cat_conv : term -> thm
  61       (* BUTLAST, LAST *)
  62     val eval_butlast_last : term -> thm * thm
  63       (* take, drop *)
  64     val eval_take : term -> term -> thm
  65     val eval_drop : term -> term -> thm
  66     val eval_take_drop : term -> term -> thm * thm
  67       (* rot *)
  68     val eval_rot : term -> term -> thm
  69     val eval_rot1 : term -> thm
  70     val eval_rotr1 : term -> thm
  71       (* index *)
  72     val eval_index_univ : (term -> thm) -> term -> term -> thm
  73     val index_conv_univ : (term -> thm) -> term -> thm
  74   end;;
  75
  76
  77 module List_conversions : List_conversions_sig = struct
  78
  79 open Arith_nat;;
  80 open Arith_misc;;
  81 open Misc_vars;;
  82 open Seq;;
  83
  84
  85 let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  86 let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
  87 let TO_NUM = REWRITE_RULE[Arith_hash.NUM_THM] o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
  88 let to_num = rand o concl o TO_NUM;;
  89
  90
  91
  92 (***********************************************)
  93 (* pair_eq_conv *)
  94
  95 let PAIR_EQ_TT = (MY_RULE o prove)(`(n = x <=> T) /\ (m = y <=> T) ==> (n:A,m:B = x,y <=> T)`, SIMP_TAC[PAIR_EQ]) and
  96     PAIR_NEQ_FST = (MY_RULE o prove)(`(n = x <=> F) ==> (n:A,m:B = x,y <=> F)`, SIMP_TAC[PAIR_EQ]) and
  97     PAIR_NEQ_SND = (MY_RULE o prove)(`(m = y <=> F) ==> (n:A,m:B = x,y <=> F)`, SIMP_TAC[PAIR_EQ]);;
  98
  99
 100 let eval_pair_eq_univ (eq1_f, eq2_f) p1_tm p2_tm =
 101   if (p1_tm = p2_tm) then
 102     EQT_INTRO (REFL p1_tm)
 103   else
 104     let n_tm, m_tm = dest_pair p1_tm in
 105     let x_tm, y_tm = dest_pair p2_tm in
 106     let ty1 = type_of n_tm and
 107         ty2 = type_of m_tm in
 108     let n_var, m_var = mk_var("n", ty1), mk_var("m", ty2) and
 109         x_var, y_var = mk_var("x", ty1), mk_var("y", ty2) in
 110     let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 111     let inst = INST[n_tm, n_var; m_tm, m_var; x_tm, x_var; y_tm, y_var] in
 112     let fst_th = eq1_f (mk_eq (n_tm, x_tm)) in
 113       if (rand(concl fst_th) = f_const) then
 114         MY_PROVE_HYP fst_th ((inst o inst_t) PAIR_NEQ_FST)
 115       else
 116         let snd_th = eq2_f (mk_eq (m_tm, y_tm)) in
 117           if (rand(concl snd_th) = f_const) then
 118             MY_PROVE_HYP snd_th ((inst o inst_t) PAIR_NEQ_SND)
 119           else
 120             let th0 = (inst o inst_t) PAIR_EQ_TT in
 121               MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0);;
 122
 123
 124 let pair_eq_conv_univ (eq1_f, eq2_f) eq_tm =
 125   let lhs, rhs = dest_eq eq_tm in
 126     eval_pair_eq_univ (eq1_f, eq2_f) lhs rhs;;
 127
 128
 129 let eval_pair_eq_num =
 130   let inst_t = INST_TYPE[num_type, aty; num_type, bty] in
 131   let pair_eq, pair_neq_fst, pair_neq_snd =
 132     inst_t PAIR_EQ_TT, inst_t PAIR_NEQ_FST, inst_t PAIR_NEQ_SND in
 133     fun p1_tm p2_tm ->
 134       if (p1_tm = p2_tm) then
 135         EQT_INTRO (REFL p1_tm)
 136       else
 137         let n_tm, m_tm = dest_pair p1_tm in
 138         let x_tm, y_tm = dest_pair p2_tm in
 139         let inst = INST[n_tm, n_var_num; m_tm, m_var_num; x_tm, x_var_num; y_tm, y_var_num] in
 140         let fst_th = raw_eq_hash_conv (mk_eq (n_tm, x_tm)) in
 141           if (rand(concl fst_th) = f_const) then
 142             MY_PROVE_HYP fst_th (inst pair_neq_fst)
 143           else
 144             let snd_th = raw_eq_hash_conv (mk_eq (m_tm, y_tm)) in
 145               if (rand(concl snd_th) = f_const) then
 146                 MY_PROVE_HYP snd_th (inst pair_neq_snd)
 147               else
 148                 let th0 = inst pair_eq in
 149                   MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0);;
 150
 151
 152 let pair_eq_conv_num eq_tm =
 153   let lhs, rhs = dest_eq eq_tm in
 154     eval_pair_eq_num lhs rhs;;
 155
 156
 157
 158 (******************************)
 159
 160 (* HD conversions *)
 161
 162 let HD_A_CONS = prove(`HD (CONS (h:A) t) = h`, REWRITE_TAC[HD]);;
 163
 164 (* Takes a term `[a;...]` and returns the theorem |- HD [a;...] = a *)
 165 let eval_hd list_tm =
 166   let ltm, t_tm = dest_comb list_tm in
 167   let h_tm = rand ltm in
 168   let list_ty = type_of t_tm and
 169       ty = type_of h_tm in
 170   let h_var = mk_var("h", ty) and
 171       t_var = mk_var("t", list_ty) in
 172     (INST[h_tm, h_var; t_tm, t_var] o INST_TYPE[ty, aty]) HD_A_CONS;;
 173
 174 (* Takes a term `HD [a;...]` and returns the theorem |- HD [a;...] = a *)
 175 let hd_conv hd_tm =
 176   if (fst o dest_const o rator) hd_tm <> "HD" then failwith "hd_conv"
 177   else eval_hd (rand hd_tm);;
 178
 179
 180
 181 (*********************************)
 182 (* EL conversion *)
 183
 184 let EL_0' = (MY_RULE_NUM o prove)(`EL 0 (CONS (h:A) t) = h`, REWRITE_TAC[EL; HD]);;
 185 let EL_n' = (MY_RULE_NUM o prove)(`0 < n /\ PRE n = m ==> EL n (CONS (h:A) t) = EL m t`,
 186    STRIP_TAC THEN SUBGOAL_THEN `n = SUC m` ASSUME_TAC THENL
 187      [ REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC ] THEN ASM_REWRITE_TAC[EL; TL]);;
 188
 189
 190 (* Takes a raw numeral term and a list term and returns the theorem |- EL n [...] = x *)
 191 let eval_el n_tm list_tm =
 192   let list_ty = type_of list_tm in
 193   let ty = (hd o snd o dest_type) list_ty in
 194   let inst_t = INST_TYPE[ty, aty] in
 195   let el_0, el_n = inst_t EL_0', inst_t EL_n' in
 196   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
 197
 198   let rec el_conv_raw = fun n_tm list_tm ->
 199     let h_tm, t_tm = dest_cons list_tm in
 200     let inst0 = INST[h_tm, h_var; t_tm, t_var] in
 201     if n_tm = zero_const then
 202       inst0 el_0
 203     else
 204       let n_gt0 = (EQT_ELIM o raw_gt0_hash_conv) n_tm in
 205       let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
 206       let m_tm = (rand o concl) pre_n in
 207       let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o
 208                    INST[n_tm, n_var_num; m_tm, m_var_num] o inst0) el_n in
 209       let th1 = el_conv_raw m_tm t_tm in
 210         TRANS th0 th1 in
 211     el_conv_raw n_tm list_tm;;
 212
 213
 214
 215 (* Takes a term `EL n [...]` and returns the theorem |- EL n [...] = x *)
 216 (* Note: n must be a raw numeral term Dx (Dy ... _0) *)
 217 let el_conv el_tm =
 218   let ltm, list_tm = dest_comb el_tm in
 219   let el, n_tm = dest_comb ltm in
 220   if (fst o dest_const) el <> "EL" then failwith "el_conv"
 221   else eval_el n_tm list_tm;;
 222
 223
 224
 225 (*******************************)
 226 (* FST, SND conversions *)
 227
 228 let FST' = ISPECL[`x:A`; `y:B`] FST;;
 229 let SND' = ISPECL[`x:A`; `y:B`] SND;;
 230
 231 let fst_conv tm =
 232   let x_tm, y_tm = dest_pair (rand tm) in
 233   let x_ty, y_ty = type_of x_tm, type_of y_tm in
 234   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
 235     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';;
 236
 237 let snd_conv tm =
 238   let x_tm, y_tm = dest_pair (rand tm) in
 239   let x_ty, y_ty = type_of x_tm, type_of y_tm in
 240   let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in
 241     (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';;
 242
 243
 244
 245 (******************************)
 246 (* LENGTH conversions *)
 247
 248 let LENGTH_0' = (MY_RULE_NUM o prove) (`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and
 249     LENGTH_CONS' = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);;
 250
 251 (* Takes a term `[...]` and returns the theorem |- LENGTH [...] = n *)
 252 let eval_length list_tm =
 253   let list_ty = type_of list_tm in
 254   let ty = (hd o snd o dest_type) list_ty in
 255   let inst_t = INST_TYPE[ty, aty] in
 256   let length_empty, length_cons = inst_t LENGTH_0', inst_t LENGTH_CONS' in
 257   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in
 258
 259   let rec length_conv_raw = fun list_tm ->
 260     if (is_comb list_tm) then
 261       let ltm, t_tm = dest_comb list_tm in
 262       let h_tm = rand ltm in
 263       let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in
 264       let th1' = length_conv_raw t_tm in
 265       let th1 = AP_TERM suc_op_num th1' in
 266       let th2 = raw_suc_conv_hash (rand(concl th1)) in
 267         TRANS (TRANS th0 th1) th2
 268     else
 269       length_empty in
 270     length_conv_raw list_tm;;
 271
 272
 273 (* Takes a term `LENGTH [...]` and returns the theorem |- LENGTH [...] = n *)
 274 let length_conv length_tm =
 275   if (fst o dest_const o rator) length_tm <> "LENGTH" then failwith "length_conv"
 276   else eval_length (rand length_tm);;
 277
 278
 279
 280
 281 (************************)
 282 (* eval_zip *)
 283
 284 let ZIP_0' = prove(`ZIP ([]:(A)list) ([]:(B)list) = []`, REWRITE_TAC[ZIP]) and
 285     ZIP_CONS' = prove(`ZIP (CONS (h1:A) t1) (CONS (h2:B) t2) = CONS (h1, h2) (ZIP t1 t2)`,
 286                       REWRITE_TAC[ZIP]);;
 287
 288 let eval_zip list1_tm list2_tm =
 289   let list1_ty = type_of list1_tm and
 290       list2_ty = type_of list2_tm in
 291   let ty1 = (hd o snd o dest_type) list1_ty and
 292       ty2 = (hd o snd o dest_type) list2_ty in
 293   let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 294   let zip0, zip_cons = inst_t ZIP_0', inst_t ZIP_CONS' in
 295   let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
 296       h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) in
 297
 298   let rec zip_conv_rec = fun list1_tm list2_tm ->
 299     if (is_comb list1_tm) then
 300       let ltm1, t1_tm = dest_comb list1_tm and
 301           ltm2, t2_tm = dest_comb list2_tm in
 302       let h1_tm, h2_tm = rand ltm1, rand ltm2 in
 303       let th0 = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var] zip_cons in
 304       let cons_tm = (rator o rand o concl) th0 in
 305       let th1' = zip_conv_rec t1_tm t2_tm in
 306       let th1 = AP_TERM cons_tm th1' in
 307         TRANS th0 th1
 308     else
 309       zip0 in
 310     zip_conv_rec list1_tm list2_tm;;
 311
 312
 313 (******************)
 314 (* ALL conversion *)
 315 (******************)
 316
 317 let ALL_0' = prove(`ALL P ([]:(A)list) <=> T`, REWRITE_TAC[ALL]) and
 318     ALL_CONS_T' = (MY_RULE o prove)(`(P h <=> T) /\ (ALL P t <=> T) ==> (ALL P (CONS (h:A) t) <=> T)`,
 319                                     REWRITE_TAC[ALL]) and
 320     ALL_CONS_F2' = (MY_RULE o prove)(`(ALL P t <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
 321                                      SIMP_TAC[ALL]) and
 322     ALL_CONS_F1' = (MY_RULE o prove)(`(P h <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`,
 323                                      SIMP_TAC[ALL]);;
 324
 325
 326 (* Note: p_conv should return theorems of the form |- P a <=> T *)
 327 let all_conv_univ p_conv tm =
 328   let ltm, list_tm = dest_comb tm in
 329   let p_tm = rand ltm in
 330
 331   let list_ty = type_of list_tm and
 332       p_ty = type_of p_tm in
 333   let ty = (hd o snd o dest_type) list_ty in
 334   let inst_t = INST_TYPE[ty, aty] in
 335
 336   let all_0, all_t, all_f1, all_f2 = inst_t ALL_0', inst_t ALL_CONS_T',
 337     inst_t ALL_CONS_F1', inst_t ALL_CONS_F2' in
 338   let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) and
 339       p_var = mk_var("P", p_ty) in
 340
 341   let rec all_conv_rec = fun list_tm ->
 342     if is_comb list_tm then
 343       let ltm, t_tm = dest_comb list_tm in
 344       let h_tm = rand ltm in
 345       let p_th = p_conv (mk_comb (p_tm, h_tm)) in
 346       let inst = INST[h_tm, h_var; t_tm, t_var; p_tm, p_var] in
 347         if (rand o concl) p_th = t_const then
 348           let all_th = all_conv_rec t_tm in
 349             if (rand o concl) all_th = t_const then
 350               (MY_PROVE_HYP all_th o MY_PROVE_HYP p_th o inst) all_t
 351             else
 352               (MY_PROVE_HYP all_th o inst) all_f2
 353         else
 354           (MY_PROVE_HYP p_th o inst) all_f1
 355     else
 356       INST[p_tm, p_var] all_0 in
 357     all_conv_rec list_tm;;
 358
 359
 360
 361 (*******************)
 362 (* ALL2 conversion *)
 363 (*******************)
 364
 365 let ALL2_0' = prove(`ALL2 P ([]:(A)list) ([]:(B)list) <=> T`, REWRITE_TAC[ALL2]) and
 366     ALL2_CONS_T' = (MY_RULE o prove)(`(P h1 h2 <=> T) /\ (ALL2 P t1 t2 <=> T) ==>
 367                                        (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> T)`,
 368                                      REWRITE_TAC[ALL2]) and
 369     ALL2_CONS_F2' = (MY_RULE o prove)(`(ALL2 P t1 t2 <=> F) ==>
 370                                         (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
 371                                       SIMP_TAC[ALL2]) and
 372     ALL2_CONS_F1' = (MY_RULE o prove)(`(P h1 h2 <=> F) ==>
 373                                         (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`,
 374                                       SIMP_TAC[ALL2]);;
 375
 376
 377 (* Note: p_conv should return theorems of the form |- P a b <=> T *)
 378 let all2_conv_univ p_conv tm =
 379   let ltm, list2_tm = dest_comb tm in
 380   let ltm2, list1_tm = dest_comb ltm in
 381   let p_tm = rand ltm2 in
 382
 383   let list1_ty = type_of list1_tm and
 384       list2_ty = type_of list2_tm and
 385       p_ty = type_of p_tm in
 386   let ty1 = (hd o snd o dest_type) list1_ty and
 387       ty2 = (hd o snd o dest_type) list2_ty in
 388   let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
 389
 390   let all2_0, all2_t, all2_f1, all2_f2 = inst_t ALL2_0', inst_t ALL2_CONS_T',
 391     inst_t ALL2_CONS_F1', inst_t ALL2_CONS_F2' in
 392   let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and
 393       h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) and
 394       p_var = mk_var("P", p_ty) in
 395
 396   let rec all2_conv_rec = fun list1_tm list2_tm ->
 397     if is_comb list1_tm then
 398       let ltm1, t1_tm = dest_comb list1_tm and
 399           ltm2, t2_tm = dest_comb list2_tm in
 400       let h1_tm, h2_tm = rand ltm1, rand ltm2 in
 401       let p_th = p_conv (mk_binop p_tm h1_tm h2_tm) in
 402       let inst = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var; p_tm, p_var] in
 403         if (rand o concl) p_th = t_const then
 404           let all2_th = all2_conv_rec t1_tm t2_tm in
 405             if (rand o concl) all2_th = t_const then
 406               (MY_PROVE_HYP all2_th o MY_PROVE_HYP p_th o inst) all2_t
 407             else
 408               (MY_PROVE_HYP all2_th o inst) all2_f2
 409         else
 410           (MY_PROVE_HYP p_th o inst) all2_f1
 411     else
 412       if is_comb list2_tm then failwith ("all2_conv_univ: l1 = []; l2 = "^string_of_term list2_tm) else
 413         INST[p_tm, p_var] all2_0 in
 414     all2_conv_rec list1_tm list2_tm;;
 415
 416
 417
 418 (******************************)
 419 (* MEM conversions *)
 420
 421 let MEM_A_EMPTY = prove(`MEM (x:A) [] <=> F`, REWRITE_TAC[MEM]) and
 422     MEM_A_HD = (MY_RULE o prove) (`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`, SIMP_TAC[MEM]) and
 423     MEM_A_TL = (MY_RULE o prove) (`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]);;
 424
 425
 426 let rec eval_mem_univ eq_conv x_tm list_tm =
 427   let ty = type_of x_tm in
 428   let inst_t = INST_TYPE[ty, aty] in
 429   let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in
 430   let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and
 431       t_var = mk_var("t", mk_type("list", [ty])) in
 432
 433   let rec mem_conv_raw list_tm =
 434     if (is_comb list_tm) then
 435       let h_tm', t_tm = dest_comb list_tm in
 436       let h_tm = rand h_tm' in
 437       let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
 438         if (rand(concl eq_th) = t_const) then
 439           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in
 440             MY_PROVE_HYP eq_th th0'
 441         else
 442           let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in
 443           let th0 = MY_PROVE_HYP eq_th th0' in
 444           let th1 = mem_conv_raw t_tm in
 445             TRANS th0 th1
 446     else
 447       INST[x_tm, x_var] mem_empty in
 448
 449     mem_conv_raw list_tm;;
 450
 451
 452 let mem_conv_univ eq_conv mem_tm =
 453   let ltm, list_tm = dest_comb mem_tm in
 454   let c_tm, x_tm = dest_comb ltm in
 455     if (fst o dest_const) c_tm <> "MEM" then failwith "mem_conv_univ" else
 456       eval_mem_univ eq_conv x_tm list_tm;;
 457
 458
 459
 460 (**********************************)
 461 (* FILTER conversions *)
 462
 463 let FILTER_A_EMPTY = prove(`FILTER (P:A->bool) [] = []`, REWRITE_TAC[FILTER]) and
 464     FILTER_A_HD = (MY_RULE o prove) (`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`,
 465                                     SIMP_TAC[FILTER]) and
 466     FILTER_A_TL = (MY_RULE o prove) (`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`,
 467                                     SIMP_TAC[FILTER]);;
 468
 469
 470 let filter_conv_univ p_conv tm =
 471   let ltm, list_tm = dest_comb tm in
 472   let p_tm = rand ltm in
 473   let p_ty = type_of p_tm in
 474   let ty = (hd o snd o dest_type) p_ty in
 475   let inst_t = INST_TYPE[ty, aty] in
 476   let filter_empty, filter_hd, filter_tl =
 477     inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in
 478   let p_var = mk_var("P", p_ty) in
 479   let h_var = mk_var("h", ty) in
 480   let t_var = mk_var("t", mk_type("list",[ty])) in
 481
 482   let rec filter_conv_raw = fun list_tm ->
 483     if (is_comb list_tm) then
 484       let ltm, t_tm = dest_comb list_tm in
 485       let h_tm = rand ltm in
 486       let p_th = p_conv (mk_comb(p_tm, h_tm)) in
 487         if (rand(concl p_th) = t_const) then
 488           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in
 489           let th0 = MY_PROVE_HYP p_th th0' in
 490           let ltm = rator(rand(concl th0)) in
 491           let th1 = filter_conv_raw t_tm in
 492             TRANS th0 (AP_TERM ltm th1)
 493         else
 494           let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in
 495           let th0 = MY_PROVE_HYP p_th th0' in
 496           let th1 = filter_conv_raw t_tm in
 497             TRANS th0 th1
 498     else
 499       INST[p_tm, p_var] filter_empty in
 500     filter_conv_raw list_tm;;
 501
 502
 503 (***************************)
 504 (* MAP conversions *)
 505
 506 let MAP_AB_EMPTY = prove(`MAP (f:A->B) [] = []`, REWRITE_TAC[MAP]) and
 507     MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
 508
 509
 510 let map_conv_univ f_conv tm =
 511   let ltm, list_tm = dest_comb tm in
 512   let ftm = rand ltm in
 513   let ftm_ty = type_of ftm in
 514   let f_var = mk_var("f", ftm_ty) in
 515   let [a_type; b_type] = snd(dest_type ftm_ty) in
 516   let h_var = mk_var("h", a_type) in
 517   let t_var = mk_var("t", mk_type("list", [a_type])) in
 518   let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in
 519   let map_empty, map_cons =
 520     inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in
 521
 522   let rec map_conv_raw list_tm =
 523     if (is_comb list_tm) then
 524       let h_tm', t_tm = dest_comb list_tm in
 525       let h_tm = rand h_tm' in
 526       let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in
 527       let ltm, rtm = dest_comb (rand(concl th0)) in
 528       let cons_tm, f_h_tm = dest_comb ltm in
 529       let f_h_th = f_conv f_h_tm in
 530       let map_t_th = map_conv_raw t_tm in
 531         TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th))
 532     else
 533       map_empty in
 534
 535     map_conv_raw list_tm;;
 536
 537
 538 (*****************************************)
 539 (* ALL rules *)
 540
 541 let ALL_A_HD = (MY_RULE o prove) (`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL]) and
 542     ALL_A_TL = (MY_RULE o prove) (`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]);;
 543
 544
 545 (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *)
 546 let get_all th =
 547   let ltm, list_tm = dest_comb (concl th) in
 548   let p_tm = rand ltm in
 549   let list_ty = type_of list_tm in
 550   let p_ty = type_of p_tm in
 551   let ty = (hd o snd o dest_type) list_ty in
 552   let p_var = mk_var("P", p_ty) in
 553   let h_var = mk_var("h", ty) in
 554   let t_var = mk_var("t", list_ty) in
 555
 556   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 557   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 558
 559   let rec get_all_raw all_th list_tm =
 560     if (is_comb list_tm) then
 561       let h_tm', t_tm = dest_comb list_tm in
 562       let h_tm = rand h_tm' in
 563       let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 564       let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 565       let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 566         th_hd :: get_all_raw th_tl t_tm
 567     else
 568       [] in
 569     get_all_raw th list_tm;;
 570
 571
 572
 573 (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in)
 574    where i1,...,in are given indices.
 575    The list of indices should be sorted *)
 576 let select_all th indices =
 577   let ltm, list_tm = dest_comb (concl th) in
 578   let p_tm = rand ltm in
 579   let list_ty = type_of list_tm in
 580   let p_ty = type_of p_tm in
 581   let ty = (hd o snd o dest_type) list_ty in
 582   let p_var = mk_var("P", p_ty) in
 583   let h_var = mk_var("h", ty) in
 584   let t_var = mk_var("t", list_ty) in
 585
 586   let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in
 587   let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in
 588
 589   let rec get_all_raw all_th list_tm indices n =
 590     match indices with
 591         [] -> []
 592       | i::is ->
 593           let h_tm', t_tm = dest_comb list_tm in
 594           let h_tm = rand h_tm' in
 595           let inst_t = INST[h_tm, h_var; t_tm, t_var] in
 596           let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in
 597
 598           if (i - n = 0) then
 599             let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in
 600               th_hd :: get_all_raw th_tl t_tm is (n + 1)
 601           else
 602             get_all_raw th_tl t_tm (i::is) (n + 1) in
 603     get_all_raw th list_tm indices 0;;
 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 let eval_set_of_list list_tm =
 615   let list_ty = type_of list_tm in
 616   let ty = (hd o snd o dest_type) list_ty in
 617   let h_var = mk_var("h", ty) in
 618   let t_var = mk_var("t", list_ty) in
 619   let inst_t = INST_TYPE[ty, aty] in
 620   let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in
 621
 622   let rec set_of_list_conv_raw = fun h_tm t_tm ->
 623     if (is_comb t_tm) then
 624       let h_tm', t_tm' = dest_comb t_tm in
 625       let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in
 626       let ltm, rtm = dest_comb(rand(concl th0)) in
 627         TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm'))
 628     else
 629       INST[h_tm, h_var] set_of_list_h in
 630
 631     if (is_comb list_tm) then
 632       let h_tm, t_tm = dest_comb list_tm in
 633         set_of_list_conv_raw (rand h_tm) t_tm
 634     else
 635       inst_t SET_OF_LIST_A_EMPTY;;
 636
 637 let set_of_list_conv tm =
 638   if (fst o dest_const o rator) tm <> "set_of_list" then failwith "set_of_list_conv"
 639   else eval_set_of_list (rand tm);;
 640
 641
 642 (*****************************************)
 643 (* flatten conversions *)
 644
 645 let flatten_empty = prove(`flatten ([]:((A)list)list) = []`, REWRITE_TAC[flatten; foldr; cat]) and
 646     flatten_cons_empty = prove(`flatten (CONS ([]:(A)list) tt) = flatten tt`, REWRITE_TAC[flatten; foldr; cat]) and
 647     flatten_cons_cons = prove(`flatten (CONS (CONS (h:A) t) tt) = CONS h (flatten (CONS t tt))`, REWRITE_TAC[flatten; foldr; cat]);;
 648
 649
 650 (* Works for any list of lists *)
 651 let eval_flatten list_list_tm =
 652   let list_list_ty = type_of list_list_tm in
 653   let list_ty = (hd o snd o dest_type) list_list_ty in
 654   let ty = (hd o snd o dest_type) list_ty in
 655   let inst_t = INST_TYPE[ty, aty] in
 656   let flatten_empty, flatten_cons_empty, flatten_cons_cons =
 657     inst_t flatten_empty, inst_t flatten_cons_empty, inst_t flatten_cons_cons in
 658   let tt_var = mk_var("tt", list_list_ty) in
 659   let t_var = mk_var("t", list_ty) in
 660   let h_var = mk_var("h", ty) in
 661
 662   let rec flatten_conv_raw list_list_tm =
 663     if (is_comb list_list_tm) then
 664       let hh_tm', tt_tm = dest_comb list_list_tm in
 665       let hh_tm = rand hh_tm' in
 666         if (is_comb hh_tm) then
 667           let h_tm', t_tm = dest_comb hh_tm in
 668           let h_tm = rand h_tm' in
 669           let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] flatten_cons_cons in
 670           let ltm, rtm = dest_comb(rand(concl th0)) in
 671           let th1 = AP_TERM ltm (flatten_conv_raw (rand rtm)) in
 672             TRANS th0 th1
 673         else
 674           let th0 = INST[tt_tm, tt_var] flatten_cons_empty in
 675           let th1 = flatten_conv_raw tt_tm in
 676             TRANS th0 th1
 677     else
 678       flatten_empty in
 679
 680     flatten_conv_raw list_list_tm;;
 681
 682
 683 let flatten_conv flatten_tm =
 684   if (fst o dest_const o rator) flatten_tm <> "flatten" then failwith "flatten_conv"
 685   else eval_flatten (rand flatten_tm);;
 686
 687
 688 (********************************)
 689 (* uniq conversion *)
 690
 691 let uniq_empty = prove(`uniq ([]:(A)list) <=> T`, REWRITE_TAC[uniq]) and
 692     uniq_cons_F = (MY_RULE o prove) (`(MEM (h:A) t <=> F) ==> (uniq (CONS h t) <=> uniq t)`, SIMP_TAC[uniq]) and
 693     uniq_cons_T = (MY_RULE o prove) (`(MEM (h:A) t <=> T) ==> (uniq (CONS h t) <=> F)`, SIMP_TAC[uniq]);;
 694
 695
 696 let eval_uniq_univ eq_conv list_tm =
 697   let list_ty = type_of list_tm in
 698   let ty = (hd o snd o dest_type) list_ty in
 699   let h_var = mk_var("h", ty) in
 700   let t_var = mk_var("t", list_ty) in
 701   let inst_t = INST_TYPE[ty, aty] in
 702   let uniq_empty, uniq_cons_F, uniq_cons_T =
 703     inst_t uniq_empty, inst_t uniq_cons_F, inst_t uniq_cons_T in
 704   let rec uniq_rec list_tm =
 705     if (is_comb list_tm) then
 706       let h_tm', t_tm = dest_comb list_tm in
 707       let h_tm = rand h_tm' in
 708       let inst = INST[h_tm, h_var; t_tm, t_var] in
 709       let mem_th = eval_mem_univ eq_conv h_tm t_tm in
 710         if (rand (concl mem_th) = t_const) then
 711           MY_PROVE_HYP mem_th (inst uniq_cons_T)
 712         else
 713           let th0 = MY_PROVE_HYP mem_th (inst uniq_cons_F) in
 714           let th1 = uniq_rec t_tm in
 715             TRANS th0 th1
 716                 else
 717                   uniq_empty in
 718     uniq_rec list_tm;;
 719
 720
 721 let uniq_conv_univ eq_conv tm =
 722   if (fst o dest_const o rator) tm <> "uniq" then failwith "uniq_conv"
 723   else eval_uniq_univ eq_conv (rand tm);;
 724
 725
 726 (**********************************)
 727 (* undup conversion *)
 728
 729 let undup_empty = prove(`undup ([]:(num)list) = []`, REWRITE_TAC[undup]) and
 730     undup_mem_T = (MY_RULE o prove) (`(MEM (h:A) t <=> T) ==> undup (CONS h t) = undup t`, SIMP_TAC[undup]) and
 731     undup_mem_F = (MY_RULE o prove) (`(MEM (h:A) t <=> F) ==> undup (CONS h t) = CONS h (undup t)`, SIMP_TAC[undup]);;
 732
 733
 734 let eval_undup_univ eq_conv list_tm =
 735   let list_ty = type_of list_tm in
 736   let ty = (hd o snd o dest_type) list_ty in
 737   let h_var = mk_var("h", ty) in
 738   let t_var = mk_var("t", list_ty) in
 739   let inst_t = INST_TYPE[ty, aty] in
 740   let empty, mem_T, mem_F =
 741     inst_t undup_empty, inst_t undup_mem_T, inst_t undup_mem_F in
 742
 743   let rec undup_rec list_tm =
 744     if (is_comb list_tm) then
 745       let h_tm', t_tm = dest_comb list_tm in
 746       let h_tm = rand h_tm' in
 747       let inst = INST[h_tm, h_var; t_tm, t_var] in
 748       let mem_th = eval_mem_univ eq_conv h_tm t_tm in
 749         if (rand(concl mem_th) = t_const) then
 750           let th0 = MY_PROVE_HYP mem_th (inst mem_T) in
 751           let th1 = undup_rec t_tm in
 752             TRANS th0 th1
 753         else
 754           let th0 = MY_PROVE_HYP mem_th (inst mem_F) in
 755           let ltm, rtm = dest_comb (rand(concl th0)) in
 756           let th1 = undup_rec (rand rtm) in
 757             TRANS th0 (AP_TERM ltm th1)
 758     else
 759       empty in
 760
 761     undup_rec list_tm;;
 762
 763
 764 let undup_conv_univ eq_conv tm =
 765   if (fst o dest_const o rator) tm <> "undup" then failwith "undup_conv"
 766   else eval_undup_univ eq_conv (rand tm);;
 767
 768
 769 (**********************************)
 770 (* cat conversion *)
 771
 772 let cat_empty' = prove(`cat [] (s:(A)list) = s`, REWRITE_TAC[cat]) and
 773     cat_cons' = prove(`cat (CONS (h:A) t) s = CONS h (cat t s)`, REWRITE_TAC[cat]);;
 774
 775
 776 let eval_cat list1_tm list2_tm =
 777   let list_ty = type_of list1_tm in
 778   let ty = (hd o snd o dest_type) list_ty in
 779   let h_var = mk_var("h", ty) and
 780       t_var = mk_var("t", list_ty) and
 781       s_var = mk_var("s", list_ty) in
 782   let inst_t = INST_TYPE[ty, aty] in
 783   let empty, cons = inst_t cat_empty', inst_t cat_cons' in
 784   let rec cat_rec list_tm =
 785     if (is_comb list_tm) then
 786       let h_tm', t_tm = dest_comb list_tm in
 787       let h_tm = rand h_tm' in
 788       let inst = INST[h_tm, h_var; t_tm, t_var; list2_tm, s_var] in
 789       let th0 = inst cons in
 790       let ltm = rator (rand (concl th0)) in
 791       let th1 = cat_rec t_tm in
 792         TRANS th0 (AP_TERM ltm th1)
 793     else
 794       INST[list2_tm, s_var] empty in
 795
 796     cat_rec list1_tm;;
 797
 798
 799 let cat_conv tm =
 800   let ltm, list2_tm = dest_comb tm in
 801   let cat, list1_tm = dest_comb ltm in
 802     if (fst o dest_const) cat <> "cat" then failwith "cat_conv"
 803     else eval_cat list1_tm list2_tm;;
 804
 805
 806 (**********************************)
 807 (* BUTLAST and LAST conversions *)
 808
 809 let last1' = prove(`LAST [h:A] = h`, REWRITE_TAC[LAST]) and
 810     last_cons2' = prove(`LAST (CONS (h:A) (CONS h2 s)) = LAST (CONS h2 s)`, REWRITE_TAC[LAST; NOT_CONS_NIL]) and
 811     butlast1' = prove(`BUTLAST [h:A] = []`, REWRITE_TAC[BUTLAST]) and
 812     butlast_cons2' = prove(`BUTLAST (CONS (h:A) (CONS h2 s)) = CONS h (BUTLAST (CONS h2 s))`,
 813                            REWRITE_TAC[BUTLAST; NOT_CONS_NIL]);;
 814
 815
 816 let eval_butlast_last list_tm =
 817   let list_ty = type_of list_tm in
 818   let ty = (hd o snd o dest_type) list_ty in
 819   let inst_t = INST_TYPE[ty, aty] in
 820   let last1, last2 = inst_t last1', inst_t last_cons2' in
 821   let butlast1, butlast2 = inst_t butlast1', inst_t butlast_cons2' in
 822   let h_var, h2_var, s_var = mk_var("h", ty), mk_var("h2", ty), mk_var("s", list_ty) in
 823
 824   let rec butlast_last_rec list_tm =
 825     let h_tm', t_tm = dest_comb list_tm in
 826     let h_tm = rand h_tm' in
 827       if is_comb t_tm then
 828         let h_tm', s_tm = dest_comb t_tm in
 829         let h2_tm = rand h_tm' in
 830         let inst = INST[h_tm, h_var; h2_tm, h2_var; s_tm, s_var] in
 831         let butlast_th0 = inst butlast2 in
 832         let last_th0 = inst last2 in
 833         let butlast_th1, last_th1 = butlast_last_rec t_tm in
 834         let ltm = (rator o rand o concl) butlast_th0 in
 835           TRANS butlast_th0 (AP_TERM ltm butlast_th1), TRANS last_th0 last_th1
 836       else
 837         let inst = INST[h_tm, h_var; t_tm, s_var] in
 838           inst butlast1, inst last1 in
 839
 840     butlast_last_rec list_tm;;
 841
 842
 843
 844 (**********************************)
 845 (* take and drop conversions *)
 846
 847 let take0' = (MY_RULE_NUM o prove)(`take 0 (s:(A)list) = []`, REWRITE_TAC[take]) and
 848     take_nil' = prove(`take n ([]:(A)list) = []`, REWRITE_TAC[take]) and
 849     take_pre' = (MY_RULE_NUM o prove)(`!n. (0 < n <=> T) /\ PRE n = m ==> take n (CONS (h:A) s) = CONS h (take m s)`,
 850                                       INDUCT_TAC THEN SIMP_TAC[take; PRE] THEN ARITH_TAC);;
 851
 852
 853 let eval_take n_tm list_tm =
 854   let list_ty = type_of list_tm in
 855   let ty = (hd o snd o dest_type) list_ty in
 856   let inst_t = INST_TYPE[ty, aty] in
 857   let take0, take_nil, take_pre = inst_t take0', inst_t take_nil', inst_t take_pre' in
 858   let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
 859
 860   let rec take_rec n_tm list_tm =
 861     if is_comb list_tm then
 862       if n_tm = zero_const then
 863         INST[list_tm, s_var] take0
 864       else
 865         let h_tm', t_tm = dest_comb list_tm in
 866         let h_tm = rand h_tm' in
 867         let n_gt0 = raw_gt0_hash_conv n_tm in
 868         let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
 869         let m_tm = (rand o concl) pre_n in
 870         let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in
 871         let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) take_pre in
 872         let ltm = (rator o rand o concl) th0 in
 873         let th1 = take_rec m_tm t_tm in
 874           TRANS th0 (AP_TERM ltm th1)
 875     else
 876       INST[n_tm, n_var_num] take_nil in
 877
 878     take_rec n_tm list_tm;;
 879
 880
 881 (* drop *)
 882 let drop0' = (MY_RULE_NUM o prove)(`dropl 0 (s:(A)list) = s`, REWRITE_TAC[drop]) and
 883     drop_nil' = prove(`dropl n ([]:(A)list) = []`, REWRITE_TAC[drop]) and
 884     drop_pre' = (MY_RULE_NUM o prove)(`!n. (0 < n <=> T) /\ PRE n = m ==> dropl n (CONS (h:A) s) = dropl m s`,
 885                                       INDUCT_TAC THEN SIMP_TAC[drop; PRE] THEN ARITH_TAC);;
 886
 887
 888 let eval_drop n_tm list_tm =
 889   let list_ty = type_of list_tm in
 890   let ty = (hd o snd o dest_type) list_ty in
 891   let inst_t = INST_TYPE[ty, aty] in
 892   let drop0, drop_nil, drop_pre = inst_t drop0', inst_t drop_nil', inst_t drop_pre' in
 893   let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
 894
 895   let rec drop_rec n_tm list_tm =
 896     if is_comb list_tm then
 897       if n_tm = zero_const then
 898         INST[list_tm, s_var] drop0
 899       else
 900         let h_tm', t_tm = dest_comb list_tm in
 901         let h_tm = rand h_tm' in
 902         let n_gt0 = raw_gt0_hash_conv n_tm in
 903         let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
 904         let m_tm = (rand o concl) pre_n in
 905         let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in
 906         let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) drop_pre in
 907         let th1 = drop_rec m_tm t_tm in
 908           TRANS th0 th1
 909     else
 910       INST[n_tm, n_var_num] drop_nil in
 911
 912     drop_rec n_tm list_tm;;
 913
 914
 915 (* take_drop *)
 916
 917 let eval_take_drop n_tm list_tm =
 918   let list_ty = type_of list_tm in
 919   let ty = (hd o snd o dest_type) list_ty in
 920   let inst_t = INST_TYPE[ty, aty] in
 921   let drop0, drop_nil, drop_pre = inst_t drop0', inst_t drop_nil', inst_t drop_pre' in
 922   let take0, take_nil, take_pre = inst_t take0', inst_t take_nil', inst_t take_pre' in
 923   let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
 924
 925   let rec take_drop_rec n_tm list_tm =
 926     if is_comb list_tm then
 927       if n_tm = zero_const then
 928         let inst = INST[list_tm, s_var] in
 929           inst take0, inst drop0
 930       else
 931         let h_tm', t_tm = dest_comb list_tm in
 932         let h_tm = rand h_tm' in
 933         let n_gt0 = raw_gt0_hash_conv n_tm in
 934         let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in
 935         let m_tm = (rand o concl) pre_n in
 936         let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in
 937         let drop_th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) drop_pre in
 938         let take_th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) take_pre in
 939         let take_th1, drop_th1 = take_drop_rec m_tm t_tm in
 940         let take_ltm = (rator o rand o concl) take_th0 in
 941           TRANS take_th0 (AP_TERM take_ltm take_th1), TRANS drop_th0 drop_th1
 942     else
 943       let inst = INST[n_tm, n_var_num] in
 944         inst take_nil, inst drop_nil in
 945
 946     take_drop_rec n_tm list_tm;;
 947
 948
 949 (**************************)
 950 (* rot *)
 951
 952 let rot' = prove(`rot n (s:(A)list) = cat (dropl n s) (take n s)`, REWRITE_TAC[rot]);;
 953
 954 let eval_rot n_tm list_tm =
 955   let list_ty = type_of list_tm in
 956   let ty = (hd o snd o dest_type) list_ty in
 957   let s_var = mk_var("s", list_ty) in
 958   let inst_t = INST_TYPE[ty, aty] in
 959   let take_th, drop_th = eval_take_drop n_tm list_tm in
 960   let cat_th = eval_cat (rand (concl drop_th)) (rand (concl take_th)) in
 961   let cat_tm = (rator o rator o lhand o concl) cat_th in
 962   let th0 = (INST[n_tm, n_var_num; list_tm, s_var] o inst_t) rot' in
 963   let th1 = MK_COMB (AP_TERM cat_tm drop_th, take_th) in
 964     TRANS (TRANS th0 th1) cat_th;;
 965
 966
 967 (*******************************)
 968 (* shift_left = rot 1 *)
 969
 970 let shift_left_empty' = prove(`rot 1 [] = ([]:(A)list)`, REWRITE_TAC[rot; take; drop; cat]) and
 971     shift_left_cons' = prove(`rot 1 (CONS (h:A) s) = cat s [h]`, REWRITE_TAC[rot1_cons; GSYM cats1]);;
 972
 973
 974 let eval_rot1 list_tm =
 975   let list_ty = type_of list_tm in
 976   let ty = (hd o snd o dest_type) list_ty in
 977   let inst_t = INST_TYPE[ty, aty] in
 978   let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
 979     if is_comb list_tm then
 980       let h_tm', t_tm = dest_comb list_tm in
 981       let h_tm = rand h_tm' in
 982       let th0 = (INST[h_tm, h_var; t_tm, s_var] o inst_t) shift_left_cons' in
 983       let h_list = (rand o rand o concl) th0 in
 984       let th1 = eval_cat t_tm h_list in
 985         TRANS th0 th1
 986     else
 987       inst_t shift_left_empty';;
 988
 989
 990 (* shift_right = rotr 1 *)
 991 let shift_right_empty' = prove(`rotr 1 [] = ([]:(A)list)`, REWRITE_TAC[rotr; rot; take; drop; cat]) and
 992     shift_right_cons' = prove(`rotr 1 (CONS (h:A) s) = CONS (LAST (CONS h s)) (BUTLAST (CONS h s))`,
 993                               MP_TAC (ISPECL [`h:A`; `s:(A)list`] lastI) THEN
 994                                 DISCH_THEN (fun th -> REWRITE_TAC[th; rotr1_rcons]) THEN
 995                                 REWRITE_TAC[GSYM lastI] THEN SPEC_TAC (`h:A`, `h:A`) THEN
 996                                 SPEC_TAC (`s:(A)list`, `s:(A)list`) THEN
 997                                 LIST_INDUCT_TAC THEN REWRITE_TAC[last; belast; last1'; butlast1'] THEN GEN_TAC THEN
 998                                 REWRITE_TAC[last_cons2'; butlast_cons2'] THEN
 999                                 POP_ASSUM (MP_TAC o SPEC `h:A`) THEN
1000                                 REWRITE_TAC[injectivity "list"]);;
1001
1002
1003 let eval_rotr1 list_tm =
1004   let list_ty = type_of list_tm in
1005   let ty = (hd o snd o dest_type) list_ty in
1006   let inst_t = INST_TYPE[ty, aty] in
1007   let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in
1008     if is_comb list_tm then
1009       let h_tm', t_tm = dest_comb list_tm in
1010       let h_tm = rand h_tm' in
1011       let th0 = (INST[h_tm, h_var; t_tm, s_var] o inst_t) shift_right_cons' in
1012       let butlast_th, last_th = eval_butlast_last list_tm in
1013       let cons_tm = (rator o rator o rand o concl) th0 in
1014         TRANS th0 (MK_COMB (AP_TERM cons_tm last_th, butlast_th))
1015     else
1016       inst_t shift_right_empty';;
1017
1018
1019
1020 (******************************)
1021 (* index conversions *)
1022
1023 let index_empty = (MY_RULE_NUM o prove)(`indexl (x:A) [] = 0`, REWRITE_TAC[index; find]) and
1024     index_cons_eq = (MY_RULE_NUM o prove)(`(x = h <=> T) ==> indexl (x:A) (CONS h t) = 0`,
1025                                       SIMP_TAC[index; find; pred1]) and
1026     index_cons_neq = (MY_RULE o prove)(`(x = h <=> F) ==> indexl (x:A) (CONS h t) = SUC (indexl x t)`,
1027                                            SIMP_TAC[index; find; pred1]);;
1028
1029
1030 let rec eval_index_univ eq_conv x_tm list_tm =
1031   let ty = type_of x_tm in
1032   let inst_t = INST_TYPE[ty, aty] in
1033   let index_empty, index_eq, index_neq =
1034     inst_t index_empty, inst_t index_cons_eq, inst_t index_cons_neq in
1035   let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and
1036       t_var = mk_var("t", mk_type("list", [ty])) in
1037
1038   let rec index_rec list_tm =
1039     if (is_comb list_tm) then
1040       let h_tm', t_tm = dest_comb list_tm in
1041       let h_tm = rand h_tm' in
1042       let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in
1043         if (rand(concl eq_th) = t_const) then
1044           let th0 = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] index_eq in
1045             MY_PROVE_HYP eq_th th0
1046         else
1047           let th0 = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] index_neq in
1048           let th1 = MY_PROVE_HYP eq_th th0 in
1049           let th2 = AP_TERM suc_op_num (index_rec t_tm) in
1050           let suc_th = raw_suc_conv_hash (rand (concl th2)) in
1051             TRANS th1 (TRANS th2 suc_th)
1052     else
1053       INST[x_tm, x_var] index_empty in
1054
1055     index_rec list_tm;;
1056
1057
1058 let index_conv_univ eq_conv mem_tm =
1059   let ltm, list_tm = dest_comb mem_tm in
1060   let c_tm, x_tm = dest_comb ltm in
1061     if (fst o dest_const) c_tm <> "indexl" then failwith "index_conv_univ" else
1062       eval_index_univ eq_conv x_tm list_tm;;
1063
1064
1065 end;;