1 (* ========================================================================= *)
2 (* Permuted lists and finite permutations. *)
4 (* Author: Marco Maggesi *)
5 (* University of Florence, Italy *)
6 (* http://www.math.unifi.it/~maggesi/ *)
8 (* (c) Copyright, Marco Maggesi, 2005-2007 *)
9 (* ========================================================================= *)
11 needs "Permutation/permuted.ml";;
13 (* ------------------------------------------------------------------------- *)
14 (* Permutation that reverse a list. *)
15 (* ------------------------------------------------------------------------- *)
19 REVPERM (SUC n) = n :: REVPERM n`;;
21 let MEM_REVPERM = prove
22 (`!n m. MEM m (REVPERM n) <=> m < n`,
23 INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; MEM; LT]);;
25 let LIST_UNIQ_REVPERM = prove
26 (`!n. LIST_UNIQ (REVPERM n)`,
27 INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; LIST_UNIQ; MEM_REVPERM]
30 let DELETE1_REVPERM = prove
31 (`!n. DELETE1 n (REVPERM (SUC n)) = REVPERM n`,
32 INDUCT_TAC THEN ASM_REWRITE_TAC [REVPERM; DELETE1; MEM]);;
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);;
38 let SET_OF_LIST_REVPERM = prove
39 (`!n. set_of_list (REVPERM n) = {m | m < n}`,
41 ASM_REWRITE_TAC [REVPERM; set_of_list; LT; EMPTY_GSPEC; EXTENSION;
42 IN_INSERT; IN_ELIM_THM; NOT_IN_EMPTY]);;
44 (* ------------------------------------------------------------------------- *)
46 (* ------------------------------------------------------------------------- *)
48 let PERMUTATION = new_definition
49 `!l. PERMUTATION l <=> REVPERM (LENGTH l) PERMUTED l`;;
51 let PERMUTATION_NIL = prove
53 REWRITE_TAC [PERMUTATION; LENGTH; REVPERM; PERMUTED_RULES]);;
55 let PERMUTATION_LIST_UNIQ = prove
56 (`!l. PERMUTATION l ==> LIST_UNIQ l`,
57 MESON_TAC [PERMUTATION; PERMUTED_LIST_UNIQ; LIST_UNIQ_REVPERM]);;
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]);;
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
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 []);;
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]]]);;
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]);;
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]);;
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]);;