(* ========================================================================= *)
(*  Permuted lists and finite permutations.                                  *)
(*                                                                           *)
(*  Author: Marco Maggesi                                                    *)
(*          University of Florence, Italy                                    *)
(*          http://www.math.unifi.it/~maggesi/                               *)
(*                                                                           *)
(*          (c) Copyright, Marco Maggesi, 2005-2007                          *)
(* ========================================================================= *)

needs "Permutation/permuted.ml";;

(* ------------------------------------------------------------------------- *)
(*  Permutation that reverse a list.                                         *)
(* ------------------------------------------------------------------------- *)


let REVPERM = define
  `REVPERM 0 = [] /\
   REVPERM (SUC n) = n :: REVPERM n`;;


let MEM_REVPERM = 
prove
  (`!n m. MEM m (REVPERM n) <=> m < n`,

   INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; MEM; LT]);;


let LIST_UNIQ_REVPERM = 
prove
  (`!n. LIST_UNIQ (REVPERM n)`,

   INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; LIST_UNIQ; MEM_REVPERM]
   THEN ARITH_TAC);;


let DELETE1_REVPERM = 
prove
  (`!n. DELETE1 n (REVPERM (SUC n)) = REVPERM n`,

   INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; DELETE1; MEM]);;


let COUNT_REVPERM = 
prove
  (`!n i. COUNT i (REVPERM n) = if i < n then 1 else 0`,

   INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; COUNT] THEN ARITH_TAC);;


let SET_OF_LIST_REVPERM = 
prove
  (`!n. set_of_list (REVPERM n) = {m | m < n}`,

   INDUCT_TAC THEN
   ASM_REWRITE_TAC [REVPERM; set_of_list; LT; EMPTY_GSPEC; EXTENSION;
                    IN_INSERT; IN_ELIM_THM; NOT_IN_EMPTY]);;

(* ------------------------------------------------------------------------- *)
(*  Permutations.                                                            *)
(* ------------------------------------------------------------------------- *)


let PERMUTATION = new_definition
  `!l. PERMUTATION l <=> REVPERM (LENGTH l) PERMUTED l`;;


let PERMUTATION_NIL = 
prove
  (`PERMUTATION []`,

   REWRITE_TAC [PERMUTATION; LENGTH; REVPERM; PERMUTED_RULES]);;


let PERMUTATION_LIST_UNIQ = 
prove
  (`!l. PERMUTATION l ==> LIST_UNIQ l`,


let PERMUTATION_MEM = 
prove
  (`!l. PERMUTATION l ==> (!i. MEM i l <=> i < LENGTH l)`,

   REWRITE_TAC [PERMUTATION] THEN
   MESON_TAC [MEM_REVPERM; PERMUTED_MEM]);;


let PERMUTATION_COUNT = 
prove
  (`!l. PERMUTATION l <=> (!x. COUNT x l = if x < LENGTH l then 1 else 0)`,

   REWRITE_TAC [PERMUTATION; PERMUTED_COUNT; COUNT_REVPERM] THEN
   MESON_TAC[]);;


let LIST_UNIQ_PERMUTED_SET_OF_LIST = 
prove
  (`!l1 l2. LIST_UNIQ l1 /\ LIST_UNIQ l2
           ==> (l1 PERMUTED l2 <=> set_of_list l1 = set_of_list l2)`,

   REWRITE_TAC [LIST_UNIQ_COUNT] THEN REPEAT STRIP_TAC THEN
   REWRITE_TAC [EXTENSION; IN_SET_OF_LIST; PERMUTED_COUNT; MEM_COUNT] THEN
   ASM_REWRITE_TAC [] THEN MESON_TAC []);;


let PERMUTATION_SET_OF_LIST = 
prove
  (`!l. PERMUTATION l <=> set_of_list l = {n | n < LENGTH l}`,

   GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
   [REWRITE_TAC [GSYM SET_OF_LIST_REVPERM] THEN
    ASM_MESON_TAC [LIST_UNIQ_PERMUTED_SET_OF_LIST; PERMUTATION;
                   PERMUTED_LIST_UNIQ; LIST_UNIQ_REVPERM];
    REWRITE_TAC [PERMUTATION] THEN ASSERT_TAC `LIST_UNIQ (l:num list)` THENL
    [REWRITE_TAC [LIST_UNIQ_CARD_LENGTH] THEN FIRST_X_ASSUM SUBST1_TAC THEN
     REWRITE_TAC [CARD_NUMSEG_LT];
     ASM_SIMP_TAC [SET_OF_LIST_REVPERM; LIST_UNIQ_REVPERM;
                   LIST_UNIQ_PERMUTED_SET_OF_LIST]]]);;


let MEM_PERMUTATION = 
prove
  (`!l. (!n. n < LENGTH l ==> MEM n l) ==> PERMUTATION l`,

   REPEAT STRIP_TAC THEN REWRITE_TAC [PERMUTATION_SET_OF_LIST] THEN
   MATCH_MP_TAC (GSYM CARD_SUBSET_LE) THEN
   REWRITE_TAC [FINITE_SET_OF_LIST; CARD_NUMSEG_LT; CARD_LENGTH] THEN
   ASM_SIMP_TAC [SUBSET; IN_ELIM_THM; IN_SET_OF_LIST]);;


let LIST_UNIQ_MEM_PERMUTATION = 
prove
  (`!l. LIST_UNIQ l /\ (!n. MEM n l ==> n < LENGTH l) ==> PERMUTATION l`,

   REWRITE_TAC [LIST_UNIQ_CARD_LENGTH; PERMUTATION_SET_OF_LIST] THEN
   REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_SUBSET_LE THEN
   ASM_REWRITE_TAC [FINITE_NUMSEG_LT; SUBSET; IN_ELIM_THM; IN_SET_OF_LIST;
                    CARD_NUMSEG_LT; LE_REFL]);;


let PERMUTATION_UNIQ_LT = 
prove
  (`!l. PERMUTATION l <=> LIST_UNIQ l /\ (!n. MEM n l ==> n < LENGTH l)`,