(* ========================================================================= *)
(*  More definitions and theorems and tactics about lists.                   *)
(*                                                                           *)
(*  Author: Marco Maggesi                                                    *)
(*          University of Florence, Italy                                    *)
(*          http://www.math.unifi.it/~maggesi/                               *)
(*                                                                           *)
(*          (c) Copyright, Marco Maggesi, 2005-2007                          *)
(* ========================================================================= *)

parse_as_infix ("::",(23,"right"));;
override_interface("::",`CONS`);;

(* ------------------------------------------------------------------------- *)
(*  Some handy tactics.                                                      *)
(* ------------------------------------------------------------------------- *)

let ASSERT_TAC tm = SUBGOAL_THEN tm ASSUME_TAC;;

let SUFFICE_TAC thl tm =
  SUBGOAL_THEN tm (fun th -> MESON_TAC (th :: thl));;

let LIST_CASES_TAC =
  
let th = 
prove (`!P. P [] /\ (!h t. P (h :: t)) ==> !l. P l`,
GEN_TAC THEN STRIP_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC []) in MATCH_MP_TAC th THEN CONJ_TAC THENL [ALL_TAC; GEN_TAC THEN GEN_TAC];;
(* ------------------------------------------------------------------------- *) (* Occasionally useful stuff. *) (* ------------------------------------------------------------------------- *)
let NULL_EQ_NIL = 
prove (`!l. NULL l <=> l = []`,
LIST_CASES_TAC THEN REWRITE_TAC [NULL; NOT_CONS_NIL]);;
let NULL_LENGTH = 
prove (`!l. NULL l <=> LENGTH l = 0`,
LIST_CASES_TAC THEN REWRITE_TAC [NULL; LENGTH; NOT_SUC]);;
let LENGTH_FILTER_LE = 
prove (`!f l:A list. LENGTH (FILTER f l) <= LENGTH l`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [FILTER; LENGTH; LE_0] THEN COND_CASES_TAC THEN ASM_SIMP_TAC [LENGTH; LE_SUC; ARITH_RULE `n<=m ==> n<= SUC m`]);;
(* ------------------------------------------------------------------------- *) (* Well-founded induction on lists. *) (* ------------------------------------------------------------------------- *)
let list_WF = 
prove (`!P. (!l. (!l'. LENGTH l' < LENGTH l ==> P l') ==> P l) ==> (!l:A list. P l)`,
MP_TAC (ISPEC `LENGTH:A list->num` WF_MEASURE) THEN REWRITE_TAC [WF_IND; MEASURE]);;
(* ------------------------------------------------------------------------- *) (* Delete one element from a list. *) (* ------------------------------------------------------------------------- *)
let DELETE1 = define
  `(!x. DELETE1 x [] = []) /\
   (!x h t. DELETE1 x (h :: t) = if x = h then t
                                          else h :: DELETE1 x t)`;;
let DELETE1_ID = 
prove (`!x l. ~MEM x l ==> DELETE1 x l = l`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC [NOT_CONS_NIL; CONS_11]);;
let DELETE1_APPEND = 
prove (`!x l1 l2. DELETE1 x (APPEND l1 l2) = if MEM x l1 then APPEND (DELETE1 x l1) l2 else APPEND l1 (DELETE1 x l2)`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [APPEND; DELETE1; MEM] THEN GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM; APPEND] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[]);;
let FILTER_DELETE1 = 
prove (`!P x l. FILTER P (DELETE1 x l) = if P x then DELETE1 x (FILTER P l) else FILTER P l`,
GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REPEAT (REWRITE_TAC [DELETE1; FILTER] THEN COND_CASES_TAC) THEN ASM_MESON_TAC []);;
let LENGTH_DELETE1 = 
prove (`!l x:A. LENGTH (DELETE1 x l) = if MEM x l then PRE (LENGTH l) else LENGTH l`,
LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; LENGTH; DELETE1] THEN GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[PRE; LENGTH] THEN COND_CASES_TAC THEN REWRITE_TAC [ARITH_RULE `SUC (PRE n)=n <=> ~(n=0)`; LENGTH_EQ_NIL] THEN ASM_MESON_TAC [MEM]);;
let MEM_DELETE1_MEM_IMP = 
prove (`!h t x. MEM x (DELETE1 h t) ==> MEM x t`,
GEN_TAC THEN LIST_INDUCT_TAC THEN GEN_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN COND_CASES_TAC THEN REWRITE_TAC [MEM] THEN STRIP_TAC THEN ASM_SIMP_TAC []);;
let NOT_MEM_DELETE1 = 
prove (`!t h x. ~MEM x t ==> ~MEM x (DELETE1 h t)`,
LIST_INDUCT_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN COND_CASES_TAC THEN REWRITE_TAC [MEM; DE_MORGAN_THM] THEN STRIP_TAC THEN ASM_SIMP_TAC []);;
let MEM_DELETE1 = 
prove (`!l x y:A. MEM x l /\ ~(x = y) ==> MEM x (DELETE1 y l)`,
LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN GEN_TAC THEN GEN_TAC THEN COND_CASES_TAC THENL [EXPAND_TAC "h" THEN MESON_TAC []; REWRITE_TAC [MEM] THEN ASM_MESON_TAC []]);;
let ALL_DELETE1_ALL_IMP = 
prove (`!P x l. P x /\ ALL P (DELETE1 x l) ==> ALL P l`,
GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [ALL; DELETE1] THEN COND_CASES_TAC THEN ASM_SIMP_TAC [ALL]);;
(* ------------------------------------------------------------------------- *) (* Counting occurrences of a given element in a list. *) (* ------------------------------------------------------------------------- *)
let COUNT = define
  `(!x. COUNT x [] = 0) /\
   (!x h t. COUNT x (CONS h t) = if x=h then SUC (COUNT x t) else COUNT x t)`;;
