Permutation/permutation.ml

   1 (* ========================================================================= *)
   2 (*  Permuted lists and finite permutations.                                  *)
   3 (*                                                                           *)
   4 (*  Author: Marco Maggesi                                                    *)
   5 (*          University of Florence, Italy                                    *)
   6 (*          http://www.math.unifi.it/~maggesi/                               *)
   7 (*                                                                           *)
   8 (*          (c) Copyright, Marco Maggesi, 2005-2007                          *)
   9 (* ========================================================================= *)
  10
  11 needs "Permutation/permuted.ml";;
  12
  13 (* ------------------------------------------------------------------------- *)
  14 (*  Permutation that reverse a list.                                         *)
  15 (* ------------------------------------------------------------------------- *)
  16
  17 let REVPERM = define
  18   `REVPERM 0 = [] /\
  19    REVPERM (SUC n) = n :: REVPERM n`;;
  20
  21 let MEM_REVPERM = prove
  22   (`!n m. MEM m (REVPERM n) <=> m < n`,
  23    INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; MEM; LT]);;
  24
  25 let LIST_UNIQ_REVPERM = prove
  26   (`!n. LIST_UNIQ (REVPERM n)`,
  27    INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; LIST_UNIQ; MEM_REVPERM]
  28    THEN ARITH_TAC);;
  29
  30 let DELETE1_REVPERM = prove
  31   (`!n. DELETE1 n (REVPERM (SUC n)) = REVPERM n`,
  32    INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; DELETE1; MEM]);;
  33
  34 let COUNT_REVPERM = prove
  35   (`!n i. COUNT i (REVPERM n) = if i < n then 1 else 0`,
  36    INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; COUNT] THEN ARITH_TAC);;
  37
  38 let SET_OF_LIST_REVPERM = prove
  39   (`!n. set_of_list (REVPERM n) = {m | m < n}`,
  40    INDUCT_TAC THEN
  41    ASM_REWRITE_TAC [REVPERM; set_of_list; LT; EMPTY_GSPEC; EXTENSION;
  42                     IN_INSERT; IN_ELIM_THM; NOT_IN_EMPTY]);;
  43
  44 (* ------------------------------------------------------------------------- *)
  45 (*  Permutations.                                                            *)
  46 (* ------------------------------------------------------------------------- *)
  47
  48 let PERMUTATION = new_definition
  49   `!l. PERMUTATION l <=> REVPERM (LENGTH l) PERMUTED l`;;
  50
  51 let PERMUTATION_NIL = prove
  52   (`PERMUTATION []`,
  53    REWRITE_TAC [PERMUTATION; LENGTH; REVPERM; PERMUTED_RULES]);;
  54
  55 let PERMUTATION_LIST_UNIQ = prove
  56   (`!l. PERMUTATION l ==> LIST_UNIQ l`,
  57    MESON_TAC [PERMUTATION; PERMUTED_LIST_UNIQ; LIST_UNIQ_REVPERM]);;
  58
  59 let PERMUTATION_MEM = prove
  60   (`!l. PERMUTATION l ==> (!i. MEM i l <=> i < LENGTH l)`,
  61    REWRITE_TAC [PERMUTATION] THEN
  62    MESON_TAC [MEM_REVPERM; PERMUTED_MEM]);;
  63
  64 let PERMUTATION_COUNT = prove
  65   (`!l. PERMUTATION l <=> (!x. COUNT x l = if x < LENGTH l then 1 else 0)`,
  66    REWRITE_TAC [PERMUTATION; PERMUTED_COUNT; COUNT_REVPERM] THEN
  67    MESON_TAC[]);;
  68
  69 let LIST_UNIQ_PERMUTED_SET_OF_LIST = prove
  70   (`!l1 l2. LIST_UNIQ l1 /\ LIST_UNIQ l2
  71            ==> (l1 PERMUTED l2 <=> set_of_list l1 = set_of_list l2)`,
  72    REWRITE_TAC [LIST_UNIQ_COUNT] THEN REPEAT STRIP_TAC THEN
  73    REWRITE_TAC [EXTENSION; IN_SET_OF_LIST; PERMUTED_COUNT; MEM_COUNT] THEN
  74    ASM_REWRITE_TAC [] THEN MESON_TAC []);;
  75
  76 let PERMUTATION_SET_OF_LIST = prove
  77   (`!l. PERMUTATION l <=> set_of_list l = {n | n < LENGTH l}`,
  78    GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
  79    [REWRITE_TAC [GSYM SET_OF_LIST_REVPERM] THEN
  80     ASM_MESON_TAC [LIST_UNIQ_PERMUTED_SET_OF_LIST; PERMUTATION;
  81                    PERMUTED_LIST_UNIQ; LIST_UNIQ_REVPERM];
  82     REWRITE_TAC [PERMUTATION] THEN ASSERT_TAC `LIST_UNIQ (l:num list)` THENL
  83     [REWRITE_TAC [LIST_UNIQ_CARD_LENGTH] THEN FIRST_X_ASSUM SUBST1_TAC THEN
  84      REWRITE_TAC [CARD_NUMSEG_LT];
  85      ASM_SIMP_TAC [SET_OF_LIST_REVPERM; LIST_UNIQ_REVPERM;
  86                    LIST_UNIQ_PERMUTED_SET_OF_LIST]]]);;
  87
  88 let MEM_PERMUTATION = prove
  89   (`!l. (!n. n < LENGTH l ==> MEM n l) ==> PERMUTATION l`,
  90    REPEAT STRIP_TAC THEN REWRITE_TAC [PERMUTATION_SET_OF_LIST] THEN
  91    MATCH_MP_TAC (GSYM CARD_SUBSET_LE) THEN
  92    REWRITE_TAC [FINITE_SET_OF_LIST; CARD_NUMSEG_LT; CARD_LENGTH] THEN
  93    ASM_SIMP_TAC [SUBSET; IN_ELIM_THM; IN_SET_OF_LIST]);;
  94
  95 let LIST_UNIQ_MEM_PERMUTATION = prove
  96   (`!l. LIST_UNIQ l /\ (!n. MEM n l ==> n < LENGTH l) ==> PERMUTATION l`,
  97    REWRITE_TAC [LIST_UNIQ_CARD_LENGTH; PERMUTATION_SET_OF_LIST] THEN
  98    REPEAT STRIP_TAC THEN MATCH_MP_TAC CARD_SUBSET_LE THEN
  99    ASM_REWRITE_TAC [FINITE_NUMSEG_LT; SUBSET; IN_ELIM_THM; IN_SET_OF_LIST;
 100                     CARD_NUMSEG_LT; LE_REFL]);;
 101
 102 let PERMUTATION_UNIQ_LT = prove
 103   (`!l. PERMUTATION l <=> LIST_UNIQ l /\ (!n. MEM n l ==> n < LENGTH l)`,
 104    MESON_TAC [PERMUTATION_LIST_UNIQ; PERMUTATION_MEM;
 105               LIST_UNIQ_MEM_PERMUTATION]);;