let aacons_tm = `CONS:A -> A list -> A list` ;;
let HD_CONV conv tm = 
  let h::rest = dest_list tm in
  let ty = type_of h in  
  let thm = conv h in
  let thm2 = REFL (mk_list(rest,ty)) in
  let cs = inst [ty,aty] aacons_tm in
    MK_COMB ((AP_TERM cs thm),thm2);;

let TL_CONV conv tm = 
(*   try *)
    let h::t = dest_list tm in
    let lty = type_of h in
    let cs = inst [lty,aty] aacons_tm in
      MK_COMB ((AP_TERM cs (REFL h)), (LIST_CONV conv (mk_list(t,lty))))
(*   with _ -> failwith "TL_CONV" *)

let rec EL_CONV conv i tm = 
  if i = 0 then HD_CONV conv tm
  else 
    let h::t = dest_list tm in
    let lty = type_of h in
    let cs = inst [lty,aty] aacons_tm in
      MK_COMB ((AP_TERM cs (REFL h)), (EL_CONV conv (i - 1) (mk_list(t,lty))))


(*

  let conv = (REWRITE_CONV[ARITH_RULE `x + x = &2 * x`])
  let tm = `[&5 + &5; &6 + &6; &7 + &7]`
  HD_CONV conv tm 
  TL_CONV conv tm 
  HD_CONV(TL_CONV conv) tm 
  CONS_CONV conv tm
  EL_CONV conv 0 tm
  EL_CONV conv 1 tm
  EL_CONV conv 2 tm

*)

let NOT_CONS = prove_by_refinement(
  `!l. (~ ?(h:A) t. (l = CONS h t)) ==> (l = [])`,
(* {{{ Proof *)

[
  MESON_TAC[list_CASES];
]);;

(* }}} *)

let REMOVE = new_recursive_definition list_RECURSION
  `(REMOVE x [] = []) /\ 
   (REMOVE x (CONS (h:A) t) = 
     let rest = REMOVE x t in
       if x = h then rest else CONS h rest)`;;   

let CHOP_LIST = new_recursive_definition num_RECURSION
  `(CHOP_LIST 0 l = [],l) /\ 
   (CHOP_LIST (SUC n) l = 
     let a,b = CHOP_LIST n (TL l) in
      CONS (HD l) a,b)`;;

let REM_NIL = prove(
 `REMOVE x [] = []`,
 MESON_TAC[REMOVE]);;

let REM_FALSE = prove_by_refinement(
 `!x l. ~(MEM x (REMOVE x l))`,
(* {{{ Proof *)
[
 STRIP_TAC;
 LIST_INDUCT_TAC;
 ASM_MESON_TAC[MEM;REM_NIL];
 CASES_ON `x = h`;
 ASM_REWRITE_TAC[];
 ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
 ASM_MESON_TAC[];
 ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
 ASM_MESON_TAC[MEM];
]);;
(* }}} *)

let MEM_REMOVE = prove_by_refinement(
  `!x y z l. MEM x (REMOVE y l) ==> MEM x (REMOVE y (CONS z l))`,
(* {{{ Proof *)
[
  REPEAT_N 3 STRIP_TAC;
  CASES_ON `y = z`;
  ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
  ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF];
  ASM_MESON_TAC[MEM];
]);;
(* }}} *)

let REM_NEQ = prove_by_refinement(
  `!x x1 l. MEM x l /\ ~(x = x1) ==> MEM x (REMOVE x1 l)`,
(* {{{ Proof *)
[
  STRIP_TAC THEN STRIP_TAC;
  LIST_INDUCT_TAC;
  MESON_TAC[MEM];
  CASES_ON `x = h`;
  POP_ASSUM SUBST1_TAC;
  STRIP_TAC;
  ASM_REWRITE_TAC[REMOVE;LET_DEF;LET_END_DEF;COND_CLAUSES;MEM];
  STRIP_TAC;
  CLAIM `MEM x t`;
  ASM_MESON_TAC[MEM];
  STRIP_TAC;
  CLAIM `MEM x (REMOVE x1 t)`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  MATCH_MP_TAC MEM_REMOVE;
  FIRST_ASSUM MATCH_ACCEPT_TAC;
]);;
(* }}} *)


