permutesScript.sml

1(* ========================================================================= *)
2(* Permutations, both general and specifically on finite sets.               *)
3(*    (HOL-Light's Library/permutations.ml)                                  *)
4(*                                                                           *)
5(*              (c) Copyright, John Harrison 2010                            *)
6(*              (c) Copyright, Liming Li 2011                                *)
7(* ========================================================================= *)
8Theory permutes[bare]
9Ancestors
10  arithmetic combin pred_set pair num
11Libs
12  HolKernel Parse boolLib BasicProvers PairedLambda pred_setLib
13  tautLib numLib hurdUtils pureSimps metisLib simpLib
14
15
16val qx_gen_tac = Q.X_GEN_TAC;
17val qx_genl_tac = map_every qx_gen_tac;
18val qexists_tac = Q.EXISTS_TAC;
19val qexistsl_tac = map_every qexists_tac;
20val qid_spec_tac = Q.ID_SPEC_TAC;
21val rename1 = Q.RENAME1_TAC;
22val rw = SRW_TAC [];
23fun simp ths = ASM_SIMP_TAC (srw_ss()) ths;
24
25(* ========================================================================= *)
26(* HOL-Light compatibility layer                                             *)
27(* ========================================================================= *)
28
29(* |- CARD {} = 0 /\
30      !x s. FINITE s ==>
31            CARD (x INSERT s) = if x IN s then CARD s else SUC (CARD s)
32 *)
33val CARD_CLAUSES = CONJ CARD_EMPTY (PROVE [CARD_INSERT]
34  ``!x s. FINITE s ==>
35           (CARD (x INSERT s) = (if x IN s then CARD s else SUC (CARD s)))``);
36
37(* |- (!f. IMAGE f {} = {}) /\
38      !f x s. IMAGE f (x INSERT s) = f x INSERT IMAGE f s *)
39val IMAGE_CLAUSES = CONJ IMAGE_EMPTY IMAGE_INSERT;
40
41(* |- FINITE {} /\ !x s. FINITE (x INSERT s) <=> FINITE s *)
42val FINITE_RULES = CONJ FINITE_EMPTY FINITE_INSERT;
43
44(* |- !m n. SUC m = SUC n <=> m = n *)
45val SUC_INJ = prim_recTheory.INV_SUC_EQ;
46
47(* |- (!m. ~(m < 0)) /\ !m n. m < SUC n <=> m = n \/ m < n *)
48val LT = CONJ (DECIDE ``!m:num. ~(m < 0)``) prim_recTheory.LESS_THM;
49
50(* |- !n. ~(n < n) *)
51val LT_REFL = prim_recTheory.LESS_REFL;
52
53Theorem CONJ_EQ_IMP[local] :
54    !p q r. p /\ q ==> r <=> p ==> q ==> r
55Proof
56    REWRITE_TAC [AND_IMP_INTRO]
57QED
58
59Theorem IMP_CONJ_ALT[local] :
60    !p q r. p /\ q ==> r <=> q ==> p ==> r
61Proof
62    METIS_TAC [AND_IMP_INTRO]
63QED
64
65(* |- !(f :'a -> 'a) (g :'a -> 'a). f o g = (\(x :'a). f (g x)) *)
66Theorem o_ALPHA[local] = o_DEF |> INST_TYPE [gamma |-> alpha, beta |-> alpha]
67
68(* |- !(f :'a -> 'b) (g :'b -> 'a). f o g = (\(x :'b). f (g x)) *)
69Theorem o_BETA[local] = o_DEF |> INST_TYPE [alpha |-> beta]
70                              |> INST_TYPE [gamma |-> alpha]
71
72(* |- !(f :'a -> 'a) (g :'a -> 'a) (h :'a -> 'a). f o g o h = (f o g) o h *)
73Theorem o_ASSOC[local] = combinTheory.o_ASSOC
74     |> INST_TYPE [gamma |-> alpha, beta |-> alpha, delta |-> alpha]
75
76(* ========================================================================= *)
77(* Permutations, both general and specifically on finite sets.               *)
78(* ========================================================================= *)
79
80(* NOTE: the old name `PERMUTES` is conflict with pred_setTheory:
81
82   val _ = overload_on("PERMUTES", ``\f s. BIJ f s s``);
83
84   but the two definitions are not equivalent, according to Michael Norrish.
85   So I've chosen to use lower-case name: permutes.
86                                           -- Chun Tian (binghe), May 28, 2018
87 *)
88val _ = set_fixity "permutes" (Infix(NONASSOC, 450)); (* same as relation *)
89
90Definition permutes[nocompute]:
91   p permutes s <=> (!x. ~(x IN s) ==> (p(x) = x)) /\ (!y. ?!x. p x = y)
92End
93
94(* connection to ‘pred_set$PERMUTES’, added by Chun Tian *)
95Theorem permutes_alt :
96    !f s. f permutes s <=> f PERMUTES s /\ !x. x NOTIN s ==> f(x) = x
97Proof
98    RW_TAC std_ss [permutes, BIJ_ALT, IN_FUNSET]
99 >> EQ_TAC >> RW_TAC bool_ss []
100 >| [ (* goal 1 (of 3) : f x IN s *)
101      CCONTR_TAC \\
102     ‘f x <> x’ by PROVE_TAC [] \\
103     ‘f (f x) = f x’ by PROVE_TAC [] \\
104      Q.PAT_X_ASSUM ‘!y. ?!x. f x = y’ (MP_TAC o (Q.SPEC ‘f (x:'a)’)) \\
105      RW_TAC std_ss [EXISTS_UNIQUE_THM] \\
106      DISJ2_TAC >> qexistsl_tac [‘f x’, ‘x’] >> art [],
107      (* goal 2 (of 3): ?!x. x IN s /\ y = f x *)
108      Q.PAT_X_ASSUM ‘!y. ?!x. f x = y’ (MP_TAC o (Q.SPEC ‘y’)) \\
109      RW_TAC pure_ss [EXISTS_UNIQUE_THM]
110      >- (Q.EXISTS_TAC ‘x’ >> METIS_TAC []) \\
111      rename1 ‘y = z’ \\
112      FIRST_X_ASSUM MATCH_MP_TAC >> art [],
113      (* goal 3 (of 3): f x = x *)
114      Cases_on ‘y IN s’
115      >- (Q.PAT_X_ASSUM ‘!y. y IN s ==> ?!x. x IN s /\ y = f x’
116            (MP_TAC o (Q.SPEC ‘y’)) \\
117          RW_TAC bool_ss [EXISTS_UNIQUE_THM] >- (Q.EXISTS_TAC ‘x’ >> rw []) \\
118          rename1 ‘y = z’ \\
119          FIRST_X_ASSUM MATCH_MP_TAC >> art [] \\
120          CONJ_TAC >> CCONTR_TAC >> METIS_TAC []) \\
121     ‘f y = y’ by PROVE_TAC [] \\
122      SIMP_TAC std_ss [EXISTS_UNIQUE_THM] \\
123      CONJ_TAC >- (Q.EXISTS_TAC ‘y’ >> rw []) \\
124      qx_genl_tac [‘x’, ‘z’] >> rpt STRIP_TAC \\
125     ‘x NOTIN s’ by METIS_TAC [] \\
126     ‘z NOTIN s’ by METIS_TAC [] \\
127     ‘f x = x /\ f z = z’ by PROVE_TAC [] \\
128      PROVE_TAC [] ]
129QED
130
131Theorem permutes_alt_univ :
132    !f. f permutes UNIV <=> f PERMUTES UNIV
133Proof
134    rw [permutes_alt]
135QED
136
137Theorem permutes_imp :
138    !f s. f permutes s ==> f PERMUTES s
139Proof
140    RW_TAC bool_ss [permutes_alt]
141QED
142
143(* ------------------------------------------------------------------------- *)
144(* Inverse function (on whole universe).                                     *)
145(* ------------------------------------------------------------------------- *)
146
147Definition inverse[nocompute]:
148   inverse (f :'a->'b) = \y. @x. f x = y
149End
150
151(* This connection was suggested by Jeremy Dawson *)
152Theorem inverse_alt_LINV :
153    !f. (!y. ?x. f x = y) /\ (!x y. (f x = f y) ==> (x = y)) ==>
154        inverse f = LINV f UNIV
155Proof
156    Q.X_GEN_TAC ‘f’ >> STRIP_TAC
157 >> simp [FUN_EQ_THM]
158 >> Q.X_GEN_TAC ‘y’ >> rw [inverse]
159 >> SELECT_ELIM_TAC >> rw []
160 >> ONCE_REWRITE_TAC [EQ_SYM_EQ]
161 >> irule LINV_DEF >> rw [INJ_DEF]
162 >> Q.EXISTS_TAC ‘UNIV’ >> rw []
163QED
164
165Theorem SURJECTIVE_INVERSE :
166   !f. (!y. ?x. f x = y) <=> !y. f (inverse f y) = y
167Proof
168  GEN_TAC THEN EQ_TAC THEN REPEAT STRIP_TAC THENL[
169REWRITE_TAC[inverse] THEN
170CONV_TAC (ONCE_DEPTH_CONV Thm.BETA_CONV) THEN CONV_TAC SELECT_CONV,
171Q.EXISTS_TAC(`inverse f y`)] THEN PROVE_TAC[]
172QED
173
174Theorem SURJECTIVE_INVERSE_o :
175   !f. (!y. ?x. f x = y) <=> (f o inverse f = I)
176Proof
177    Q.X_GEN_TAC ‘f’
178 >> SIMP_TAC bool_ss [FUN_EQ_THM, o_BETA, I_THM]
179 >> PROVE_TAC [SURJECTIVE_INVERSE]
180QED
181
182(* cf. cardinalTheory.INJECTIVE_LEFT_INVERSE *)
183Theorem INJECTIVE_INVERSE :
184   !f. (!x y. (f x = f y) ==> (x = y)) <=> (!x. inverse f (f x) = x)
185Proof
186  GEN_TAC THEN EQ_TAC THENL[
187REPEAT STRIP_TAC THEN
188REWRITE_TAC[inverse] THEN
189CONV_TAC (ONCE_DEPTH_CONV Thm.BETA_CONV) THEN FIRST_ASSUM MATCH_MP_TAC THEN
190CONV_TAC SELECT_CONV THEN Q.EXISTS_TAC(`x`) THEN REFL_TAC,
191PROVE_TAC[]]
192QED
193
194Theorem INJECTIVE_INVERSE_o :
195   !f. (!x y. (f x = f y) ==> (x = y)) = (inverse f o f = I)
196Proof
197    Q.X_GEN_TAC ‘f’
198 >> SIMP_TAC bool_ss [FUN_EQ_THM, o_BETA, I_THM]
199 >> PROVE_TAC[INJECTIVE_INVERSE]
200QED
201
202Theorem INVERSE_UNIQUE_o :
203   !f g. (f o g = I) /\ (g o f = I) ==> (inverse f = g)
204Proof
205    rpt GEN_TAC
206 >> SIMP_TAC bool_ss [FUN_EQ_THM, o_BETA, I_THM]
207 >> PROVE_TAC[INJECTIVE_INVERSE, SURJECTIVE_INVERSE]
208QED
209
210(* NOTE: Previously this proof used combinTheory.I_o_ID, which has issues when
211         exporting permutes.ot.art. *)
212Theorem INVERSE_I :
213   inverse I = (I :'a -> 'a)
214Proof
215    MATCH_MP_TAC INVERSE_UNIQUE_o
216 >> SIMP_TAC bool_ss [FUN_EQ_THM, o_ALPHA, I_THM]
217QED
218
219(* ------------------------------------------------------------------------- *)
220(* Transpositions.                                                           *)
221(* ------------------------------------------------------------------------- *)
222
223(* cf. “pair$SWAP” (pairTheory.SWAP_def) *)
224Definition swap_def[nocompute]:
225   swap (i,j) k = if k = i then j else if k = j then i else k
226End
227
228Theorem SWAP_REFL :
229   !a. swap (a,a) = I
230Proof
231  REWRITE_TAC[FUN_EQ_THM, swap_def, I_THM] THEN PROVE_TAC[]
232QED
233
234Theorem SWAP_SYM :
235   !a b. swap(a,b) = swap(b,a)
236Proof
237  REWRITE_TAC[FUN_EQ_THM, swap_def, I_THM] THEN PROVE_TAC[]
238QED
239
240Theorem SWAP_IDEMPOTENT :
241   !a b. swap(a,b) o swap(a,b) = I
242Proof
243    rpt GEN_TAC
244 >> SIMP_TAC bool_ss [FUN_EQ_THM, swap_def, o_BETA, I_THM]
245 >> PROVE_TAC[]
246QED
247
248Theorem INVERSE_SWAP :
249   !a b. inverse(swap(a,b)) = swap(a,b)
250Proof
251  REPEAT GEN_TAC THEN MATCH_MP_TAC INVERSE_UNIQUE_o THEN
252  REWRITE_TAC[SWAP_IDEMPOTENT]
253QED
254
255Theorem SWAP_GALOIS :
256   !a b x y. (x = swap(a,b) y) = (y = swap(a,b) x)
257Proof
258  REWRITE_TAC[swap_def] THEN PROVE_TAC[]
259QED
260
261(* ------------------------------------------------------------------------- *)
262(* Basic consequences of the definition.                                     *)
263(* ------------------------------------------------------------------------- *)
264
265Theorem PERMUTES_IN_IMAGE :
266   !p s x. p permutes s ==> (p(x) IN s <=> x IN s)
267Proof
268  REWRITE_TAC[permutes] THEN PROVE_TAC[]
269QED
270
271Theorem PERMUTES_IMAGE :
272   !p s. p permutes s ==> (IMAGE p s = s)
273Proof
274  REWRITE_TAC[permutes, EXTENSION, IN_IMAGE] THEN PROVE_TAC[]
275QED
276
277Theorem PERMUTES_INJECTIVE :
278   !p s. p permutes s ==> !x y. (p(x) = p(y)) = (x = y)
279Proof
280  REWRITE_TAC[permutes] THEN PROVE_TAC[]
281QED
282
283Theorem PERMUTES_SURJECTIVE :
284   !p s. p permutes s ==> !y. ?x. p(x) = y
285Proof
286  REWRITE_TAC[permutes] THEN PROVE_TAC[]
287QED
288
289Theorem PERMUTES_INVERSES_o :
290   !p s. p permutes s ==> (p o inverse(p) = I) /\ (inverse(p) o p = I)
291Proof
292  REWRITE_TAC[GSYM INJECTIVE_INVERSE_o, GSYM SURJECTIVE_INVERSE_o] THEN
293  REWRITE_TAC[permutes] THEN PROVE_TAC[]
294QED
295
296Theorem PERMUTES_INVERSES :
297   !p s. p permutes s
298         ==> (!x. p(inverse(p) x) = x) /\ (!x. inverse(p) (p x) = x)
299Proof
300  REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP PERMUTES_INVERSES_o) THEN
301  SIMP_TAC bool_ss [FUN_EQ_THM, o_ALPHA, I_THM]
302QED
303
304Theorem PERMUTES_SUBSET :
305   !p s t. p permutes s /\ s SUBSET t ==> p permutes t
306Proof
307  REWRITE_TAC[permutes, SUBSET_DEF] THEN PROVE_TAC[]
308QED
309
310Theorem PERMUTES_EMPTY :
311   !p. p permutes {} <=> (p = I)
312Proof
313  REWRITE_TAC[FUN_EQ_THM, I_THM, permutes, NOT_IN_EMPTY] THEN PROVE_TAC[]
314QED
315
316Theorem PERMUTES_SING :
317   !p a. p permutes {a} <=> (p = I)
318Proof
319  REWRITE_TAC[FUN_EQ_THM, I_THM, permutes, IN_SING] THEN PROVE_TAC[]
320QED
321
322Theorem PERMUTES_UNIV :
323   !p. p permutes UNIV <=> !y. ?!x. p x = y
324Proof
325  REWRITE_TAC[permutes, IN_UNIV]
326QED
327
328Theorem PERMUTES_INVERSE_EQ :
329   !p s. p permutes s ==> !x y. (inverse(p) y = x) <=> (p x = y)
330Proof
331  REWRITE_TAC[permutes, inverse] THEN METIS_TAC[]
332QED
333
334Theorem PERMUTES_SWAP :
335   !a b s. a IN s /\ b IN s ==> swap(a,b) permutes s
336Proof
337  REWRITE_TAC[permutes, swap_def] THEN METIS_TAC[]
338QED
339
340Theorem PERMUTES_SUPERSET :
341   !p s t. p permutes s /\ (!x. x IN (s DIFF t) ==> (p(x) = x))
342           ==> p permutes t
343Proof
344  REWRITE_TAC[permutes, IN_DIFF] THEN PROVE_TAC[]
345QED
346
347(* ------------------------------------------------------------------------- *)
348(* Group properties.                                                         *)
349(* ------------------------------------------------------------------------- *)
350
351Theorem PERMUTES_I :
352   !s. I permutes s
353Proof
354  REWRITE_TAC[permutes, I_THM] THEN PROVE_TAC[]
355QED
356
357Theorem PERMUTES_COMPOSE :
358   !p q s x. p permutes s /\ q permutes s ==> (q o p) permutes s
359Proof
360    rpt GEN_TAC
361 >> SIMP_TAC bool_ss [permutes, o_ALPHA] >> PROVE_TAC[]
362QED
363
364Theorem PERMUTES_INVERSE :
365   !p s. p permutes s ==> inverse(p) permutes s
366Proof
367  REPEAT STRIP_TAC THEN
368  FIRST_ASSUM(MP_TAC o MATCH_MP PERMUTES_INVERSE_EQ) THEN
369  POP_ASSUM MP_TAC THEN REWRITE_TAC[permutes] THEN PROVE_TAC[]
370QED
371
372Theorem PERMUTES_INVERSE_INVERSE :
373   !p s. p permutes s ==> (inverse(inverse(p)) = p)
374Proof
375  REWRITE_TAC [FUN_EQ_THM] THEN
376  PROVE_TAC[PERMUTES_INVERSE_EQ, PERMUTES_INVERSE]
377QED
378
379(* ------------------------------------------------------------------------- *)
380(* The number of permutations on a finite set.                               *)
381(* ------------------------------------------------------------------------- *)
382
383Theorem PERMUTES_INSERT_LEMMA :
384   !p a s. p permutes (a INSERT s) ==> (swap(a,p(a)) o p) permutes s
385Proof
386  REPEAT STRIP_TAC THEN MATCH_MP_TAC PERMUTES_SUPERSET THEN
387  Q.EXISTS_TAC `a INSERT s` THEN CONJ_TAC THEN
388  METIS_TAC[PERMUTES_SWAP, PERMUTES_IN_IMAGE, IN_INSERT, PERMUTES_COMPOSE,
389            o_ALPHA, swap_def, IN_DIFF]
390QED
391
392Theorem PERMUTES_INSERT :
393   {p | p permutes (a INSERT s)} =
394        IMAGE (\(b,p). swap(a,b) o p)
395              {(b,p) | b IN a INSERT s /\ p IN {p | p permutes s}}
396Proof
397  REWRITE_TAC[EXTENSION, IN_IMAGE] THEN Q.X_GEN_TAC `p: 'a -> 'a` THEN
398  CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
399  CONV_TAC(DEPTH_CONV GEN_BETA_CONV) THEN
400  SIMP_TAC std_ss[EXISTS_PROD]THEN EQ_TAC THENL
401   [DISCH_TAC THEN
402    qexistsl_tac [`(p: 'a -> 'a) a`, `swap(a,p a) o (p: 'a -> 'a)`]  THEN
403    ASM_REWRITE_TAC[SWAP_IDEMPOTENT, o_ASSOC, I_o_ID] THEN
404    PROVE_TAC[PERMUTES_IN_IMAGE, IN_INSERT, PERMUTES_INSERT_LEMMA],
405    SIMP_TAC std_ss[GSYM LEFT_FORALL_IMP_THM] THEN
406    qx_genl_tac [`b: 'a `, `q: 'a -> 'a `] THEN
407    STRIP_TAC THEN MATCH_MP_TAC PERMUTES_COMPOSE THEN
408    PROVE_TAC[PERMUTES_SUBSET, SUBSET_DEF, IN_INSERT, PERMUTES_SWAP]]
409QED
410
411Theorem HAS_SIZE_PERMUTATIONS :
412  !s:'a ->bool n: num.
413    (s HAS_SIZE n) ==> ({p | p permutes s} HAS_SIZE (FACT n))
414Proof
415    SIMP_TAC std_ss [HAS_SIZE, GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM]
416 >> SET_INDUCT_TAC (* 2 sub-goals here *)
417 >> SIMP_TAC std_ss [PERMUTES_EMPTY, CARD_CLAUSES, GSPEC_EQ, FINITE_SING,
418                     CARD_SING, FACT]
419 >> REWRITE_TAC [GSYM HAS_SIZE, PERMUTES_INSERT]
420 >> MATCH_MP_TAC HAS_SIZE_IMAGE_INJ
421 >> CONJ_TAC (* still 2 sub-goals here *)
422 >| [ (* goal 1 (of 2) *)
423      SIMP_TAC std_ss [FORALL_PROD] \\
424      CONV_TAC (DEPTH_CONV SET_SPEC_CONV) \\
425      REWRITE_TAC[PAIR_EQ] \\
426      qx_genl_tac [`b: 'a`, `q: 'a -> 'a`, `c: 'a`, `r: 'a -> 'a`] \\
427      STRIP_TAC \\
428      Q.SUBGOAL_THEN `c: 'a = b` SUBST_ALL_TAC >| (* 2 sub-goals here *)
429      [ (* goal 1.1 (of 2) *)
430        FIRST_X_ASSUM (MP_TAC o C Q.AP_THM `e: 'a`) \\
431        REWRITE_TAC [o_ALPHA, swap_def] \\
432        Q.SUBGOAL_THEN `((q: 'a -> 'a) e = e) /\ ((r: 'a -> 'a) e = e)`
433                (fn th => SIMP_TAC std_ss[th]) \\
434        PROVE_TAC [permutes],
435        (* goal 1.2 (of 2) *)
436        FIRST_X_ASSUM (MP_TAC o Q.AP_TERM `(\q:'a -> 'a. swap(e:'a,b) o q)`) \\
437        BETA_TAC \\
438        REWRITE_TAC [SWAP_IDEMPOTENT, o_ASSOC, I_o_ID] ],
439      (* goal 2 (of 2) *)
440      Know `{(b,p) | b IN e INSERT s /\ p IN {p | p permutes s}} =
441            (e INSERT s) CROSS {p | p permutes s}`
442      >- (REWRITE_TAC [EXTENSION, CROSS_DEF] \\
443          GEN_TAC >> REWRITE_TAC [GSPECIFICATION] >> BETA_TAC \\
444          REWRITE_TAC [PAIR_EQ] >> EQ_TAC >> STRIP_TAC >| (* 2 sub-goals here *)
445          [ (* goal 2.1 (of 2) *)
446            Cases_on `x'` >> FULL_SIMP_TAC std_ss [],
447            (* goal 2.2 (of 2) *)
448            Q.EXISTS_TAC `(FST x, SND x)` >> FULL_SIMP_TAC std_ss [] ] ) \\
449      DISCH_TAC >> ASM_REWRITE_TAC [] \\
450      ASM_SIMP_TAC std_ss [HAS_SIZE, FINITE_INSERT, CARD_CLAUSES, FINITE_CROSS,
451                           CARD_CROSS,FACT] ]
452QED
453
454Theorem FINITE_PERMUTATIONS :
455   !s. FINITE s ==> FINITE {p | p permutes s}
456Proof
457  METIS_TAC[HAS_SIZE_PERMUTATIONS, HAS_SIZE]
458QED
459
460Theorem CARD_PERMUTATIONS :
461   !s. FINITE s ==> (CARD {p | p permutes s} = FACT(CARD s))
462Proof
463  METIS_TAC[HAS_SIZE, HAS_SIZE_PERMUTATIONS]
464QED
465
466(* ------------------------------------------------------------------------- *)
467(* Alternative characterizations of permutation of finite set.               *)
468(* ------------------------------------------------------------------------- *)
469
470(* TODO: the following 2 theorem need long proof search of METIC_TAC *)
471Theorem PERMUTES_FINITE_INJECTIVE :
472   !s: 'a->bool p.
473        FINITE s
474        ==> (p permutes s <=>
475             (!x. ~(x IN s) ==> (p x = x)) /\
476             (!x. x IN s ==> p x IN s) /\
477             (!x y. x IN s /\ y IN s /\ (p x = p y) ==> (x = y)))
478Proof
479  REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC THEN
480  MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
481  DISCH_TAC THEN EQ_TAC THENL [PROVE_TAC[], ALL_TAC] THEN STRIP_TAC THEN
482  FIRST_ASSUM(MP_TAC o Q.SPEC `p: 'a -> 'a ` o MATCH_MP
483   (REWRITE_RULE[GSYM AND_IMP_INTRO] SURJECTIVE_IFF_INJECTIVE)) THEN
484  ASM_SIMP_TAC std_ss[SUBSET_DEF, FORALL_IN_IMAGE] THEN
485  STRIP_TAC THEN Q.X_GEN_TAC `y: 'a ` THEN
486  Q.ASM_CASES_TAC `(y: 'a) IN s` THEN METIS_TAC[]
487QED
488
489Theorem PERMUTES_FINITE_SURJECTIVE :
490   !s: 'a ->bool p.
491        FINITE s
492        ==> (p permutes s <=>
493             (!x. ~(x IN s) ==> (p x = x)) /\ (!x. x IN s ==> p x IN s) /\
494             (!y. y IN s ==> ?x. x IN s /\ (p x = y)))
495Proof
496  REWRITE_TAC[permutes] THEN REPEAT STRIP_TAC THEN
497  MATCH_MP_TAC(TAUT `(p ==> (q <=> r)) ==> (p /\ q <=> p /\ r)`) THEN
498  DISCH_TAC THEN EQ_TAC THENL [PROVE_TAC[], ALL_TAC] THEN STRIP_TAC THEN
499  FIRST_ASSUM(MP_TAC o Q.SPEC `p: 'a -> 'a ` o MATCH_MP
500   (REWRITE_RULE[GSYM AND_IMP_INTRO] SURJECTIVE_IFF_INJECTIVE)) THEN
501  ASM_SIMP_TAC std_ss[SUBSET_DEF, FORALL_IN_IMAGE] THEN
502  STRIP_TAC THEN Q.X_GEN_TAC `y: 'a ` THEN
503  Q.ASM_CASES_TAC `(y: 'a) IN s` THEN METIS_TAC[]
504QED
505
506(* ------------------------------------------------------------------------- *)
507(* Various combinations of transpositions with 2, 1 and 0 common elements.   *)
508(* ------------------------------------------------------------------------- *)
509
510Theorem SWAP_COMMON :
511  !a b c: 'a. ~(a = c) /\ ~(b = c) ==>
512              (swap(a,b) o swap(a,c) = swap(b,c) o swap(a,b))
513Proof
514    REPEAT GEN_TAC
515 >> SIMP_TAC bool_ss[FUN_EQ_THM, swap_def, o_ALPHA]
516 >> DISCH_TAC >> GEN_TAC
517 >> MAP_EVERY Q.ASM_CASES_TAC [`x: 'a = a`, `x: 'a = b`, `x: 'a = c`]
518 >> REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) >> ASM_REWRITE_TAC[]
519 >> PROVE_TAC[]
520QED
521
522Theorem SWAP_COMMON' :
523   !a b c:'a. ~(a = b) /\ ~(a = c)
524             ==> (swap(a,c) o swap(b,c) = swap(b,c) o swap(a,b))
525Proof
526  REPEAT STRIP_TAC THEN
527  GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) empty_rewrites [SWAP_SYM] THEN
528  ASM_SIMP_TAC std_ss[GSYM SWAP_COMMON] THEN
529  GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) empty_rewrites [SWAP_SYM] THEN
530  REFL_TAC
531QED
532
533Theorem SWAP_INDEPENDENT :
534   !a b c d:'a. ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d)
535               ==> (swap(a,b) o swap(c,d) = swap(c,d) o swap(a,b))
536Proof
537    REPEAT GEN_TAC
538 >> SIMP_TAC bool_ss[FUN_EQ_THM, swap_def, o_ALPHA]
539 >> DISCH_TAC >> GEN_TAC
540 >> MAP_EVERY Q.ASM_CASES_TAC [`x: 'a = a`, `x: 'a = b`, `x: 'a = c`]
541 >> REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) >> ASM_REWRITE_TAC[]
542 >> PROVE_TAC[]
543QED
544
545(* ------------------------------------------------------------------------- *)
546(* Permutations as transposition sequences.                                  *)
547(* ------------------------------------------------------------------------- *)
548
549Inductive swapseq :
550   (swapseq 0 I) /\
551   (!a b p n. swapseq n p /\ ~(a = b) ==> swapseq (SUC n) (swap(a,b) o p))
552End
553
554Definition permutation[nocompute]:
555   permutation p = ?n. swapseq n p
556End
557
558(* ------------------------------------------------------------------------- *)
559(* Some closure properties of the set of permutations, with lengths.         *)
560(* ------------------------------------------------------------------------- *)
561
562Theorem SWAPSEQ_I = CONJUNCT1 swapseq_rules
563
564Theorem PERMUTATION_I :
565   permutation I
566Proof
567  REWRITE_TAC[permutation] THEN PROVE_TAC[SWAPSEQ_I]
568QED
569
570Theorem SWAPSEQ_SWAP :
571   !a b. swapseq (if a = b then 0 else 1) (swap(a,b))
572Proof
573  REPEAT GEN_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[ONE] THEN
574  PROVE_TAC[swapseq_rules, I_o_ID, SWAPSEQ_I, SWAP_REFL]
575QED
576
577Theorem PERMUTATION_SWAP :
578   !a b. permutation (swap(a,b))
579Proof
580  REWRITE_TAC[permutation] THEN PROVE_TAC[SWAPSEQ_SWAP]
581QED
582
583Theorem SWAPSEQ_COMPOSE :
584   !n p m q. swapseq n p /\ swapseq m q ==> swapseq (n + m) (p o q)
585Proof
586  SIMP_TAC std_ss[RIGHT_FORALL_IMP_THM, GSYM AND_IMP_INTRO] THEN
587  HO_MATCH_MP_TAC swapseq_ind THEN
588  REWRITE_TAC[ADD_CLAUSES, I_o_ID, GSYM o_ASSOC] THEN
589  PROVE_TAC[swapseq_rules]
590QED
591
592Theorem PERMUTATION_COMPOSE :
593   !p q. permutation p /\ permutation q ==> permutation (p o q)
594Proof
595  REWRITE_TAC[permutation] THEN PROVE_TAC[SWAPSEQ_COMPOSE]
596QED
597
598Theorem SWAPSEQ_ENDSWAP :
599   !n p a b:'a. swapseq n p /\ ~(a = b) ==> swapseq (SUC n) (p o swap(a,b))
600Proof
601  SIMP_TAC std_ss[RIGHT_FORALL_IMP_THM, GSYM AND_IMP_INTRO] THEN
602  HO_MATCH_MP_TAC swapseq_ind THEN REWRITE_TAC[I_o_ID, GSYM o_ASSOC] THEN
603  PROVE_TAC[o_ASSOC, swapseq_rules, I_o_ID]
604QED
605
606Theorem SWAPSEQ_INVERSE_EXISTS :
607   !n p:'a->'a. swapseq n p ==> ?q. swapseq n q /\ (p o q = I) /\ (q o p = I)
608Proof
609  HO_MATCH_MP_TAC swapseq_ind THEN CONJ_TAC THENL
610   [PROVE_TAC[I_o_ID, swapseq_rules], ALL_TAC] THEN
611  REPEAT STRIP_TAC THEN
612  MP_TAC(Q.SPECL [`n:num`, `q:'a->'a`, `a:'a`, `b:'a`] SWAPSEQ_ENDSWAP) THEN
613  ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
614  Q.EXISTS_TAC `(q:'a->'a) o swap(a,b)` THEN
615  ASM_REWRITE_TAC[GSYM o_ASSOC] THEN
616  GEN_REWRITE_TAC (BINOP_CONV o LAND_CONV o RAND_CONV)
617                  empty_rewrites [o_ASSOC] THEN
618  ASM_REWRITE_TAC[SWAP_IDEMPOTENT, I_o_ID]
619QED
620
621Theorem SWAPSEQ_INVERSE :
622   !n p. swapseq n p ==> swapseq n (inverse p)
623Proof
624  PROVE_TAC[SWAPSEQ_INVERSE_EXISTS, INVERSE_UNIQUE_o]
625QED
626
627Theorem PERMUTATION_INVERSE :
628   !p. permutation p ==> permutation (inverse p)
629Proof
630  REWRITE_TAC[permutation] THEN PROVE_TAC[SWAPSEQ_INVERSE]
631QED
632
633(* ------------------------------------------------------------------------- *)
634(* The identity map only has even transposition sequences.                   *)
635(* ------------------------------------------------------------------------- *)
636
637Theorem SYMMETRY_LEMMA[local] :
638  (!a b c d:'a. P a b c d ==> P a b d c) /\
639  (!a b c d.
640     ~(a = b) /\ ~(c = d) /\
641     ((a = c) /\ (b = d) \/ (a = c) /\ ~(b = d) \/ ~(a = c) /\ (b = d) \/
642      ~(a = c) /\ ~(a = d) /\ ~(b = c) /\ ~(b = d))
643     ==> P a b c d)
644  ==> (!a b c d. ~(a = b) /\ ~(c = d) ==> P a b c d)
645Proof
646  REPEAT STRIP_TAC THEN MAP_EVERY Q.ASM_CASES_TAC
647   [`a:'a = c`, `a:'a = d`, `b:'a = c`, `b:'a = d`] THEN
648  PROVE_TAC[]
649QED
650
651Theorem SWAP_GENERAL :
652   !a b c d:'a.
653        ~(a = b) /\ ~(c = d)
654        ==> (swap(a,b) o swap(c,d) = I) \/
655            ?x y z. ~(x = a) /\ ~(y = a) /\ ~(z = a) /\ ~(x = y) /\
656                    (swap(a,b) o swap(c,d) = swap(x,y) o swap(a,z))
657Proof
658  HO_MATCH_MP_TAC SYMMETRY_LEMMA THEN CONJ_TAC THENL
659   [SIMP_TAC std_ss[SWAP_SYM], ALL_TAC] THEN
660  REPEAT STRIP_TAC THEN REPEAT(FIRST_X_ASSUM SUBST_ALL_TAC) THENL
661   [PROVE_TAC[SWAP_IDEMPOTENT],
662    DISJ2_TAC THEN qexistsl_tac [`b:'a`, `d:'a`, `b:'a`] THEN
663    PROVE_TAC[SWAP_COMMON],
664    DISJ2_TAC THEN qexistsl_tac [`c:'a`, `d:'a`, `c:'a`] THEN
665    PROVE_TAC[SWAP_COMMON'],
666    DISJ2_TAC THEN qexistsl_tac [`c:'a`, `d:'a`, `b:'a`] THEN
667  PROVE_TAC[SWAP_INDEPENDENT]]
668QED
669
670Theorem FIXING_SWAPSEQ_DECREASE :
671   !n p a b:'a.
672      swapseq n p /\ ~(a = b) /\ ((swap(a,b) o p) a = a)
673      ==> ~(n = 0) /\ swapseq (n - 1) (swap(a,b) o p)
674Proof
675  INDUCT_TAC THEN REPEAT GEN_TAC THEN
676  GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) empty_rewrites [swapseq_cases] THEN
677  REWRITE_TAC[SUC_NOT, GSYM SUC_NOT] THENL
678   [DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
679    ASM_SIMP_TAC bool_ss[I_THM, o_ALPHA, swap_def],
680    ALL_TAC] THEN
681  SIMP_TAC bool_ss[GSYM LEFT_FORALL_IMP_THM, GSYM LEFT_EXISTS_AND_THM] THEN
682  qx_genl_tac [`c:'a`, `d:'a`, `q:'a->'a`, `m:num`] THEN
683  REWRITE_TAC[ADD1,EQ_ADD_RCANCEL, GSYM CONJ_ASSOC] THEN
684  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
685  FIRST_X_ASSUM(SUBST_ALL_TAC o SYM) THEN
686  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
687  FIRST_X_ASSUM SUBST_ALL_TAC THEN REWRITE_TAC[o_ASSOC] THEN STRIP_TAC THEN
688  MP_TAC(Q.SPECL [`a:'a`, `b:'a`, `c:'a`, `d:'a`] SWAP_GENERAL) THEN
689  ASM_REWRITE_TAC[] THEN
690  DISCH_THEN(DISJ_CASES_THEN2 SUBST_ALL_TAC MP_TAC) THEN
691  ASM_REWRITE_TAC[I_o_ID, ADD_SUB] THEN
692  SIMP_TAC bool_ss[GSYM LEFT_FORALL_IMP_THM] THEN
693  qx_genl_tac [`x:'a`, `y:'a`, `z:'a`] THEN
694  REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
695  DISCH_THEN SUBST_ALL_TAC THEN FIRST_X_ASSUM(MP_TAC o Q.SPECL
696   [`q:'a->'a`, `a:'a`, `z:'a`]) THEN
697  GEN_REWRITE_TAC (LAND_CONV) empty_rewrites [IMP_DISJ_THM] THEN
698  REWRITE_TAC[DISJ_IMP_THM] THEN CONJ_TAC THENL
699  [ (* goal 1 (of 2) *)
700    GEN_REWRITE_TAC (RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)
701    empty_rewrites [EQ_SYM_EQ] THEN ASM_REWRITE_TAC[] THEN
702    Q.PAT_X_ASSUM `$= X Y` MP_TAC THEN
703    REWRITE_TAC[GSYM o_ASSOC] THEN
704    Q.ABBREV_TAC `r:'a->'a = swap(a:'a,z) o q` THEN
705    ASM_SIMP_TAC bool_ss[FUN_EQ_THM, o_ALPHA, swap_def] THEN PROVE_TAC[],
706    (* goal 2 (of 2) *)
707    qid_spec_tac `n:num` THEN INDUCT_TAC THEN
708    REWRITE_TAC[SUC_NOT, SUC_SUB1, GSYM o_ASSOC] THEN
709    PROVE_TAC[swapseq_rules] ]
710QED
711
712Theorem SWAPSEQ_IDENTITY_EVEN :
713   !n. swapseq n (I:'a->'a) ==> EVEN n
714Proof
715  HO_MATCH_MP_TAC COMPLETE_INDUCTION THEN Q.X_GEN_TAC `n:num` THEN
716  DISCH_TAC THEN
717  GEN_REWRITE_TAC LAND_CONV empty_rewrites [swapseq_cases] THEN
718  DISCH_THEN(DISJ_CASES_THEN2 (SUBST_ALL_TAC o CONJUNCT1) MP_TAC) THEN
719  REWRITE_TAC[EVEN] THEN SIMP_TAC bool_ss[GSYM LEFT_FORALL_IMP_THM] THEN
720  qx_genl_tac [`a:'a`, `b:'a`, `p:'a->'a`, `m:num`] THEN
721  DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
722  MP_TAC(Q.SPECL [`m:num`, `p:'a->'a`, `a:'a`, `b:'a`]
723    FIXING_SWAPSEQ_DECREASE) THEN
724  GEN_REWRITE_TAC
725    (LAND_CONV o LAND_CONV o RAND_CONV o LAND_CONV o ONCE_DEPTH_CONV)
726    empty_rewrites [EQ_SYM_EQ] THEN ASM_REWRITE_TAC[I_THM] THEN STRIP_TAC THEN
727  FIRST_X_ASSUM(MP_TAC o SPEC ``(m - 1):num``) THEN
728  Q.UNDISCH_THEN `SUC m = n` (SUBST_ALL_TAC o SYM) THEN
729  ASM_REWRITE_TAC[DECIDE ``m - 1 < SUC m``] THEN Q.UNDISCH_TAC `~(m = 0)` THEN
730  qid_spec_tac `m:num` THEN INDUCT_TAC THEN
731  REWRITE_TAC[SUC_SUB1, EVEN]
732QED
733
734(* ------------------------------------------------------------------------- *)
735(* Therefore we have a welldefined notion of parity.                         *)
736(* ------------------------------------------------------------------------- *)
737
738Definition evenperm[nocompute]:
739   evenperm p = EVEN(@n. swapseq n p)
740End
741
742Theorem SWAPSEQ_EVEN_EVEN :
743   !m n p:'a->'a. swapseq m p /\ swapseq n p ==> (EVEN m <=> EVEN n)
744Proof
745  REPEAT STRIP_TAC THEN
746  FIRST_X_ASSUM(MP_TAC o MATCH_MP SWAPSEQ_INVERSE_EXISTS) THEN
747  STRIP_TAC THEN
748  FIRST_X_ASSUM(MP_TAC o AP_TERM ``swapseq (n + m) :('a->'a)->bool``) THEN
749  ASM_SIMP_TAC bool_ss[SWAPSEQ_COMPOSE] THEN
750  DISCH_THEN(MP_TAC o MATCH_MP SWAPSEQ_IDENTITY_EVEN) THEN
751  SIMP_TAC bool_ss[EVEN_ADD]
752QED
753
754Theorem EVENPERM_UNIQUE :
755   !n p b. swapseq n p /\ (EVEN n = b) ==> (evenperm p = b)
756Proof
757  REWRITE_TAC[evenperm] THEN METIS_TAC[SWAPSEQ_EVEN_EVEN]
758QED
759
760(* ------------------------------------------------------------------------- *)
761(* And it has the expected composition properties.                           *)
762(* ------------------------------------------------------------------------- *)
763
764Theorem EVENPERM_I :
765   evenperm I = T
766Proof
767  MATCH_MP_TAC EVENPERM_UNIQUE THEN PROVE_TAC[swapseq_rules, EVEN]
768QED
769
770Theorem EVENPERM_SWAP :
771   !a b:'a. evenperm (swap(a,b)) <=> (a = b)
772Proof
773  REPEAT GEN_TAC THEN MATCH_MP_TAC EVENPERM_UNIQUE THEN
774  METIS_TAC[SWAPSEQ_SWAP, EVEN, num_CONV ``1:num``]
775QED
776
777Theorem EVENPERM_COMPOSE :
778   !p q. permutation p /\ permutation q
779         ==> (evenperm (p o q) = (evenperm p = evenperm q))
780Proof
781  REWRITE_TAC[permutation] THEN
782  SIMP_TAC bool_ss[GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM] THEN
783  SIMP_TAC bool_ss[GSYM LEFT_FORALL_IMP_THM] THEN REPEAT GEN_TAC THEN
784  DISCH_THEN(fn th => ASSUME_TAC th THEN
785               ASSUME_TAC(MATCH_MP SWAPSEQ_COMPOSE th)) THEN
786  METIS_TAC[EVENPERM_UNIQUE, SWAPSEQ_COMPOSE, EVEN_ADD]
787QED
788
789Theorem EVENPERM_INVERSE :
790   !p. permutation p ==> (evenperm (inverse p) = evenperm p)
791Proof
792  REWRITE_TAC[permutation] THEN REPEAT STRIP_TAC THEN
793  MATCH_MP_TAC EVENPERM_UNIQUE THEN
794  METIS_TAC[SWAPSEQ_INVERSE, EVENPERM_UNIQUE]
795QED
796
797(* ------------------------------------------------------------------------- *)
798(* A more abstract characterization of permutations.                         *)
799(* ------------------------------------------------------------------------- *)
800
801(* cf. pred_setTheory.BIJ_ALT *)
802Theorem PERMUTATION_BIJECTIVE :
803   !p. permutation p ==> !y. ?!x. p(x) = y
804Proof
805  REWRITE_TAC[permutation] THEN REPEAT STRIP_TAC THEN
806  FIRST_X_ASSUM(MP_TAC o MATCH_MP SWAPSEQ_INVERSE_EXISTS) THEN
807  SIMP_TAC bool_ss[FUN_EQ_THM, I_THM, o_ALPHA, GSYM LEFT_FORALL_IMP_THM] THEN
808  METIS_TAC[]
809QED
810
811Theorem PERMUTATION_FINITE_SUPPORT :
812   !p. permutation p ==> FINITE {x:'a| ~(p x = x)}
813Proof
814  SIMP_TAC bool_ss[permutation, GSYM LEFT_FORALL_IMP_THM] THEN
815  CONV_TAC SWAP_VARS_CONV THEN HO_MATCH_MP_TAC swapseq_ind THEN
816  REWRITE_TAC[I_THM, FINITE_RULES,
817              Q.prove (`{x | F} = {}`,REWRITE_TAC[EXTENSION] THEN
818              CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
819              REWRITE_TAC[NOT_IN_EMPTY])] THEN
820  qx_genl_tac [`a:'a`, `b:'a`, `p:'a->'a`] THEN
821  STRIP_TAC THEN MATCH_MP_TAC SUBSET_FINITE_I THEN
822  Q.EXISTS_TAC `(a:'a) INSERT b INSERT {x | ~(p x = x)}` THEN
823  ASM_REWRITE_TAC[FINITE_INSERT, SUBSET_DEF, IN_INSERT] THEN
824  CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
825  SIMP_TAC bool_ss[o_ALPHA, swap_def] THEN PROVE_TAC[]
826QED
827
828Theorem PERMUTATION_LEMMA :
829   !s p:'a->'a.
830       FINITE s /\
831       (!y. ?!x. p(x) = y) /\ (!x. ~(x IN s) ==> (p x = x))
832       ==> permutation p
833Proof
834  ONCE_REWRITE_TAC[GSYM AND_IMP_INTRO] THEN
835  SIMP_TAC bool_ss[RIGHT_FORALL_IMP_THM] THEN
836  HO_MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL
837   [REWRITE_TAC[NOT_IN_EMPTY] THEN REPEAT STRIP_TAC THEN
838    Q.SUBGOAL_THEN `p:'a->'a = I` (fn th => REWRITE_TAC[th, PERMUTATION_I]) THEN
839    ASM_REWRITE_TAC[FUN_EQ_THM, I_THM],
840    ALL_TAC] THEN
841  Q.X_GEN_TAC `s:'a->bool` THEN STRIP_TAC THEN Q.X_GEN_TAC `a:'a` THEN
842  REWRITE_TAC[IN_INSERT] THEN REPEAT STRIP_TAC THEN
843  Q.SUBGOAL_THEN `permutation ((swap(a,p(a)) o swap(a,p(a))) o (p:'a->'a))`
844  MP_TAC THENL [ALL_TAC, REWRITE_TAC[SWAP_IDEMPOTENT, I_o_ID]] THEN
845  REWRITE_TAC[GSYM o_ASSOC] THEN MATCH_MP_TAC PERMUTATION_COMPOSE THEN
846  REWRITE_TAC[PERMUTATION_SWAP] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
847  CONJ_TAC THENL
848   [Q.UNDISCH_TAC `!y. ?!x. (p:'a->'a) x = y` THEN
849    SIMP_TAC bool_ss[EXISTS_UNIQUE_THM, swap_def, o_ALPHA] THEN
850    Q.ASM_CASES_TAC `(p:'a->'a) a = a` THEN ASM_REWRITE_TAC[] THENL
851     [PROVE_TAC[], ALL_TAC] THEN
852    REWRITE_TAC[Q.prove(
853     ‘((if p then x else y) = a) <=> if p then x = a else y = a’,
854     PROVE_TAC[])] THEN
855    REWRITE_TAC[TAUT `(if p then x else y) <=> p /\ x \/ ~p /\ y`] THEN
856    PROVE_TAC[],
857    SIMP_TAC bool_ss[swap_def, o_ALPHA] THEN
858    Q.ASM_CASES_TAC `(p:'a->'a) a = a` THEN ASM_REWRITE_TAC[] THEN
859    PROVE_TAC[]]
860QED
861
862Theorem PERMUTATION :
863   !p. permutation p <=> (!y. ?!x. p(x) = y) /\ FINITE {x:'a| ~(p(x) = x)}
864Proof
865  GEN_TAC THEN EQ_TAC THEN
866  SIMP_TAC bool_ss[PERMUTATION_BIJECTIVE, PERMUTATION_FINITE_SUPPORT] THEN
867  STRIP_TAC THEN MATCH_MP_TAC PERMUTATION_LEMMA THEN
868  Q.EXISTS_TAC `{x:'a| ~(p x = x)}` THEN
869  CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
870  ASM_REWRITE_TAC[]
871QED
872
873Theorem PERMUTATION_INVERSE_WORKS :
874   !p. permutation p ==> (inverse p o p = I) /\ (p o inverse p = I)
875Proof
876  PROVE_TAC[PERMUTATION_BIJECTIVE, SURJECTIVE_INVERSE_o,
877            INJECTIVE_INVERSE_o]
878QED
879
880Theorem PERMUTATION_INVERSE_COMPOSE :
881   !p q. permutation p /\ permutation q
882         ==> (inverse (p o q) = inverse q o inverse p)
883Proof
884  REPEAT STRIP_TAC THEN MATCH_MP_TAC INVERSE_UNIQUE_o THEN
885  REPEAT(FIRST_X_ASSUM(MP_TAC o MATCH_MP PERMUTATION_INVERSE_WORKS)) THEN
886  REWRITE_TAC[GSYM o_ASSOC] THEN REPEAT STRIP_TAC THEN
887  GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) empty_rewrites [o_ASSOC] THEN
888  ASM_REWRITE_TAC[I_o_ID]
889QED
890
891val IMP_CONJ = CONJ_EQ_IMP;
892
893Theorem PERMUTATION_COMPOSE_EQ :
894   (!p q:'a->'a. permutation(p) ==> (permutation(p o q) <=> permutation q)) /\
895   (!p q:'a->'a. permutation(q) ==> (permutation(p o q) <=> permutation p))
896Proof
897  REPEAT STRIP_TAC THEN
898  FIRST_ASSUM(ASSUME_TAC o MATCH_MP PERMUTATION_INVERSE) THEN
899  EQ_TAC THEN ASM_SIMP_TAC std_ss [PERMUTATION_COMPOSE] THENL
900   [DISCH_THEN(MP_TAC o Q.SPEC `inverse(p:'a->'a)` o MATCH_MP
901     (REWRITE_RULE[IMP_CONJ_ALT] PERMUTATION_COMPOSE)),
902    DISCH_THEN(MP_TAC o Q.SPEC `inverse(q:'a->'a)` o MATCH_MP
903     (REWRITE_RULE[IMP_CONJ] PERMUTATION_COMPOSE))] THEN
904  ASM_SIMP_TAC std_ss [GSYM o_ASSOC, PERMUTATION_INVERSE_WORKS] THEN
905  ASM_SIMP_TAC bool_ss [o_ASSOC, PERMUTATION_INVERSE_WORKS] THEN
906  REWRITE_TAC[I_o_ID]
907QED
908
909Theorem PERMUTATION_COMPOSE_SWAP :
910   (!p a b:'a. permutation(swap(a,b) o p) <=> permutation p) /\
911   (!p a b:'a. permutation(p o swap(a,b)) <=> permutation p)
912Proof
913  SIMP_TAC bool_ss [PERMUTATION_COMPOSE_EQ, PERMUTATION_SWAP]
914QED
915
916(* ------------------------------------------------------------------------- *)
917(* Relation to "permutes".                                                   *)
918(* ------------------------------------------------------------------------- *)
919
920Theorem PERMUTATION_PERMUTES :
921   !p:'a->'a. permutation p <=> ?s. FINITE s /\ p permutes s
922Proof
923  GEN_TAC THEN REWRITE_TAC[PERMUTATION, permutes] THEN
924  EQ_TAC THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THENL
925   [Q.EXISTS_TAC `{x:'a | ~(p x = x)}` THEN
926    CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
927    ASM_REWRITE_TAC[],
928    MATCH_MP_TAC SUBSET_FINITE_I THEN Q.EXISTS_TAC `s:'a->bool` THEN
929    ASM_REWRITE_TAC[SUBSET_DEF] THEN
930    CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN PROVE_TAC[]]
931QED
932
933(* ------------------------------------------------------------------------- *)
934(* Hence a sort of induction principle composing by swaps.                   *)
935(* ------------------------------------------------------------------------- *)
936
937Theorem PERMUTES_INDUCT :
938   !P s. FINITE s /\
939         P I /\
940         (!a b:'a p. a IN s /\ b IN s /\ P p /\ permutation p
941                    ==> P (swap(a,b) o p))
942         ==> (!p. p permutes s ==> P p)
943Proof
944  ONCE_REWRITE_TAC[TAUT `a /\ b /\ c ==> d <=> b ==> a ==> c ==> d`] THEN
945  SIMP_TAC std_ss[RIGHT_FORALL_IMP_THM] THEN GEN_TAC THEN DISCH_TAC THEN
946  HO_MATCH_MP_TAC FINITE_INDUCT THEN
947  ASM_REWRITE_TAC[PERMUTES_EMPTY, IN_INSERT] THEN REPEAT STRIP_TAC THEN
948  ASM_REWRITE_TAC[] THEN
949  Q.SUBGOAL_THEN `p = swap(e,p e) o swap(e,p e) o (p:'a->'a)` SUBST1_TAC THENL
950   [REWRITE_TAC[o_ASSOC, SWAP_IDEMPOTENT, I_o_ID], ALL_TAC] THEN
951  Q.PAT_X_ASSUM `$==> X Y` MP_TAC THEN
952  GEN_REWRITE_TAC (LAND_CONV) empty_rewrites [IMP_DISJ_THM] THEN
953  REWRITE_TAC[DISJ_IMP_THM] THEN CONJ_TAC THENL [PROVE_TAC[], ALL_TAC] THEN
954  DISCH_THEN(fn th => FIRST_X_ASSUM MATCH_MP_TAC THEN ASSUME_TAC th) THEN
955  PROVE_TAC[PERMUTES_IN_IMAGE, IN_INSERT, PERMUTES_INSERT_LEMMA,
956                PERMUTATION_PERMUTES, FINITE_INSERT, PERMUTATION_COMPOSE,
957                PERMUTATION_SWAP]
958QED
959
960(* ------------------------------------------------------------------------- *)
961(* More lemmas about permutations.                                           *)
962(* ------------------------------------------------------------------------- *)
963
964Theorem PERMUTES_NUMSET_LE :
965   !p s:num->bool. p permutes s /\ (!i. i IN s ==> p(i) <= i) ==> (p = I)
966Proof
967  REPEAT GEN_TAC THEN REWRITE_TAC[FUN_EQ_THM, I_THM] THEN STRIP_TAC THEN
968  HO_MATCH_MP_TAC COMPLETE_INDUCTION THEN Q.X_GEN_TAC `n:num` THEN
969  DISCH_TAC THEN
970  Q.ASM_CASES_TAC `(n:num) IN s` THENL [ALL_TAC, PROVE_TAC[permutes]] THEN
971  ASM_SIMP_TAC bool_ss[EQ_LESS_EQ] THEN REWRITE_TAC[GSYM NOT_LESS] THEN
972  PROVE_TAC[PERMUTES_INJECTIVE, LESS_EQ_REFL,NOT_LESS]
973QED
974
975Theorem PERMUTES_NUMSET_GE :
976   !p s:num->bool. p permutes s /\ (!i. i IN s ==> i <= p(i)) ==> (p = I)
977Proof
978  REPEAT STRIP_TAC THEN
979  MP_TAC(Q.SPECL [`inverse(p:num->num)`, `s:num->bool`] PERMUTES_NUMSET_LE) THEN
980  GEN_REWRITE_TAC (LAND_CONV) empty_rewrites [IMP_DISJ_THM] THEN
981  REWRITE_TAC[DISJ_IMP_THM] THEN CONJ_TAC THENL
982   [PROVE_TAC[PERMUTES_INVERSE, PERMUTES_INVERSES, PERMUTES_IN_IMAGE],
983    PROVE_TAC[PERMUTES_INVERSE_INVERSE, INVERSE_I]]
984QED
985
986Theorem IMAGE_INVERSE_PERMUTATIONS :
987   !s:'a->bool. {inverse p | p permutes s} = {p | p permutes s}
988Proof
989  REWRITE_TAC[EXTENSION] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
990  PROVE_TAC[PERMUTES_INVERSE_INVERSE, PERMUTES_INVERSE]
991QED
992
993Theorem IMAGE_COMPOSE_PERMUTATIONS_L :
994   !s q:'a->'a. q permutes s ==> ({q o p | p permutes s} = {p | p permutes s})
995Proof
996  REWRITE_TAC[EXTENSION] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
997  REPEAT GEN_TAC THEN STRIP_TAC THEN
998  Q.X_GEN_TAC `p:'a->'a` THEN EQ_TAC THENL
999   [PROVE_TAC[PERMUTES_COMPOSE],
1000    DISCH_TAC THEN Q.EXISTS_TAC `inverse (q:'a->'a) o (p:'a->'a)` THEN
1001    ASM_SIMP_TAC bool_ss[o_ASSOC, PERMUTES_INVERSE, PERMUTES_COMPOSE] THEN
1002    PROVE_TAC [PERMUTES_INVERSES_o, I_o_ID]]
1003QED
1004
1005Theorem IMAGE_COMPOSE_PERMUTATIONS_R :
1006   !s q:'a->'a. q permutes s ==> ({p o q | p permutes s} = {p | p permutes s})
1007Proof
1008  REWRITE_TAC[EXTENSION] THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
1009  REPEAT GEN_TAC THEN STRIP_TAC THEN
1010  Q.X_GEN_TAC `p:'a->'a` THEN EQ_TAC THENL
1011   [PROVE_TAC[PERMUTES_COMPOSE],
1012    DISCH_TAC THEN Q.EXISTS_TAC `(p:'a->'a) o inverse (q:'a->'a)` THEN
1013    ASM_SIMP_TAC bool_ss[GSYM o_ASSOC, PERMUTES_INVERSE, PERMUTES_COMPOSE] THEN
1014    PROVE_TAC [PERMUTES_INVERSES_o, I_o_ID]]
1015QED
1016
1017Theorem PERMUTES_IN_COUNT :
1018   !p n i. p permutes count n /\ i IN count n ==> p(i) < n
1019Proof
1020  REWRITE_TAC[permutes, IN_COUNT] THEN PROVE_TAC[]
1021QED
1022