sortingScript.sml

1(*---------------------------------------------------------------------------*
2 *  General specification of sorting and correctness of quicksort            *
3 *---------------------------------------------------------------------------*)
4Theory sorting
5Ancestors
6  rich_list combin pair relation list arithmetic pred_set
7Libs
8  markerLib metisLib BasicProvers
9
10
11(*---------------------------------------------------------------------------*
12 * What's a permutation? This definition uses universal quantification to    *
13 * define it. There are other ways, which could be compared to this, e.g.    *
14 * as an inductive definition, or as a particular kind of function.          *
15 *---------------------------------------------------------------------------*)
16
17Definition PERM_DEF:  PERM L1 L2 = !x. FILTER ($= x) L1 = FILTER ($= x) L2
18End
19
20Theorem PERM_REFL[simp]:  !L. PERM L L
21Proof PROVE_TAC[PERM_DEF]
22QED
23
24Theorem PERM_INTRO:
25  !x y. (x=y) ==> PERM x y
26Proof PROVE_TAC[PERM_REFL]
27QED
28
29Theorem PERM_transitive:
30  transitive PERM
31Proof
32 RW_TAC list_ss [relationTheory.transitive_def] THEN PROVE_TAC[PERM_DEF]
33QED
34
35Theorem PERM_TRANS:
36  !x y z. PERM x y /\ PERM y z ==> PERM x z
37Proof
38 METIS_TAC [relationTheory.transitive_def, PERM_transitive]
39QED
40
41Theorem PERM_SYM:
42  !l1 l2. PERM l1 l2 = PERM l2 l1
43Proof PROVE_TAC [PERM_DEF]
44QED
45
46Theorem PERM_CONG:
47  !(L1:'a list) L2 L3 L4.
48     PERM L1 L3 /\ PERM L2 L4 ==>
49     PERM (APPEND L1 L2) (APPEND L3 L4)
50Proof PROVE_TAC [PERM_DEF,FILTER_APPEND_DISTRIB]
51QED
52
53Theorem CONS_APPEND[local] = PROVE [APPEND] “!L h. h::L = APPEND [h] L”
54
55Theorem PERM_MONO:
56  !l1 l2 x. PERM l1 l2 ==> PERM (x::l1) (x::l2)
57Proof PROVE_TAC [CONS_APPEND,PERM_CONG, PERM_REFL]
58QED
59
60Theorem PERM_MONO_CONVERSE[local]:
61  PERM (x::l1) (x::l2) ==> PERM l1 l2
62Proof
63  RW_TAC list_ss [PERM_DEF,FILTER]
64  THEN POP_ASSUM (MP_TAC o Q.SPEC‘x'’)
65  THEN RW_TAC list_ss []
66QED
67
68(* PERM (x::l1) (x::l2) <=> PERM l1 l2 *)
69Theorem PERM_CONS_IFF[simp] =
70  GEN_ALL(IMP_ANTISYM_RULE PERM_MONO_CONVERSE (SPEC_ALL PERM_MONO))
71
72Theorem PERM_NIL[simp]:
73  !L. (PERM L [] = (L=[])) /\ (PERM [] L = (L=[]))
74Proof
75  Cases THEN RW_TAC list_ss [PERM_DEF,FILTER]
76  THEN Q.EXISTS_TAC ‘h’
77  THEN RW_TAC list_ss []
78QED
79
80Theorem PERM_SING[simp]:
81  (PERM L [x] <=> L = [x]) /\ (PERM [x] L <=> L = [x])
82Proof
83 Q_TAC SUFF_TAC ‘PERM L [x] = (L = [x])’
84       THEN1 METIS_TAC [PERM_SYM] THEN
85 Cases_on ‘L’ THEN SIMP_TAC (srw_ss()) [PERM_DEF, EQ_IMP_THM] THEN
86 Q_TAC SUFF_TAC
87       ‘(!y. (if y = h then h :: FILTER ($= h) t else FILTER ($= y) t) =
88             (if y = x then [x] else [])) ==>
89        (h = x) /\ (t = [])’
90       THEN1 METIS_TAC [] THEN
91 STRIP_TAC THEN
92 ‘h = x’ by (POP_ASSUM (Q.SPEC_THEN ‘h’ MP_TAC) THEN SRW_TAC [][]) THEN
93 SRW_TAC [][] THEN
94 ‘!y. FILTER ($= y) t = []’ by METIS_TAC [CONS_11] THEN
95 Cases_on ‘t’ THEN FULL_SIMP_TAC (srw_ss()) [] THEN
96 METIS_TAC [NOT_CONS_NIL]
97QED
98
99Theorem MEM_FILTER_EQ[local]:
100  !l x. MEM x l = ~(FILTER ($= x) l = [])
101Proof
102 Induct THEN SRW_TAC [][]
103QED
104
105Theorem MEM_APPEND_SPLIT[local]:
106  !L x. MEM x L ==> ?M N. L = M ++ x::N
107Proof
108 Induct THEN SRW_TAC [][] THENL [
109   Q.EXISTS_TAC ‘[]’ THEN SRW_TAC [][],
110   ‘?M N. L = M ++ x::N’ by METIS_TAC [] THEN
111   Q.EXISTS_TAC ‘h::M’ THEN SRW_TAC [][]
112 ]
113QED
114
115Theorem FILTER_EQ_CONS_APPEND[local]:
116  !M N x. FILTER ($= x) M ++ x::N = x::FILTER ($= x) M ++ N
117Proof
118 Induct THEN SRW_TAC [][]
119QED
120
121Theorem PERM_CONS_EQ_APPEND:
122  !L h. PERM (h::t) L = ?M N. (L = M ++ h::N) /\ PERM t (M ++ N)
123Proof
124 SRW_TAC [][PERM_DEF, FILTER_APPEND_DISTRIB, EQ_IMP_THM] THENL [
125   ‘MEM h L’ by METIS_TAC [NOT_CONS_NIL, MEM_FILTER_EQ] THEN
126   ‘?M N. L = M ++ h::N’ by METIS_TAC [MEM_APPEND_SPLIT] THEN
127   MAP_EVERY Q.EXISTS_TAC [‘M’, ‘N’] THEN
128   SRW_TAC [][] THEN Cases_on ‘x = h’ THEN
129   FIRST_X_ASSUM (Q.SPEC_THEN ‘x’ MP_TAC) THEN
130   SRW_TAC [][FILTER_APPEND_DISTRIB, FILTER_EQ_CONS_APPEND],
131   SRW_TAC [][FILTER_APPEND_DISTRIB, FILTER_EQ_CONS_APPEND]
132 ]
133QED
134
135Theorem PERM_APPEND:
136  !l1 l2. PERM (APPEND l1 l2) (APPEND l2 l1)
137Proof
138 Induct THEN SRW_TAC [][PERM_CONS_EQ_APPEND] THEN METIS_TAC []
139QED
140
141Theorem CONS_PERM:
142  !x L M N. PERM L (APPEND M N)
143            ==>
144           PERM (x::L) (APPEND M (x::N))
145Proof
146METIS_TAC [PERM_CONS_EQ_APPEND]
147QED
148
149
150Theorem APPEND_PERM_SYM:
151  !A B C. PERM (APPEND A B) C ==> PERM (APPEND B A) C
152Proof
153PROVE_TAC [PERM_TRANS, PERM_APPEND]
154QED
155
156Theorem PERM_SPLIT_IF:
157  !P Q l. EVERY (\x. P x = ~ Q x) l ==>
158   PERM l (APPEND (FILTER P l) (FILTER Q l))
159Proof
160 Induct_on ‘l’
161 THEN RW_TAC list_ss [FILTER,PERM_REFL]
162 THEN RES_TAC
163 THEN ASM_SIMP_TAC std_ss [PERM_MONO, CONS_PERM]
164QED
165
166Theorem PERM_SPLIT:
167  !P l. PERM l (APPEND (FILTER P l) (FILTER ($~ o P) l))
168Proof
169 REPEAT GEN_TAC
170 THEN irule PERM_SPLIT_IF
171 THEN SIMP_TAC list_ss []
172QED
173
174(* ----------------------------------------------------------------------
175    Alternative definition of PERM
176   ---------------------------------------------------------------------- *)
177
178Theorem FILTER_EQ_REP:
179  FILTER ($= x) l = REPLICATE (LENGTH (FILTER ($= x) l)) x
180Proof
181  EVERY [Induct_on ‘l’,
182         SIMP_TAC list_ss [rich_listTheory.REPLICATE], GEN_TAC,
183         COND_CASES_TAC THENL [ BasicProvers.VAR_EQ_TAC, ALL_TAC],
184         ASM_SIMP_TAC list_ss [rich_listTheory.REPLICATE] ]
185QED
186
187Theorem FILTER_EQ_LENGTHS_EQ:
188  (LENGTH (FILTER ($= x) l1) = LENGTH (FILTER ($= x) l2)) ==>
189    (FILTER ($= x) l1 = FILTER ($= x) l2)
190Proof
191  EVERY [ DISCH_TAC, ONCE_REWRITE_TAC [FILTER_EQ_REP],
192          ASM_SIMP_TAC bool_ss [] ]
193QED
194
195Theorem PERM_alt:
196  !L1 L2. PERM L1 L2 <=>
197          !x. LENGTH (FILTER ($= x) L1) = LENGTH (FILTER ($= x) L2)
198Proof
199  EVERY [REWRITE_TAC [PERM_DEF], REPEAT GEN_TAC,
200         EQ_TAC, REPEAT STRIP_TAC ]
201  THENL [
202    ASM_SIMP_TAC bool_ss [],
203    irule FILTER_EQ_LENGTHS_EQ THEN ASM_REWRITE_TAC []
204  ]
205QED
206
207(* ----------------------------------------------------------------------
208    Inductive characterisation of PERM
209   ---------------------------------------------------------------------- *)
210
211(* things become slightly awkward because I avoid actually defining an
212   inductive version of the permutation constant.  Instead, I do a bunch
213   of proofs subject to an assumption "defining" perm to be the
214   appropriate RHS; an alernative would be to define the constant, work
215   with it, and then to delete it, so that it didn't get exported. *)
216
217(* the definition assumption is 'backwards' so that it will be OK as an
218   assumption and not cause perm to get rewritten out *)
219val perm_t =
220  “permdef :- !l1 l2:'a list.
221                  perm l1 l2 =
222                    (!P. P [] [] /\
223                         (!x l1 l2. P l1 l2 ==> P (x::l1) (x::l2)) /\
224                         (!x y l1 l2. P l1 l2 ==> P (x::y::l1) (y::x::l2)) /\
225                         (!l1 l2 l3. P l1 l2 /\ P l2 l3 ==> P l1 l3) ==>
226                         P l1 l2)”
227
228(* perm's induction principle *)
229val _ = print "Proving perm induction principle\n"
230Theorem perm_ind[local]:
231  ^perm_t ==> !P. P [] [] /\
232                    (!x l1 l2. P l1 l2 ==> P (x::l1) (x::l2)) /\
233                    (!x y l1 l2. P l1 l2 ==> P (x::y::l1) (y::x::l2)) /\
234                    (!l1 l2 l3. P l1 l2 /\ P l2 l3 ==> P l1 l3) ==>
235                    !l1 l2. perm l1 l2 ==> P l1 l2
236Proof
237  STRIP_TAC THEN LABEL_X_ASSUM "permdef" (REWRITE_TAC o C cons nil) THEN
238  REPEAT STRIP_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC []
239QED
240val perm_ind = UNDISCH perm_ind
241
242val _ = print "Proving perm rules\n"
243Theorem perm_rules:
244  ^perm_t ==> perm [] [] /\
245              (!x l1 l2. perm l1 l2 ==> perm (x::l1) (x::l2)) /\
246              (!x y l1 l2. perm l1 l2 ==> perm (x::y::l1) (y::x::l2)) /\
247              (!l1 l2 l3. perm l1 l2 /\ perm l2 l3 ==> perm l1 l3)
248Proof
249  STRIP_TAC THEN LABEL_X_ASSUM "permdef" (REWRITE_TAC o C cons nil) THEN
250  REPEAT STRIP_TAC THEN
251  REPEAT
252    (FIRST_X_ASSUM (MP_TAC o SPEC “P : 'a list -> 'a list -> bool”)) THEN
253  ASM_REWRITE_TAC [] THEN METIS_TAC []
254QED
255
256val perm_rules = UNDISCH perm_rules;
257
258val _ = print "Proving perm symmetric, reflexive & transitive\n"
259
260Theorem perm_sym[local]:
261   ^perm_t ==> (perm l1 l2 = perm l2 l1)
262Proof
263  STRIP_TAC THEN
264  Q_TAC SUFF_TAC
265        ‘!l1 l2. perm l1 l2 ==> perm l2 l1’
266        THEN1 METIS_TAC [] THEN
267  HO_MATCH_MP_TAC perm_ind THEN
268  SRW_TAC [][perm_rules] THEN METIS_TAC [perm_rules]
269QED
270val perm_sym = UNDISCH perm_sym
271
272Theorem perm_refl[local]:
273   ^perm_t ==> !l. perm l l
274Proof
275  STRIP_TAC THEN Induct THEN SRW_TAC [][perm_rules]
276QED
277val perm_refl = UNDISCH perm_refl
278
279val perm_trans = last (CONJUNCTS perm_rules)
280
281val _ = print "Proving perm ==> PERM\n"
282
283Theorem perm_PERM[local]:
284   ^perm_t ==> !l1 l2. perm l1 l2 ==> PERM l1 l2
285Proof
286  STRIP_TAC THEN HO_MATCH_MP_TAC perm_ind THEN SRW_TAC [][] THENL [
287    SRW_TAC [][PERM_CONS_EQ_APPEND] THEN
288    MAP_EVERY Q.EXISTS_TAC [‘[y]’, ‘l2’] THEN SRW_TAC [][] THEN
289    MAP_EVERY Q.EXISTS_TAC [‘[]’, ‘l2’] THEN SRW_TAC [][],
290    METIS_TAC [PERM_TRANS]
291  ]
292QED
293val perm_PERM = UNDISCH perm_PERM
294
295val _ = print "Proving perm has primitive recursive characterisation\n"
296
297Theorem perm_cons_append'[local]:
298    ^perm_t ==> !M. perm (h::M ++ N) (M ++ [h] ++ N)
299Proof
300  STRIP_TAC >> ASSUME_TAC perm_rules >> ASSUME_TAC perm_refl >>
301    RULE_L_ASSUM_TAC CONJUNCTS >>
302    Induct >> ASM_SIMP_TAC list_ss [] >> GEN_TAC >>
303    MATCH_MP_TAC perm_trans >> Q.EXISTS_TAC ‘h'::h::(M ++ N)’ >>
304    RES_TAC >> ASM_SIMP_TAC list_ss []
305QED
306
307Theorem perm_cons_append[local]:
308   ^perm_t ==> !l1 l2. perm l1 l2 ==>
309                        !M N. (l2 = M ++ N) ==>
310                              !h. perm (h::l1) (M ++ [h] ++ N)
311Proof
312  REPEAT STRIP_TAC >> MATCH_MP_TAC perm_trans >>
313    Q.EXISTS_TAC ‘h :: l2’ >> CONJ_TAC
314  THENL [ ASSUME_TAC perm_rules >> ASM_SIMP_TAC list_ss [],
315    BasicProvers.VAR_EQ_TAC >>
316    MATCH_ACCEPT_TAC (REWRITE_RULE [APPEND] (UNDISCH perm_cons_append')) ]
317QED
318
319val perm_cons_append =
320    SIMP_RULE (bool_ss ++ boolSimps.DNF_ss) [] (UNDISCH perm_cons_append)
321
322val _ = print "Proving PERM ==> perm\n"
323
324Theorem PERM_perm[local]:
325   ^perm_t ==> !l1 l2. PERM l1 l2 ==> perm l1 l2
326Proof
327  STRIP_TAC THEN Induct THEN SRW_TAC [][perm_rules, PERM_CONS_EQ_APPEND] THEN
328  METIS_TAC [perm_cons_append]
329QED
330val PERM_perm = UNDISCH PERM_perm
331
332val perm_elim = GEN_ALL
333                  (IMP_ANTISYM_RULE (SPEC_ALL perm_PERM) (SPEC_ALL PERM_perm))
334fun remove_eq_asm th = let
335  val th0 =
336      CONV_RULE (LAND_CONV
337                   (SIMP_CONV (bool_ss ++ boolSimps.ETA_ss)
338                              [GSYM FUN_EQ_THM, markerTheory.label_def]))
339                (DISCH_ALL (REWRITE_RULE [perm_elim] th))
340in
341  CONV_RULE Unwind.UNWIND_FORALL_CONV
342            (GEN “perm : 'a list -> 'a list -> bool” th0)
343end
344
345Theorem PERM_IND = remove_eq_asm perm_ind
346
347val PERM_MONO' = PERM_MONO |> SPEC_ALL |> Q.GENL [‘x’, ‘l1’, ‘l2’]
348
349Theorem PERM_SWAP_AT_FRONT:
350   PERM (x::y::l1) (y::x::l2) = PERM l1 l2
351Proof
352  METIS_TAC [remove_eq_asm (List.nth(CONJUNCTS perm_rules, 2)),
353             PERM_REFL, PERM_TRANS, PERM_CONS_IFF]
354QED
355
356Theorem PERM_SWAP_L_AT_FRONT:
357   !x y. PERM (x++y++l1) (y++x++l2) = PERM l1 l2
358Proof
359  SIMP_TAC list_ss [PERM_alt, FILTER_APPEND_DISTRIB]
360QED
361
362(* alternative proof of PERM_SWAP_AT_FRONT
363val PERM_SWAP_AT_FRONT' = SPECL [``[x]``, ``[y]``] PERM_SWAP_L_AT_FRONT ;
364
365val PERM_SWAP_AT_FRONT = save_thm( "PERM_SWAP_AT_FRONT",
366  SIMP_RULE list_ss [] PERM_SWAP_AT_FRONT') ;
367*)
368
369val PERM_SWAP = PERM_SWAP_AT_FRONT |> EQ_IMP_RULE |> #2
370                                   |> Q.GENL [‘x’, ‘y’, ‘l1’, ‘l2’]
371
372Theorem PERM_NILNIL[local]:
373  PERM [][]
374Proof SRW_TAC[][]
375QED
376
377Theorem PERM_STRONG_IND =
378  IndDefLib.derive_strong_induction(
379    LIST_CONJ [PERM_NILNIL, PERM_MONO', PERM_SWAP, PERM_TRANS],
380    PERM_IND)
381val _ = IndDefLib.export_rule_induction "PERM_STRONG_IND"
382
383Theorem PERM_LENGTH:
384   !l1 l2. PERM l1 l2 ==> (LENGTH l1 = LENGTH l2)
385Proof
386  HO_MATCH_MP_TAC PERM_IND THEN SRW_TAC [][]
387QED
388
389Theorem PERM_NULL_EQ:
390  !l1 l2. PERM l1 l2 ==> NULL l1 = NULL l2
391Proof
392  ho_match_mp_tac PERM_IND
393  \\ rw[NULL_EQ]
394QED
395
396Theorem PERM_MEM_EQ:
397   !l1 l2. PERM l1 l2 ==> !x. MEM x l1 = MEM x l2
398Proof
399  HO_MATCH_MP_TAC PERM_IND THEN SRW_TAC [][AC DISJ_ASSOC DISJ_COMM]
400QED
401
402Theorem PERM_LIST_TO_SET:
403  !l1 l2. PERM l1 l2 ==> (set l1 = set l2)
404Proof SRW_TAC[][EXTENSION,PERM_MEM_EQ]
405QED
406
407Theorem PERM_BIJ:
408  !l1 l2. PERM l1 l2 ==>
409          ?f. (BIJ f (count(LENGTH l1)) (count(LENGTH l1)) /\
410              (l2 = GENLIST (\i. EL (f i) l1) (LENGTH l1)))
411Proof
412  Induct_on ‘PERM’ >> simp[BIJ_EMPTY] >> conj_tac
413  >- (
414    simp[GENLIST_CONS] >>
415    srw_tac[][combinTheory.o_DEF] >>
416    qexists_tac‘\i. case i of 0 => 0 | SUC i => SUC(f i)’ >>
417    fs[BIJ_IFF_INV, EL_CONS, PRE_SUB1] >>
418    conj_tac >- (Cases >> simp[]) >>
419    qexists_tac ‘\i. case i of 0 => 0 | SUC i => SUC(g i)’ >>
420    conj_tac >- (Cases >> simp[]) >>
421    conj_tac >- (Cases >> simp[]) >>
422    (Cases >> simp[])
423  ) >> conj_tac >- (
424    simp[GENLIST_CONS] >>
425    srw_tac[][combinTheory.o_DEF] >>
426    qexists_tac
427      ‘\i. case i of 0 => 1 | SUC 0 => 0 | SUC(SUC n) => SUC(SUC(f n))’ >>
428    simp[PRE_SUB1,EL_CONS] >>
429    REWRITE_TAC[ONE] >> simp[] >> fs[BIJ_IFF_INV] >>
430    conj_tac >- (Cases >> simp[]>> Cases_on‘n’>>simp[]) >>
431    qexists_tac
432      ‘\i. case i of 0 => 1 | SUC 0 => 0 | SUC(SUC n) => SUC(SUC(g n))’ >>
433    simp[] >>
434    conj_tac >- (Cases >> simp[]>> Cases_on‘n’>>simp[]) >>
435    conj_tac >- (Cases >> simp[]>> TRY(Cases_on‘n’)>>simp[] >>
436                 REWRITE_TAC[ONE]>>simp[]) >>
437    (Cases >> simp[]>> TRY(Cases_on‘n’)>>simp[] >> REWRITE_TAC[ONE]>>simp[])
438  ) >>
439  ntac 2 (srw_tac[][LENGTH_GENLIST]) >>
440  simp[LIST_EQ_REWRITE,EL_GENLIST] >>
441  full_simp_tac(srw_ss())[LENGTH_GENLIST] >>
442  qexists_tac‘f o f'’ >>
443  simp[combinTheory.o_DEF] >>
444  full_simp_tac(srw_ss())[BIJ_IFF_INV] >>
445  qexists_tac‘g' o g’ >>
446  simp[combinTheory.o_DEF]
447QED
448
449Theorem PERM_BIJ_IFF:
450  PERM l1 l2 <=>
451  ?p. p PERMUTES count (LENGTH l1) /\
452      l2 = GENLIST (\i. EL (p i) l1) (LENGTH l1)
453Proof
454  eq_tac
455  >- metis_tac[PERM_BIJ]
456  \\ rw[] \\ fs[]
457  \\ pop_assum mp_tac
458  \\ qid_spec_tac‘p’
459  \\ qid_spec_tac‘l1’
460  \\ Induct
461  \\ rw[]
462  \\ simp[PERM_CONS_EQ_APPEND]
463  \\ pop_assum mp_tac
464  \\ rw[BIJ_IFF_INV]
465  \\ qexists_tac‘GENLIST (\i. EL (p i - 1) l1) (g 0)’
466  \\ qexists_tac‘GENLIST (\i. EL (p (g 0 + i + 1) - 1) l1)
467                         (LENGTH l1 - g 0)’
468  \\ simp[LIST_EQ_REWRITE, GSYM CONJ_ASSOC]
469  \\ conj_tac
470  >- ( rpt(first_x_assum(qspec_then‘0’mp_tac)) \\ simp[] )
471  \\ conj_tac
472  >- (
473    simp[EL_APPEND_EQN]
474    \\ rpt strip_tac
475    \\ Cases_on‘x < g 0’ \\ gs[]
476    >- (
477      Cases_on‘p x’ \\ gs[]
478      \\ Cases_on‘g 0’ \\ gs[]
479      \\ metis_tac[prim_recTheory.LESS_REFL] )
480    \\ Cases_on‘x = g 0’ \\ gs[]
481    \\ Cases_on‘p x’ \\ gs[]
482    \\ metis_tac[prim_recTheory.LESS_0])
483  \\ qspecl_then[‘\i. EL (p (if i < g 0 then i else i + 1) - 1) l1’,
484                 ‘LENGTH l1 - g 0’, ‘g 0’] (mp_tac o SYM) GENLIST_APPEND
485  \\ simp[]
486  \\ qmatch_goalsub_abbrev_tac‘l2 ++ l3’
487  \\ strip_tac
488  \\ qmatch_goalsub_abbrev_tac‘l4 ++ l3’
489  \\ ‘l4 = l2’ by ( simp[Abbr‘l4’, Abbr‘l2’, LIST_EQ_REWRITE] )
490  \\ ‘g 0 < SUC (LENGTH l1)’ by gs[]
491  \\ ‘g 0 <= LENGTH l1’ by simp[]
492  \\ simp[Abbr‘l4’, Abbr‘l2’]
493  \\ qho_match_abbrev_tac‘PERM _ (GENLIST (\i. EL (q i) l1) _)’
494  \\ first_x_assum irule
495  \\ simp[BIJ_DEF, SURJ_DEF, INJ_DEF, GSYM CONJ_ASSOC]
496  \\ conj_asm1_tac
497  >- (
498    simp[Abbr‘q’]
499    \\ rpt strip_tac
500    \\ ‘p x < SUC (LENGTH l1)’ by gs[]
501    \\ ‘p (x + 1) < SUC (LENGTH l1)’ by gs[]
502    \\ rw[] )
503  \\ simp[]
504  \\ reverse conj_tac
505  >- (
506    simp[Abbr‘q’]
507    \\ rpt strip_tac
508    \\ qexists_tac‘if g (x + 1) < g 0 then g (x + 1) else g (x + 1) - 1’
509    \\ IF_CASES_TAC \\ simp[]
510    \\ ‘g (x + 1) < SUC (LENGTH l1)’by gs[]
511    \\ simp[]
512    \\ Cases_on‘g (x + 1) = g 0’ \\ gs[]
513    \\ ‘(0 < SUC (LENGTH l1)) /\ x + 1 < SUC (LENGTH l1)’ by gs[]
514    \\ ‘0 = x + 1’ by metis_tac[]
515    \\ fs[] )
516  \\ simp[Abbr‘q’]
517  \\ rpt strip_tac
518  \\ ‘(x + 1 < SUC (LENGTH l1)) /\ y + 1 < SUC (LENGTH l1)’ by gs[]
519  \\ wlog_tac ‘x < y’ [‘x’, ‘y’]
520  >- (
521    CCONTR_TAC
522    \\ first_x_assum(qspecl_then[‘y’,‘x’]mp_tac)
523    \\ simp[] )
524  \\ ‘x < SUC (LENGTH l1)’ by gs[]
525  \\ ‘y < SUC (LENGTH l1)’ by gs[]
526  \\ Cases_on‘y < g 0’
527  >- (
528    fs[]
529    \\ Cases_on‘p x’ \\ fs[]
530    >- ( ‘y < x’ by metis_tac[] \\ fs[] )
531    \\ Cases_on‘p y’ \\ fs[]
532    >- ( ‘y < y’ by metis_tac[] \\ fs[] )
533    \\ ‘x = y’ by metis_tac[] \\ fs[] )
534  \\ qpat_x_assum‘p _ - _ = _’mp_tac
535  \\ Cases_on‘x < g 0’ \\ simp[]
536  >- (
537    Cases_on‘p x’ \\ simp[]
538    >- ( ‘x < x’ by metis_tac[] \\ fs[] )
539    \\ Cases_on‘p (y + 1)’ \\ simp[]
540    >- ( ‘g 0 = y + 1’ by metis_tac[] \\ gs[] )
541    \\ strip_tac
542    \\ ‘x = y + 1’ by metis_tac[] \\ fs[] )
543  \\ Cases_on‘p (x + 1)’ \\ simp[]
544  >- ( ‘g 0 = x + 1’ by metis_tac[] \\ gs[] )
545  \\ Cases_on‘p (y + 1)’ \\ simp[]
546  >- ( ‘g 0 = y + 1’ by metis_tac[] \\ gs[] )
547  \\ strip_tac
548  \\ ‘x + 1 = y + 1’ by metis_tac[]
549  \\ fs[]
550QED
551
552Theorem PERM_EVERY:
553  !ls ls'. PERM ls ls' ==> (EVERY P ls <=> EVERY P ls')
554Proof Induct_on ‘PERM’ >> srw_tac[][] >> metis_tac[]
555QED
556
557
558(*---------------------------------------------------------------------------*
559 * The idea of sortedness requires a "permutation" relation for lists, and   *
560 * a "chain" predicate that holds just when the relation R holds between     *
561 * all adjacent elements of the list.                                        *
562 *---------------------------------------------------------------------------*)
563
564Definition SORTED_DEF[simp]:
565   (SORTED R [] = T) /\
566   (SORTED R [x] = T) /\
567   (SORTED R (x::y::rst) <=> R x y /\ SORTED R (y::rst))
568End
569
570Definition SORTS_DEF:
571  SORTS f R <=> !l. PERM l (f R l) /\ SORTED R (f R l)
572End
573
574Theorem SORTED_adjacent:
575  SORTED R L <=> adjacent L RSUBSET R
576Proof
577  Induct_on ‘L’ >> simp[relationTheory.RSUBSET] >>
578  rename [‘SORTED R L’] >> Cases_on ‘L’ >>
579  simp[adjacent_iff, DISJ_IMP_THM, FORALL_AND_THM,
580       relationTheory.RSUBSET]
581QED
582
583
584(*---------------------------------------------------------------------------*
585 *    When consing onto a sorted list yields a sorted list                   *
586 *---------------------------------------------------------------------------*)
587
588Theorem SORTED_EQ:
589  !R L x.
590    transitive R ==> (SORTED R (x::L) <=> SORTED R L /\ !y. MEM y L ==> R x y)
591Proof
592Induct_on ‘L’
593 THEN RW_TAC list_ss [SORTED_DEF,MEM]
594 THEN PROVE_TAC [relationTheory.transitive_def]
595QED
596
597
598(*---------------------------------------------------------------------------*
599 *       When appending sorted lists gives a sorted list.                    *
600 *---------------------------------------------------------------------------*)
601
602Theorem SORTED_APPEND:
603 !R L1 L2.
604 transitive R ==>
605 (SORTED R (L1 ++ L2) <=> SORTED R L1 /\ SORTED R L2 /\
606                          (!x y. MEM x L1 ==> MEM y L2 ==> R x y))
607Proof
608 Induct_on ‘L1’ \\ fs [SORTED_EQ] \\ metis_tac []
609QED
610
611Theorem SORTED_APPEND_IMP:
612 !R L1 L2.
613     transitive R
614 /\  SORTED R L1
615 /\  SORTED R L2
616 /\ (!x y. MEM x L1 /\ MEM y L2 ==> R x y)
617  ==>
618    SORTED R (L1 ++ L2)
619Proof
620Induct_on ‘L1’
621  THEN SRW_TAC [boolSimps.CONJ_ss][SORTED_EQ]
622  THEN PROVE_TAC []
623QED
624
625Theorem SORTED_APPEND_GEN:
626  !R L1 L2. SORTED R (L1 ++ L2) <=>
627              SORTED R L1 /\ SORTED R L2 /\
628                ((L1 = []) \/ (L2 = []) \/ (R (LAST L1) (HD L2)))
629Proof
630  REPEAT STRIP_TAC >> Induct_on ‘L1’ >>
631    ASM_SIMP_TAC list_ss [SORTED_DEF] >> GEN_TAC >>
632    Cases_on ‘L1’ >> Cases_on ‘L2’ >>
633    FULL_SIMP_TAC list_ss [SORTED_DEF]
634  THENL [
635    SIMP_TAC bool_ss [CONJ_COMM],
636    SIMP_TAC bool_ss [CONJ_ASSOC] ]
637QED
638
639(*---------------------------------------------------------------------------
640                 Partition a list by a predicate.
641 ---------------------------------------------------------------------------*)
642
643Definition PART_DEF:
644      (PART P [] l1 l2 = (l1,l2))
645  /\  (PART P (h::rst) l1 l2 =
646          if P h then PART P rst (h::l1) l2
647                 else PART P rst  l1  (h::l2))
648End
649
650(*---------------------------------------------------------------------------
651              Theorems about "PART"
652 ---------------------------------------------------------------------------*)
653
654Theorem PART_LENGTH:
655  !P L l1 l2 p q.
656    ((p,q) = PART P L l1 l2)
657    ==> (LENGTH L + LENGTH l1 + LENGTH l2 = LENGTH p + LENGTH q)
658Proof
659Induct_on ‘L’
660  THEN RW_TAC list_ss [PART_DEF]
661  THEN RES_THEN MP_TAC
662  THEN RW_TAC list_ss []
663QED
664
665
666Theorem PART_LENGTH_LEM:
667 !P L l1 l2 p q.
668    ((p,q) = PART P L l1 l2)
669    ==>  LENGTH p <= LENGTH L + LENGTH l1 + LENGTH l2 /\
670         LENGTH q <= LENGTH L + LENGTH l1 + LENGTH l2
671Proof
672RW_TAC bool_ss []
673 THEN IMP_RES_THEN MP_TAC PART_LENGTH
674 THEN RW_TAC list_ss []
675QED
676
677
678(*---------------------------------------------------------------------------
679       Each element in the positive and negative partitions has
680       the desired property. The simplifier loops on some of the
681       subgoals here, so we have to take round-about measures.
682 ---------------------------------------------------------------------------*)
683
684Theorem PARTs_HAVE_PROP:
685  !P L A B l1 l2.
686   ((A,B) = PART P L l1 l2) /\
687   (!x. MEM x l1 ==> P x) /\ (!x. MEM x l2 ==> ~P x)
688    ==>
689      (!z. MEM z A ==>  P z) /\ (!z. MEM z B ==> ~P z)
690Proof
691Induct_on ‘L’
692 THEN REWRITE_TAC [PART_DEF,CLOSED_PAIR_EQ] THENL
693 [PROVE_TAC[],
694  POP_ASSUM (fn th => REPEAT GEN_TAC THEN
695     COND_CASES_TAC THEN STRIP_TAC THEN MATCH_MP_TAC th)
696   THENL [MAP_EVERY Q.EXISTS_TAC [‘h::l1’, ‘l2’],
697          MAP_EVERY Q.EXISTS_TAC [‘l1’, ‘h::l2’]]
698  THEN RW_TAC list_ss [MEM] THEN RW_TAC bool_ss []]
699QED
700
701
702(*---------------------------------------------------------------------------*)
703(* Appending the two partitions of the original list is a permutation of the *)
704(* original list.                                                            *)
705(*---------------------------------------------------------------------------*)
706
707Theorem PART_PERM[local]:
708  !P L a1 a2 l1 l2.
709   ((a1,a2) = PART P L l1 l2)
710      ==>
711   PERM (L ++ (l1 ++ l2)) (a1 ++ a2)
712Proof
713Induct_on ‘L’
714  THEN RW_TAC list_ss [PART_DEF, PERM_REFL]
715  THEN RES_TAC THEN MATCH_MP_TAC PERM_TRANS THENL
716  [Q.EXISTS_TAC ‘APPEND L (APPEND (h::l1) l2)’,
717   Q.EXISTS_TAC ‘APPEND L (APPEND l1 (h::l2))’]
718  THEN PROVE_TAC [APPEND,APPEND_ASSOC,CONS_PERM,PERM_REFL]
719QED
720
721(*---------------------------------------------------------------------------
722     Everything in the partitions occurs in the original list, and
723     vice-versa. The goal has been generalized.
724 ---------------------------------------------------------------------------*)
725
726Theorem PART_MEM:
727  !P L a1 a2 l1 l2.
728     ((a1,a2) = PART P L l1 l2)
729       ==>
730      !x. MEM x (L ++ (l1 ++ l2)) = MEM x (a1 ++ a2)
731Proof
732  METIS_TAC [PART_PERM, PERM_MEM_EQ]
733QED
734
735(*---------------------------------------------------------------------------
736     A packaged version of PART. Most theorems about PARTITION
737     will be instances of theorems about PART.
738 ---------------------------------------------------------------------------*)
739
740Definition PARTITION_DEF: PARTITION P l = PART P l [] []
741End
742
743(*---------------------------------------------------------------------------*
744 *      Quicksort                                                            *
745 *---------------------------------------------------------------------------*)
746
747Definition QSORT_DEF:
748  (QSORT ord [] = []) /\
749  (QSORT ord (h::t) =
750       let (l1,l2) = PARTITION (\y. ord y h) t
751       in
752         QSORT ord l1 ++ [h] ++ QSORT ord l2)
753Termination
754  WF_REL_TAC ‘measure (LENGTH o SND)’
755     THEN RW_TAC list_ss [o_DEF,PARTITION_DEF]
756     THEN IMP_RES_THEN MP_TAC PART_LENGTH_LEM
757     THEN RW_TAC list_ss []
758End
759
760(*---------------------------------------------------------------------------*
761 *           Properties of QSORT                                            *
762 *---------------------------------------------------------------------------*)
763
764Theorem QSORT_MEM:
765  !R L x. MEM x (QSORT R L) = MEM x L
766Proof
767recInduct QSORT_IND
768 THEN RW_TAC bool_ss [QSORT_DEF,PARTITION_DEF]
769 THEN RW_TAC list_ss []
770 THEN Q.PAT_X_ASSUM ‘_ = _’ (MP_TAC o MATCH_MP PART_MEM o SYM)
771 THEN RW_TAC list_ss [] THEN PROVE_TAC []
772QED
773
774(*---------------------------------------------------------------------------*)
775(* The result list is a permutation of the input list.                       *)
776(*---------------------------------------------------------------------------*)
777
778
779Theorem QSORT_PERM:
780  !R L. PERM L (QSORT R L)
781Proof
782 recInduct QSORT_IND
783  THEN RW_TAC list_ss [QSORT_DEF,PERM_REFL,PARTITION_DEF]
784  THEN REWRITE_TAC [GSYM APPEND_ASSOC, APPEND]
785  THEN MATCH_MP_TAC CONS_PERM
786  THEN MATCH_MP_TAC PERM_TRANS
787  THEN Q.EXISTS_TAC ‘l1 ++ l2’
788  THEN RW_TAC std_ss [] THENL
789  [METIS_TAC [APPEND,APPEND_NIL,PART_PERM],
790   METIS_TAC [PERM_CONG]]
791QED
792
793
794Theorem LENGTH_QSORT[simp]:
795  LENGTH (QSORT R l) = LENGTH l
796Proof
797  metis_tac[QSORT_PERM, PERM_LENGTH]
798QED
799
800(*---------------------------------------------------------------------------
801 * The result list is sorted.
802 *---------------------------------------------------------------------------*)
803
804Theorem QSORT_SORTED:
805  !R L. transitive R /\ total R ==> SORTED R (QSORT R L)
806Proof
807 recInduct QSORT_IND
808  THEN RW_TAC bool_ss [QSORT_DEF, SORTED_DEF, PARTITION_DEF]
809  THEN REWRITE_TAC [GSYM APPEND_ASSOC, APPEND]
810  THEN MATCH_MP_TAC SORTED_APPEND_IMP
811  THEN POP_ASSUM (ASSUME_TAC o SYM)
812  THEN IMP_RES_THEN (fn th => ASM_REWRITE_TAC [th]) SORTED_EQ
813  THEN RW_TAC list_ss [MEM_FILTER,MEM,QSORT_MEM]
814  THEN ((RES_TAC THEN NO_TAC) ORELSE ALL_TAC)
815  THEN Q.PAT_X_ASSUM ‘_ = _’ (MP_TAC o MATCH_MP
816        (REWRITE_RULE[PROVE [] (Term ‘x/\y/\z ==> w <=> x ==> y/\z ==> w’)]
817            PARTs_HAVE_PROP))
818  THEN RW_TAC std_ss [MEM]
819  THEN PROVE_TAC [transitive_def,total_def]
820QED
821
822
823(*---------------------------------------------------------------------------
824 * Bring everything together.
825 *---------------------------------------------------------------------------*)
826
827Theorem QSORT_SORTS:
828  !R. transitive R /\ total R ==> SORTS QSORT R
829Proof
830  PROVE_TAC [SORTS_DEF, QSORT_PERM, QSORT_SORTED]
831QED
832
833
834(*---------------------------------------------------------------------------
835 * Theorems about Permutations. Added by Thomas Tuerk. 19 March 2009
836 *---------------------------------------------------------------------------*)
837
838Theorem PERM_APPEND_IFF:
839 (!l:'a list l1 l2. PERM (l++l1) (l++l2) = PERM l1 l2) /\
840  (!l:'a list l1 l2. PERM (l1++l) (l2++l) = PERM l1 l2)
841Proof
842  SIMP_TAC list_ss [PERM_alt, FILTER_APPEND_DISTRIB]
843QED
844
845Definition PERM_SINGLE_SWAP_DEF:   PERM_SINGLE_SWAP l1 l2 =
846    ?x1 x2 x3. (l1 = x1 ++ x2 ++ x3) /\ (l2 = x1 ++ x3 ++ x2)
847End
848
849Theorem PERM_SINGLE_SWAP_SYM:
850 !l1 l2. PERM_SINGLE_SWAP l1 l2 = PERM_SINGLE_SWAP l2 l1
851Proof
852  PROVE_TAC[PERM_SINGLE_SWAP_DEF]
853QED
854
855Theorem PERM_SINGLE_SWAP_I:
856   PERM_SINGLE_SWAP (x1 ++ x2 ++ x3) (x1 ++ x3 ++ x2)
857Proof
858  PROVE_TAC [PERM_SINGLE_SWAP_DEF]
859QED
860
861Theorem PERM_SINGLE_SWAP_APPEND =
862  REWRITE_RULE [APPEND] (Q.INST [‘x1’ |-> ‘NIL’] PERM_SINGLE_SWAP_I) ;
863
864Theorem PERM_SINGLE_SWAP_REFL =
865  GEN_ALL (REWRITE_RULE [APPEND, APPEND_NIL]
866    (Q.INST [‘x2’ |-> ‘NIL’, ‘x3’ |-> ‘l’] PERM_SINGLE_SWAP_APPEND)) ;
867
868val [_, TC_TRANS] = CONJUNCTS (SPEC_ALL TC_RULES) ;
869
870Theorem PERM_SINGLE_SWAP_CONS:
871   PERM_SINGLE_SWAP M N ==> PERM_SINGLE_SWAP (x :: M) (x :: N)
872Proof
873  SIMP_TAC list_ss [PERM_SINGLE_SWAP_DEF] >> REPEAT STRIP_TAC >>
874    Q.EXISTS_TAC ‘x :: x1’ >> Q.EXISTS_TAC ‘x2’ >> Q.EXISTS_TAC ‘x3’ >>
875    ASM_SIMP_TAC list_ss []
876QED
877
878Theorem PERM_SINGLE_SWAP_TC_CONS:
879  !M N. TC PERM_SINGLE_SWAP M N ==> TC PERM_SINGLE_SWAP (x :: M) (x :: N)
880Proof
881  HO_MATCH_MP_TAC TC_INDUCT >> reverse CONJ_TAC >- MATCH_ACCEPT_TAC TC_TRANS >>
882  rpt strip_tac >> irule TC_SUBSET >>
883  irule PERM_SINGLE_SWAP_CONS >> FIRST_ASSUM ACCEPT_TAC
884QED
885
886Theorem PERM_is_TC_PSS[local]:
887   !l1 l2. PERM l1 l2 ==> TC PERM_SINGLE_SWAP l1 l2
888Proof
889  Induct THEN1 (SIMP_TAC list_ss [PERM_NIL] >>
890      irule TC_SUBSET >> irule PERM_SINGLE_SWAP_REFL) >>
891    REPEAT STRIP_TAC >> IMP_RES_TAC PERM_CONS_EQ_APPEND >>
892    BasicProvers.VAR_EQ_TAC >> irule TC_TRANS >>
893    Q.EXISTS_TAC ‘(h :: N) ++ M’ >> CONJ_TAC
894  THENL [
895    SIMP_TAC list_ss [] >> irule PERM_SINGLE_SWAP_TC_CONS >>
896      RES_TAC >> irule TC_TRANS >> Q.EXISTS_TAC ‘M ++ N’ >>
897      CONJ_TAC THEN1 POP_ASSUM ACCEPT_TAC >>
898      irule TC_SUBSET >> irule PERM_SINGLE_SWAP_APPEND,
899    irule TC_SUBSET >> irule PERM_SINGLE_SWAP_APPEND ]
900QED
901
902Theorem PSS_is_PERM[local]:
903   !l1 l2. PERM_SINGLE_SWAP l1 l2 ==> PERM l1 l2
904Proof
905  SIMP_TAC list_ss [PERM_SINGLE_SWAP_DEF, PERM_alt] >>
906    REPEAT STRIP_TAC >>
907    ASM_SIMP_TAC list_ss [FILTER_APPEND_DISTRIB]
908QED
909
910val TC_PSS_is_PERM =
911  REWRITE_RULE [MATCH_MP transitive_TC_identity PERM_transitive]
912  (MATCH_MP TC_MONOTONE PSS_is_PERM) ;
913
914Theorem PERM_TC:
915   PERM = TC PERM_SINGLE_SWAP
916Proof
917  SIMP_TAC std_ss [FUN_EQ_THM] >> REPEAT STRIP_TAC >> EQ_TAC
918  THENL [ MATCH_ACCEPT_TAC PERM_is_TC_PSS,
919    MATCH_ACCEPT_TAC TC_PSS_is_PERM ]
920QED
921
922Theorem PERM_RTC:
923     PERM = RTC PERM_SINGLE_SWAP
924Proof
925
926REWRITE_TAC[GSYM (CONJUNCT2 (SIMP_RULE std_ss [FORALL_AND_THM] TC_RC_EQNS)),
927            PERM_TC] THEN
928AP_TERM_TAC THEN
929SIMP_TAC std_ss [RC_DEF, FUN_EQ_THM] THEN
930PROVE_TAC[PERM_SINGLE_SWAP_REFL]
931QED
932
933
934Theorem PERM_EQC:
935     PERM = EQC PERM_SINGLE_SWAP
936Proof
937
938‘SC PERM_SINGLE_SWAP = PERM_SINGLE_SWAP’ by (
939   SIMP_TAC std_ss [FUN_EQ_THM, SC_DEF, PERM_SINGLE_SWAP_SYM]
940) THEN
941ASM_REWRITE_TAC[EQC_DEF, GSYM PERM_TC] THEN
942SIMP_TAC std_ss [RC_DEF, FUN_EQ_THM] THEN
943PROVE_TAC[PERM_REFL]
944QED
945
946
947
948val PERM_lift_TC_RULE =
949  (GEN_ALL o
950   SIMP_RULE std_ss [GSYM PERM_TC, PERM_SINGLE_SWAP_DEF,
951                     GSYM LEFT_FORALL_IMP_THM,
952                     GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_EXISTS_AND_THM] o
953   Q.ISPEC ‘PERM_SINGLE_SWAP’ o
954   Q.GEN ‘R’);
955
956
957Theorem PERM_lifts_transitive_relations =
958PERM_lift_TC_RULE TC_lifts_transitive_relations;
959
960Theorem PERM_lifts_equalities =
961PERM_lift_TC_RULE TC_lifts_equalities;
962
963Theorem PERM_lifts_invariants =
964PERM_lift_TC_RULE TC_lifts_invariants;
965
966
967Theorem PERM_lifts_monotonicities:
968 !f. (!x1:'a list x2 x3. ?x1':'b list x2' x3'.
969       (f (x1 ++ x2 ++ x3) = x1' ++ x2' ++ x3') /\
970       (f (x1 ++ x3 ++ x2) = x1' ++ x3' ++ x2')) ==>
971      !x y. PERM x y ==> PERM (f x) (f y)
972Proof
973GEN_TAC THEN STRIP_TAC THEN
974MATCH_MP_TAC PERM_lifts_transitive_relations THEN
975REWRITE_TAC[PERM_transitive] THEN
976REPEAT GEN_TAC THEN
977POP_ASSUM (STRIP_ASSUME_TAC o (Q.SPECL [‘x1’,‘x2’,‘x3’])) THEN
978ASM_REWRITE_TAC[PERM_APPEND, PERM_APPEND_IFF, GSYM APPEND_ASSOC]
979QED
980
981
982Theorem PERM_EQUIVALENCE:
983 equivalence PERM
984Proof
985REWRITE_TAC [PERM_EQC, EQC_EQUIVALENCE]
986QED
987
988Theorem PERM_EQUIVALENCE_ALT_DEF:
989 !x y. PERM x y = (PERM x = PERM y)
990Proof
991SIMP_TAC std_ss [GSYM ALT_equivalence,
992                 PERM_EQUIVALENCE]
993QED
994
995Theorem ALL_DISTINCT_PERM:
996    !l1 l2. PERM l1 l2 ==> (ALL_DISTINCT l1 = ALL_DISTINCT l2)
997Proof
998   MATCH_MP_TAC PERM_lifts_equalities THEN
999   SIMP_TAC list_ss [ALL_DISTINCT_APPEND] THEN
1000   PROVE_TAC[]
1001QED
1002
1003
1004Theorem PERM_ALL_DISTINCT:
1005 !l1 l2. (ALL_DISTINCT l1 /\ ALL_DISTINCT l2 /\ (!x. MEM x l1 = MEM x l2)) ==>
1006           PERM l1 l2
1007Proof
1008
1009SIMP_TAC std_ss [ALL_DISTINCT_FILTER, PERM_DEF, MEM_FILTER_EQ] THEN
1010METIS_TAC[]
1011QED
1012
1013Theorem ALL_DISTINCT_PERM_LIST_TO_SET_TO_LIST:
1014 !ls. ALL_DISTINCT ls = PERM ls (SET_TO_LIST (set ls))
1015Proof
1016SRW_TAC[][EQ_IMP_THM] THEN1 (
1017  MATCH_MP_TAC PERM_ALL_DISTINCT THEN
1018  SRW_TAC[][] ) THEN
1019IMP_RES_TAC ALL_DISTINCT_PERM THEN
1020FULL_SIMP_TAC (srw_ss()) []
1021QED
1022
1023Theorem PERM_SET_TO_LIST_INSERT:
1024  FINITE s ==>
1025    PERM (SET_TO_LIST (x INSERT s))
1026         (if x IN s then SET_TO_LIST s else x :: SET_TO_LIST s)
1027Proof
1028  SRW_TAC[][] THEN1 (‘x INSERT s = s’ by (SRW_TAC[][EXTENSION] \\ METIS_TAC[])
1029                     THEN SRW_TAC[][])
1030  THEN Cases_on ‘CHOICE (x INSERT s) = x’
1031  THEN1 (
1032    SRW_TAC[][Once SET_TO_LIST_THM]
1033    THEN ‘REST (x INSERT s) = s’ by (
1034      Q.SPEC_THEN‘x INSERT s’MP_TAC CHOICE_INSERT_REST
1035      THEN ASM_SIMP_TAC(srw_ss())[]
1036      THEN Q.SPEC_THEN‘x INSERT s’MP_TAC (CONV_RULE SWAP_FORALL_CONV IN_REST)
1037      THEN SRW_TAC[][EXTENSION]
1038      THEN METIS_TAC[])
1039    THEN SRW_TAC[][])
1040  THEN SRW_TAC[][Once SET_TO_LIST_THM]
1041  THEN MATCH_MP_TAC PERM_ALL_DISTINCT
1042  THEN SRW_TAC[][CHOICE_NOT_IN_REST]
1043  THEN METIS_TAC[CHOICE_INSERT_REST, NOT_EMPTY_INSERT, IN_INSERT]
1044QED
1045
1046Theorem PERM_MAP:
1047 !f l1 l2. PERM l1 l2 ==> PERM (MAP f l1) (MAP f l2)
1048Proof
1049   GEN_TAC THEN
1050   MATCH_MP_TAC PERM_lifts_monotonicities THEN
1051   REWRITE_TAC[MAP_APPEND] THEN
1052   PROVE_TAC[]
1053QED
1054
1055Theorem PERM_SUM:
1056 !l1 l2. PERM l1 l2 ==> (SUM l1 = SUM l2)
1057Proof
1058HO_MATCH_MP_TAC PERM_IND THEN
1059SRW_TAC [][] THEN DECIDE_TAC
1060QED
1061
1062Theorem PERM_FILTER:
1063 !P l1 l2. PERM l1 l2 ==> (PERM (FILTER P l1) (FILTER P l2))
1064Proof
1065   GEN_TAC THEN
1066   MATCH_MP_TAC PERM_lifts_monotonicities THEN
1067   REWRITE_TAC[FILTER_APPEND_DISTRIB] THEN
1068   PROVE_TAC []
1069QED
1070
1071Theorem PERM_REVERSE:
1072   PERM ls (REVERSE ls)
1073Proof
1074  SIMP_TAC list_ss [PERM_alt, FILTER_REVERSE]
1075QED
1076
1077Theorem PERM_REVERSE_EQ[simp]:
1078   (PERM (REVERSE l1) l2 = PERM l1 l2) /\
1079    (PERM l1 (REVERSE l2) = PERM l1 l2)
1080Proof
1081  METIS_TAC [PERM_TRANS, PERM_SYM, PERM_REVERSE]
1082QED
1083
1084Theorem FOLDR_PERM:
1085 !f l1 l2 e.
1086(ASSOC f /\ COMM f) ==>
1087((PERM l1 l2) ==>
1088(FOLDR f e l1 = FOLDR f e l2))
1089Proof
1090
1091SIMP_TAC std_ss [RIGHT_FORALL_IMP_THM] THEN
1092GEN_TAC THEN STRIP_TAC THEN
1093HO_MATCH_MP_TAC PERM_IND THEN
1094SIMP_TAC list_ss [] THEN
1095PROVE_TAC[ASSOC_DEF, COMM_DEF]
1096QED
1097
1098Theorem PERM_SET_TO_LIST_count_COUNT_LIST:
1099  PERM (SET_TO_LIST (count n)) (COUNT_LIST n)
1100Proof
1101  MATCH_MP_TAC PERM_ALL_DISTINCT THEN
1102  CONJ_TAC
1103  >- (MATCH_MP_TAC ALL_DISTINCT_SET_TO_LIST THEN
1104      MATCH_ACCEPT_TAC pred_setTheory.FINITE_COUNT ) THEN
1105  SRW_TAC [][rich_listTheory.COUNT_LIST_GENLIST,ALL_DISTINCT_GENLIST,
1106             MEM_GENLIST]
1107QED
1108
1109Theorem SORTED_NIL:     !R. SORTED R []
1110Proof SRW_TAC[][]
1111QED
1112
1113Theorem SORTED_SING:    !R x. SORTED R [x]
1114Proof SRW_TAC[][]
1115QED
1116
1117Theorem SORTED_TL:
1118   SORTED R (x :: xs) ==> SORTED R xs
1119Proof
1120    Cases_on ‘xs’ THEN (SIMP_TAC list_ss [SORTED_DEF])
1121QED
1122
1123Theorem SORTED_EL_SUC:
1124 !R ls. SORTED R ls =
1125        !n. (SUC n) < LENGTH ls ==>
1126            R (EL n ls) (EL (SUC n) ls)
1127Proof
1128GEN_TAC THEN Induct THEN SRW_TAC[][] THEN
1129Cases_on ‘ls’ THEN SRW_TAC[][SORTED_DEF] THEN
1130SRW_TAC[][EQ_IMP_THM] THEN1 (
1131  Cases_on ‘n’ THEN SRW_TAC[][] THEN
1132  FULL_SIMP_TAC (srw_ss()) [] )
1133THEN1 (
1134  POP_ASSUM (Q.SPEC_THEN ‘0’ MP_TAC) THEN
1135  SRW_TAC[][] ) THEN
1136FIRST_X_ASSUM (Q.SPEC_THEN ‘SUC n’ MP_TAC) THEN
1137SRW_TAC [][]
1138QED
1139
1140Theorem SORTED_EL_LESS:
1141 !R. transitive R ==>
1142  !ls. SORTED R ls =
1143       !m n. m < n /\ n < LENGTH ls ==>
1144             R (EL m ls) (EL n ls)
1145Proof
1146GEN_TAC THEN STRIP_TAC THEN
1147Induct THEN SRW_TAC[][] THEN
1148SRW_TAC[][SORTED_EQ,EQ_IMP_THM] THEN1 (
1149  Cases_on ‘n’ THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1150  Cases_on ‘m’ THEN SRW_TAC[][] THEN1
1151    METIS_TAC[MEM_EL] THEN
1152  FULL_SIMP_TAC (srw_ss()) [] )
1153THEN1 (
1154  FIRST_X_ASSUM (Q.SPECL_THEN [‘SUC m’,‘SUC n’] MP_TAC) THEN
1155  SRW_TAC [][] ) THEN
1156FULL_SIMP_TAC (srw_ss()) [MEM_EL] THEN
1157FIRST_X_ASSUM (Q.SPECL_THEN [‘0’,‘SUC n’] MP_TAC) THEN
1158SRW_TAC [][]
1159QED
1160
1161Theorem MEM_PERM:
1162     !l1 l2. PERM l1 l2 ==> (!a. MEM a l1 = MEM a l2)
1163Proof
1164    METIS_TAC [Q.SPEC ‘$= a’ MEM_FILTER, PERM_DEF]
1165QED
1166
1167
1168Theorem SORTED_PERM_EQ:
1169   !R. transitive R /\ antisymmetric R ==>
1170    !l1 l2. SORTED R l1 /\ SORTED R l2 /\ PERM l1 l2 ==> (l1 = l2)
1171Proof
1172  GEN_TAC >> STRIP_TAC >>
1173    Induct THEN1 SIMP_TAC list_ss [PERM_NIL] >>
1174    REPEAT STRIP_TAC >>
1175    Cases_on ‘l2’ THEN1 FULL_SIMP_TAC list_ss [PERM_NIL] >>
1176    SIMP_TAC list_ss [] >> CONJ_ASM1_TAC
1177  THENL [
1178    IMP_RES_TAC SORTED_EQ >> IMP_RES_TAC MEM_PERM >>
1179      POP_ASSUM (ASSUME_TAC o Q.SPEC ‘h'’) >>
1180      FIRST_X_ASSUM (ASSUME_TAC o Q.SPEC ‘h’) >>
1181      FULL_SIMP_TAC list_ss [relationTheory.antisymmetric_def],
1182    FIRST_X_ASSUM MATCH_MP_TAC >>
1183      BasicProvers.VAR_EQ_TAC >> IMP_RES_TAC SORTED_TL >>
1184      FULL_SIMP_TAC list_ss [PERM_CONS_IFF] ]
1185QED
1186
1187Theorem QSORT_eq_if_PERM:
1188 !R. total R /\ transitive R /\ antisymmetric R ==>
1189  !l1 l2. (QSORT R l1 = QSORT R l2) = PERM l1 l2
1190Proof
1191PROVE_TAC[QSORT_PERM,QSORT_SORTED,SORTED_PERM_EQ,PERM_TRANS,PERM_SYM]
1192QED
1193
1194(* generalisation of the above *)
1195Theorem SORTS_PERM_EQ:
1196  !R. transitive R /\ antisymmetric R /\ SORTS f R ==>
1197  !l1 l2. (f R l1 = f R l2) = PERM l1 l2
1198Proof
1199  PROVE_TAC[SORTED_PERM_EQ, PERM_SYM, PERM_TRANS, SORTS_DEF]
1200QED
1201
1202Theorem SORTED_FILTER:
1203  !R ls P. transitive R /\ SORTED R ls ==> SORTED R (FILTER P ls)
1204Proof
1205  Induct_on ‘ls’ >> csimp[SORTED_EQ] >> rw[SORTED_EQ] >> fs[MEM_FILTER]
1206QED
1207
1208Theorem ALL_DISTINCT_SORTED_WEAKEN:
1209   !R R' ls. (!x y. MEM x ls /\ MEM y ls /\ x <> y ==> (R x y <=> R' x y)) /\
1210        ALL_DISTINCT ls /\ SORTED R ls ==> SORTED R' ls
1211Proof
1212  gen_tac \\ ho_match_mp_tac SORTED_IND \\ rw[]
1213  \\ pop_assum mp_tac
1214  \\ simp_tac(srw_ss())[SORTED_DEF]
1215  \\ metis_tac[]
1216QED
1217
1218(*Perm theorems for the simplication*)
1219
1220(* was PERM_FUN_APPEND but this name is used again lower down *)
1221Theorem PERM_FUN_APPEND_C:
1222 !l1 l1' l2 l2'.
1223(PERM l1 = PERM l1') ==>
1224(PERM l2 = PERM l2') ==>
1225(PERM (l1 ++ l2) = PERM (l1' ++ l2'))
1226Proof
1227SIMP_TAC std_ss [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_CONG]
1228QED
1229
1230
1231Theorem PERM_FUN_CONS:
1232 !x l1 l1'.
1233(PERM l1 = PERM l1') ==>
1234(PERM (x::l1) = PERM (x::l1'))
1235Proof
1236SIMP_TAC std_ss [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_CONS_IFF]
1237QED
1238
1239
1240Theorem PERM_FUN_APPEND_CONS:
1241 !x l1 l2. PERM (l1 ++ x::l2) = PERM (x::l1++l2)
1242Proof
1243METIS_TAC[PERM_EQUIVALENCE_ALT_DEF,
1244          PERM_APPEND, PERM_CONS_IFF,
1245          APPEND]
1246QED
1247
1248
1249Theorem PERM_FUN_SWAP_AT_FRONT:
1250 !x y l. PERM (x::y::l) = PERM (y::x::l)
1251Proof
1252REWRITE_TAC[GSYM PERM_EQUIVALENCE_ALT_DEF,
1253            PERM_SWAP_AT_FRONT, PERM_REFL]
1254QED
1255
1256Theorem PERM_FUN_CONS_11_SWAP_AT_FRONT:
1257 !y l1 x l2.
1258(PERM l1 = PERM (x::l2)) ==>
1259(PERM (y::l1) = PERM (x::y::l2))
1260Proof
1261REPEAT STRIP_TAC THEN
1262ASSUME_TAC (Q.SPECL [‘x’, ‘y’,‘l2’] PERM_FUN_SWAP_AT_FRONT) THEN
1263ASM_REWRITE_TAC[] THEN
1264FULL_SIMP_TAC std_ss [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_CONS_IFF]
1265QED
1266
1267
1268Theorem PERM_FUN_CONS_11_APPEND:
1269 !y l1 l2 l3.
1270(PERM l1 = PERM (l2++l3)) ==>
1271(PERM (y::l1) = PERM (l2++(y::l3)))
1272Proof
1273EVERY [SIMP_TAC list_ss
1274    [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_alt, FILTER_APPEND_DISTRIB],
1275  REPEAT STRIP_TAC, COND_CASES_TAC, ASM_SIMP_TAC list_ss [] ]
1276QED
1277
1278Theorem PERM_FUN_CONS_APPEND_1:
1279 !l l1 x l2.
1280(PERM l1 = PERM (x::l2)) ==>
1281(PERM (l1 ++ l) = PERM (x::(l2++l)))
1282Proof
1283EVERY [SIMP_TAC list_ss
1284    [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_alt, FILTER_APPEND_DISTRIB],
1285  REPEAT STRIP_TAC, COND_CASES_TAC, ASM_SIMP_TAC list_ss [] ]
1286QED
1287
1288Theorem PERM_FUN_CONS_APPEND_2:
1289 !l l1 x l2.
1290(PERM l1 = PERM (x::l2)) ==>
1291(PERM (l ++ l1) = PERM (x::(l ++ l2)))
1292Proof
1293EVERY [SIMP_TAC list_ss
1294    [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_alt, FILTER_APPEND_DISTRIB],
1295  REPEAT STRIP_TAC, COND_CASES_TAC, ASM_SIMP_TAC list_ss [] ]
1296QED
1297
1298Theorem PERM_FUN_APPEND_APPEND_1:
1299 !l1 l2 l3 l4.
1300(PERM l1 = PERM (l2++l3)) ==>
1301(PERM (l1 ++ l4) = PERM (l2++(l3++l4)))
1302Proof
1303SIMP_TAC list_ss
1304    [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_alt, FILTER_APPEND_DISTRIB]
1305QED
1306
1307Theorem PERM_FUN_APPEND_APPEND_2:
1308 !l1 l2 l3 l4.
1309(PERM l1 = PERM (l2++l3)) ==>
1310(PERM (l4 ++ l1) = PERM (l2++(l4++l3)))
1311Proof
1312SIMP_TAC list_ss
1313    [GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_alt, FILTER_APPEND_DISTRIB]
1314QED
1315
1316Theorem PERM_FUN_APPEND:
1317 !l1 l2. PERM (l1 ++ l2) = PERM (l2 ++ l1)
1318Proof
1319REWRITE_TAC[GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_APPEND]
1320QED
1321
1322
1323Theorem PERM_FUN_CONS_IFF:
1324 !x l1 l2. (PERM l1 = PERM l2) ==> (PERM (x::l1) = PERM (x::l2))
1325Proof
1326REWRITE_TAC[GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_CONS_IFF]
1327QED
1328
1329
1330
1331Theorem PERM_FUN_APPEND_IFF:
1332 !l l1 l2. (PERM l1 = PERM l2) ==> (PERM (l++l1) = PERM (l++l2))
1333Proof
1334REWRITE_TAC[GSYM PERM_EQUIVALENCE_ALT_DEF, PERM_APPEND_IFF]
1335QED
1336
1337
1338
1339Theorem PERM_FUN_CONG:
1340 !l1 l1' l2 l2'.
1341(PERM l1 = PERM l1') ==>
1342(PERM l2 = PERM l2') ==>
1343(PERM l1 l2 = PERM l1' l2')
1344Proof
1345METIS_TAC[PERM_EQUIVALENCE_ALT_DEF]
1346QED
1347
1348
1349Theorem PERM_CONG_2:
1350 !l1 l1' l2 l2'.
1351(PERM l1 l1') ==>
1352(PERM l2 l2') ==>
1353(PERM l1 l2 = PERM l1' l2')
1354Proof
1355METIS_TAC[PERM_EQUIVALENCE_ALT_DEF]
1356QED
1357
1358
1359Theorem PERM_CONG_APPEND_IFF:
1360 !l l1 l1' l2 l2'.
1361(PERM l1 (l++l1')) ==>
1362(PERM l2 (l++l2')) ==>
1363(PERM l1 l2 = PERM l1' l2')
1364Proof
1365METIS_TAC [PERM_EQUIVALENCE_ALT_DEF, PERM_APPEND_IFF]
1366QED
1367
1368
1369Theorem PERM_CONG_APPEND_IFF2:
1370 !l1 l1' l1'' l2 l2' l2''.
1371(PERM l1 (l1'++l1'')) ==>
1372(PERM l2 (l2'++l2'')) ==>
1373(PERM l1' l2') ==>
1374(PERM l1 l2 = PERM l1'' l2'')
1375Proof
1376METIS_TAC [PERM_EQUIVALENCE_ALT_DEF, PERM_APPEND_IFF]
1377QED
1378
1379
1380Theorem PERM_FUN_SPLIT:
1381 !l l1 l1' l2.
1382(PERM l (l1++l2)) ==>
1383(PERM l1' l1) ==>
1384(PERM l (l1'++l2))
1385Proof
1386METIS_TAC [PERM_EQUIVALENCE_ALT_DEF, PERM_APPEND_IFF]
1387QED
1388
1389
1390Theorem PERM_REWR:
1391 !l r l1 l2.
1392(PERM l r) ==>
1393(PERM (l++l1) l2 = PERM (r++l1) l2)
1394Proof
1395PROVE_TAC [PERM_EQUIVALENCE_ALT_DEF, PERM_APPEND_IFF]
1396QED
1397
1398
1399Theorem PERM_CENTRE1[local]:
1400 (PERM (xs ++ l) (r1 ++ xs ++ r2) = PERM l (r1 ++ r2))
1401Proof
1402METIS_TAC [APPEND_ASSOC, PERM_APPEND_IFF,
1403    PERM_APPEND, PERM_EQUIVALENCE_ALT_DEF]
1404QED
1405val PERM_CENTRE2 = PERM_CENTRE1 |> Q.GEN ‘xs’ |> Q.SPEC ‘[x]’
1406  |> SIMP_RULE bool_ss [APPEND, GSYM APPEND_ASSOC]
1407
1408Theorem PERM_TO_APPEND_SIMPS:
1409 (PERM (x::l) ((x::r1) ++ r2) = PERM l (r1 ++ r2)) /\
1410(PERM (x::l) (r1 ++ (x::r2)) = PERM l (r1 ++ r2)) /\
1411(PERM ((xs ++ ys) ++ zs) r = PERM (xs ++ (ys ++ zs)) r) /\
1412(PERM ((x :: ys) ++ zs) r = PERM (x :: (ys ++ zs)) r) /\
1413(PERM ([] ++ l) r = PERM l r) /\
1414(PERM (xs ++ l) ((xs ++ r1) ++ r2) = PERM l (r1 ++ r2)) /\
1415(PERM (xs ++ l) (r1 ++ (xs ++ r2)) = PERM l (r1 ++ r2)) /\
1416(PERM [] ([] ++ []) = T) /\
1417(PERM xs ((xs ++ []) ++ []) = T) /\
1418(PERM xs ([] ++ (xs ++ [])) = T)
1419Proof
1420SIMP_TAC list_ss [PERM_REFL, PERM_CONS_IFF, PERM_CENTRE1, PERM_CENTRE2]
1421  \\ SIMP_TAC bool_ss [GSYM APPEND_ASSOC, PERM_APPEND_IFF]
1422QED
1423
1424Theorem PERM_FLAT:
1425  !l1 l2. PERM l1 l2 ==> PERM (FLAT l1) (FLAT l2)
1426Proof
1427  ho_match_mp_tac PERM_IND
1428  \\ rw[PERM_APPEND_IFF, PERM_SWAP_L_AT_FRONT]
1429  \\ metis_tac[PERM_TRANS]
1430QED
1431
1432Theorem PERM_FLAT_MAP_CONS:
1433  !h t ls. PERM (FLAT (MAP (\x. h x :: t x) ls)) (MAP h ls ++ FLAT (MAP t ls))
1434Proof
1435  ntac 2 gen_tac
1436  \\ Induct
1437  \\ rw[]
1438  \\ irule PERM_TRANS
1439  \\ qmatch_goalsub_abbrev_tac`PERM _ (a ++ b ++ c)`
1440  \\ qexists_tac`b ++ (a ++ c)`
1441  \\ simp[PERM_APPEND_IFF, PERM_APPEND]
1442QED
1443
1444Theorem PERM_FLAT_MAP_SWAP:
1445  !f l1 l2.
1446    PERM (FLAT (MAP (\x. MAP (f x) l2) l1))
1447         (FLAT (MAP (\x. MAP (flip f x) l1) l2))
1448Proof
1449  gen_tac
1450  \\ Induct
1451  \\ rw[]
1452  >- (
1453    qmatch_goalsub_abbrev_tac`MAP g l2`
1454    \\ `g = K []` by simp[Abbr`g`, FUN_EQ_THM]
1455    \\ rw[FLAT_MAP_K_NIL] )
1456  \\ irule PERM_TRANS
1457  \\ qexists_tac`MAP (f h) l2 ++ FLAT (MAP (\x. MAP (flip f x) l1) l2)`
1458  \\ simp[PERM_APPEND_IFF]
1459  \\ simp[Once PERM_SYM]
1460  \\ qho_match_abbrev_tac`PERM (FLAT (MAP (\x. hf x :: ht x) l2)) _`
1461  \\ `MAP (f h) l2 = MAP hf l2`
1462  by ( simp[Abbr`hf`, MAP_EQ_f] \\ metis_tac[] )
1463  \\ pop_assum SUBST1_TAC
1464  \\ simp[PERM_FLAT_MAP_CONS]
1465QED
1466
1467Theorem PERM_MAP_SET_TO_LIST_IMAGE:
1468  !s. FINITE s ==> !f. (!x y. x IN s /\ y IN s /\ f x = f y ==> x = y) ==>
1469  PERM (MAP f (SET_TO_LIST s)) (SET_TO_LIST (IMAGE f s))
1470Proof
1471  ho_match_mp_tac FINITE_INDUCT
1472  \\ rw[]
1473  \\ rw[Once PERM_SYM]
1474  \\ irule PERM_TRANS
1475  \\ qexists_tac`f e :: SET_TO_LIST (IMAGE f s)`
1476  \\ conj_tac
1477  >- (
1478    `FINITE (IMAGE f s)` by simp[]
1479    \\ drule PERM_SET_TO_LIST_INSERT
1480    \\ disch_then(qspec_then`f e`mp_tac)
1481    \\ simp[]
1482    \\ metis_tac[])
1483  \\ irule PERM_TRANS
1484  \\ qexists_tac`f e :: MAP f (SET_TO_LIST s)`
1485  \\ conj_tac >- metis_tac[PERM_SYM, PERM_CONS_IFF]
1486  \\ rewrite_tac[GSYM MAP]
1487  \\ irule PERM_MAP
1488  \\ rw[Once PERM_SYM]
1489  \\ drule PERM_SET_TO_LIST_INSERT
1490  \\ metis_tac[]
1491QED
1492
1493Theorem PERM_BIJ_SET_TO_LIST:
1494  !f s1 s2. FINITE s1 /\ FINITE s2 /\ BIJ f s1 s2 ==>
1495  PERM (MAP f (SET_TO_LIST s1)) (SET_TO_LIST s2)
1496Proof
1497  rw[]
1498  \\ irule PERM_TRANS
1499  \\ qexists_tac`SET_TO_LIST (IMAGE f s1)`
1500  \\ conj_tac
1501  >- (
1502    irule PERM_MAP_SET_TO_LIST_IMAGE
1503    \\ fs[BIJ_DEF, INJ_DEF] )
1504  \\ imp_res_tac BIJ_IMAGE
1505  \\ rw[]
1506QED
1507
1508Theorem PERM_SET_TO_LIST_DISJOINT_UNION_APPEND:
1509  !s1 s2. FINITE s1 /\ FINITE s2 /\ DISJOINT s1 s2 ==>
1510  PERM (SET_TO_LIST (s1 UNION s2)) (SET_TO_LIST s1 ++ SET_TO_LIST s2)
1511Proof
1512  rpt strip_tac
1513  \\ irule PERM_ALL_DISTINCT
1514  \\ simp[ALL_DISTINCT_APPEND]
1515  \\ fs[IN_DISJOINT]
1516  \\ PROVE_TAC[]
1517QED
1518
1519Theorem LIST_REL_PERM:
1520  !l1 l2 l3. LIST_REL P l1 l2 /\ PERM l2 l3 ==>
1521             ?l4. PERM l1 l4 /\ LIST_REL P l4 l3
1522Proof
1523  Induct_on ‘LIST_REL’
1524  \\ rw[PERM_CONS_EQ_APPEND, PULL_EXISTS]
1525  \\ ntac 2 (irule_at Any listTheory.LIST_REL_APPEND_suff)
1526  \\ simp[]
1527  \\ first_x_assum $ drule_then strip_assume_tac
1528  \\ gs[LIST_REL_SPLIT2, SF SFY_ss]
1529QED
1530
1531(*---------------------------------------------------------------------------*)
1532(* QSORT3 - A stable version of QSORT (James Reynolds - 10/2010)             *)
1533(*    Lists are stable if filtering using any predicate that implies two     *)
1534(*    elements are unordered is unaffected by sorting.                       *)
1535(*---------------------------------------------------------------------------*)
1536
1537Definition STABLE_DEF:
1538    STABLE sort r <=>
1539      SORTS sort r /\
1540      !p. (!x y. p x /\ p y ==> r x y) ==>
1541          (!l. FILTER p l = FILTER p (sort r l))
1542End
1543
1544(*---------------------------------------------------------------------------*)
1545(* PART3 - Split a list into < h, = h and > h                                *)
1546(*---------------------------------------------------------------------------*)
1547
1548Definition PART3_DEF:
1549    (PART3 R h [] = ([],[],[])) /\
1550    (PART3 R h (hd::tl) =
1551         if R h hd /\ R hd h
1552            then (I ## CONS hd ## I) (PART3 R h tl)
1553            else if R hd h
1554                    then (CONS hd ## I ## I) (PART3 R h tl)
1555                    else (I ## I ## CONS hd) (PART3 R h tl))
1556End
1557
1558Theorem LENGTH_FILTER[local]:
1559  !a. LENGTH (FILTER P a) <= LENGTH a
1560Proof
1561    Induct THEN RW_TAC arith_ss [FILTER, LENGTH]
1562QED
1563
1564Theorem length_lem[local]:
1565  !a h. LENGTH (FILTER P a) < LENGTH (h::a)
1566Proof
1567    REPEAT STRIP_TAC THEN REWRITE_TAC [LENGTH] THEN
1568    MATCH_MP_TAC (DECIDE “!a b. a <= b ==> a < SUC b”) THEN
1569    MATCH_ACCEPT_TAC LENGTH_FILTER
1570QED
1571
1572(*---------------------------------------------------------------------------*)
1573(* PART3_FILTER - Partition is the same as filtering.                        *)
1574(*---------------------------------------------------------------------------*)
1575
1576Theorem PART3_FILTER:
1577     !tl hd. PART3 R hd tl = (FILTER (\x. R x hd /\ ~R hd x) tl,
1578                            FILTER (\x. R x hd /\ R hd x) tl,
1579                            FILTER (\x. ~R x hd) tl)
1580Proof
1581    Induct THEN RW_TAC std_ss [PART3_DEF, PAIR_MAP, FILTER] THEN
1582    FULL_SIMP_TAC std_ss []
1583QED
1584
1585(*---------------------------------------------------------------------------*)
1586(* QSORT3 - Partition three ways but only recurse on < and >                 *)
1587(*---------------------------------------------------------------------------*)
1588
1589Definition QSORT3_DEF:
1590    (QSORT3 R [] = []) /\
1591    (QSORT3 R (hd::tl) =
1592        let (lo,eq,hi) = PART3 R hd tl
1593        in QSORT3 R lo ++ (hd::eq) ++ QSORT3 R hi)
1594Termination
1595  WF_REL_TAC ‘measure (LENGTH o SND)’ THEN
1596  RW_TAC arith_ss [PART3_FILTER, length_lem]
1597End
1598
1599Theorem PERM3:
1600     !x a a' b b' c c'.
1601      (PERM a a' /\ PERM b b' /\ PERM c c') /\ PERM x (a ++ b ++ c)
1602      ==> PERM x (a' ++ b' ++ c')
1603Proof
1604    RW_TAC std_ss [PERM_DEF, FILTER_APPEND_DISTRIB]
1605QED
1606
1607val PULL_CONV =
1608  REPEATC (DEPTH_CONV (RIGHT_IMP_FORALL_CONV ORELSEC AND_IMP_INTRO_CONV))
1609val PULL_RULE = CONV_RULE PULL_CONV;
1610
1611val IND_STEP_TAC = PAT_X_ASSUM “!y. P ==> Q” (MATCH_MP_TAC o PULL_RULE);
1612
1613val tospec =
1614    Q.GEN ‘P’
1615      (MATCH_MP (SPEC_ALL
1616        (REWRITE_RULE [GSYM AND_IMP_INTRO] PERM_TRANS)) (SPEC_ALL PERM_SPLIT));
1617
1618Theorem filter_filter[local]:
1619
1620     !l P Q. FILTER P (FILTER Q l) = FILTER (\x. P x /\ Q x) l
1621Proof
1622    Induct THEN NTAC 2 (RW_TAC std_ss [FILTER]) THEN PROVE_TAC []
1623QED
1624
1625Theorem PERM3_FILTER:
1626  !l h.
1627    PERM l
1628         (FILTER (\x. R x h /\ ~R h x) l ++ FILTER (\x. R x h /\ R h x) l ++
1629          FILTER (\x. ~R x h) l)
1630Proof
1631  REPEAT STRIP_TAC THEN
1632  MATCH_MP_TAC (SPEC “\x. (R:'a -> 'a -> bool) x h” tospec) THEN
1633  REWRITE_TAC [APPEND_ASSOC] THEN MATCH_MP_TAC PERM_CONG THEN
1634  RW_TAC std_ss [combinTheory.o_DEF, PERM_REFL] THEN
1635  MATCH_MP_TAC (SPEC “(R :'a -> 'a -> bool) h” tospec) THEN
1636  RW_TAC std_ss [o_DEF, PERM_REFL, filter_filter, FILTER_APPEND_DISTRIB] THEN
1637  MATCH_MP_TAC
1638    (PROVE [PERM_APPEND] “(A = C) /\ (B = D) ==> (PERM (A ++ B) (D ++ C))”) THEN
1639  REPEAT CONJ_TAC THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
1640  PROVE_TAC []
1641QED
1642
1643Theorem PERM_QSORT3:
1644  !l R. PERM l (QSORT3 R l)
1645Proof
1646  completeInduct_on ‘LENGTH l’ THEN Cases THEN
1647  RW_TAC std_ss [PERM_CONS_EQ_APPEND, QSORT3_DEF, PERM_NIL, PART3_FILTER] THEN
1648  Q.EXISTS_TAC ‘QSORT3 R (FILTER (\x. R x h /\ ~R h x) t)’ THEN
1649  Q.EXISTS_TAC
1650   ‘FILTER (\x. R x h /\ R h x) t ++ QSORT3 R (FILTER (\x. ~R x h) t) ’ THEN
1651  RW_TAC std_ss [APPEND_ASSOC, GSYM APPEND] THEN
1652  MATCH_MP_TAC PERM3 THEN
1653  MAP_EVERY Q.EXISTS_TAC [
1654      ‘FILTER (\x. R x h /\ ~R h x) t’,
1655      ‘FILTER (\x. R x h /\ R h x) t’,
1656      ‘FILTER (\x. ~R x h) t’] THEN
1657  RW_TAC std_ss [PERM_REFL] THEN TRY IND_STEP_TAC THEN
1658  RW_TAC arith_ss [length_lem] THEN METIS_TAC [PERM3_FILTER]
1659QED
1660
1661Theorem SORTED_EQ_PART:
1662     !l R. transitive R ==> SORTED R (FILTER (\x. R x hd /\ R hd x) l)
1663Proof
1664    Induct THEN REPEAT STRIP_TAC THEN
1665    RW_TAC std_ss [SORTED_DEF, FILTER, SORTED_EQ, MEM_FILTER] THEN
1666    PROVE_TAC [relationTheory.transitive_def]
1667QED
1668
1669Theorem QSORT3_SORTS:
1670  !R. transitive R /\ total R ==> SORTS QSORT3 R
1671Proof
1672  RW_TAC std_ss [SORTS_DEF, PERM_QSORT3] THEN
1673  completeInduct_on ‘LENGTH l’ THEN
1674  Cases_on ‘l’ THEN
1675  RW_TAC std_ss [QSORT3_DEF, SORTED_DEF, PART3_FILTER] THEN
1676  REPEAT (MATCH_MP_TAC SORTED_APPEND_IMP THEN REPEAT CONJ_TAC) THEN
1677  ASM_REWRITE_TAC [] THEN
1678  TRY IND_STEP_TAC THEN
1679  RW_TAC std_ss [length_lem, SORTED_EQ, MEM_FILTER, SORTED_EQ_PART, MEM,
1680                 MEM_FILTER, MEM_APPEND] THEN
1681  IMP_RES_TAC (PROVE[MEM_PERM, PERM_QSORT3] “MEM x (QSORT3 R b) ==> MEM x b”) >>
1682  FULL_SIMP_TAC std_ss [MEM_FILTER] THEN
1683  PROVE_TAC [relationTheory.total_def,relationTheory.transitive_def]
1684QED
1685
1686Theorem LENGTH_QSORT3[local] =
1687   PROVE [PERM_LENGTH, PERM_QSORT3] “!l R. LENGTH (QSORT3 R l) = LENGTH l”
1688
1689fun SPLIT_APPEND_TAC x =
1690    MATCH_MP_TAC
1691      (prove(x, REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [APPEND_ASSOC])) THEN
1692    REPEAT CONJ_TAC
1693
1694fun LIND_STEP (a,goal) =
1695  FIRST_ASSUM
1696    (CONV_TAC o LAND_CONV o REWR_CONV o
1697     SIMP_RULE std_ss [length_lem,LENGTH_QSORT3] o
1698     SPEC (mk_comb(“LENGTH:'a list -> num”,lhs goal)) o
1699     Q.GEN ‘m’ o C (PART_MATCH (lhs o rand)) (lhs goal) o PULL_RULE) (a,goal)
1700
1701Theorem FILTER_P[local]:
1702
1703     !R h. p h /\ transitive R /\ total R /\ (!x y. p x /\ p y ==> R x y) ==>
1704             !l. (FILTER (\x. p x /\ R x h /\ R h x) l = FILTER p l) /\
1705                 (FILTER p (FILTER (\x. R x h /\ ~R h x) l) = []) /\
1706                 (FILTER p (FILTER (\x. ~R x h) l) = [])
1707Proof
1708    NTAC 3 STRIP_TAC THEN Induct THEN RW_TAC std_ss [FILTER] THEN
1709    PROVE_TAC [relationTheory.transitive_def, relationTheory.total_def]
1710QED
1711
1712Theorem QSORT3_SPLIT:
1713  !R. transitive R /\ total R ==>
1714      !l e.
1715        QSORT3 R l = QSORT3 R (FILTER (\x. R x e /\ ~R e x) l) ++
1716                     FILTER (\x. R x e /\ R e x) l ++
1717                     QSORT3 R (FILTER (\x. ~R x e) l)
1718Proof
1719  NTAC 2 STRIP_TAC THEN completeInduct_on ‘LENGTH l’ THEN Cases THEN
1720  RW_TAC std_ss [FILTER, QSORT3_DEF, PART3_FILTER, APPEND, APPEND_ASSOC] THEN
1721  RW_TAC std_ss [filter_filter, QSORT3_DEF, PART3_FILTER] THEN
1722  FULL_SIMP_TAC bool_ss [APPEND_ASSOC] THENL [
1723    SPLIT_APPEND_TAC “(a = d) /\ (b = e) /\ (c = f ++ g ++ h) ==>
1724                      (a ++ b ++ c = d ++ e ++ f ++ g ++ h)”,
1725    SPLIT_APPEND_TAC “(a = d) /\ (b = e) /\ (c = f) ==>
1726                      (a ++ b ++ c = d ++ e ++ f)”,
1727    SPLIT_APPEND_TAC “(a = d ++ e ++ f) /\ (b = g) /\ (c = h) ==>
1728                      (a ++ b ++ c = d ++ e ++ f ++ g ++ h)”
1729  ] THEN
1730  TRY (LIND_STEP THEN
1731       SPLIT_APPEND_TAC “(a = d) /\ (b = e) /\ (c = f) ==>
1732                         (a ++ b ++ c = d ++ e ++ f)”) THEN
1733  RW_TAC std_ss [filter_filter] THEN
1734  REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
1735  PROVE_TAC [relationTheory.total_def,relationTheory.transitive_def]
1736QED
1737
1738(*---------------------------------------------------------------------------*)
1739(* Final proof: QSORT3 is a stable sort.                                     *)
1740(*---------------------------------------------------------------------------*)
1741
1742Theorem QSORT3_STABLE:
1743  !R. transitive R /\ total R ==> STABLE QSORT3 R
1744Proof
1745  RW_TAC std_ss [STABLE_DEF, QSORT3_SORTS] >>
1746  completeInduct_on ‘LENGTH l’ >> Cases_on ‘l’ >>
1747  RW_TAC std_ss [QSORT3_DEF, FILTER, PART3_FILTER] >>
1748  RW_TAC std_ss [FILTER_APPEND_DISTRIB, filter_filter, GSYM APPEND, FILTER]
1749  >- METIS_TAC [FILTER_P, APPEND_NIL, length_lem, CONJUNCT1 APPEND] >>
1750  MATCH_MP_TAC EQ_TRANS >> Q.EXISTS_TAC ‘FILTER p (QSORT3 R t)’ >> CONJ_TAC
1751  >- (IND_STEP_TAC >> RW_TAC arith_ss [LENGTH]) >>
1752  METIS_TAC [FILTER_APPEND_DISTRIB, filter_filter, QSORT3_SPLIT]
1753QED
1754
1755
1756(*---------------------------------------------------------------------------*)
1757(* Various useful theorems from the CakeML project https://cakeml.org.       *)
1758(*---------------------------------------------------------------------------*)
1759
1760local open rich_listTheory in
1761
1762Theorem QSORT3_MEM:
1763  !R L x. MEM x (QSORT3 R L) <=> MEM x L
1764Proof
1765 ho_match_mp_tac QSORT3_IND >>
1766 rw [QSORT3_DEF] >>
1767 fs [] >>
1768 eq_tac >>
1769 rw [] >>
1770 fs [PART3_FILTER] >>
1771 rw [] >>
1772 fs [MEM_FILTER] >>
1773 metis_tac []
1774QED
1775
1776Theorem QSORT3_SORTED:
1777 !R L. transitive R /\ total R ==> SORTED R (QSORT3 R L)
1778Proof
1779 rw [] >>
1780 imp_res_tac QSORT3_SORTS >>
1781 fs [SORTS_DEF]
1782QED
1783
1784Theorem sorted_lt_count_list:
1785 !n. SORTED $< (COUNT_LIST n)
1786Proof
1787 Induct_on ‘n’
1788 >- rw [COUNT_LIST_def] >>
1789 rw [COUNT_LIST_SNOC, SNOC_APPEND] >>
1790 match_mp_tac SORTED_APPEND_IMP >>
1791 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [transitive_def, MEM_COUNT_LIST] >>
1792 decide_tac
1793QED
1794
1795Theorem SORTED_weaken:
1796   !R R' ls. SORTED R ls /\ (!x y. MEM x ls /\ MEM y ls /\ R x y ==> R' x y)
1797      ==> SORTED R' ls
1798Proof
1799  NTAC 2 GEN_TAC THEN
1800  Induct THEN SRW_TAC[][] THEN
1801  Cases_on‘ls’ THEN
1802  FULL_SIMP_TAC(srw_ss())[SORTED_DEF] THEN
1803  FIRST_X_ASSUM MATCH_MP_TAC THEN
1804  METIS_TAC[]
1805QED
1806
1807Theorem sorted_count_list:
1808 !n. SORTED $<= (COUNT_LIST n)
1809Proof
1810 gen_tac \\ irule SORTED_weaken \\ qexists_tac‘$<’
1811 \\ simp[sorted_lt_count_list]
1812QED
1813
1814Theorem sorted_map:
1815 !R f l. (SORTED R (MAP f l) <=> SORTED (inv_image R f) l)
1816Proof
1817 Induct_on ‘l’ >> rw [SORTED_EL_SUC, EL_MAP]
1818QED
1819
1820Theorem sorted_perm_count_list:
1821 !y f l n.
1822  SORTED (inv_image $<= f) l /\
1823  PERM (MAP f l) (COUNT_LIST n)
1824  ==>
1825  (MAP f l = COUNT_LIST n)
1826Proof
1827 rw [] >>
1828 ‘transitive $<= /\ antisymmetric $<=’
1829          by srw_tac [ARITH_ss] [transitive_def,antisymmetric_def] >>
1830 metis_tac [sorted_map, SORTED_PERM_EQ, sorted_count_list]
1831QED
1832
1833Theorem greater_sorted_eq:
1834  SORTED $> (x::L) ⇔ SORTED $> L ∧ ∀y. MEM y L ⇒ y < x
1835Proof
1836  qsuff_tac ‘(∀y. MEM y L ⇒ y < x) = (∀y. MEM y L ⇒ x > y)’
1837  >- (strip_tac \\ gvs [] \\ irule SORTED_EQ \\ rw [transitive_def])
1838  \\ eq_tac \\ rpt strip_tac \\ res_tac \\ decide_tac
1839QED
1840
1841Theorem less_sorted_eq =
1842  MATCH_MP SORTED_EQ arithmeticTheory.transitive_LESS
1843
1844Theorem SORTED_GENLIST_PLUS:
1845   !n k. SORTED $< (GENLIST ($+ k) n)
1846Proof
1847  Induct >> simp[GENLIST_CONS,less_sorted_eq,MEM_GENLIST] >> gen_tac >>
1848  ‘$+ k o SUC = $+ (k+1)’ by (
1849    simp[FUN_EQ_THM] ) >>
1850  metis_tac[]
1851QED
1852
1853Theorem SORTED_ALL_DISTINCT:
1854   irreflexive R /\ transitive R ==> !ls. SORTED R ls ==> ALL_DISTINCT ls
1855Proof
1856  STRIP_TAC THEN Induct THEN SRW_TAC[][] THEN
1857  IMP_RES_TAC SORTED_EQ THEN
1858  FULL_SIMP_TAC (srw_ss()) [SORTED_DEF] THEN
1859  METIS_TAC[relationTheory.irreflexive_def]
1860QED
1861
1862Theorem sorted_filter:
1863   !R ls. transitive R ==> SORTED R ls ==> SORTED R (FILTER P ls)
1864Proof
1865  HO_MATCH_MP_TAC SORTED_IND >>
1866  rw[SORTED_DEF] >> fs[] >>
1867  rfs[SORTED_EQ,MEM_FILTER] >>
1868  rw[] >> metis_tac[transitive_def]
1869QED
1870
1871end
1872
1873Theorem SORTED_ALL_DISTINCT_LIST_TO_SET_EQ:
1874  !R. transitive R /\ antisymmetric R ==>
1875      !l1 l2. SORTED R l1 /\ SORTED R l2 /\ ALL_DISTINCT l1 /\
1876              ALL_DISTINCT l2 /\ set l1 = set l2 ==>
1877              l1 = l2
1878Proof
1879  gen_tac \\ strip_tac
1880  \\ Induct \\ simp[]
1881  \\ gen_tac \\ Cases \\ simp[]
1882  \\ simp[SORTED_EQ]
1883  \\ strip_tac
1884  \\ fs[EXTENSION]
1885  \\ metis_tac[antisymmetric_def]
1886QED
1887
1888Theorem EL_FILTER_COUNT_LIST_LEAST:
1889!n i.
1890  (i < LENGTH (FILTER P (COUNT_LIST n))) ==>
1891    EL i (FILTER P (COUNT_LIST n))
1892    = LEAST j.
1893        ((0 < i) ==> EL (i-1) (FILTER P (COUNT_LIST n)) < j) /\
1894        (j < n) /\ P j
1895Proof
1896  rw[]
1897  \\ ‘SORTED $< (FILTER P (COUNT_LIST n))’
1898    by ( irule SORTED_FILTER \\ rw[sorted_lt_count_list] )
1899  \\ qmatch_abbrev_tac‘x = _’
1900  \\ ‘MEM x (FILTER P (COUNT_LIST n))’ by metis_tac[MEM_EL]
1901  \\ numLib.LEAST_ELIM_TAC
1902  \\ conj_tac
1903  >- (
1904    qexists_tac‘x’
1905    \\ fs[MEM_FILTER, MEM_COUNT_LIST]
1906    \\ strip_tac
1907    \\ fs[SORTED_EL_LESS, Abbr‘x’] )
1908  \\ qx_gen_tac‘y’
1909  \\ strip_tac
1910  \\ ‘MEM y (FILTER P (COUNT_LIST n))’ by simp[MEM_FILTER, MEM_COUNT_LIST]
1911  \\ pop_assum mp_tac \\ simp[MEM_EL]
1912  \\ disch_then(qx_choose_then‘j’strip_assume_tac)
1913  \\ Cases_on‘i = j’ >- fs[]
1914  \\ Cases_on‘i < j’ >- (
1915    ‘x < y’ by fs[SORTED_EL_LESS, Abbr‘x’]
1916    \\ first_x_assum drule
1917    \\ fs[SORTED_EL_LESS, MEM_FILTER]
1918    \\ simp[Abbr‘x’]
1919    \\ Cases_on‘i = 0’ \\ simp[] )
1920  \\ ‘j < i’ by simp[]
1921  \\ ‘0 < i’ by simp[]
1922  \\ Cases_on ‘j = i-1’ \\ fs[]
1923  \\ ‘j < i-1’ by fs[]
1924  \\ fs[SORTED_EL_LESS]
1925  \\ last_x_assum drule
1926  \\ simp[]
1927QED
1928
1929Theorem SORTED_FILTER_COUNT_LIST:
1930  SORTED R (FILTER P (COUNT_LIST m)) <=>
1931  !i j. (i < j) /\ (j < m) /\ P i /\ P j /\ (!k. (i < k) /\ (k < j) ==> ~P k)
1932        ==> R i j
1933Proof
1934  ‘SORTED $< (FILTER P (COUNT_LIST m))’
1935  by ( irule SORTED_FILTER \\ simp[sorted_lt_count_list] )
1936  \\ rw[SORTED_EL_SUC, EQ_IMP_THM]
1937  >- (
1938    ‘MEM i (FILTER P (COUNT_LIST m))’ by simp[MEM_FILTER, MEM_COUNT_LIST]
1939    \\ ‘MEM j (FILTER P (COUNT_LIST m))’ by simp[MEM_FILTER, MEM_COUNT_LIST]
1940    \\ fs[MEM_EL]
1941    \\ qmatch_assum_rename_tac‘i = EL ni _’
1942    \\ qmatch_assum_rename_tac‘j = EL nj _’
1943    \\ ‘ni < nj’
1944    by (
1945      CCONTR_TAC \\ gs[NOT_LESS, LESS_OR_EQ]
1946      \\ fs[SORTED_EL_LESS]
1947      \\ res_tac \\ fs[] )
1948    \\ last_x_assum(qspec_then‘nj-1’mp_tac)
1949    \\ simp[ADD1]
1950    \\ ‘ni = nj - 1’ suffices_by rw[]
1951    \\ CCONTR_TAC
1952    \\ first_x_assum(qspec_then‘EL (nj-1) (FILTER P (COUNT_LIST m))’mp_tac)
1953    \\ fs[SORTED_EL_LESS]
1954    \\ qmatch_abbrev_tac‘P x’
1955    \\ ‘nj - 1 < LENGTH (FILTER P (COUNT_LIST m))’ by simp[]
1956    \\ ‘MEM x (FILTER P (COUNT_LIST m))’ by metis_tac[MEM_EL]
1957    \\ fs[MEM_FILTER] )
1958  \\ first_x_assum irule
1959  \\ qmatch_abbrev_tac‘P x /\ P y /\ _’
1960  \\ ‘n < LENGTH (FILTER P (COUNT_LIST m))’ by simp[]
1961  \\ ‘MEM x (FILTER P (COUNT_LIST m))’ by metis_tac[MEM_EL]
1962  \\ ‘MEM y (FILTER P (COUNT_LIST m))’ by metis_tac[MEM_EL]
1963  \\ fs[MEM_FILTER, MEM_COUNT_LIST]
1964  \\ fs[SORTED_EL_LESS]
1965  \\ reverse conj_asm2_tac >- metis_tac[prim_recTheory.LESS_SUC_REFL]
1966  \\ simp[Abbr‘y’, Once EL_FILTER_COUNT_LIST_LEAST]
1967  \\ numLib.LEAST_ELIM_TAC
1968  \\ conj_tac >- metis_tac[]
1969  \\ rw[]
1970  \\ first_x_assum(qspec_then‘k’mp_tac)
1971  \\ simp[]
1972QED
1973
1974Theorem SORTED_nub:
1975  transitive R /\ SORTED R ls ==> SORTED R (nub ls)
1976Proof
1977  qspec_then‘ls’(SUBST1_TAC o Q.AP_TERM‘nub’ o SYM)GENLIST_ID
1978  \\ simp[nub_GENLIST, sorted_map]
1979  \\ qmatch_goalsub_abbrev_tac‘FILTER P’
1980  \\ qmatch_goalsub_abbrev_tac‘COUNT_LIST m’
1981  \\ simp[SORTED_FILTER_COUNT_LIST]
1982  \\ rw[]
1983  \\ gs[SORTED_EL_LESS]
1984QED
1985
1986Theorem QSORT_nub:
1987  transitive R /\ antisymmetric R /\ total R ==>
1988  QSORT R (nub ls) = nub (QSORT R ls)
1989Proof
1990  rw[]
1991  \\ irule SORTED_ALL_DISTINCT_LIST_TO_SET_EQ
1992  \\ simp[]
1993  \\ conj_tac >- metis_tac[ALL_DISTINCT_PERM, QSORT_PERM, all_distinct_nub]
1994  \\ conj_tac >- simp[EXTENSION, QSORT_MEM]
1995  \\ qexists_tac‘R’
1996  \\ simp[QSORT_SORTED]
1997  \\ irule SORTED_nub
1998  \\ simp[QSORT_SORTED]
1999QED
2000
2001Theorem SORTED_FST_ZIP:
2002  !R ls rs.
2003  SORTED R ls /\ LENGTH ls = LENGTH rs ==>
2004  SORTED (\x y. R (FST x) (FST y)) (ZIP (ls,rs))
2005Proof
2006  ho_match_mp_tac SORTED_IND>>rw[]
2007  >- (Cases_on`rs`>>fs[])>>
2008  `?a b rss. rs = a::b::rss` by
2009    (Cases_on`rs` \\ fs[] \\
2010     metis_tac[list_CASES,LENGTH_NIL,SUC_NOT]) >>
2011  fs[]>>
2012  first_x_assum(qspec_then`b::rss` mp_tac)>>
2013  simp[]
2014QED
2015
2016Theorem lcp_PERM:
2017  PERM l1 l2 ==> lcp l1 = lcp l2
2018Proof
2019  rw[lcp_def] >> AP_TERM_TAC >> irule PERM_LIST_TO_SET >> simp[]
2020QED