(* ========================================================================= *) (* 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. *) (* ------------------------------------------------------------------------- *)(* ------------------------------------------------------------------------- *) (* Permutations. *) (* ------------------------------------------------------------------------- *)let SET_OF_LIST_REVPERM =prove (`!n. set_of_list (REVPERM n) = {m | m < n}`,let PERMUTATION = new_definition `!l. PERMUTATION l <=> REVPERM (LENGTH l) PERMUTED l`;;let PERMUTATION_NIL =prove (`PERMUTATION []`,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)`,let PERMUTATION_COUNT =prove (`!l. PERMUTATION l <=> (!x. COUNT x l = if x < LENGTH l then 1 else 0)`,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)`,let PERMUTATION_SET_OF_LIST =prove (`!l. PERMUTATION l <=> set_of_list l = {n | n < LENGTH l}`,let MEM_PERMUTATION =prove (`!l. (!n. n < LENGTH l ==> MEM n l) ==> PERMUTATION l`,let LIST_UNIQ_MEM_PERMUTATION =prove (`!l. LIST_UNIQ l /\ (!n. MEM n l ==> n < LENGTH l) ==> PERMUTATION l`,let PERMUTATION_UNIQ_LT =prove (`!l. PERMUTATION l <=> LIST_UNIQ l /\ (!n. MEM n l ==> n < LENGTH l)`,