(* =========================================================== *)
(* Efficient formal list conversions                           *)
(* Author: Alexey Solovyev                                     *)
(* Date: 2012-10-27                                            *)
(* =========================================================== *)

needs "../formal_lp/hypermap/arith_link.hl";;
needs "misc/vars.hl";;
needs "Examples/seq-compiled.hl";;

module type List_conversions_sig =
  sig
    (* pair *)
    val eval_pair_eq_univ : (term -> thm) * (term -> thm) -> term -> term -> thm
    val pair_eq_conv_univ : (term -> thm) * (term -> thm) -> term -> thm
    val eval_pair_eq_num : term -> term -> thm
    val pair_eq_conv_num : term -> thm
    (* HD *)
    val eval_hd : term -> thm
    val hd_conv : term -> thm
      (* EL *)
    val eval_el : term -> term -> thm
    val el_conv : term -> thm
      (* FST, SND *)
    val fst_conv : term -> thm
    val snd_conv : term -> thm
      (* LENGTH *)
    val eval_length : term -> thm
    val length_conv : term -> thm
      (* ZIP *)
    val eval_zip : term -> term -> thm
      (* ALL *)
    val all_conv_univ : (term -> thm) -> term -> thm
      (* ALL2 *)
    val all2_conv_univ : (term -> thm) -> term -> thm
      (* MEM *)
    val eval_mem_univ : (term -> thm) -> term -> term -> thm
    val mem_conv_univ : (term -> thm) -> term -> thm
      (* FILTER *)
    val filter_conv_univ : (term -> thm) -> term -> thm
      (* MAP *)
    val map_conv_univ : (term -> thm) -> term -> thm
      (* ALL theorems *)
    val get_all : thm -> thm list
    val select_all : thm -> int list -> thm list
      (* set_of_list *)
    val eval_set_of_list : term -> thm
    val set_of_list_conv : term -> thm
      (* flatten *)
    val eval_flatten : term -> thm
    val flatten_conv : term -> thm
      (* uniq *)
    val eval_uniq_univ : (term -> thm) -> term -> thm
    val uniq_conv_univ : (term -> thm) -> term -> thm
      (* undup *)
    val eval_undup_univ : (term -> thm) -> term -> thm
    val undup_conv_univ : (term -> thm) -> term -> thm
      (* cat *)
    val eval_cat : term -> term -> thm
    val cat_conv : term -> thm
      (* BUTLAST, LAST *)
    val eval_butlast_last : term -> thm * thm
      (* take, drop *)
    val eval_take : term -> term -> thm
    val eval_drop : term -> term -> thm
    val eval_take_drop : term -> term -> thm * thm
      (* rot *)
    val eval_rot : term -> term -> thm
    val eval_rot1 : term -> thm
    val eval_rotr1 : term -> thm
      (* index *)
    val eval_index_univ : (term -> thm) -> term -> term -> thm
    val index_conv_univ : (term -> thm) -> term -> thm
  end;;


module List_conversions : List_conversions_sig = struct

open Arith_nat;;
open Arith_misc;;
open Misc_vars;;
open Seq;;


let MY_RULE = UNDISCH_ALL o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
let MY_RULE_NUM = UNDISCH_ALL o NUMERALS_TO_NUM o PURE_REWRITE_RULE[GSYM IMP_IMP] o SPEC_ALL;;
let TO_NUM = REWRITE_RULE[Arith_hash.NUM_THM] o DEPTH_CONV NUMERAL_TO_NUM_CONV;;
let to_num = rand o concl o TO_NUM;;



(***********************************************)
(* pair_eq_conv *)

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
    PAIR_NEQ_FST = (MY_RULE o prove)(`(n = x <=> F) ==> (n:A,m:B = x,y <=> F)`, SIMP_TAC[PAIR_EQ]) and
    PAIR_NEQ_SND = (MY_RULE o prove)(`(m = y <=> F) ==> (n:A,m:B = x,y <=> F)`, SIMP_TAC[PAIR_EQ]);;


let eval_pair_eq_univ (eq1_f, eq2_f) p1_tm p2_tm =
  if (p1_tm = p2_tm) then
    EQT_INTRO (REFL p1_tm)
  else
    let n_tm, m_tm = dest_pair p1_tm in
    let x_tm, y_tm = dest_pair p2_tm in
    let ty1 = type_of n_tm and
	ty2 = type_of m_tm in
    let n_var, m_var = mk_var("n", ty1), mk_var("m", ty2) and
	x_var, y_var = mk_var("x", ty1), mk_var("y", ty2) in
    let inst_t = INST_TYPE[ty1, aty; ty2, bty] in
    let inst = INST[n_tm, n_var; m_tm, m_var; x_tm, x_var; y_tm, y_var] in
    let fst_th = eq1_f (mk_eq (n_tm, x_tm)) in
      if (rand(concl fst_th) = f_const) then
	MY_PROVE_HYP fst_th ((inst o inst_t) PAIR_NEQ_FST)
      else
	let snd_th = eq2_f (mk_eq (m_tm, y_tm)) in
	  if (rand(concl snd_th) = f_const) then
	    MY_PROVE_HYP snd_th ((inst o inst_t) PAIR_NEQ_SND)
	  else
	    let th0 = (inst o inst_t) PAIR_EQ_TT in
	      MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0);;


let pair_eq_conv_univ (eq1_f, eq2_f) eq_tm =
  let lhs, rhs = dest_eq eq_tm in
    eval_pair_eq_univ (eq1_f, eq2_f) lhs rhs;;


