1 (* ========================================================================= *)
2 (* Quick sort algorithm. *)
4 (* Author: Marco Maggesi *)
5 (* University of Florence, Italy *)
6 (* http://www.math.unifi.it/~maggesi/ *)
8 (* (c) Copyright, Marco Maggesi, 2005-2007 *)
9 (* ========================================================================= *)
11 needs "Permutation/permuted.ml";;
13 (* ------------------------------------------------------------------------- *)
15 (* ------------------------------------------------------------------------- *)
17 let ORDERED_RULES, ORDERED_INDUCT, ORDERED_CASES = new_inductive_definition
18 `(!le. ORDERED le []) /\
19 (!le h t. ORDERED le t /\ ALL (le h) t ==> ORDERED le (CONS h t))`;;
21 let ORDERED_CONS = prove
22 (`!le (h:A) t. ORDERED le (h :: t) <=> (ORDERED le t /\ ALL (le h) t)`,
24 `!le (h:A) t. ORDERED le (h :: t) ==> (ORDERED le t /\ ALL (le h) t)`
25 (fun th -> MESON_TAC [th; ORDERED_RULES]) THEN
27 DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE [ORDERED_CASES]) THEN
28 REWRITE_TAC [NOT_CONS_NIL; CONS_11] THEN MESON_TAC []);;
30 let ORDERED_APPEND = prove
32 ORDERED le (APPEND l1 l2) <=>
33 ORDERED le l1 /\ ORDERED le l2 /\ ALL (\x. ALL (le x) l2) l1`,
36 ORDERED le (APPEND l1 l2)
37 ==> ORDERED le l1 /\ ORDERED le l2 /\ ALL (\x. ALL (le x) l2) l1) /\
38 (!l1 l2. ORDERED le l1 /\ ORDERED le l2 /\ ALL (\x. ALL (le x) l2) l1
39 ==> ORDERED le (APPEND l1 l2))`
40 (fun th -> MESON_TAC [th]) THEN
41 CONJ_TAC THEN LIST_INDUCT_TAC THEN
42 REWRITE_TAC [APPEND; ALL; ORDERED_RULES; ORDERED_CONS] THEN
43 ASM_SIMP_TAC [ORDERED_CONS; ALL_APPEND] THEN ASM_MESON_TAC [ALL_APPEND]);;
45 (* ------------------------------------------------------------------------- *)
47 (* ------------------------------------------------------------------------- *)
50 let PROVE_RECURSIVE_FUNCTION_EXISTS_TAC : tactic = fun g ->
51 let th = pure_prove_recursive_function_exists (snd g) in
52 MATCH_MP_TAC (DISCH_ALL th) g in
53 new_specification ["QSORT"] (prove
54 (`?f. (!le. f le [] = [] : A list) /\
55 (!le h t. f le (CONS h t) =
56 APPEND (f le (FILTER (\x. ~le h x) t))
57 (CONS h (f le (FILTER (\x. le h x) t))))`,
58 REWRITE_TAC [GSYM SKOLEM_THM; AND_FORALL_THM] THEN GEN_TAC THEN
59 PROVE_RECURSIVE_FUNCTION_EXISTS_TAC THEN
60 EXISTS_TAC `MEASURE (LENGTH:A list -> num)` THEN
61 REWRITE_TAC [WF_MEASURE; MEASURE; LENGTH; FILTER] THEN
62 REWRITE_TAC [LT_SUC_LE; LENGTH_FILTER_LE]));;
64 let COUNT_QSORT = prove
65 (`!le x l. COUNT x (QSORT le l) = COUNT x l`,
66 GEN_TAC THEN GEN_TAC THEN MATCH_MP_TAC list_WF THEN LIST_INDUCT_TAC THEN
67 REWRITE_TAC [QSORT; COUNT; LENGTH; LT_SUC_LE; COUNT_APPEND] THEN
68 DISCH_TAC THEN ASM_SIMP_TAC [COUNT; LENGTH_FILTER_LE] THEN
69 REWRITE_TAC [COUNT_FILTER] THEN
70 REPEAT (ASM_REWRITE_TAC [ADD; ADD_SUC; ADD_0] THEN COND_CASES_TAC) THEN
71 ASM_MESON_TAC[ADD_SUC]);;
73 let QSORT_PERMUTED = prove
74 (`!le (l:A list). QSORT le l PERMUTED l`,
75 REWRITE_TAC [PERMUTED_COUNT; COUNT_QSORT]);;
78 (`!P le l. ALL P (QSORT le l) <=> ALL P l`,
79 MESON_TAC [QSORT_PERMUTED; PERMUTED_ALL]);;
81 let LENGTH_QSORT = prove
82 (`!le l. LENGTH (QSORT le l) = LENGTH l`,
83 MESON_TAC [QSORT_PERMUTED; PERMUTED_LENGTH]);;
86 (`!le l x. MEM x (QSORT le l) <=> MEM x l`,
87 MESON_TAC [QSORT_PERMUTED; PERMUTED_MEM]);;
89 let ORDERED_QSORT = prove
91 (!x y. le x y \/ le y x) /\ (!x y z. le x y \/ le y z ==> le x z)
92 ==> ORDERED le (QSORT le l)`,
93 REWRITE_TAC [GSYM RIGHT_IMP_FORALL_THM] THEN GEN_TAC THEN STRIP_TAC THEN
94 MATCH_MP_TAC list_WF THEN LIST_CASES_TAC THEN
95 REWRITE_TAC [QSORT; LENGTH; ORDERED_RULES; LT_SUC_LE] THEN DISCH_TAC THEN
96 REWRITE_TAC [ORDERED_APPEND; ORDERED_CONS; ALL; ALL_QSORT; ALL_T] THEN
97 ASM_SIMP_TAC [LENGTH_FILTER_LE] THEN REWRITE_TAC [GSYM ALL_MEM] THEN
101 REWRITE_CONV [QSORT; ARITH_LE; ARITH_LT; FILTER; APPEND]
102 `QSORT (<=) [12;3;5;1;23;2;1]`;;