author | nipkow |
Tue, 29 May 2018 14:05:59 +0200 | |
changeset 68312 | e9b5f25f6712 |
parent 68249 | 949d93804740 |
child 68386 | 98cf1c823c48 |
permissions | -rw-r--r-- |
67612 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
3 |
theory Radix_Sort |
|
4 |
imports |
|
68312 | 5 |
"HOL-Library.List_Lexorder" |
67612 | 6 |
"HOL-Library.Sublist" |
67688 | 7 |
"HOL-Library.Multiset" |
8 |
begin |
|
9 |
||
68176 | 10 |
text \<open>The \<open>Radix_Sort\<close> locale provides a sorting function \<open>radix_sort\<close> that sorts |
11 |
lists of lists. It is parameterized by a sorting function \<open>sort1 f\<close> that also sorts |
|
12 |
lists of lists, but only w.r.t. the column selected by \<open>f\<close>. |
|
13 |
Working with lists, \<open>f\<close> is instantiated with @{term"\<lambda>xs. xs ! n"} to select the \<open>n\<close>-th element. |
|
14 |
A more efficient implementation would sort lists of arrays because arrays support |
|
15 |
constant time access to every element.\<close> |
|
16 |
||
67688 | 17 |
locale Radix_Sort = |
18 |
fixes sort1 :: "('a list \<Rightarrow> 'a::linorder) \<Rightarrow> 'a list list \<Rightarrow> 'a list list" |
|
68176 | 19 |
assumes sorted: "sorted (map f (sort1 f xss))" |
20 |
assumes mset: "mset (sort1 f xss) = mset xss" |
|
67688 | 21 |
assumes stable: "stable_sort_key sort1" |
67612 | 22 |
begin |
23 |
||
68176 | 24 |
lemma set_sort1[simp]: "set(sort1 f xss) = set xss" |
67688 | 25 |
by (metis mset set_mset_mset) |
26 |
||
27 |
abbreviation "sort_col i xss \<equiv> sort1 (\<lambda>xs. xs ! i) xss" |
|
28 |
abbreviation "sorted_col i xss \<equiv> sorted (map (\<lambda>xs. xs ! i) xss)" |
|
29 |
||
30 |
fun radix_sort :: "nat \<Rightarrow> 'a list list \<Rightarrow> 'a list list" where |
|
67612 | 31 |
"radix_sort 0 xss = xss" | |
67688 | 32 |
"radix_sort (Suc i) xss = radix_sort i (sort_col i xss)" |
33 |
||
34 |
lemma mset_radix_sort: "mset (radix_sort i xss) = mset xss" |
|
35 |
by(induction i arbitrary: xss) (auto simp: mset) |
|
67612 | 36 |
|
37 |
abbreviation "sorted_from i xss \<equiv> sorted (map (drop i) xss)" |
|
38 |
||
67688 | 39 |
definition "cols xss n = (\<forall>xs \<in> set xss. length xs = n)" |
67612 | 40 |
|
67688 | 41 |
lemma cols_sort1: "cols xss n \<Longrightarrow> cols (sort1 f xss) n" |
67612 | 42 |
by(simp add: cols_def) |
43 |
||
67688 | 44 |
lemma sorted_from_Suc2: |
45 |
"\<lbrakk> cols xss n; i < n; |
|
46 |
sorted_col i xss; |
|
68249
949d93804740
First step to remove nonstandard "[x <- xs. P]" syntax: only input
nipkow
parents:
68176
diff
changeset
|
47 |
\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss) \<rbrakk> |
67612 | 48 |
\<Longrightarrow> sorted_from i xss" |
49 |
proof(induction xss rule: induct_list012) |
|
50 |
case 1 show ?case by simp |
|
51 |
next |
|
52 |
case 2 show ?case by simp |
|
53 |
next |
|
54 |
case (3 xs1 xs2 xss) |
|
55 |
have lxs1: "length xs1 = n" and lxs2: "length xs2 = n" |
|
56 |
using "3.prems"(1) by(auto simp: cols_def) |
|
57 |
have *: "drop i xs1 \<le> drop i xs2" |
|
58 |
proof - |
|
59 |
have "drop i xs1 = xs1!i # drop (i+1) xs1" |
|
60 |
using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1) |
|
67688 | 61 |
also have "\<dots> \<le> xs2!i # drop (i+1) xs2" |
62 |
using "3.prems"(3) "3.prems"(4)[of "xs2!i"] by(auto) |
|
67612 | 63 |
also have "\<dots> = drop i xs2" |
64 |
using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2) |
|
65 |
finally show ?thesis . |
|
66 |
qed |
|
67 |
have "sorted_from i (xs2 # xss)" |
|
68 |
proof(rule "3.IH"[OF _ "3.prems"(2)]) |
|
69 |
show "cols (xs2 # xss) n" using "3.prems"(1) by(simp add: cols_def) |
|
67688 | 70 |
show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp |
68249
949d93804740
First step to remove nonstandard "[x <- xs. P]" syntax: only input
nipkow
parents:
68176
diff
changeset
|
71 |
show "\<And>x. sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (xs2 # xss))" |
67612 | 72 |
using "3.prems"(4) |
73 |
sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.order.refl]]]] |
|
74 |
by fastforce |
|
75 |
qed |
|
76 |
with * show ?case by (auto) |
|
77 |
qed |
|
78 |
||
79 |
lemma sorted_from_radix_sort_step: |
|
67688 | 80 |
assumes "cols xss n" and "i < n" and "sorted_from (i+1) xss" |
81 |
shows "sorted_from i (sort_col i xss)" |
|
82 |
proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)]) |
|
83 |
show "sorted_col i (sort_col i xss)" by(simp add: sorted) |
|
68249
949d93804740
First step to remove nonstandard "[x <- xs. P]" syntax: only input
nipkow
parents:
68176
diff
changeset
|
84 |
fix x show "sorted_from (i+1) (filter (\<lambda>ys. ys ! i = x) (sort_col i xss))" |
67688 | 85 |
proof - |
86 |
from assms(3) |
|
87 |
have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)" |
|
88 |
by(rule sorted_filter) |
|
89 |
thus "sorted (map (drop (i+1)) (filter (\<lambda>ys. ys!i = x) (sort_col i xss)))" |
|
90 |
by (metis stable stable_sort_key_def) |
|
91 |
qed |
|
92 |
qed |
|
67612 | 93 |
|
94 |
lemma sorted_from_radix_sort: |
|
67688 | 95 |
"\<lbrakk> cols xss n; i \<le> n; sorted_from i xss \<rbrakk> \<Longrightarrow> sorted_from 0 (radix_sort i xss)" |
96 |
proof(induction i arbitrary: xss) |
|
97 |
case 0 thus ?case by simp |
|
98 |
next |
|
99 |
case (Suc i) |
|
100 |
thus ?case by(simp add: sorted_from_radix_sort_step cols_sort1) |
|
101 |
qed |
|
67612 | 102 |
|
67688 | 103 |
corollary sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)" |
67612 | 104 |
apply(frule sorted_from_radix_sort[OF _ le_refl]) |
68176 | 105 |
apply(auto simp add: cols_def sorted_iff_nth_mono) |
67612 | 106 |
done |
107 |
||
108 |
end |
|
67688 | 109 |
|
110 |
end |