let LAST_SING = prove_by_refinement(
  `!h. LAST [h] = h`,
(* {{{ Proof *)

[
  MESON_TAC[LAST];
]);;

(* }}} *)

let LAST_CONS = prove_by_refinement(
  `!h t. ~(t = []) ==> (LAST (CONS h t) = LAST t)`,
(* {{{ Proof *)
[
  ASM_MESON_TAC[LAST];
]);;  
(* }}} *)


let LAST_CONS_CONS = prove_by_refinement(
  `!h1 h2 t. ~(t = []) ==> (LAST (CONS h1 (CONS h2 t)) = LAST (CONS h1 t))`,
(* {{{ Proof *)
[
  REWRITE_TAC[LAST;NOT_CONS_NIL];
  MESON_TAC[LAST;NOT_CONS_NIL;COND_CLAUSES];
]);;
(* }}} *)
  
let HD_APPEND = prove_by_refinement(
  `!h t l. HD (APPEND (CONS h t) l) = h`,
(* {{{ Proof *)
[
  ASM_MESON_TAC[HD;APPEND];
]);;
(* }}} *)

let LENGTH_0 = prove_by_refinement(
  `!l. (LENGTH l = 0) <=> (l = [])`,
(* {{{ Proof *)
[
  LIST_INDUCT_TAC;
  REWRITE_TAC[LENGTH];
  ASM_MESON_TAC[LENGTH;NOT_CONS_NIL;ARITH_RULE `~(0 = SUC n)`];
]);;
(* }}} *)

let LENGTH_1 = prove_by_refinement(
  `!l. (LENGTH l = 1) <=> ?x. l = [x]`,
(* {{{ Proof *)
[
  LIST_INDUCT_TAC;
  EQ_TAC;
  MESON_TAC[LENGTH;ARITH_RULE `~(1 = 0)`];
  MESON_TAC[NOT_CONS_NIL];
  EQ_TAC;
  REWRITE_TAC[LENGTH;ARITH_RULE `~(0 = 1)`];
  REWRITE_TAC[LENGTH];
  STRIP_TAC;
  CLAIM `LENGTH t = 0`;
  POP_ASSUM MP_TAC THEN ARITH_TAC;
  STRIP_TAC;
  CLAIM `t = []`;
  ASM_MESON_TAC[LENGTH_0];
  STRIP_TAC;
  ASM_REWRITE_TAC[];
  ASM_MESON_TAC[];
  STRIP_TAC;
  ASM_MESON_TAC[LENGTH;ONE];
]);;
(* }}} *)

let LIST_TRI = prove_by_refinement(
  `!p. (p = []) \/ (?x. p = [x:A]) \/ (?x y t. p = CONS x (CONS y t))`,
(* {{{ Proof *)
[
  STRIP_TAC;
  DISJ_CASES_TAC (ISPEC `p:A list` list_CASES);
  ASM_REWRITE_TAC[];
  POP_ASSUM MP_TAC THEN STRIP_TAC;
  DISJ_CASES_TAC (ISPEC `t:A list` list_CASES);  
  ASM_MESON_TAC[];
  ASM_MESON_TAC[];
]);;  
(* }}} *)

