Library/permutations.ml

   1 (* ========================================================================= *)
   2 (* Permutations, both general and specifically on finite sets.               *)
   3 (* ========================================================================= *)
   4
   5 parse_as_infix("permutes",(12,"right"));;
   6
   7 let permutes = new_definition
   8  `p permutes s <=> (!x. ~(x IN s) ==> p(x) = x) /\ (!y. ?!x. p x = y)`;;
   9
  10 (* ------------------------------------------------------------------------- *)
  11 (* Inverse function (on whole universe).                                     *)
  12 (* ------------------------------------------------------------------------- *)
  13
  14 let inverse = new_definition
  15  `inverse(f) = \y. @x. f x = y`;;
  16
  17 let SURJECTIVE_INVERSE = prove
  18  (`!f. (!y. ?x. f x = y) <=> !y. f(inverse f y) = y`,
  19   REWRITE_TAC[SURJECTIVE_RIGHT_INVERSE; inverse] THEN MESON_TAC[]);;
  20
  21 let SURJECTIVE_INVERSE_o = prove
  22  (`!f. (!y. ?x. f x = y) <=> (f o inverse f = I)`,
  23   REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; SURJECTIVE_INVERSE]);;
  24
  25 let INJECTIVE_INVERSE = prove
  26  (`!f. (!x x'. f x = f x' ==> x = x') <=> !x. inverse f (f x) = x`,
  27   MESON_TAC[inverse]);;
  28
  29 let INJECTIVE_INVERSE_o = prove
  30  (`!f. (!x x'. f x = f x' ==> x = x') <=> (inverse f o f = I)`,
  31   REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM; INJECTIVE_INVERSE]);;
  32
  33 let INVERSE_UNIQUE_o = prove
  34  (`!f g. f o g = I /\ g o f = I ==> inverse f = g`,
  35   REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM] THEN
  36   MESON_TAC[INJECTIVE_INVERSE; SURJECTIVE_INVERSE]);;
  37
  38 let INVERSE_I = prove
  39  (`inverse I = I`,
  40   MATCH_MP_TAC INVERSE_UNIQUE_o THEN REWRITE_TAC[I_O_ID]);;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* Transpositions.                                                           *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let swap = new_definition
  47  `swap(i,j) k = if k = i then j else if k = j then i else k`;;
  48
  49 let SWAP_REFL = prove
  50  (`!a. swap(a,a) = I`,
  51   REWRITE_TAC[FUN_EQ_THM; swap; I_THM] THEN MESON_TAC[]);;
  52
  53 let SWAP_SYM = prove
  54  (`!a b. swap(a,b) = swap(b,a)`,
  55   REWRITE_TAC[FUN_EQ_THM; swap; I_THM] THEN MESON_TAC[]);;
  56
  57 let SWAP_IDEMPOTENT = prove
  58  (`!a b. swap(a,b) o swap(a,b) = I`,
  59   REWRITE_TAC[FUN_EQ_THM; swap; o_THM; I_THM] THEN MESON_TAC[]);;
  60
  61 let INVERSE_SWAP = prove
  62  (`!a b. inverse(swap(a,b)) = swap(a,b)`,
  63   REPEAT GEN_TAC THEN MATCH_MP_TAC INVERSE_UNIQUE_o THEN
  64   REWRITE_TAC[SWAP_SYM; SWAP_IDEMPOTENT]);;
  65
  66 let SWAP_GALOIS = prove
  67  (`!a b x y. x = swap(a,b) y <=> y = swap(a,b) x`,
  68   REWRITE_TAC[swap] THEN MESON_TAC[]);;
  69
  70 (* ------------------------------------------------------------------------- *)
  71 (* Basic consequences of the definition.                                     *)
  72 (* ------------------------------------------------------------------------- *)
  73
  74 let PERMUTES_IN_IMAGE = prove
  75  (`!p s x. p permutes s ==> (p(x) IN s <=> x IN s)`,
  76   REWRITE_TAC[permutes] THEN MESON_TAC[]);;
  77
  78 let PERMUTES_IMAGE = prove
  79  (`!p s. p permutes s ==> IMAGE p s = s`,
  80   REWRITE_TAC[permutes; EXTENSION; IN_IMAGE] THEN MESON_TAC[]);;
  81
  82 let PERMUTES_INJECTIVE = prove
  83  (`!p s. p permutes s ==> !x y. p(x) = p(y) <=> x = y`,
  84   REWRITE_TAC[permutes] THEN MESON_TAC[]);;
  85
  86 let PERMUTES_SURJECTIVE = prove
  87  (`!p s. p permutes s ==> !y. ?x. p(x) = y`,
  88   REWRITE_TAC[permutes] THEN MESON_TAC[]);;
  89
  90 let PERMUTES_INVERSES_o = prove
  91  (`!p s. p permutes s ==> p o inverse(p) = I /\ inverse(p) o p = I`,
  92   REWRITE_TAC[GSYM INJECTIVE_INVERSE_o; GSYM SURJECTIVE_INVERSE_o] THEN
  93   REWRITE_TAC[permutes] THEN MESON_TAC[]);;
  94
  95 let PERMUTES_INVERSES = prove
  96  (`!p s. p permutes s
  97          ==> (!x. p(inverse p x) = x) /\ (!x. inverse p (p x) = x)`,
  98   REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
  99   REWRITE_TAC[FUN_EQ_THM; o_THM; I_THM]);;
 100
 101 let PERMUTES_SUBSET = prove
 102  (`!p s t. p permutes s /\ s SUBSET t ==> p permutes t`,
 103   REWRITE_TAC[permutes; SUBSET] THEN MESON_TAC[]);;
 104
 105 let PERMUTES_EMPTY = prove
 106  (`!p. p permutes {} <=> p = I`,
 107   REWRITE_TAC[FUN_EQ_THM; I_THM; permutes; NOT_IN_EMPTY] THEN MESON_TAC[]);;
 108
 109 let PERMUTES_SING = prove
 110  (`!p a.  p permutes {a} <=> p = I`,
 111   REWRITE_TAC[FUN_EQ_THM; I_THM; permutes; IN_SING] THEN MESON_TAC[]);;
 112
 113 let PERMUTES_UNIV = prove
 114  (`!p. p permutes UNIV <=> !y:A. ?!x. p x = y`,
 115   REWRITE_TAC[permutes; IN_UNIV] THEN MESON_TAC[]);;
 116
 117 let PERMUTES_INVERSE_EQ = prove
 118  (`!p s. p permutes s ==> !x y. inverse p y = x <=> p x = y`,
 119   REWRITE_TAC[permutes; inverse] THEN MESON_TAC[]);;
 120
 121 let PERMUTES_SWAP = prove
 122  (`!a b s. a IN s /\ b IN s ==> swap(a,b) permutes s`,
 123   REWRITE_TAC[permutes; swap] THEN MESON_TAC[]);;
 124
 125 let PERMUTES_SUPERSET = prove
 126  (`!p s t. p permutes s /\ (!x. x IN (s DIFF t) ==> p(x) = x)
 127            ==> p permutes t`,
 128   REWRITE_TAC[permutes; IN_DIFF] THEN MESON_TAC[]);;
 129
 130 let PERMUTES_BIJECTIONS = prove
 131  (`!p q. (!x. x IN s ==> p x IN s) /\ (!x. ~(x IN s) ==> p x = x) /\
 132          (!x. x IN s ==> q x IN s) /\ (!x. ~(x IN s) ==> q x = x) /\
 133          (!x. p(q x) = x) /\ (!x. q(p x) = x)
 134          ==> p permutes s`,
 135   REWRITE_TAC[permutes] THEN MESON_TAC[]);;
 136
 137 (* ------------------------------------------------------------------------- *)
 138 (* Group properties.                                                         *)
 139 (* ------------------------------------------------------------------------- *)
 140
 141 let PERMUTES_I = prove
 142  (`!s. I permutes s`,
 143   REWRITE_TAC[permutes; I_THM] THEN MESON_TAC[]);;
 144
 145 let PERMUTES_COMPOSE = prove
 146  (`!p q s. p permutes s /\ q permutes s ==> (q o p) permutes s`,
 147   REWRITE_TAC[permutes; o_THM] THEN MESON_TAC[]);;
 148
 149 let PERMUTES_INVERSE = prove
 150  (`!p s. p permutes s ==> inverse(p) permutes s`,
 151   REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o MATCH_MP PERMUTES_INVERSE_EQ) THEN
 152   POP_ASSUM MP_TAC THEN REWRITE_TAC[permutes] THEN MESON_TAC[]);;
 153
 154 let PERMUTES_INVERSE_INVERSE = prove
 155  (`!p. p permutes s ==> inverse(inverse p) = p`,
 156   SIMP_TAC[FUN_EQ_THM] THEN MESON_TAC[PERMUTES_INVERSE_EQ; PERMUTES_INVERSE]);;
 157
 158 (* ------------------------------------------------------------------------- *)
 159 (* The number of permutations on a finite set.                               *)
 160 (* ------------------------------------------------------------------------- *)
 161
 162 let PERMUTES_INSERT_LEMMA = prove
 163  (`!p a:A s. p permutes (a INSERT s) ==> (swap(a,p(a)) o p) permutes s`,
 164   REPEAT STRIP_TAC THEN MATCH_MP_TAC PERMUTES_SUPERSET THEN
 165   EXISTS_TAC `(a:A) INSERT s` THEN CONJ_TAC THENL
 166    [ASM_MESON_TAC[PERMUTES_SWAP; PERMUTES_IN_IMAGE;
 167                   IN_INSERT; PERMUTES_COMPOSE];
 168     REWRITE_TAC[o_THM; swap; IN_INSERT; IN_DIFF] THEN ASM_MESON_TAC[]]);;
 169
 170 let PERMUTES_INSERT = prove
 171  (`{p:A->A | p permutes (a INSERT s)} =
 172         IMAGE (\(b,p). swap(a,b) o p)
 173               {(b,p) | b IN a INSERT s /\ p IN {p | p permutes s}}`,
 174   REWRITE_TAC[EXTENSION; IN_ELIM_PAIR_THM; IN_IMAGE; EXISTS_PAIR_THM] THEN
 175   X_GEN_TAC `p:A->A` THEN REWRITE_TAC[IN_ELIM_THM] THEN
 176   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN EQ_TAC THENL
 177    [DISCH_TAC THEN MAP_EVERY EXISTS_TAC
 178       [`(p:A->A) a`; `swap(a,p a) o (p:A->A)`] THEN
 179     ASM_SIMP_TAC[SWAP_IDEMPOTENT; o_ASSOC; I_O_ID; PERMUTES_INSERT_LEMMA] THEN
 180     ASM_MESON_TAC[PERMUTES_IN_IMAGE; IN_INSERT];
 181     REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
 182     MAP_EVERY X_GEN_TAC [`b:A`; `q:A->A`] THEN
 183     STRIP_TAC THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC PERMUTES_COMPOSE THEN
 184     CONJ_TAC THENL
 185      [ASM_MESON_TAC[PERMUTES_SUBSET; SUBSET; IN_INSERT];
 186       MATCH_MP_TAC PERMUTES_SWAP THEN
 187       ASM_MESON_TAC[PERMUTES_IN_IMAGE; IN_INSERT]]]);;
 188
 189 let HAS_SIZE_PERMUTATIONS = prove
 190  (`!s:A->bool n. s HAS_SIZE n ==> {p | p permutes s} HAS_SIZE (FACT n)`,
 191   REWRITE_TAC[HAS_SIZE; IMP_CONJ; RIGHT_FORALL_IMP_THM] THEN
 192   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 193   SIMP_TAC[PERMUTES_EMPTY; CARD_CLAUSES; SET_RULE `{x | x = a} = {a}`] THEN
 194   SIMP_TAC[CARD_CLAUSES; FINITE_INSERT; FINITE_EMPTY] THEN
 195   REWRITE_TAC[NOT_IN_EMPTY] THEN CONJ_TAC THENL
 196    [GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN CONV_TAC NUM_REDUCE_CONV;
 197     ALL_TAC] THEN
 198   MAP_EVERY X_GEN_TAC [`a:A`; `s:A->bool`] THEN REWRITE_TAC[GSYM HAS_SIZE] THEN
 199   STRIP_TAC THEN X_GEN_TAC `k:num` THEN DISCH_THEN(SUBST_ALL_TAC o SYM) THEN
 200   REWRITE_TAC[FACT; PERMUTES_INSERT] THEN MATCH_MP_TAC HAS_SIZE_IMAGE_INJ THEN
 201   ASM_SIMP_TAC[HAS_SIZE_PRODUCT; HAS_SIZE; FINITE_INSERT; CARD_CLAUSES] THEN
 202   REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM; IN_ELIM_THM; PAIR_EQ] THEN
 203   CONV_TAC(ONCE_DEPTH_CONV GEN_BETA_CONV) THEN
 204   MAP_EVERY X_GEN_TAC [`b:A`; `q:A->A`; `c:A`; `r:A->A`] THEN
 205   STRIP_TAC THEN SUBGOAL_THEN `c:A = b` SUBST_ALL_TAC THENL
 206    [FIRST_X_ASSUM(MP_TAC o C AP_THM `a:A`) THEN REWRITE_TAC[o_THM; swap] THEN
 207     SUBGOAL_THEN `(q:A->A) a = a /\ (r:A->A) a = a` (fun t -> SIMP_TAC[t]) THEN
 208     ASM_MESON_TAC[permutes];
 209     FIRST_X_ASSUM(MP_TAC o AP_TERM `(\q:A->A. swap(a:A,b) o q)`) THEN
 210     ASM_SIMP_TAC[SWAP_IDEMPOTENT; o_ASSOC; I_O_ID]]);;
 211
 212 let FINITE_PERMUTATIONS = prove
 213  (`!s. FINITE s ==> FINITE {p | p permutes s}`,
 214   MESON_TAC[HAS_SIZE_PERMUTATIONS; HAS_SIZE]);;
 215
 216 let CARD_PERMUTATIONS = prove
 217  (`!s. FINITE s ==> CARD {p | p permutes s} = FACT(CARD s)`,
 218   MESON_TAC[HAS_SIZE; HAS_SIZE_PERMUTATIONS]);;
 219
 220 (* ------------------------------------------------------------------------- *)
 221 (* Alternative characterizations of permutation of finite set.               *)
 222 (* ------------------------------------------------------------------------- *)
 223
 224 let PERMUTES_FINITE_INJECTIVE = prove
 225  (`!s:A->bool p.
 226         FINITE s
 227         ==> (p permutes s <=>
 228              (!x. ~(x IN s) ==> p x = x) /\
 229              (!x. x IN s ==> p x IN s) /\
 230              (!x y. x IN s /\ y IN s /\ p x = p y ==> x = y))`,
 231   REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC THEN
 232   MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
 233   DISCH_TAC THEN EQ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN STRIP_TAC THEN
 234   FIRST_ASSUM(MP_TAC o SPEC `p:A->A` o MATCH_MP
 235    (REWRITE_RULE[IMP_CONJ] SURJECTIVE_IFF_INJECTIVE)) THEN
 236   ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IMP_IMP; GSYM CONJ_ASSOC] THEN
 237   STRIP_TAC THEN X_GEN_TAC `y:A` THEN
 238   ASM_CASES_TAC `(y:A) IN s` THEN ASM_MESON_TAC[]);;
 239
 240 let PERMUTES_FINITE_SURJECTIVE = prove
 241  (`!s:A->bool p.
 242         FINITE s
 243         ==> (p permutes s <=>
 244              (!x. ~(x IN s) ==> p x = x) /\ (!x. x IN s ==> p x IN s) /\
 245              (!y. y IN s ==> ?x. x IN s /\ p x = y))`,
 246   REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC THEN
 247   MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
 248   DISCH_TAC THEN EQ_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN STRIP_TAC THEN
 249   FIRST_ASSUM(MP_TAC o SPEC `p:A->A` o MATCH_MP
 250    (REWRITE_RULE[IMP_CONJ] SURJECTIVE_IFF_INJECTIVE)) THEN
 251   ASM_REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IMP_IMP; GSYM CONJ_ASSOC] THEN
 252   STRIP_TAC THEN X_GEN_TAC `y:A` THEN
 253   ASM_CASES_TAC `(y:A) IN s` THEN ASM_MESON_TAC[]);;
 254
 255 (* ------------------------------------------------------------------------- *)
 256 (* Permutations of index set for iterated operations.                        *)
 257 (* ------------------------------------------------------------------------- *)
 258
 259 let ITERATE_PERMUTE = prove
 260  (`!op. monoidal op
 261         ==> !f p s. p permutes s ==> iterate op s f = iterate op s (f o p)`,
 262   REPEAT STRIP_TAC THEN
 263   FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP ITERATE_BIJECTION) THEN
 264   ASM_MESON_TAC[permutes]);;
 265
 266 let NSUM_PERMUTE = prove
 267  (`!f p s. p permutes s ==> nsum s f = nsum s (f o p)`,
 268   REWRITE_TAC[nsum] THEN MATCH_MP_TAC ITERATE_PERMUTE THEN
 269   REWRITE_TAC[MONOIDAL_ADD]);;
 270
 271 let NSUM_PERMUTE_NUMSEG = prove
 272  (`!f p m n. p permutes m..n ==> nsum(m..n) f = nsum(m..n) (f o p)`,
 273   MESON_TAC[NSUM_PERMUTE; FINITE_NUMSEG]);;
 274
 275 let SUM_PERMUTE = prove
 276  (`!f p s. p permutes s ==> sum s f = sum s (f o p)`,
 277   REWRITE_TAC[sum] THEN MATCH_MP_TAC ITERATE_PERMUTE THEN
 278   REWRITE_TAC[MONOIDAL_REAL_ADD]);;
 279
 280 let SUM_PERMUTE_NUMSEG = prove
 281  (`!f p m n. p permutes m..n ==> sum(m..n) f = sum(m..n) (f o p)`,
 282   MESON_TAC[SUM_PERMUTE; FINITE_NUMSEG]);;
 283
 284 (* ------------------------------------------------------------------------- *)
 285 (* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
 286 (* ------------------------------------------------------------------------- *)
 287
 288 let SWAP_COMMON = prove
 289  (`!a b c:A. ~(a = c) /\ ~(b = c)
 290              ==> swap(a,b) o swap(a,c) = swap(b,c) o swap(a,b)`,
 291   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; swap; o_THM; I_THM] THEN
 292   DISCH_TAC THEN X_GEN_TAC `x:A` THEN
 293   MAP_EVERY ASM_CASES_TAC [`x:A = a`; `x:A = b`; `x:A = c`] THEN
 294   REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN ASM_REWRITE_TAC[] THEN
 295   ASM_MESON_TAC[]);;
 296
 297 let SWAP_COMMON' = prove
 298  (`!a b c:A. ~(a = b) /\ ~(a = c)
 299              ==> swap(a,c) o swap(b,c) = swap(b,c) o swap(a,b)`,
 300   REPEAT STRIP_TAC THEN
 301   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [SWAP_SYM] THEN
 302   ASM_SIMP_TAC[GSYM SWAP_COMMON] THEN REWRITE_TAC[SWAP_SYM]);;
 303
 304 let SWAP_INDEPENDENT = prove
 305  (`!a b c d:A. ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d)
 306                ==> swap(a,b) o swap(c,d) = swap(c,d) o swap(a,b)`,
 307   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; swap; o_THM; I_THM] THEN
 308   DISCH_TAC THEN X_GEN_TAC `x:A` THEN
 309   MAP_EVERY ASM_CASES_TAC [`x:A = a`; `x:A = b`; `x:A = c`] THEN
 310   REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THEN ASM_REWRITE_TAC[] THEN
 311   ASM_MESON_TAC[]);;
 312
 313 (* ------------------------------------------------------------------------- *)
 314 (* Permutations as transposition sequences.                                  *)
 315 (* ------------------------------------------------------------------------- *)
 316
 317 let swapseq_RULES,swapseq_INDUCT,swapseq_CASES = new_inductive_definition
 318  `(swapseq 0 I) /\
 319   (!a b p n. swapseq n p /\ ~(a = b) ==> swapseq (SUC n) (swap(a,b) o p))`;;
 320
 321 let permutation = new_definition
 322  `permutation p <=> ?n. swapseq n p`;;
 323
 324 (* ------------------------------------------------------------------------- *)
 325 (* Some closure properties of the set of permutations, with lengths.         *)
 326 (* ------------------------------------------------------------------------- *)
 327
 328 let SWAPSEQ_I = CONJUNCT1 swapseq_RULES;;
 329
 330 let PERMUTATION_I = prove
 331  (`permutation I`,
 332   REWRITE_TAC[permutation] THEN MESON_TAC[SWAPSEQ_I]);;
 333
 334 let SWAPSEQ_SWAP = prove
 335  (`!a b. swapseq (if a = b then 0 else 1) (swap(a,b))`,
 336   REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[num_CONV `1`] THEN
 337   ASM_MESON_TAC[swapseq_RULES; I_O_ID; SWAPSEQ_I; SWAP_REFL]);;
 338
 339 let PERMUTATION_SWAP = prove
 340  (`!a b. permutation(swap(a,b))`,
 341   REWRITE_TAC[permutation] THEN MESON_TAC[SWAPSEQ_SWAP]);;
 342
 343 let SWAPSEQ_COMPOSE = prove
 344  (`!n p m q. swapseq n p /\ swapseq m q ==> swapseq (n + m) (p o q)`,
 345   REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
 346   MATCH_MP_TAC swapseq_INDUCT THEN
 347   REWRITE_TAC[ADD_CLAUSES; I_O_ID; GSYM o_ASSOC] THEN
 348   MESON_TAC[swapseq_RULES]);;
 349
 350 let PERMUTATION_COMPOSE = prove
 351  (`!p q. permutation p /\ permutation q ==> permutation(p o q)`,
 352   REWRITE_TAC[permutation] THEN MESON_TAC[SWAPSEQ_COMPOSE]);;
 353
 354 let SWAPSEQ_ENDSWAP = prove
 355  (`!n p a b:A. swapseq n p /\ ~(a = b) ==> swapseq (SUC n) (p o swap(a,b))`,
 356   REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN
 357   MATCH_MP_TAC swapseq_INDUCT THEN REWRITE_TAC[I_O_ID; GSYM o_ASSOC] THEN
 358   MESON_TAC[o_ASSOC; swapseq_RULES; I_O_ID]);;
 359
 360 let SWAPSEQ_INVERSE_EXISTS = prove
 361  (`!n p:A->A. swapseq n p ==> ?q. swapseq n q /\ p o q = I /\ q o p = I`,
 362   MATCH_MP_TAC swapseq_INDUCT THEN CONJ_TAC THENL
 363    [MESON_TAC[I_O_ID; swapseq_RULES]; ALL_TAC] THEN
 364   REPEAT STRIP_TAC THEN
 365   MP_TAC(SPECL [`n:num`; `q:A->A`; `a:A`; `b:A`] SWAPSEQ_ENDSWAP) THEN
 366   ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
 367   EXISTS_TAC `(q:A->A) o swap (a,b)` THEN
 368   ASM_REWRITE_TAC[GSYM o_ASSOC] THEN
 369   GEN_REWRITE_TAC (BINOP_CONV o LAND_CONV o RAND_CONV) [o_ASSOC] THEN
 370   ASM_REWRITE_TAC[SWAP_IDEMPOTENT; I_O_ID]);;
 371
 372 let SWAPSEQ_INVERSE = prove
 373  (`!n p. swapseq n p ==> swapseq n (inverse p)`,
 374   MESON_TAC[SWAPSEQ_INVERSE_EXISTS; INVERSE_UNIQUE_o]);;
 375
 376 let PERMUTATION_INVERSE = prove
 377  (`!p. permutation p ==> permutation(inverse p)`,
 378   REWRITE_TAC[permutation] THEN MESON_TAC[SWAPSEQ_INVERSE]);;
 379
 380 (* ------------------------------------------------------------------------- *)
 381 (* The identity map only has even transposition sequences.                   *)
 382 (* ------------------------------------------------------------------------- *)
 383
 384 let SYMMETRY_LEMMA = prove
 385  (`(!a b c d. P a b c d ==> P a b d c) /\
 386    (!a b c d. ~(a = b) /\ ~(c = d) /\
 387               (a = c /\ b = d \/ a = c /\ ~(b = d) \/ ~(a = c) /\ b = d \/
 388                ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d))
 389               ==> P a b c d)
 390    ==> (!a b c d:A. ~(a = b) /\ ~(c = d) ==> P a b c d)`,
 391   REPEAT STRIP_TAC THEN MAP_EVERY ASM_CASES_TAC
 392    [`a:A = c`; `a:A = d`; `b:A = c`; `b:A = d`] THEN
 393   ASM_MESON_TAC[]);;
 394
 395 let SWAP_GENERAL = prove
 396  (`!a b c d:A.
 397         ~(a = b) /\ ~(c = d)
 398         ==> swap(a,b) o swap(c,d) = I \/
 399             ?x y z. ~(x = a) /\ ~(y = a) /\ ~(z = a) /\ ~(x = y) /\
 400                     swap(a,b) o swap(c,d) = swap(x,y) o swap(a,z)`,
 401   MATCH_MP_TAC SYMMETRY_LEMMA THEN CONJ_TAC THENL
 402    [REWRITE_TAC[SWAP_SYM] THEN SIMP_TAC[]; ALL_TAC] THEN
 403   REPEAT STRIP_TAC THEN REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THENL
 404    [MESON_TAC[SWAP_IDEMPOTENT];
 405     DISJ2_TAC THEN MAP_EVERY EXISTS_TAC [`b:A`; `d:A`; `b:A`] THEN
 406     ASM_MESON_TAC[SWAP_COMMON];
 407     DISJ2_TAC THEN MAP_EVERY EXISTS_TAC [`c:A`; `d:A`; `c:A`] THEN
 408     ASM_MESON_TAC[SWAP_COMMON'];
 409     DISJ2_TAC THEN MAP_EVERY EXISTS_TAC [`c:A`; `d:A`; `b:A`] THEN
 410     ASM_MESON_TAC[SWAP_INDEPENDENT]]);;
 411
 412 let FIXING_SWAPSEQ_DECREASE = prove
 413  (`!n p a b:A.
 414       swapseq n p /\ ~(a = b) /\ (swap(a,b) o p) a = a
 415       ==> ~(n = 0) /\ swapseq (n - 1) (swap(a,b) o p)`,
 416   INDUCT_TAC THEN REPEAT GEN_TAC THEN
 417   GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [swapseq_CASES] THEN
 418   REWRITE_TAC[NOT_SUC] THENL
 419    [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 420     ASM_REWRITE_TAC[I_THM; o_THM; swap] THEN MESON_TAC[];
 421     ALL_TAC] THEN
 422   REWRITE_TAC[LEFT_IMP_EXISTS_THM; LEFT_AND_EXISTS_THM] THEN
 423   MAP_EVERY X_GEN_TAC [`c:A`; `d:A`; `q:A->A`; `m:num`] THEN
 424   REWRITE_TAC[SUC_INJ; GSYM CONJ_ASSOC] THEN
 425   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 426   FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
 427   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 428   FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[o_ASSOC] THEN STRIP_TAC THEN
 429   MP_TAC(SPECL [`a:A`; `b:A`; `c:A`; `d:A`] SWAP_GENERAL) THEN
 430   ASM_REWRITE_TAC[] THEN
 431   DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC MP_TAC) THEN
 432   ASM_REWRITE_TAC[I_O_ID; SUC_SUB1; LEFT_IMP_EXISTS_THM] THEN
 433   MAP_EVERY X_GEN_TAC [`x:A`; `y:A`; `z:A`] THEN
 434   REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
 435   DISCH_THEN SUBST_ALL_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
 436    [`q:A->A`; `a:A`; `z:A`]) THEN
 437   ANTS_TAC THENL
 438    [ASM_REWRITE_TAC[] THEN
 439     FIRST_X_ASSUM(MP_TAC o check(is_eq o concl)) THEN
 440     REWRITE_TAC[GSYM o_ASSOC] THEN
 441     ABBREV_TAC `r:A->A = swap(a:A,z) o q` THEN
 442     ASM_REWRITE_TAC[FUN_EQ_THM; o_THM; swap] THEN ASM_MESON_TAC[];
 443     SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN
 444     REWRITE_TAC[NOT_SUC; SUC_SUB1; GSYM o_ASSOC] THEN
 445     ASM_MESON_TAC[swapseq_RULES]]);;
 446
 447 let SWAPSEQ_IDENTITY_EVEN = prove
 448  (`!n. swapseq n (I:A->A) ==> EVEN n`,
 449   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 450   GEN_REWRITE_TAC LAND_CONV [swapseq_CASES] THEN
 451   DISCH_THEN(DISJ_CASES_THEN2 (SUBST_ALL_TAC o CONJUNCT1) MP_TAC) THEN
 452   REWRITE_TAC[EVEN; LEFT_IMP_EXISTS_THM] THEN
 453   MAP_EVERY X_GEN_TAC [`a:A`; `b:A`; `p:A->A`; `m:num`] THEN
 454   DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
 455   MP_TAC(SPECL [`m:num`; `p:A->A`; `a:A`; `b:A`] FIXING_SWAPSEQ_DECREASE) THEN
 456   ASM_REWRITE_TAC[I_THM] THEN STRIP_TAC THEN
 457   FIRST_X_ASSUM(MP_TAC o SPEC `m - 1`) THEN
 458   UNDISCH_THEN `SUC m = n` (SUBST_ALL_TAC o SYM) THEN
 459   ASM_REWRITE_TAC[ARITH_RULE `m - 1 < SUC m`] THEN UNDISCH_TAC `~(m = 0)` THEN
 460   SPEC_TAC(`m:num`,`m:num`) THEN INDUCT_TAC THEN
 461   REWRITE_TAC[SUC_SUB1; EVEN]);;
 462
 463 (* ------------------------------------------------------------------------- *)
 464 (* Therefore we have a welldefined notion of parity.                         *)
 465 (* ------------------------------------------------------------------------- *)
 466
 467 let evenperm = new_definition `evenperm(p) = EVEN(@n. swapseq n p)`;;
 468
 469 let SWAPSEQ_EVEN_EVEN = prove
 470  (`!m n p:A->A. swapseq m p /\ swapseq n p ==> (EVEN m <=> EVEN n)`,
 471   REPEAT STRIP_TAC THEN
 472   FIRST_X_ASSUM(MP_TAC o MATCH_MP SWAPSEQ_INVERSE_EXISTS) THEN
 473   STRIP_TAC THEN
 474   FIRST_X_ASSUM(MP_TAC o AP_TERM `swapseq (n + m) :(A->A)->bool`) THEN
 475   ASM_SIMP_TAC[SWAPSEQ_COMPOSE] THEN
 476   DISCH_THEN(MP_TAC o MATCH_MP SWAPSEQ_IDENTITY_EVEN) THEN
 477   SIMP_TAC[EVEN_ADD]);;
 478
 479 let EVENPERM_UNIQUE = prove
 480  (`!n p b. swapseq n p /\ EVEN n = b ==> evenperm p = b`,
 481   REWRITE_TAC[evenperm] THEN MESON_TAC[SWAPSEQ_EVEN_EVEN]);;
 482
 483 (* ------------------------------------------------------------------------- *)
 484 (* And it has the expected composition properties.                           *)
 485 (* ------------------------------------------------------------------------- *)
 486
 487 let EVENPERM_I = prove
 488  (`evenperm I = T`,
 489   MATCH_MP_TAC EVENPERM_UNIQUE THEN MESON_TAC[swapseq_RULES; EVEN]);;
 490
 491 let EVENPERM_SWAP = prove
 492  (`!a b:A. evenperm(swap(a,b)) = (a = b)`,
 493   REPEAT GEN_TAC THEN MATCH_MP_TAC EVENPERM_UNIQUE THEN
 494   MESON_TAC[SWAPSEQ_SWAP; NUM_RED_CONV `EVEN 0`; NUM_RED_CONV `EVEN 1`]);;
 495
 496 let EVENPERM_COMPOSE = prove
 497  (`!p q. permutation p /\ permutation q
 498          ==> evenperm (p o q) = (evenperm p = evenperm q)`,
 499   REWRITE_TAC[permutation; LEFT_AND_EXISTS_THM; RIGHT_AND_EXISTS_THM] THEN
 500   REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN REPEAT GEN_TAC THEN
 501   DISCH_THEN(fun th -> ASSUME_TAC th THEN
 502                ASSUME_TAC(MATCH_MP SWAPSEQ_COMPOSE th)) THEN
 503   ASM_MESON_TAC[EVENPERM_UNIQUE; SWAPSEQ_COMPOSE; EVEN_ADD]);;
 504
 505 let EVENPERM_INVERSE = prove
 506  (`!p. permutation p ==> evenperm(inverse p) = evenperm p`,
 507   REWRITE_TAC[permutation] THEN REPEAT STRIP_TAC THEN
 508   MATCH_MP_TAC EVENPERM_UNIQUE THEN
 509   ASM_MESON_TAC[SWAPSEQ_INVERSE; EVENPERM_UNIQUE]);;
 510
 511 (* ------------------------------------------------------------------------- *)
 512 (* A more abstract characterization of permutations.                         *)
 513 (* ------------------------------------------------------------------------- *)
 514
 515 let PERMUTATION_BIJECTIVE = prove
 516  (`!p. permutation p ==> !y. ?!x. p(x) = y`,
 517   REWRITE_TAC[permutation] THEN REPEAT STRIP_TAC THEN
 518   FIRST_X_ASSUM(MP_TAC o MATCH_MP SWAPSEQ_INVERSE_EXISTS) THEN
 519   REWRITE_TAC[FUN_EQ_THM; I_THM; o_THM; LEFT_IMP_EXISTS_THM] THEN
 520   MESON_TAC[]);;
 521
 522 let PERMUTATION_FINITE_SUPPORT = prove
 523  (`!p. permutation p ==> FINITE {x:A | ~(p x = x)}`,
 524   REWRITE_TAC[permutation; LEFT_IMP_EXISTS_THM] THEN
 525   ONCE_REWRITE_TAC[SWAP_FORALL_THM] THEN MATCH_MP_TAC swapseq_INDUCT THEN
 526   REWRITE_TAC[I_THM; FINITE_RULES; SET_RULE `{x | F} = {}`] THEN
 527   MAP_EVERY X_GEN_TAC [`a:A`; `b:A`; `p:A->A`] THEN
 528   STRIP_TAC THEN MATCH_MP_TAC FINITE_SUBSET THEN
 529   EXISTS_TAC `(a:A) INSERT b INSERT {x | ~(p x = x)}` THEN
 530   ASM_REWRITE_TAC[FINITE_INSERT; SUBSET; IN_INSERT; IN_ELIM_THM] THEN
 531   REWRITE_TAC[o_THM; swap] THEN MESON_TAC[]);;
 532
 533 let PERMUTATION_LEMMA = prove
 534  (`!s p:A->A.
 535        FINITE s /\
 536        (!y. ?!x. p(x) = y) /\ (!x. ~(x IN s) ==> p x = x)
 537        ==> permutation p`,
 538   ONCE_REWRITE_TAC[IMP_CONJ] THEN REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN
 539   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN CONJ_TAC THENL
 540    [REWRITE_TAC[NOT_IN_EMPTY] THEN REPEAT STRIP_TAC THEN
 541     SUBGOAL_THEN `p:A->A = I` (fun th -> REWRITE_TAC[th; PERMUTATION_I]) THEN
 542     ASM_REWRITE_TAC[FUN_EQ_THM; I_THM];
 543     ALL_TAC] THEN
 544   MAP_EVERY X_GEN_TAC [`a:A`; `s:A->bool`] THEN STRIP_TAC THEN
 545   REWRITE_TAC[IN_INSERT] THEN REPEAT STRIP_TAC THEN
 546   SUBGOAL_THEN `permutation((swap(a,p(a)) o swap(a,p(a))) o (p:A->A))`
 547   MP_TAC THENL [ALL_TAC; REWRITE_TAC[SWAP_IDEMPOTENT; I_O_ID]] THEN
 548   REWRITE_TAC[GSYM o_ASSOC] THEN MATCH_MP_TAC PERMUTATION_COMPOSE THEN
 549   REWRITE_TAC[PERMUTATION_SWAP] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
 550   CONJ_TAC THENL
 551    [UNDISCH_TAC `!y. ?!x. (p:A->A) x = y` THEN
 552     REWRITE_TAC[EXISTS_UNIQUE_THM; swap; o_THM] THEN
 553     ASM_CASES_TAC `(p:A->A) a = a` THEN ASM_REWRITE_TAC[] THENL
 554      [ASM_MESON_TAC[]; ALL_TAC] THEN
 555     REWRITE_TAC[TAUT
 556      `(if p then x else y) = a <=> if p then x = a else y = a`] THEN
 557     REWRITE_TAC[TAUT `(if p then x else y) <=> p /\ x \/ ~p /\ y`] THEN
 558     ASM_MESON_TAC[];
 559     REWRITE_TAC[swap; o_THM] THEN
 560     ASM_CASES_TAC `(p:A->A) a = a` THEN ASM_REWRITE_TAC[] THEN
 561     ASM_MESON_TAC[]]);;
 562
 563 let PERMUTATION = prove
 564  (`!p. permutation p <=> (!y. ?!x. p(x) = y) /\ FINITE {x:A | ~(p(x) = x)}`,
 565   GEN_TAC THEN EQ_TAC THEN
 566   SIMP_TAC[PERMUTATION_BIJECTIVE; PERMUTATION_FINITE_SUPPORT] THEN
 567   STRIP_TAC THEN MATCH_MP_TAC PERMUTATION_LEMMA THEN
 568   EXISTS_TAC `{x:A | ~(p x = x)}` THEN
 569   ASM_SIMP_TAC[IN_ELIM_THM]);;
 570
 571 let PERMUTATION_INVERSE_WORKS = prove
 572  (`!p. permutation p ==> inverse p o p = I /\ p o inverse p = I`,
 573   MESON_TAC[PERMUTATION_BIJECTIVE; SURJECTIVE_INVERSE_o;
 574             INJECTIVE_INVERSE_o]);;
 575
 576 let PERMUTATION_INVERSE_COMPOSE = prove
 577  (`!p q. permutation p /\ permutation q
 578          ==> inverse(p o q) = inverse q o inverse p`,
 579   REPEAT STRIP_TAC THEN MATCH_MP_TAC INVERSE_UNIQUE_o THEN
 580   REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP PERMUTATION_INVERSE_WORKS)) THEN
 581   REWRITE_TAC[GSYM o_ASSOC] THEN REPEAT STRIP_TAC THEN
 582   GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [o_ASSOC] THEN
 583   ASM_REWRITE_TAC[I_O_ID]);;
 584
 585 let PERMUTATION_COMPOSE_EQ = prove
 586  (`(!p q:A->A. permutation(p) ==> (permutation(p o q) <=> permutation q)) /\
 587    (!p q:A->A. permutation(q) ==> (permutation(p o q) <=> permutation p))`,
 588   REPEAT STRIP_TAC THEN
 589   FIRST_ASSUM(ASSUME_TAC o MATCH_MP PERMUTATION_INVERSE) THEN
 590   EQ_TAC THEN ASM_SIMP_TAC[PERMUTATION_COMPOSE] THENL
 591    [DISCH_THEN(MP_TAC o SPEC `inverse(p:A->A)` o MATCH_MP
 592      (REWRITE_RULE[IMP_CONJ_ALT] PERMUTATION_COMPOSE));
 593     DISCH_THEN(MP_TAC o SPEC `inverse(q:A->A)` o MATCH_MP
 594      (REWRITE_RULE[IMP_CONJ] PERMUTATION_COMPOSE))] THEN
 595   ASM_SIMP_TAC[GSYM o_ASSOC; PERMUTATION_INVERSE_WORKS] THEN
 596   ASM_SIMP_TAC[o_ASSOC; PERMUTATION_INVERSE_WORKS] THEN
 597   REWRITE_TAC[I_O_ID]);;
 598
 599 let PERMUTATION_COMPOSE_SWAP = prove
 600  (`(!p a b:A. permutation(swap(a,b) o p) <=> permutation p) /\
 601    (!p a b:A. permutation(p o swap(a,b)) <=> permutation p)`,
 602   SIMP_TAC[PERMUTATION_COMPOSE_EQ; PERMUTATION_SWAP]);;
 603
 604 (* ------------------------------------------------------------------------- *)
 605 (* Relation to "permutes".                                                   *)
 606 (* ------------------------------------------------------------------------- *)
 607
 608 let PERMUTATION_PERMUTES = prove
 609  (`!p:A->A. permutation p <=> ?s. FINITE s /\ p permutes s`,
 610   GEN_TAC THEN REWRITE_TAC[PERMUTATION; permutes] THEN
 611   EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
 612    [EXISTS_TAC `{x:A | ~(p x = x)}` THEN ASM_SIMP_TAC[IN_ELIM_THM];
 613     MATCH_MP_TAC FINITE_SUBSET THEN EXISTS_TAC `s:A->bool` THEN
 614     ASM_SIMP_TAC[IN_ELIM_THM; SUBSET] THEN ASM_MESON_TAC[]]);;
 615
 616 (* ------------------------------------------------------------------------- *)
 617 (* Hence a sort of induction principle composing by swaps.                   *)
 618 (* ------------------------------------------------------------------------- *)
 619
 620 let PERMUTES_INDUCT = prove
 621  (`!P s. FINITE s /\
 622          P I /\
 623          (!a b:A p. a IN s /\ b IN s /\ P p /\ permutation p
 624                     ==> P (swap(a,b) o p))
 625          ==> (!p. p permutes s ==> P p)`,
 626   ONCE_REWRITE_TAC[TAUT `a /\ b /\ c ==> d <=> b ==> a ==> c ==> d`] THEN
 627   REWRITE_TAC[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
 628   MATCH_MP_TAC FINITE_INDUCT_STRONG THEN
 629   ASM_REWRITE_TAC[PERMUTES_EMPTY; IN_INSERT] THEN REPEAT STRIP_TAC THEN
 630   ASM_REWRITE_TAC[] THEN
 631   SUBGOAL_THEN `p = swap(x,p x) o swap(x,p x) o (p:A->A)` SUBST1_TAC THENL
 632    [REWRITE_TAC[o_ASSOC; SWAP_IDEMPOTENT; I_O_ID]; ALL_TAC] THEN
 633   FIRST_X_ASSUM(MP_TAC o check (is_imp o concl)) THEN
 634   ANTS_TAC THENL [ASM_MESON_TAC[]; ALL_TAC] THEN
 635   DISCH_THEN(fun th -> FIRST_X_ASSUM MATCH_MP_TAC THEN ASSUME_TAC th) THEN
 636   ASM_MESON_TAC[PERMUTES_IN_IMAGE; IN_INSERT; PERMUTES_INSERT_LEMMA;
 637                 PERMUTATION_PERMUTES; FINITE_INSERT; PERMUTATION_COMPOSE;
 638                 PERMUTATION_SWAP]);;
 639
 640 (* ------------------------------------------------------------------------- *)
 641 (* Sign of a permutation as a real number.                                   *)
 642 (* ------------------------------------------------------------------------- *)
 643
 644 let sign = new_definition
 645  `(sign p):real = if evenperm p then &1 else -- &1`;;
 646
 647 let SIGN_NZ = prove
 648  (`!p. ~(sign p = &0)`,
 649   REWRITE_TAC[sign] THEN REAL_ARITH_TAC);;
 650
 651 let SIGN_I = prove
 652  (`sign I = &1`,
 653   REWRITE_TAC[sign; EVENPERM_I]);;
 654
 655 let SIGN_INVERSE = prove
 656  (`!p. permutation p ==> sign(inverse p) = sign p`,
 657   SIMP_TAC[sign; EVENPERM_INVERSE] THEN REAL_ARITH_TAC);;
 658
 659 let SIGN_COMPOSE = prove
 660  (`!p q. permutation p /\ permutation q ==> sign(p o q) = sign(p) * sign(q)`,
 661   SIMP_TAC[sign; EVENPERM_COMPOSE] THEN REAL_ARITH_TAC);;
 662
 663 let SIGN_SWAP = prove
 664  (`!a b. sign(swap(a,b)) = if a = b then &1 else -- &1`,
 665   REWRITE_TAC[sign; EVENPERM_SWAP]);;
 666
 667 let SIGN_IDEMPOTENT = prove
 668  (`!p. sign(p) * sign(p) = &1`,
 669   GEN_TAC THEN REWRITE_TAC[sign] THEN
 670   COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV);;
 671
 672 let REAL_ABS_SIGN = prove
 673  (`!p. abs(sign p) = &1`,
 674   REWRITE_TAC[sign] THEN REAL_ARITH_TAC);;
 675
 676 (* ------------------------------------------------------------------------- *)
 677 (* More lemmas about permutations.                                           *)
 678 (* ------------------------------------------------------------------------- *)
 679
 680 let PERMUTES_NUMSET_LE = prove
 681  (`!p s:num->bool. p permutes s /\ (!i. i IN s ==> p(i) <= i) ==> p = I`,
 682   REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM; I_THM] THEN STRIP_TAC THEN
 683   MATCH_MP_TAC num_WF THEN X_GEN_TAC `n:num` THEN DISCH_TAC THEN
 684   ASM_CASES_TAC `(n:num) IN s` THENL [ALL_TAC; ASM_MESON_TAC[permutes]] THEN
 685   ASM_SIMP_TAC[GSYM LE_ANTISYM] THEN REWRITE_TAC[GSYM NOT_LT] THEN
 686   ASM_MESON_TAC[PERMUTES_INJECTIVE; LT_REFL]);;
 687
 688 let PERMUTES_NUMSET_GE = prove
 689  (`!p s:num->bool. p permutes s /\ (!i. i IN s ==> i <= p(i)) ==> p = I`,
 690   REPEAT STRIP_TAC THEN
 691   MP_TAC(SPECL [`inverse(p:num->num)`; `s:num->bool`] PERMUTES_NUMSET_LE) THEN
 692   ANTS_TAC THENL
 693    [ASM_MESON_TAC[PERMUTES_INVERSE; PERMUTES_INVERSES; PERMUTES_IN_IMAGE];
 694     ASM_MESON_TAC[PERMUTES_INVERSE_INVERSE; INVERSE_I]]);;
 695
 696 let IMAGE_INVERSE_PERMUTATIONS = prove
 697  (`!s:A->bool. {inverse p | p permutes s} = {p | p permutes s}`,
 698   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN
 699   MESON_TAC[PERMUTES_INVERSE_INVERSE; PERMUTES_INVERSE]);;
 700
 701 let IMAGE_COMPOSE_PERMUTATIONS_L = prove
 702  (`!s q:A->A. q permutes s ==> {q o p | p permutes s} = {p | p permutes s}`,
 703   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 704   X_GEN_TAC `p:A->A` THEN EQ_TAC THENL
 705    [ASM_MESON_TAC[PERMUTES_COMPOSE];
 706     DISCH_TAC THEN EXISTS_TAC `inverse(q:A->A) o (p:A->A)` THEN
 707     ASM_SIMP_TAC[o_ASSOC; PERMUTES_INVERSE; PERMUTES_COMPOSE] THEN
 708     ASM_MESON_TAC[PERMUTES_INVERSES_o; I_O_ID]]);;
 709
 710 let IMAGE_COMPOSE_PERMUTATIONS_R = prove
 711  (`!s q:A->A. q permutes s ==> {p o q | p permutes s} = {p | p permutes s}`,
 712   REWRITE_TAC[EXTENSION; IN_ELIM_THM] THEN REPEAT GEN_TAC THEN STRIP_TAC THEN
 713   X_GEN_TAC `p:A->A` THEN EQ_TAC THENL
 714    [ASM_MESON_TAC[PERMUTES_COMPOSE];
 715     DISCH_TAC THEN EXISTS_TAC `(p:A->A) o inverse(q:A->A)` THEN
 716     ASM_SIMP_TAC[GSYM o_ASSOC; PERMUTES_INVERSE; PERMUTES_COMPOSE] THEN
 717     ASM_MESON_TAC[PERMUTES_INVERSES_o; I_O_ID]]);;
 718
 719 let PERMUTES_IN_NUMSEG = prove
 720  (`!p n i. p permutes 1..n /\ i IN 1..n ==> 1 <= p(i) /\ p(i) <= n`,
 721   REWRITE_TAC[permutes; IN_NUMSEG] THEN MESON_TAC[]);;
 722
 723 let SUM_PERMUTATIONS_INVERSE = prove
 724  (`!f m n. sum {p | p permutes m..n} f =
 725            sum {p | p permutes m..n} (\p. f(inverse p))`,
 726   REPEAT GEN_TAC THEN
 727   GEN_REWRITE_TAC (funpow 2 LAND_CONV) [GSYM IMAGE_INVERSE_PERMUTATIONS] THEN
 728   GEN_REWRITE_TAC (funpow 2 LAND_CONV)
 729    [SET_RULE `{f x | p x} = IMAGE f {x | p x}`] THEN
 730   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM o_DEF] THEN
 731   MATCH_MP_TAC SUM_IMAGE THEN
 732   SIMP_TAC[FINITE_PERMUTATIONS; FINITE_NUMSEG; IN_ELIM_THM] THEN
 733   MESON_TAC[PERMUTES_INVERSE_INVERSE]);;
 734
 735 let SUM_PERMUTATIONS_COMPOSE_L = prove
 736  (`!f m n q.
 737         q permutes m..n
 738         ==> sum {p | p permutes m..n} f =
 739             sum {p | p permutes m..n} (\p. f(q o p))`,
 740   REPEAT STRIP_TAC THEN
 741   FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV)
 742    [GSYM(MATCH_MP IMAGE_COMPOSE_PERMUTATIONS_L th)]) THEN
 743   GEN_REWRITE_TAC (funpow 2 LAND_CONV)
 744    [SET_RULE `{f x | p x} = IMAGE f {x | p x}`] THEN
 745   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM o_DEF] THEN
 746   MATCH_MP_TAC SUM_IMAGE THEN
 747   SIMP_TAC[FINITE_PERMUTATIONS; FINITE_NUMSEG; IN_ELIM_THM] THEN
 748   REPEAT STRIP_TAC THEN
 749   FIRST_X_ASSUM(MP_TAC o AP_TERM `\p:num->num. inverse(q:num->num) o p`) THEN
 750   REWRITE_TAC[o_ASSOC] THEN
 751   EVERY_ASSUM(CONJUNCTS_THEN SUBST1_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
 752   REWRITE_TAC[I_O_ID]);;
 753
 754 let SUM_PERMUTATIONS_COMPOSE_R = prove
 755  (`!f m n q.
 756         q permutes m..n
 757         ==> sum {p | p permutes m..n} f =
 758             sum {p | p permutes m..n} (\p. f(p o q))`,
 759   REPEAT STRIP_TAC THEN
 760   FIRST_ASSUM(fun th -> GEN_REWRITE_TAC (funpow 2 LAND_CONV)
 761    [GSYM(MATCH_MP IMAGE_COMPOSE_PERMUTATIONS_R th)]) THEN
 762   GEN_REWRITE_TAC (funpow 2 LAND_CONV)
 763    [SET_RULE `{f x | p x} = IMAGE f {x | p x}`] THEN
 764   GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM o_DEF] THEN
 765   MATCH_MP_TAC SUM_IMAGE THEN
 766   SIMP_TAC[FINITE_PERMUTATIONS; FINITE_NUMSEG; IN_ELIM_THM] THEN
 767   REPEAT STRIP_TAC THEN
 768   FIRST_X_ASSUM(MP_TAC o AP_TERM `\p:num->num. p o inverse(q:num->num)`) THEN
 769   REWRITE_TAC[GSYM o_ASSOC] THEN
 770   EVERY_ASSUM(CONJUNCTS_THEN SUBST1_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
 771   REWRITE_TAC[I_O_ID]);;
 772
 773 (* ------------------------------------------------------------------------- *)
 774 (* Conversion for `{p | p permutes s}` where s is a set enumeration.         *)
 775 (* ------------------------------------------------------------------------- *)
 776
 777 let PERMSET_CONV =
 778   let pth_empty = prove
 779    (`{p | p permutes {}} = {I}`,
 780     REWRITE_TAC[PERMUTES_EMPTY] THEN SET_TAC[])
 781   and pth_cross = SET_RULE
 782     `IMAGE f {x,y | x IN {} /\ y IN t} = {} /\
 783      IMAGE f {x,y | x IN (a INSERT s) /\ y IN t} =
 784      (IMAGE (\y. f(a,y)) t) UNION (IMAGE f {x,y | x IN s /\ y IN t})`
 785   and pth_union = SET_RULE
 786     `{} UNION t = t /\
 787      (x INSERT s) UNION t = x INSERT (s UNION t)` in
 788   let rec PERMSET_CONV tm =
 789    (GEN_REWRITE_CONV I [pth_empty] ORELSEC
 790     (GEN_REWRITE_CONV I [PERMUTES_INSERT] THENC
 791      ONCE_DEPTH_CONV PERMSET_CONV THENC
 792      REWRITE_CONV[pth_cross] THENC
 793      REWRITE_CONV[IMAGE_CLAUSES] THENC
 794      REWRITE_CONV[pth_union] THENC
 795     REWRITE_CONV[SWAP_REFL; I_O_ID])) tm in
 796   PERMSET_CONV;;
 797
 798 (* ------------------------------------------------------------------------- *)
 799 (* Sum over a set of permutations (could generalize to iteration).           *)
 800 (* ------------------------------------------------------------------------- *)
 801
 802 let SUM_OVER_PERMUTATIONS_INSERT = prove
 803  (`!f a s. FINITE s /\ ~(a IN s)
 804            ==> sum {p:A->A | p permutes (a INSERT s)} f =
 805                sum (a INSERT s)
 806                    (\b. sum {p | p permutes s} (\q. f(swap(a,b) o q)))`,
 807   let lemma = prove
 808    (`(\(b,p). f (swap (a,b) o p)) = f o (\(b,p). swap(a,b) o p)`,
 809     REWRITE_TAC[FUN_EQ_THM; FORALL_PAIR_THM; o_THM]) in
 810   REPEAT STRIP_TAC THEN REWRITE_TAC[PERMUTES_INSERT] THEN
 811   ASM_SIMP_TAC[FINITE_PERMUTATIONS; FINITE_INSERT; SUM_SUM_PRODUCT] THEN
 812   REWRITE_TAC[lemma] THEN MATCH_MP_TAC SUM_IMAGE THEN
 813   REWRITE_TAC[FORALL_PAIR_THM; IN_ELIM_PAIR_THM] THEN
 814   REWRITE_TAC[IN_ELIM_THM] THEN
 815   MAP_EVERY X_GEN_TAC [`b:A`; `p:A->A`; `c:A`; `q:A->A`] THEN
 816   REPEAT STRIP_TAC THEN REWRITE_TAC[PAIR_EQ] THEN
 817   MATCH_MP_TAC(TAUT `p /\ (p ==> q) ==> p /\ q`) THEN CONJ_TAC THENL
 818    [FIRST_X_ASSUM(MP_TAC o C AP_THM `a:A`) THEN
 819     REWRITE_TAC[o_THM; swap] THEN ASM_MESON_TAC[permutes];
 820     DISCH_THEN SUBST_ALL_TAC THEN
 821     FIRST_X_ASSUM(MP_TAC o AP_TERM `(\p:A->A. swap(a:A,c) o p)`) THEN
 822     REWRITE_TAC[o_ASSOC; SWAP_IDEMPOTENT; I_O_ID]]);;
 823
 824 let SUM_OVER_PERMUTATIONS_NUMSEG = prove
 825  (`!f m n. m <= n
 826            ==> sum {p | p permutes (m..n)} f =
 827                sum(m..n) (\i. sum {p | p permutes (m+1..n)}
 828                                   (\q. f(swap(m,i) o q)))`,
 829   REPEAT STRIP_TAC THEN ASM_SIMP_TAC[GSYM NUMSEG_LREC] THEN
 830   MATCH_MP_TAC SUM_OVER_PERMUTATIONS_INSERT THEN
 831   REWRITE_TAC[FINITE_NUMSEG; IN_NUMSEG] THEN ARITH_TAC);;