let eval_pair_eq_num =
  let inst_t = INST_TYPE[num_type, aty; num_type, bty] in
  let pair_eq, pair_neq_fst, pair_neq_snd = 
    inst_t PAIR_EQ_TT, inst_t PAIR_NEQ_FST, inst_t PAIR_NEQ_SND in
    fun p1_tm p2_tm ->
      if (p1_tm = p2_tm) then
	EQT_INTRO (REFL p1_tm)
      else
	let n_tm, m_tm = dest_pair p1_tm in
	let x_tm, y_tm = dest_pair p2_tm in
	let inst = INST[n_tm, n_var_num; m_tm, m_var_num; x_tm, x_var_num; y_tm, y_var_num] in
	let fst_th = raw_eq_hash_conv (mk_eq (n_tm, x_tm)) in
	  if (rand(concl fst_th) = f_const) then
	    MY_PROVE_HYP fst_th (inst pair_neq_fst)
	  else
	    let snd_th = raw_eq_hash_conv (mk_eq (m_tm, y_tm)) in
	      if (rand(concl snd_th) = f_const) then
		MY_PROVE_HYP snd_th (inst pair_neq_snd)
	      else
		let th0 = inst pair_eq in
		  MY_PROVE_HYP fst_th (MY_PROVE_HYP snd_th th0);;


let pair_eq_conv_num eq_tm =
  let lhs, rhs = dest_eq eq_tm in
    eval_pair_eq_num lhs rhs;;



(******************************)

(* HD conversions *)