let LENGTH_PAIR = prove_by_refinement(
  `!p. (LENGTH p = 2) <=> ?h t. p = [h:A; t]`,
(* {{{ Proof *)
[
  STRIP_TAC THEN EQ_TAC;
  STRIP_TAC;
  MP_TAC (ISPEC `p:A list` list_CASES);
  STRIP_TAC;
  ASM_MESON_TAC[LENGTH_0;ARITH_RULE `~(2 = 0)`];
  MP_TAC (ISPEC `t:A list` list_CASES);
  STRIP_TAC;
  ASM_MESON_TAC[LENGTH_1;ARITH_RULE `~(1 = 2)`];
  MP_TAC (ISPEC `t':A list` list_CASES);  
  STRIP_TAC;
  EXISTS_TAC `h:A`;
  EXISTS_TAC `h':A`;
  ASM_MESON_TAC[];
  CLAIM `p = CONS h (CONS h' (CONS h'' t''))`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  CLAIM `2 < LENGTH p`; 
  POP_ASSUM SUBST1_TAC;
  REWRITE_TAC[LENGTH];
  ARITH_TAC;
  ASM_MESON_TAC[LT_REFL];
  STRIP_TAC;
  ASM_REWRITE_TAC[LENGTH];
  ARITH_TAC;
]);;
(* }}} *)

let LENGTH_SING = prove_by_refinement(
  `!p. (LENGTH p = 1) <=> ?h. p = [h:A]`,
(* {{{ Proof *)
[
  STRIP_TAC THEN EQ_TAC;
  STRIP_TAC;
  MP_TAC (ISPEC `p:A list` list_CASES);
  STRIP_TAC;
  ASM_MESON_TAC[LENGTH_0;ARITH_RULE `~(1 = 0)`];
  MP_TAC (ISPEC `t:A list` list_CASES);
  STRIP_TAC;
  EXISTS_TAC `h:A`;
  ASM_MESON_TAC[];
  CLAIM `p = CONS h (CONS h' t')`;
  ASM_MESON_TAC[];
  STRIP_TAC;
  CLAIM `1 < LENGTH p`; 
  POP_ASSUM SUBST1_TAC;
  REWRITE_TAC[LENGTH];
  ARITH_TAC;
  ASM_REWRITE_TAC[];
  ARITH_TAC;
  STRIP_TAC;
  ASM_REWRITE_TAC[LENGTH;];
  ARITH_TAC;
]);;
(* }}} *)

let TL_NIL = prove_by_refinement(
  `!l. ~(l = []) ==> ((TL l = []) <=> ?x. l = [x])`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC THEN EQ_TAC;
  CLAIM `?h t. l = CONS h t`;
  ASM_MESON_TAC[list_CASES];
  STRIP_TAC;
  ASM_REWRITE_TAC[TL];
  ASM_MESON_TAC !LIST_REWRITES;
  ASM_MESON_TAC !LIST_REWRITES;
]);;  
(* }}} *)

let LAST_TL = prove_by_refinement(
  `!l. ~(l = []) /\  ~(TL l = []) ==> (LAST (TL l) = LAST l)`,
(* {{{ Proof *)
[
  LIST_INDUCT_TAC;
  REWRITE_TAC[];
  REWRITE_TAC[TL;LAST];
  ASM_MESON_TAC[NOT_CONS_NIL];
]);;  
(* }}} *)

let LENGTH_TL = prove_by_refinement(
  `!l. ~(l = []) /\  ~(TL l = []) ==> (LENGTH (TL l) = PRE(LENGTH l))`,
(* {{{ Proof *)
[
  LIST_INDUCT_TAC;
  REWRITE_TAC[];
  REPEAT STRIP_TAC;
  LIST_SIMP_TAC;
  NUM_SIMP_TAC;
]);;
(* }}} *)

let LENGTH_NZ = prove_by_refinement(
 `!p. 0 < LENGTH p <=> ~(p = [])`,
(* {{{ Proof *)
[
  REPEAT STRIP_TAC;
  EQ_TAC;
  ASM_MESON_TAC[LENGTH;NOT_CONS_NIL;LT_REFL];
  REWRITE_TAC[LENGTH;NOT_CONS_NIL;LT_REFL;NOT_NIL];
  STRIP_TAC THEN ASM_REWRITE_TAC[];
  REWRITE_TAC[LENGTH];
  ARITH_TAC;
]);;
(* }}} *)