Permutation/permuted.ml

   1 (* ========================================================================= *)
   2 (*  Permuted lists.                                                          *)
   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/morelist.ml";;
  12
  13 parse_as_infix("PERMUTED",(12,"right"));;
  14
  15 (* ------------------------------------------------------------------------- *)
  16 (*  Permuted lists.                                                          *)
  17 (* ------------------------------------------------------------------------- *)
  18
  19 let PERMUTED_RULES, PERMUTED_INDUCT, PERMUTED_CASES =
  20   new_inductive_definition
  21   `[] PERMUTED [] /\
  22    (!h t1 t2. t1 PERMUTED t2 ==> h :: t1 PERMUTED h :: t2) /\
  23    (!l1 l2 l3. l1 PERMUTED l2 /\ l2 PERMUTED l3 ==> l1 PERMUTED l3) /\
  24    (!x y t. x :: y :: t PERMUTED y :: x :: t)`;;
  25
  26 let PERMUTED_INDUCT_STRONG =
  27   derive_strong_induction(PERMUTED_RULES,PERMUTED_INDUCT);;
  28
  29 let PERMUTED_RFL = prove
  30   (`!l. l PERMUTED l`,
  31    LIST_INDUCT_TAC THEN ASM_SIMP_TAC [PERMUTED_RULES]);;
  32
  33 let PERMUTED_SYM = prove
  34   (`!(xs:A list) l2. xs PERMUTED l2 <=> l2 PERMUTED xs`,
  35    SUFFICE_TAC []
  36      `!(xs:A list) l2. xs PERMUTED l2 ==> l2 PERMUTED xs` THEN
  37    MATCH_MP_TAC PERMUTED_INDUCT THEN ASM_MESON_TAC [PERMUTED_RULES]);;
  38
  39 let PERMUTED_TRS = prove
  40   (`!xs l2 l3. xs PERMUTED l2 /\ l2 PERMUTED l3 ==> xs PERMUTED l3`,
  41    MESON_TAC [PERMUTED_RULES]);;
  42
  43 let PERMUTED_TRS_TAC tm : tactic =
  44   MATCH_MP_TAC PERMUTED_TRS THEN EXISTS_TAC tm THEN CONJ_TAC ;;
  45
  46 let PERMUTED_TAIL_IMP = prove
  47   (`!h t1 t2. t1 PERMUTED t2 ==> h :: t1 PERMUTED h :: t2`,
  48    SIMP_TAC [PERMUTED_RULES]);;
  49
  50 let PERMUTED_MAP = prove
  51   (`!f l1 l2. l1 PERMUTED l2 ==>  MAP f l1 PERMUTED MAP f l2`,
  52    GEN_TAC THEN MATCH_MP_TAC PERMUTED_INDUCT THEN
  53    REWRITE_TAC [MAP; PERMUTED_RULES]);;
  54
  55 let PERMUTED_LENGTH = prove
  56   (`!l1 l2. l1 PERMUTED l2 ==> LENGTH l1 = LENGTH l2`,
  57    MATCH_MP_TAC PERMUTED_INDUCT THEN
  58    REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [LENGTH]);;
  59
  60 let PERMUTED_SWAP_HEAD = prove
  61   (`!a b l. a :: b :: l PERMUTED b :: a :: l`,
  62    REWRITE_TAC [PERMUTED_RULES]);;
  63
  64 let PERMUTED_MEM = prove
  65   (`!(a:A) l1 l2. l1 PERMUTED l2 ==> (MEM a l1 <=> MEM a l2)`,
  66    GEN_TAC THEN MATCH_MP_TAC PERMUTED_INDUCT THEN
  67    REWRITE_TAC [MEM] THEN REPEAT STRIP_TAC THEN
  68    ASM_REWRITE_TAC[] THEN MESON_TAC[]);;
  69
  70 let PERMUTED_ALL = prove
  71   (`!P xs ys. xs PERMUTED ys ==> (ALL P xs <=> ALL P ys)`,
  72    GEN_TAC THEN MATCH_MP_TAC PERMUTED_INDUCT THEN
  73    REWRITE_TAC [ALL] THEN REPEAT STRIP_TAC THEN
  74    ASM_SIMP_TAC[] THEN MESON_TAC[]);;
  75
  76 let PERMUTED_NIL_EQ_NIL = prove
  77   (`(!l:A list. [] PERMUTED l <=> l = []) /\
  78     (!l:A list. l PERMUTED [] <=> l = [])`,
  79    SUFFICE_TAC [PERMUTED_SYM] `!l:A list. [] PERMUTED l <=> l = []` THEN
  80    LIST_CASES_TAC THEN ASM_REWRITE_TAC [NOT_CONS_NIL; PERMUTED_RFL] THEN
  81    MESON_TAC [PERMUTED_LENGTH; LENGTH; NOT_SUC]);;
  82
  83 let PERMUTED_SINGLETON = prove
  84   (`(!(x:A) l. [x] PERMUTED l <=> l = [x]) /\
  85     (!(x:A) l. l PERMUTED [x] <=> l = [x])`,
  86    SUFFICE_TAC [PERMUTED_LENGTH; PERMUTED_RFL]
  87      `!l1 l2. l1 PERMUTED l2 ==> LENGTH l1 = LENGTH l2 /\
  88                                  (!x. l1 = [x:A] <=> l2 = [x])` THEN
  89    MATCH_MP_TAC PERMUTED_INDUCT THEN
  90    SIMP_TAC [PERMUTED_NIL_EQ_NIL; LENGTH; NOT_CONS_NIL; CONS_11;
  91              SUC_INJ; GSYM LENGTH_EQ_NIL]);;
  92
  93 let PERMUTED_CONS_DELETE1 = prove
  94   (`!(a:A) l. MEM a l ==> l PERMUTED a :: DELETE1 a l`,
  95    GEN_TAC THEN LIST_INDUCT_TAC THEN REWRITE_TAC [MEM; DELETE1] THEN
  96    COND_CASES_TAC THEN
  97    ASM_MESON_TAC [PERMUTED_RFL; PERMUTED_TAIL_IMP; PERMUTED_SWAP_HEAD;
  98                   PERMUTED_TRS]);;
  99
 100 let PERMUTED_COUNT = prove
 101   (`!l1 l2. l1 PERMUTED l2 <=> (!x:A. COUNT x l1 = COUNT x l2)`,
 102    let IFF_EXPAND = MESON [] `(p <=> q) <=> (p ==> q) /\ (q ==> p)` in
 103    REWRITE_TAC [IFF_EXPAND; FORALL_AND_THM] THEN CONJ_TAC THENL
 104    [MATCH_MP_TAC PERMUTED_INDUCT THEN REWRITE_TAC [COUNT] THEN
 105     ASM_MESON_TAC []; ALL_TAC] THEN
 106    LIST_INDUCT_TAC THEN REWRITE_TAC [COUNT; PERMUTED_NIL_EQ_NIL] THENL
 107    [LIST_CASES_TAC THEN REWRITE_TAC [COUNT; NOT_CONS_NIL] THEN
 108     MESON_TAC [NOT_SUC]; ALL_TAC] THEN
 109    REPEAT STRIP_TAC THEN ASSERT_TAC `MEM (h:A) l2` THENL
 110    [FIRST_X_ASSUM (MP_TAC o SPEC `h:A`) THEN REWRITE_TAC[MEM_COUNT]
 111     THEN ARITH_TAC; ALL_TAC] THEN
 112    ASSERT_TAC `(h:A) :: t PERMUTED h :: DELETE1 h l2` THENL
 113    [MATCH_MP_TAC PERMUTED_TAIL_IMP THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 114    ASM_REWRITE_TAC [COUNT_DELETE1] THEN GEN_TAC THEN
 115    FIRST_X_ASSUM (MP_TAC o SPEC `x:A`) THEN ARITH_TAC;
 116     ASM_MESON_TAC [PERMUTED_CONS_DELETE1; PERMUTED_SYM; PERMUTED_TRS]]);;
 117
 118 let PERMUTED_TAIL = prove
 119   (`!x t1 t2. x :: t1 PERMUTED x :: t2 <=> t1 PERMUTED t2`,
 120    REPEAT GEN_TAC THEN REWRITE_TAC [PERMUTED_COUNT; COUNT] THEN
 121    MESON_TAC [SUC_INJ]);;
 122
 123 let PERMUTED_DELETE1_L = prove
 124   (`!(h:A) t l. h :: t PERMUTED l <=> MEM h l /\ t PERMUTED DELETE1 h l`,
 125    MESON_TAC [PERMUTED_MEM; MEM; PERMUTED_TAIL; PERMUTED_CONS_DELETE1;
 126               PERMUTED_SYM; PERMUTED_TRS]);;
 127
 128 let PERMUTED_DELETE1_R = prove
 129   (`!(h:A) t l. l PERMUTED h :: t <=> MEM h l /\ DELETE1 h l PERMUTED t`,
 130    MESON_TAC [PERMUTED_SYM; PERMUTED_DELETE1_L]);;
 131
 132 let PERMUTED_LIST_UNIQ = prove
 133   (`!xs ys. xs PERMUTED ys ==> (LIST_UNIQ xs <=> LIST_UNIQ ys)`,
 134    SIMP_TAC [PERMUTED_COUNT; LIST_UNIQ_COUNT; MEM_COUNT]);;
 135
 136 let PERMUTED_IMP_PAIRWISE = prove
 137  (`!(P:A->A->bool) l l'.
 138         (!x y. P x y ==> P y x) /\ l PERMUTED l' /\ PAIRWISE P l
 139         ==> PAIRWISE P l'`,
 140   REWRITE_TAC[IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 141   GEN_TAC THEN DISCH_TAC THEN MATCH_MP_TAC PERMUTED_INDUCT_STRONG THEN
 142   ASM_SIMP_TAC[PAIRWISE; ALL] THEN MESON_TAC[PERMUTED_ALL]);;
 143
 144 let PERMUTED_PAIRWISE = prove
 145  (`!(P:A->A->bool) l l.
 146         (!x y. P x y ==> P y x) /\ l PERMUTED l'
 147         ==> (PAIRWISE P l <=> PAIRWISE P l')`,
 148   MESON_TAC[PERMUTED_IMP_PAIRWISE; PERMUTED_SYM]);;
 149
 150 let PERMUTED_APPEND_SWAP = prove
 151  (`!l1 l2. (APPEND l1 l2) PERMUTED (APPEND l2 l1)`,
 152   REWRITE_TAC[PERMUTED_COUNT; COUNT_APPEND] THEN ARITH_TAC);;