let HD_A_CONS = 
prove(`HD (CONS (h:A) t) = h`,
REWRITE_TAC[HD]);;
(* Takes a term `[a;...]` and returns the theorem |- HD [a;...] = a *) let eval_hd list_tm = let ltm, t_tm = dest_comb list_tm in let h_tm = rand ltm in let list_ty = type_of t_tm and ty = type_of h_tm in let h_var = mk_var("h", ty) and t_var = mk_var("t", list_ty) in (INST[h_tm, h_var; t_tm, t_var] o INST_TYPE[ty, aty]) HD_A_CONS;; (* Takes a term `HD [a;...]` and returns the theorem |- HD [a;...] = a *) let hd_conv hd_tm = if (fst o dest_const o rator) hd_tm <> "HD" then failwith "hd_conv" else eval_hd (rand hd_tm);; (*********************************) (* EL conversion *) let EL_0' = (MY_RULE_NUM o prove)(`EL 0 (CONS (h:A) t) = h`, REWRITE_TAC[EL; HD]);; let EL_n' = (MY_RULE_NUM o prove)(`0 < n /\ PRE n = m ==> EL n (CONS (h:A) t) = EL m t`, STRIP_TAC THEN SUBGOAL_THEN `n = SUC m` ASSUME_TAC THENL [ REPEAT (POP_ASSUM MP_TAC) THEN ARITH_TAC; ALL_TAC ] THEN ASM_REWRITE_TAC[EL; TL]);; (* Takes a raw numeral term and a list term and returns the theorem |- EL n [...] = x *) let eval_el n_tm list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let el_0, el_n = inst_t EL_0', inst_t EL_n' in let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in let rec el_conv_raw = fun n_tm list_tm -> let h_tm, t_tm = dest_cons list_tm in let inst0 = INST[h_tm, h_var; t_tm, t_var] in if n_tm = zero_const then inst0 el_0 else let n_gt0 = (EQT_ELIM o raw_gt0_hash_conv) n_tm in let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in let m_tm = (rand o concl) pre_n in let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o INST[n_tm, n_var_num; m_tm, m_var_num] o inst0) el_n in let th1 = el_conv_raw m_tm t_tm in TRANS th0 th1 in el_conv_raw n_tm list_tm;; (* Takes a term `EL n [...]` and returns the theorem |- EL n [...] = x *) (* Note: n must be a raw numeral term Dx (Dy ... _0) *) let el_conv el_tm = let ltm, list_tm = dest_comb el_tm in let el, n_tm = dest_comb ltm in if (fst o dest_const) el <> "EL" then failwith "el_conv" else eval_el n_tm list_tm;; (*******************************) (* FST, SND conversions *) let FST' = ISPECL[`x:A`; `y:B`] FST;; let SND' = ISPECL[`x:A`; `y:B`] SND;; let fst_conv tm = let x_tm, y_tm = dest_pair (rand tm) in let x_ty, y_ty = type_of x_tm, type_of y_tm in let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) FST';; let snd_conv tm = let x_tm, y_tm = dest_pair (rand tm) in let x_ty, y_ty = type_of x_tm, type_of y_tm in let x_var, y_var = mk_var("x", x_ty), mk_var("y", y_ty) in (INST[x_tm, x_var; y_tm, y_var] o INST_TYPE[x_ty, aty; y_ty, bty]) SND';; (******************************) (* LENGTH conversions *) let LENGTH_0' = (MY_RULE_NUM o prove) (`LENGTH ([]:(A)list) = 0`, REWRITE_TAC[LENGTH]) and LENGTH_CONS' = prove(`LENGTH (CONS (h:A) t) = SUC (LENGTH t)`, REWRITE_TAC[LENGTH]);; (* Takes a term `[...]` and returns the theorem |- LENGTH [...] = n *) let eval_length list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let length_empty, length_cons = inst_t LENGTH_0', inst_t LENGTH_CONS' in let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) in let rec length_conv_raw = fun list_tm -> if (is_comb list_tm) then let ltm, t_tm = dest_comb list_tm in let h_tm = rand ltm in let th0 = INST[h_tm, h_var; t_tm, t_var] length_cons in let th1' = length_conv_raw t_tm in let th1 = AP_TERM suc_op_num th1' in let th2 = raw_suc_conv_hash (rand(concl th1)) in TRANS (TRANS th0 th1) th2 else length_empty in length_conv_raw list_tm;; (* Takes a term `LENGTH [...]` and returns the theorem |- LENGTH [...] = n *) let length_conv length_tm = if (fst o dest_const o rator) length_tm <> "LENGTH" then failwith "length_conv" else eval_length (rand length_tm);; (************************) (* eval_zip *)
let ZIP_0' = 
prove(`ZIP ([]:(A)list) ([]:(B)list) = []`,
REWRITE_TAC[ZIP]) and ZIP_CONS' = prove(`ZIP (CONS (h1:A) t1) (CONS (h2:B) t2) = CONS (h1, h2) (ZIP t1 t2)`, REWRITE_TAC[ZIP]);;
let eval_zip list1_tm list2_tm = let list1_ty = type_of list1_tm and list2_ty = type_of list2_tm in let ty1 = (hd o snd o dest_type) list1_ty and ty2 = (hd o snd o dest_type) list2_ty in let inst_t = INST_TYPE[ty1, aty; ty2, bty] in let zip0, zip_cons = inst_t ZIP_0', inst_t ZIP_CONS' in let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) in let rec zip_conv_rec = fun list1_tm list2_tm -> if (is_comb list1_tm) then let ltm1, t1_tm = dest_comb list1_tm and ltm2, t2_tm = dest_comb list2_tm in let h1_tm, h2_tm = rand ltm1, rand ltm2 in let th0 = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var] zip_cons in let cons_tm = (rator o rand o concl) th0 in let th1' = zip_conv_rec t1_tm t2_tm in let th1 = AP_TERM cons_tm th1' in TRANS th0 th1 else zip0 in zip_conv_rec list1_tm list2_tm;; (******************) (* ALL conversion *) (******************)
let ALL_0' = 
prove(`ALL P ([]:(A)list) <=> T`,
REWRITE_TAC[ALL]) and ALL_CONS_T' = (MY_RULE o prove)(`(P h <=> T) /\ (ALL P t <=> T) ==> (ALL P (CONS (h:A) t) <=> T)`, REWRITE_TAC[ALL]) and ALL_CONS_F2' = (MY_RULE o prove)(`(ALL P t <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`, SIMP_TAC[ALL]) and ALL_CONS_F1' = (MY_RULE o prove)(`(P h <=> F) ==> (ALL P (CONS (h:A) t) <=> F)`, SIMP_TAC[ALL]);;
(* Note: p_conv should return theorems of the form |- P a <=> T *) let all_conv_univ p_conv tm = let ltm, list_tm = dest_comb tm in let p_tm = rand ltm in let list_ty = type_of list_tm and p_ty = type_of p_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let all_0, all_t, all_f1, all_f2 = inst_t ALL_0', inst_t ALL_CONS_T', inst_t ALL_CONS_F1', inst_t ALL_CONS_F2' in let h_var, t_var = mk_var("h", ty), mk_var("t", list_ty) and p_var = mk_var("P", p_ty) in let rec all_conv_rec = fun list_tm -> if is_comb list_tm then let ltm, t_tm = dest_comb list_tm in let h_tm = rand ltm in let p_th = p_conv (mk_comb (p_tm, h_tm)) in let inst = INST[h_tm, h_var; t_tm, t_var; p_tm, p_var] in if (rand o concl) p_th = t_const then let all_th = all_conv_rec t_tm in if (rand o concl) all_th = t_const then (MY_PROVE_HYP all_th o MY_PROVE_HYP p_th o inst) all_t else (MY_PROVE_HYP all_th o inst) all_f2 else (MY_PROVE_HYP p_th o inst) all_f1 else INST[p_tm, p_var] all_0 in all_conv_rec list_tm;; (*******************) (* ALL2 conversion *) (*******************)
let ALL2_0' = 
prove(`ALL2 P ([]:(A)list) ([]:(B)list) <=> T`,
REWRITE_TAC[ALL2]) and ALL2_CONS_T' = (MY_RULE o prove)(`(P h1 h2 <=> T) /\ (ALL2 P t1 t2 <=> T) ==> (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> T)`, REWRITE_TAC[ALL2]) and ALL2_CONS_F2' = (MY_RULE o prove)(`(ALL2 P t1 t2 <=> F) ==> (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`, SIMP_TAC[ALL2]) and ALL2_CONS_F1' = (MY_RULE o prove)(`(P h1 h2 <=> F) ==> (ALL2 P (CONS (h1:A) t1) (CONS (h2:B) t2) <=> F)`, SIMP_TAC[ALL2]);;
(* Note: p_conv should return theorems of the form |- P a b <=> T *) let all2_conv_univ p_conv tm = let ltm, list2_tm = dest_comb tm in let ltm2, list1_tm = dest_comb ltm in let p_tm = rand ltm2 in let list1_ty = type_of list1_tm and list2_ty = type_of list2_tm and p_ty = type_of p_tm in let ty1 = (hd o snd o dest_type) list1_ty and ty2 = (hd o snd o dest_type) list2_ty in let inst_t = INST_TYPE[ty1, aty; ty2, bty] in let all2_0, all2_t, all2_f1, all2_f2 = inst_t ALL2_0', inst_t ALL2_CONS_T', inst_t ALL2_CONS_F1', inst_t ALL2_CONS_F2' in let h1_var, t1_var = mk_var("h1", ty1), mk_var("t1", list1_ty) and h2_var, t2_var = mk_var("h2", ty2), mk_var("t2", list2_ty) and p_var = mk_var("P", p_ty) in let rec all2_conv_rec = fun list1_tm list2_tm -> if is_comb list1_tm then let ltm1, t1_tm = dest_comb list1_tm and ltm2, t2_tm = dest_comb list2_tm in let h1_tm, h2_tm = rand ltm1, rand ltm2 in let p_th = p_conv (mk_binop p_tm h1_tm h2_tm) in let inst = INST[h1_tm, h1_var; t1_tm, t1_var; h2_tm, h2_var; t2_tm, t2_var; p_tm, p_var] in if (rand o concl) p_th = t_const then let all2_th = all2_conv_rec t1_tm t2_tm in if (rand o concl) all2_th = t_const then (MY_PROVE_HYP all2_th o MY_PROVE_HYP p_th o inst) all2_t else (MY_PROVE_HYP all2_th o inst) all2_f2 else (MY_PROVE_HYP p_th o inst) all2_f1 else if is_comb list2_tm then failwith ("all2_conv_univ: l1 = []; l2 = "^string_of_term list2_tm) else INST[p_tm, p_var] all2_0 in all2_conv_rec list1_tm list2_tm;; (******************************) (* MEM conversions *)
let MEM_A_EMPTY = 
prove(`MEM (x:A) [] <=> F`,
REWRITE_TAC[MEM]) and MEM_A_HD = (MY_RULE o prove) (`(x = h <=> T) ==> (MEM (x:A) (CONS h t) <=> T)`, SIMP_TAC[MEM]) and MEM_A_TL = (MY_RULE o prove) (`(x = h <=> F) ==> (MEM (x:A) (CONS h t) <=> MEM x t)`, SIMP_TAC[MEM]);;
let rec eval_mem_univ eq_conv x_tm list_tm = let ty = type_of x_tm in let inst_t = INST_TYPE[ty, aty] in let mem_empty, mem_hd, mem_tl = inst_t MEM_A_EMPTY, inst_t MEM_A_HD, inst_t MEM_A_TL in let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and t_var = mk_var("t", mk_type("list", [ty])) in let rec mem_conv_raw list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in if (rand(concl eq_th) = t_const) then let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_hd in MY_PROVE_HYP eq_th th0' else let th0' = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] mem_tl in let th0 = MY_PROVE_HYP eq_th th0' in let th1 = mem_conv_raw t_tm in TRANS th0 th1 else INST[x_tm, x_var] mem_empty in mem_conv_raw list_tm;; let mem_conv_univ eq_conv mem_tm = let ltm, list_tm = dest_comb mem_tm in let c_tm, x_tm = dest_comb ltm in if (fst o dest_const) c_tm <> "MEM" then failwith "mem_conv_univ" else eval_mem_univ eq_conv x_tm list_tm;; (**********************************) (* FILTER conversions *)
let FILTER_A_EMPTY = 
prove(`FILTER (P:A->bool) [] = []`,
REWRITE_TAC[FILTER]) and FILTER_A_HD = (MY_RULE o prove) (`(P h <=> T) ==> FILTER (P:A->bool) (CONS h t) = CONS h (FILTER P t)`, SIMP_TAC[FILTER]) and FILTER_A_TL = (MY_RULE o prove) (`(P h <=> F) ==> FILTER (P:A->bool) (CONS h t) = FILTER P t`, SIMP_TAC[FILTER]);;
let filter_conv_univ p_conv tm = let ltm, list_tm = dest_comb tm in let p_tm = rand ltm in let p_ty = type_of p_tm in let ty = (hd o snd o dest_type) p_ty in let inst_t = INST_TYPE[ty, aty] in let filter_empty, filter_hd, filter_tl = inst_t FILTER_A_EMPTY, inst_t FILTER_A_HD, inst_t FILTER_A_TL in let p_var = mk_var("P", p_ty) in let h_var = mk_var("h", ty) in let t_var = mk_var("t", mk_type("list",[ty])) in let rec filter_conv_raw = fun list_tm -> if (is_comb list_tm) then let ltm, t_tm = dest_comb list_tm in let h_tm = rand ltm in let p_th = p_conv (mk_comb(p_tm, h_tm)) in if (rand(concl p_th) = t_const) then let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_hd in let th0 = MY_PROVE_HYP p_th th0' in let ltm = rator(rand(concl th0)) in let th1 = filter_conv_raw t_tm in TRANS th0 (AP_TERM ltm th1) else let th0' = INST[p_tm, p_var; h_tm, h_var; t_tm, t_var] filter_tl in let th0 = MY_PROVE_HYP p_th th0' in let th1 = filter_conv_raw t_tm in TRANS th0 th1 else INST[p_tm, p_var] filter_empty in filter_conv_raw list_tm;; (***************************) (* MAP conversions *)
let MAP_AB_EMPTY = 
prove(`MAP (f:A->B) [] = []`,
REWRITE_TAC[MAP]) and MAP_AB_CONS = prove(`MAP (f:A->B) (CONS h t) = CONS (f h) (MAP f t)`, REWRITE_TAC[MAP]);;
let map_conv_univ f_conv tm = let ltm, list_tm = dest_comb tm in let ftm = rand ltm in let ftm_ty = type_of ftm in let f_var = mk_var("f", ftm_ty) in let [a_type; b_type] = snd(dest_type ftm_ty) in let h_var = mk_var("h", a_type) in let t_var = mk_var("t", mk_type("list", [a_type])) in let inst_t = INST[ftm, f_var] o INST_TYPE[a_type, aty; b_type, bty] in let map_empty, map_cons = inst_t MAP_AB_EMPTY, inst_t MAP_AB_CONS in let rec map_conv_raw list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let th0 = INST[h_tm, h_var; t_tm, t_var] map_cons in let ltm, rtm = dest_comb (rand(concl th0)) in let cons_tm, f_h_tm = dest_comb ltm in let f_h_th = f_conv f_h_tm in let map_t_th = map_conv_raw t_tm in TRANS th0 (MK_COMB (AP_TERM cons_tm f_h_th, map_t_th)) else map_empty in map_conv_raw list_tm;; (*****************************************) (* ALL rules *) let ALL_A_HD = (MY_RULE o prove) (`ALL (P:A->bool) (CONS h t) ==> P h`, SIMP_TAC[ALL]) and ALL_A_TL = (MY_RULE o prove) (`ALL (P:A->bool) (CONS h t) ==> ALL P t`, SIMP_TAC[ALL]);; (* Given a theorem `ALL P list` returns the list of theorems (P x1),...,(P xn) *) let get_all th = let ltm, list_tm = dest_comb (concl th) in let p_tm = rand ltm in let list_ty = type_of list_tm in let p_ty = type_of p_tm in let ty = (hd o snd o dest_type) list_ty in let p_var = mk_var("P", p_ty) in let h_var = mk_var("h", ty) in let t_var = mk_var("t", list_ty) in let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in let rec get_all_raw all_th list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let inst_t = INST[h_tm, h_var; t_tm, t_var] in let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in th_hd :: get_all_raw th_tl t_tm else [] in get_all_raw th list_tm;; (* Given a theorem `ALL P list`, returns (P x_i1),..., (P x_in) where i1,...,in are given indices. The list of indices should be sorted *) let select_all th indices = let ltm, list_tm = dest_comb (concl th) in let p_tm = rand ltm in let list_ty = type_of list_tm in let p_ty = type_of p_tm in let ty = (hd o snd o dest_type) list_ty in let p_var = mk_var("P", p_ty) in let h_var = mk_var("h", ty) in let t_var = mk_var("t", list_ty) in let inst_t = INST[p_tm, p_var] o INST_TYPE[ty, aty] in let all_hd, all_tl = inst_t ALL_A_HD, inst_t ALL_A_TL in let rec get_all_raw all_th list_tm indices n = match indices with [] -> [] | i::is -> let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let inst_t = INST[h_tm, h_var; t_tm, t_var] in let th_tl = MY_PROVE_HYP all_th (inst_t all_tl) in if (i - n = 0) then let th_hd = MY_PROVE_HYP all_th (inst_t all_hd) in th_hd :: get_all_raw th_tl t_tm is (n + 1) else get_all_raw th_tl t_tm (i::is) (n + 1) in get_all_raw th list_tm indices 0;; (*****************************************) (* set_of_list conversions *)
let SET_OF_LIST_A_EMPTY = 
prove(`set_of_list ([]:(A)list) = {}`,
REWRITE_TAC[set_of_list]) and SET_OF_LIST_A_H = prove(`set_of_list [h:A] = {h}`, REWRITE_TAC[set_of_list]) and SET_OF_LIST_A_CONS = prove(`set_of_list (CONS (h:A) t) = h INSERT set_of_list t`, REWRITE_TAC[set_of_list]);;
let eval_set_of_list list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let h_var = mk_var("h", ty) in let t_var = mk_var("t", list_ty) in let inst_t = INST_TYPE[ty, aty] in let set_of_list_h, set_of_list_cons = inst_t SET_OF_LIST_A_H, inst_t SET_OF_LIST_A_CONS in let rec set_of_list_conv_raw = fun h_tm t_tm -> if (is_comb t_tm) then let h_tm', t_tm' = dest_comb t_tm in let th0 = INST[h_tm, h_var; t_tm, t_var] set_of_list_cons in let ltm, rtm = dest_comb(rand(concl th0)) in TRANS th0 (AP_TERM ltm (set_of_list_conv_raw (rand h_tm') t_tm')) else INST[h_tm, h_var] set_of_list_h in if (is_comb list_tm) then let h_tm, t_tm = dest_comb list_tm in set_of_list_conv_raw (rand h_tm) t_tm else inst_t SET_OF_LIST_A_EMPTY;; let set_of_list_conv tm = if (fst o dest_const o rator) tm <> "set_of_list" then failwith "set_of_list_conv" else eval_set_of_list (rand tm);; (*****************************************) (* flatten conversions *)
let flatten_empty = 
prove(`flatten ([]:((A)list)list) = []`,
REWRITE_TAC[flatten; foldr; cat]) and flatten_cons_empty = prove(`flatten (CONS ([]:(A)list) tt) = flatten tt`, REWRITE_TAC[flatten; foldr; cat]) and flatten_cons_cons = prove(`flatten (CONS (CONS (h:A) t) tt) = CONS h (flatten (CONS t tt))`, REWRITE_TAC[flatten; foldr; cat]);;
(* Works for any list of lists *) let eval_flatten list_list_tm = let list_list_ty = type_of list_list_tm in let list_ty = (hd o snd o dest_type) list_list_ty in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let flatten_empty, flatten_cons_empty, flatten_cons_cons = inst_t flatten_empty, inst_t flatten_cons_empty, inst_t flatten_cons_cons in let tt_var = mk_var("tt", list_list_ty) in let t_var = mk_var("t", list_ty) in let h_var = mk_var("h", ty) in let rec flatten_conv_raw list_list_tm = if (is_comb list_list_tm) then let hh_tm', tt_tm = dest_comb list_list_tm in let hh_tm = rand hh_tm' in if (is_comb hh_tm) then let h_tm', t_tm = dest_comb hh_tm in let h_tm = rand h_tm' in let th0 = INST[h_tm, h_var; t_tm, t_var; tt_tm, tt_var] flatten_cons_cons in let ltm, rtm = dest_comb(rand(concl th0)) in let th1 = AP_TERM ltm (flatten_conv_raw (rand rtm)) in TRANS th0 th1 else let th0 = INST[tt_tm, tt_var] flatten_cons_empty in let th1 = flatten_conv_raw tt_tm in TRANS th0 th1 else flatten_empty in flatten_conv_raw list_list_tm;; let flatten_conv flatten_tm = if (fst o dest_const o rator) flatten_tm <> "flatten" then failwith "flatten_conv" else eval_flatten (rand flatten_tm);; (********************************) (* uniq conversion *)
let uniq_empty = 
prove(`uniq ([]:(A)list) <=> T`,
REWRITE_TAC[uniq]) and uniq_cons_F = (MY_RULE o prove) (`(MEM (h:A) t <=> F) ==> (uniq (CONS h t) <=> uniq t)`, SIMP_TAC[uniq]) and uniq_cons_T = (MY_RULE o prove) (`(MEM (h:A) t <=> T) ==> (uniq (CONS h t) <=> F)`, SIMP_TAC[uniq]);;
let eval_uniq_univ eq_conv list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let h_var = mk_var("h", ty) in let t_var = mk_var("t", list_ty) in let inst_t = INST_TYPE[ty, aty] in let uniq_empty, uniq_cons_F, uniq_cons_T = inst_t uniq_empty, inst_t uniq_cons_F, inst_t uniq_cons_T in let rec uniq_rec list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let inst = INST[h_tm, h_var; t_tm, t_var] in let mem_th = eval_mem_univ eq_conv h_tm t_tm in if (rand (concl mem_th) = t_const) then MY_PROVE_HYP mem_th (inst uniq_cons_T) else let th0 = MY_PROVE_HYP mem_th (inst uniq_cons_F) in let th1 = uniq_rec t_tm in TRANS th0 th1 else uniq_empty in uniq_rec list_tm;; let uniq_conv_univ eq_conv tm = if (fst o dest_const o rator) tm <> "uniq" then failwith "uniq_conv" else eval_uniq_univ eq_conv (rand tm);; (**********************************) (* undup conversion *)
let undup_empty = 
prove(`undup ([]:(num)list) = []`,
REWRITE_TAC[undup]) and undup_mem_T = (MY_RULE o prove) (`(MEM (h:A) t <=> T) ==> undup (CONS h t) = undup t`, SIMP_TAC[undup]) and undup_mem_F = (MY_RULE o prove) (`(MEM (h:A) t <=> F) ==> undup (CONS h t) = CONS h (undup t)`, SIMP_TAC[undup]);;
let eval_undup_univ eq_conv list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let h_var = mk_var("h", ty) in let t_var = mk_var("t", list_ty) in let inst_t = INST_TYPE[ty, aty] in let empty, mem_T, mem_F = inst_t undup_empty, inst_t undup_mem_T, inst_t undup_mem_F in let rec undup_rec list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let inst = INST[h_tm, h_var; t_tm, t_var] in let mem_th = eval_mem_univ eq_conv h_tm t_tm in if (rand(concl mem_th) = t_const) then let th0 = MY_PROVE_HYP mem_th (inst mem_T) in let th1 = undup_rec t_tm in TRANS th0 th1 else let th0 = MY_PROVE_HYP mem_th (inst mem_F) in let ltm, rtm = dest_comb (rand(concl th0)) in let th1 = undup_rec (rand rtm) in TRANS th0 (AP_TERM ltm th1) else empty in undup_rec list_tm;; let undup_conv_univ eq_conv tm = if (fst o dest_const o rator) tm <> "undup" then failwith "undup_conv" else eval_undup_univ eq_conv (rand tm);; (**********************************) (* cat conversion *)
let cat_empty' = 
prove(`cat [] (s:(A)list) = s`,
REWRITE_TAC[cat]) and cat_cons' = prove(`cat (CONS (h:A) t) s = CONS h (cat t s)`, REWRITE_TAC[cat]);;
let eval_cat list1_tm list2_tm = let list_ty = type_of list1_tm in let ty = (hd o snd o dest_type) list_ty in let h_var = mk_var("h", ty) and t_var = mk_var("t", list_ty) and s_var = mk_var("s", list_ty) in let inst_t = INST_TYPE[ty, aty] in let empty, cons = inst_t cat_empty', inst_t cat_cons' in let rec cat_rec list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let inst = INST[h_tm, h_var; t_tm, t_var; list2_tm, s_var] in let th0 = inst cons in let ltm = rator (rand (concl th0)) in let th1 = cat_rec t_tm in TRANS th0 (AP_TERM ltm th1) else INST[list2_tm, s_var] empty in cat_rec list1_tm;; let cat_conv tm = let ltm, list2_tm = dest_comb tm in let cat, list1_tm = dest_comb ltm in if (fst o dest_const) cat <> "cat" then failwith "cat_conv" else eval_cat list1_tm list2_tm;; (**********************************) (* BUTLAST and LAST conversions *)
let last1' = 
prove(`LAST [h:A] = h`,
REWRITE_TAC[LAST]) and last_cons2' = prove(`LAST (CONS (h:A) (CONS h2 s)) = LAST (CONS h2 s)`, REWRITE_TAC[LAST; NOT_CONS_NIL]) and butlast1' = prove(`BUTLAST [h:A] = []`, REWRITE_TAC[BUTLAST]) and butlast_cons2' = prove(`BUTLAST (CONS (h:A) (CONS h2 s)) = CONS h (BUTLAST (CONS h2 s))`, REWRITE_TAC[BUTLAST; NOT_CONS_NIL]);;
let eval_butlast_last list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let last1, last2 = inst_t last1', inst_t last_cons2' in let butlast1, butlast2 = inst_t butlast1', inst_t butlast_cons2' in let h_var, h2_var, s_var = mk_var("h", ty), mk_var("h2", ty), mk_var("s", list_ty) in let rec butlast_last_rec list_tm = let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in if is_comb t_tm then let h_tm', s_tm = dest_comb t_tm in let h2_tm = rand h_tm' in let inst = INST[h_tm, h_var; h2_tm, h2_var; s_tm, s_var] in let butlast_th0 = inst butlast2 in let last_th0 = inst last2 in let butlast_th1, last_th1 = butlast_last_rec t_tm in let ltm = (rator o rand o concl) butlast_th0 in TRANS butlast_th0 (AP_TERM ltm butlast_th1), TRANS last_th0 last_th1 else let inst = INST[h_tm, h_var; t_tm, s_var] in inst butlast1, inst last1 in butlast_last_rec list_tm;; (**********************************) (* take and drop conversions *) let take0' = (MY_RULE_NUM o prove)(`take 0 (s:(A)list) = []`, REWRITE_TAC[take]) and take_nil' = prove(`take n ([]:(A)list) = []`, REWRITE_TAC[take]) and 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)`, INDUCT_TAC THEN SIMP_TAC[take; PRE] THEN ARITH_TAC);; let eval_take n_tm list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let take0, take_nil, take_pre = inst_t take0', inst_t take_nil', inst_t take_pre' in let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in let rec take_rec n_tm list_tm = if is_comb list_tm then if n_tm = zero_const then INST[list_tm, s_var] take0 else let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let n_gt0 = raw_gt0_hash_conv n_tm in let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in let m_tm = (rand o concl) pre_n in let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) take_pre in let ltm = (rator o rand o concl) th0 in let th1 = take_rec m_tm t_tm in TRANS th0 (AP_TERM ltm th1) else INST[n_tm, n_var_num] take_nil in take_rec n_tm list_tm;; (* drop *) let drop0' = (MY_RULE_NUM o prove)(`dropl 0 (s:(A)list) = s`, REWRITE_TAC[drop]) and drop_nil' = prove(`dropl n ([]:(A)list) = []`, REWRITE_TAC[drop]) and drop_pre' = (MY_RULE_NUM o prove)(`!n. (0 < n <=> T) /\ PRE n = m ==> dropl n (CONS (h:A) s) = dropl m s`, INDUCT_TAC THEN SIMP_TAC[drop; PRE] THEN ARITH_TAC);; let eval_drop n_tm list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let drop0, drop_nil, drop_pre = inst_t drop0', inst_t drop_nil', inst_t drop_pre' in let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in let rec drop_rec n_tm list_tm = if is_comb list_tm then if n_tm = zero_const then INST[list_tm, s_var] drop0 else let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let n_gt0 = raw_gt0_hash_conv n_tm in let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in let m_tm = (rand o concl) pre_n in let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in let th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) drop_pre in let th1 = drop_rec m_tm t_tm in TRANS th0 th1 else INST[n_tm, n_var_num] drop_nil in drop_rec n_tm list_tm;; (* take_drop *) let eval_take_drop n_tm list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let drop0, drop_nil, drop_pre = inst_t drop0', inst_t drop_nil', inst_t drop_pre' in let take0, take_nil, take_pre = inst_t take0', inst_t take_nil', inst_t take_pre' in let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in let rec take_drop_rec n_tm list_tm = if is_comb list_tm then if n_tm = zero_const then let inst = INST[list_tm, s_var] in inst take0, inst drop0 else let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let n_gt0 = raw_gt0_hash_conv n_tm in let pre_n = raw_pre_hash_conv (mk_comb (pre_op_num, n_tm)) in let m_tm = (rand o concl) pre_n in let inst = INST[h_tm, h_var; t_tm, s_var; m_tm, m_var_num; n_tm, n_var_num] in let drop_th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) drop_pre in let take_th0 = (MY_PROVE_HYP pre_n o MY_PROVE_HYP n_gt0 o inst) take_pre in let take_th1, drop_th1 = take_drop_rec m_tm t_tm in let take_ltm = (rator o rand o concl) take_th0 in TRANS take_th0 (AP_TERM take_ltm take_th1), TRANS drop_th0 drop_th1 else let inst = INST[n_tm, n_var_num] in inst take_nil, inst drop_nil in take_drop_rec n_tm list_tm;; (**************************) (* rot *)
let rot' = 
prove(`rot n (s:(A)list) = cat (dropl n s) (take n s)`,
REWRITE_TAC[rot]);;
let eval_rot n_tm list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let s_var = mk_var("s", list_ty) in let inst_t = INST_TYPE[ty, aty] in let take_th, drop_th = eval_take_drop n_tm list_tm in let cat_th = eval_cat (rand (concl drop_th)) (rand (concl take_th)) in let cat_tm = (rator o rator o lhand o concl) cat_th in let th0 = (INST[n_tm, n_var_num; list_tm, s_var] o inst_t) rot' in let th1 = MK_COMB (AP_TERM cat_tm drop_th, take_th) in TRANS (TRANS th0 th1) cat_th;; (*******************************) (* shift_left = rot 1 *)
let shift_left_empty' = 
prove(`rot 1 [] = ([]:(A)list)`,
REWRITE_TAC[rot; take; drop; cat]) and shift_left_cons' = prove(`rot 1 (CONS (h:A) s) = cat s [h]`, REWRITE_TAC[rot1_cons; GSYM cats1]);;
let eval_rot1 list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in if is_comb list_tm then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let th0 = (INST[h_tm, h_var; t_tm, s_var] o inst_t) shift_left_cons' in let h_list = (rand o rand o concl) th0 in let th1 = eval_cat t_tm h_list in TRANS th0 th1 else inst_t shift_left_empty';; (* shift_right = rotr 1 *)
let shift_right_empty' = 
prove(`rotr 1 [] = ([]:(A)list)`,
REWRITE_TAC[rotr; rot; take; drop; cat]) and shift_right_cons' = prove(`rotr 1 (CONS (h:A) s) = CONS (LAST (CONS h s)) (BUTLAST (CONS h s))`, MP_TAC (ISPECL [`h:A`; `s:(A)list`] lastI) THEN DISCH_THEN (fun th -> REWRITE_TAC[th; rotr1_rcons]) THEN REWRITE_TAC[GSYM lastI] THEN SPEC_TAC (`h:A`, `h:A`) THEN SPEC_TAC (`s:(A)list`, `s:(A)list`) THEN LIST_INDUCT_TAC THEN REWRITE_TAC[last; belast; last1';
butlast1'] THEN GEN_TAC THEN REWRITE_TAC[last_cons2'; butlast_cons2'] THEN POP_ASSUM (MP_TAC o SPEC `h:A`) THEN REWRITE_TAC[injectivity "list"]);; let eval_rotr1 list_tm = let list_ty = type_of list_tm in let ty = (hd o snd o dest_type) list_ty in let inst_t = INST_TYPE[ty, aty] in let h_var, s_var = mk_var("h", ty), mk_var("s", list_ty) in if is_comb list_tm then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let th0 = (INST[h_tm, h_var; t_tm, s_var] o inst_t) shift_right_cons' in let butlast_th, last_th = eval_butlast_last list_tm in let cons_tm = (rator o rator o rand o concl) th0 in TRANS th0 (MK_COMB (AP_TERM cons_tm last_th, butlast_th)) else inst_t shift_right_empty';; (******************************) (* index conversions *) let index_empty = (MY_RULE_NUM o prove)(`indexl (x:A) [] = 0`, REWRITE_TAC[index; find]) and index_cons_eq = (MY_RULE_NUM o prove)(`(x = h <=> T) ==> indexl (x:A) (CONS h t) = 0`, SIMP_TAC[index; find; pred1]) and index_cons_neq = (MY_RULE o prove)(`(x = h <=> F) ==> indexl (x:A) (CONS h t) = SUC (indexl x t)`, SIMP_TAC[index; find; pred1]);; let rec eval_index_univ eq_conv x_tm list_tm = let ty = type_of x_tm in let inst_t = INST_TYPE[ty, aty] in let index_empty, index_eq, index_neq = inst_t index_empty, inst_t index_cons_eq, inst_t index_cons_neq in let x_var, h_var = mk_var("x", ty), mk_var("h", ty) and t_var = mk_var("t", mk_type("list", [ty])) in let rec index_rec list_tm = if (is_comb list_tm) then let h_tm', t_tm = dest_comb list_tm in let h_tm = rand h_tm' in let eq_th = eq_conv (mk_eq(x_tm, h_tm)) in if (rand(concl eq_th) = t_const) then let th0 = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] index_eq in MY_PROVE_HYP eq_th th0 else let th0 = INST[x_tm, x_var; h_tm, h_var; t_tm, t_var] index_neq in let th1 = MY_PROVE_HYP eq_th th0 in let th2 = AP_TERM suc_op_num (index_rec t_tm) in let suc_th = raw_suc_conv_hash (rand (concl th2)) in TRANS th1 (TRANS th2 suc_th) else INST[x_tm, x_var] index_empty in index_rec list_tm;; let index_conv_univ eq_conv mem_tm = let ltm, list_tm = dest_comb mem_tm in let c_tm, x_tm = dest_comb ltm in if (fst o dest_const) c_tm <> "indexl" then failwith "index_conv_univ" else eval_index_univ eq_conv x_tm list_tm;; end;;