(* =========================================================== *)
(* Additional list definitions and theorems                    *)
(* Author: Alexey Solovyev                                     *)
(* Date: 2012-10-27                                            *)
(* =========================================================== *)

module More_list = struct

(* definitions *)
let REVERSE_TABLE  = define `(REVERSE_TABLE (f:num->A) 0 = []) /\
   (REVERSE_TABLE f (SUC i) = CONS (f i)  ( REVERSE_TABLE f i))`;;
 
  
let TABLE = new_definition `!(f:num->A) k. TABLE f k = REVERSE (REVERSE_TABLE f k)`;;

let l_seq = new_definition `l_seq n m = TABLE (\i. n + i) ((m + 1) - n)`;;

(* lemmas *)
let LENGTH_REVERSE_TABLE = 
prove(`!(f:num->A) n. LENGTH (REVERSE_TABLE f n) = n`,

   GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[REVERSE_TABLE; LENGTH]);;

let LENGTH_REVERSE = 
prove(`!(l:(A)list). LENGTH (REVERSE l) = LENGTH l`,

   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[REVERSE] THEN
     REPEAT STRIP_TAC THEN
     ASM_REWRITE_TAC[LENGTH_APPEND; LENGTH] THEN
     ARITH_TAC);;

let LENGTH_TABLE = 
prove(`!(f:num->A) n. LENGTH (TABLE f n) = n`,

   REWRITE_TAC[TABLE; LENGTH_REVERSE; LENGTH_REVERSE_TABLE]);;

let EL_TABLE = 
prove(`!(f:num->A) n i. i < n ==> EL i (TABLE f n) = f i`,

   REPEAT GEN_TAC THEN SPEC_TAC (`n:num`, `n:num`) THEN
     INDUCT_TAC THENL [ ARITH_TAC; ALL_TAC ] THEN
     REWRITE_TAC[TABLE; REVERSE_TABLE; REVERSE; EL_APPEND] THEN
     REWRITE_TAC[GSYM TABLE; LENGTH_TABLE] THEN
     DISCH_TAC THEN COND_CASES_TAC THENL
     [
       FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[];
       ALL_TAC
     ] THEN
     SUBGOAL_THEN `i = n:num` (fun th -> REWRITE_TAC[th]) THENL
     [
       POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
	 ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[ARITH_RULE `n - n = 0`; EL; HD]);;

let LIST_EL_EQ = 
prove(`!ul vl:(A)list. ul = vl <=> 
               (LENGTH ul = LENGTH vl /\ (!j. j < LENGTH ul ==> EL j ul = EL j vl))`,

   REPEAT STRIP_TAC THEN
     EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
     POP_ASSUM MP_TAC THEN POP_ASSUM MP_TAC THEN
     SPEC_TAC (`vl:(A)list`, `vl:(A)list`) THEN SPEC_TAC (`ul:(A)list`, `ul:(A)list`) THEN
     LIST_INDUCT_TAC THEN LIST_INDUCT_TAC THEN SIMP_TAC[LENGTH_EQ_NIL; EQ_SYM_EQ; LENGTH; ARITH_RULE `~(0 = SUC a)`] THEN
     POP_ASSUM (fun th -> ALL_TAC) THEN
     REWRITE_TAC[ARITH_RULE `SUC a = SUC b <=> a = b`] THEN
     REPEAT STRIP_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `t':(A)list`) THEN
     ASM_REWRITE_TAC[] THEN
     ANTS_TAC THENL
     [
       REPEAT STRIP_TAC THEN
	 FIRST_X_ASSUM (MP_TAC o SPEC `SUC j`) THEN
	 ASM_REWRITE_TAC[ARITH_RULE `SUC a < SUC b <=> a < b`; EL; TL];
       ALL_TAC
     ] THEN
     DISCH_TAC THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `0`) THEN
     ASM_SIMP_TAC[ARITH_RULE `0 < SUC a`; EL; HD]);;


let LENGTH_L_SEQ = 
prove(`LENGTH (l_seq n m) = (m + 1) - n`,
 REWRITE_TAC[l_seq; LENGTH_TABLE]);;

let EL_L_SEQ = 
prove(`!i m n. i < (m + 1) - n ==> EL i (l_seq n m) = n + i`,

  REWRITE_TAC[l_seq] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC EL_TABLE THEN ASM_REWRITE_TAC[]);;
  
let L_SEQ_NIL = 
prove(`!n m. l_seq n m = [] <=> (m < n)`,

  GEN_TAC THEN GEN_TAC THEN REWRITE_TAC[GSYM LENGTH_EQ_NIL; LENGTH_L_SEQ] THEN ARITH_TAC);;
  
let L_SEQ_NN = 
prove(`!n. l_seq n n = [n]`,

  GEN_TAC THEN REWRITE_TAC[l_seq; ARITH_RULE `(n + 1) - n = 1`; ONE; TABLE; REVERSE_TABLE; REVERSE] THEN
    REWRITE_TAC[APPEND; ADD_0]);;

let L_SEQ_CONS = 
prove(`!n m. n <= m ==> l_seq n m = CONS n (l_seq (n + 1) m)`,

  REPEAT STRIP_TAC THEN
    REWRITE_TAC[LIST_EL_EQ; LENGTH_L_SEQ; LENGTH] THEN CONJ_TAC THENL
    [
      ASM_ARITH_TAC;
      ALL_TAC
    ] THEN
    INDUCT_TAC THENL
    [
      ASM_SIMP_TAC[EL_L_SEQ] THEN ASM_REWRITE_TAC[EL; HD] THEN ARITH_TAC;
      DISCH_TAC THEN
	ASM_SIMP_TAC[EL_L_SEQ] THEN ASM_REWRITE_TAC[EL; TL] THEN
	MP_TAC (SPECL [`j:num`; `m:num`; `n + 1`] EL_L_SEQ) THEN ANTS_TAC THENL
	[
	  ASM_ARITH_TAC;
	  ALL_TAC
	] THEN
	DISCH_THEN (fun th -> REWRITE_TAC[th]) THEN ARITH_TAC
    ]);;


let LENGTH_BUTLAST = 
prove(`!l. LENGTH (BUTLAST l) = LENGTH l - 1`,

   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[BUTLAST; LENGTH; ARITH] THEN REPEAT STRIP_TAC THEN
     COND_CASES_TAC THEN ASM_REWRITE_TAC[LENGTH; ARITH] THEN
     POP_ASSUM MP_TAC THEN REWRITE_TAC[GSYM LENGTH_EQ_NIL] THEN
     ARITH_TAC);;

let EL_BUTLAST = 
prove(`!(l:(A)list) i. i < LENGTH l - 1 ==> EL i (BUTLAST l) = EL i l`,

   MATCH_MP_TAC list_INDUCT THEN REWRITE_TAC[BUTLAST; LENGTH] THEN REPEAT STRIP_TAC THEN
     COND_CASES_TAC THENL
     [
       UNDISCH_TAC `i < SUC (LENGTH (a1:(A)list)) - 1` THEN
	 ASM_REWRITE_TAC[LENGTH] THEN ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[EL_CONS] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
     FIRST_X_ASSUM (MP_TAC o SPEC `i - 1`) THEN
     ANTS_TAC THENL
     [
       ASM_ARITH_TAC;
       ALL_TAC
     ] THEN
     REWRITE_TAC[]);;

end;;