let COUNT_LENGTH_FILTER = 
prove (`!x l. COUNT x l = LENGTH (FILTER ((=) x) l)`,
GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [COUNT; FILTER; LENGTH] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC [LENGTH]);;
let COUNT_FILTER = 
prove (`!P x l. COUNT x (FILTER P l) = if P x then COUNT x l else 0`,
GEN_TAC THEN GEN_TAC THEN LIST_INDUCT_TAC THEN REPEAT (ASM_REWRITE_TAC [COUNT; FILTER] THEN COND_CASES_TAC) THEN ASM_MESON_TAC []);;
let COUNT_APPEND = 
prove (`!x l1 l2. COUNT x (APPEND l1 l2) = COUNT x l1 + COUNT x l2`,
let COUNT_LE_LENGTH = 
prove (`!x l. COUNT x l <= LENGTH l`,
GEN_TAC THEN LIST_INDUCT_TAC THEN ASM_REWRITE_TAC [COUNT; LENGTH; LE_REFL] THEN COND_CASES_TAC THEN ASM_SIMP_TAC [LE_SUC; ARITH_RULE `n<=m ==> n <= SUC m`]);;
let COUNT_ZERO = 
prove (`!x l. COUNT x l = 0 <=> ~MEM x l`,
GEN_TAC THEN REWRITE_TAC [COUNT_LENGTH_FILTER; LENGTH_EQ_NIL] THEN LIST_INDUCT_TAC THEN REWRITE_TAC [FILTER; MEM] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC [NOT_CONS_NIL]);;
let MEM_COUNT = 
prove (`!x l. MEM x l <=> ~(COUNT x l = 0)`,
MESON_TAC [COUNT_ZERO]);;
let COUNT_DELETE1 = 
prove (`!y x l. COUNT y (DELETE1 (x:A) l) = if y=x /\ MEM x l then PRE (COUNT y l) else COUNT y l`,
REWRITE_TAC [COUNT_LENGTH_FILTER; FILTER_DELETE1] THEN REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[MEM_FILTER; LENGTH_DELETE1]);;
(* ------------------------------------------------------------------------- *) (* Duplicates in a list. *) (* ------------------------------------------------------------------------- *) let LIST_UNIQ_RULES, LIST_UNIQ_INDUCT, LIST_UNIQ_CASES = new_inductive_definition `LIST_UNIQ [] /\ (!x xs. LIST_UNIQ xs /\ ~MEM x xs ==> LIST_UNIQ (x :: xs))`;;
let LIST_UNIQ = 
prove (`LIST_UNIQ [] /\ (!x. LIST_UNIQ [x]) /\ (!x xs. LIST_UNIQ (x :: xs) <=> ~MEM x xs /\ LIST_UNIQ xs)`,
SIMP_TAC [LIST_UNIQ_RULES; MEM] THEN REPEAT GEN_TAC THEN EQ_TAC THENL [ONCE_REWRITE_TAC [ISPEC `h :: t` LIST_UNIQ_CASES] THEN REWRITE_TAC [CONS_11; NOT_CONS_NIL] THEN DISCH_THEN (CHOOSE_THEN CHOOSE_TAC) THEN ASM_REWRITE_TAC []; SIMP_TAC [LIST_UNIQ_RULES]]);;
(* !!! forse e' meglio con IMP? *) (* Magari LIST_UNIQ_COUNT + COUNT_LIST_UNIQ *)
let LIST_UNIQ_COUNT = 
prove (`!l. LIST_UNIQ l <=> (!x:A. COUNT x l = if MEM x l then 1 else 0)`,
let IFF_EXPAND = MESON [] `(p <=> q) <=> (p ==> q) /\ (q ==> p)` in REWRITE_TAC [IFF_EXPAND; FORALL_AND_THM] THEN CONJ_TAC THENL [MATCH_MP_TAC LIST_UNIQ_INDUCT THEN REWRITE_TAC [COUNT; MEM] THEN REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ONE]; LIST_INDUCT_TAC THEN REWRITE_TAC [LIST_UNIQ; COUNT; MEM] THEN DISCH_TAC THEN FIRST_ASSUM (MP_TAC o SPEC `h:A`) THEN SIMP_TAC [MEM_COUNT; ONE; SUC_INJ] THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN FIRST_ASSUM (MP_TAC o SPEC `x:A`) THEN REWRITE_TAC [MEM_COUNT] THEN ARITH_TAC]);;
let LIST_UNIQ_DELETE1 = 
prove (`!l x. LIST_UNIQ l ==> LIST_UNIQ (DELETE1 x l)`,
LIST_INDUCT_TAC THEN GEN_TAC THEN REWRITE_TAC [LIST_UNIQ; DELETE1] THEN STRIP_TAC THEN COND_CASES_TAC THEN ASM_SIMP_TAC [LIST_UNIQ; NOT_MEM_DELETE1]);;
let DELETE1_LIST_UNIQ = 
prove (`!l x:A. ~MEM x (DELETE1 x l) /\ LIST_UNIQ (DELETE1 x l) ==> LIST_UNIQ l`,
LIST_INDUCT_TAC THEN REWRITE_TAC [LIST_UNIQ; DELETE1; MEM] THEN GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC [MEM; LIST_UNIQ] THEN STRIP_TAC THEN CONJ_TAC THENL [ASM_MESON_TAC [MEM_DELETE1]; FIRST_X_ASSUM MATCH_MP_TAC THEN EXISTS_TAC `x:A` THEN ASM_REWRITE_TAC []]);;
let LIST_UNIQ_APPEND = 
prove (`!l m. LIST_UNIQ (APPEND l m) <=> LIST_UNIQ l /\ LIST_UNIQ m /\ !x. ~(MEM x l /\ MEM x m)`,
LIST_INDUCT_TAC THEN ASM_REWRITE_TAC[APPEND; LIST_UNIQ; MEM; MEM_APPEND] THEN MESON_TAC[]);;
(* ------------------------------------------------------------------------- *) (* Lists and finite sets. *) (* ------------------------------------------------------------------------- *)
let CARD_LENGTH = 
prove (`!l:A list. CARD (set_of_list l) <= LENGTH l`,
LIST_INDUCT_TAC THEN SIMP_TAC [set_of_list; CARD_CLAUSES; LENGTH; FINITE_SET_OF_LIST; ARITH] THEN COND_CASES_TAC THENL [MATCH_MP_TAC LE_TRANS THEN EXISTS_TAC `LENGTH (t:A list)` THEN ASM_REWRITE_TAC [] THEN ARITH_TAC; ASM_REWRITE_TAC [LE_SUC]]);;
let LIST_UNIQ_CARD_LENGTH = 
prove (`!l:A list. LIST_UNIQ l <=> CARD (set_of_list l) = LENGTH l`,
LIST_INDUCT_TAC THEN SIMP_TAC [LIST_UNIQ; set_of_list; FINITE_SET_OF_LIST; LENGTH; CARD_CLAUSES; IN_SET_OF_LIST] THEN FIRST_X_ASSUM SUBST1_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[SUC_INJ] THEN MP_TAC (SPEC `t:A list` CARD_LENGTH) THEN ARITH_TAC);;
let LIST_UNIQ_LIST_OF_SET = 
prove (`!s. FINITE s ==> LIST_UNIQ(list_of_set s)`,