theory Radix_Sort imports "HOL-Library.List_Lexorder" "HOL-Library.Sublist" "HOL-Library.Multiset" begin
text\<open>The \<open>Radix_Sort\<close> locale provides a sorting function \<open>radix_sort\<close> that sorts
lists of lists. It is parameterized by a sorting function\<open>sort1 f\<close> that also sorts
lists of lists, but only w.r.t. the column selected by\<open>f\<close>.
Working with lists, \<open>f\<close> is instantiated with \<^term>\<open>\<lambda>xs. xs ! n\<close> to select the \<open>n\<close>-th element.
A more efficient implementation would sort lists of arrays because arrays support
constant time access to every element.\<close>
locale Radix_Sort = fixes sort1 :: "('a list \ 'a::linorder) \ 'a list list \ 'a list list" assumes sorted: "sorted (map f (sort1 f xss))" assumes mset: "mset (sort1 f xss) = mset xss" assumes stable: "stable_sort_key sort1" begin
lemma set_sort1[simp]: "set(sort1 f xss) = set xss" by (metis mset set_mset_mset)
fun radix_sort :: "nat \ 'a list list \ 'a list list" where "radix_sort 0 xss = xss" | "radix_sort (Suc i) xss = radix_sort i (sort_col i xss)"
lemma mset_radix_sort: "mset (radix_sort i xss) = mset xss" by(induction i arbitrary: xss) (auto simp: mset)
abbreviation"sorted_from i xss \ sorted (map (drop i) xss)"
definition"cols xss n = (\xs \ set xss. length xs = n)"
lemma cols_sort1: "cols xss n \ cols (sort1 f xss) n" by(simp add: cols_def)
lemma sorted_from_Suc2: "\ cols xss n; i < n;
sorted_col i xss; \<And>x. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = x] \<rbrakk> \<Longrightarrow> sorted_from i xss" proof(induction xss rule: induct_list012) case 1 show ?caseby simp next case 2 show ?caseby simp next case (3 xs1 xs2 xss) have lxs1: "length xs1 = n"and lxs2: "length xs2 = n" using"3.prems"(1) by(auto simp: cols_def) have *: "drop i xs1 \ drop i xs2" proof - have"drop i xs1 = xs1!i # drop (i+1) xs1" using\<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1) alsohave"\ \ xs2!i # drop (i+1) xs2" using"3.prems"(3) "3.prems"(4)[of "xs2!i"] by(auto) alsohave"\ = drop i xs2" using\<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2) finallyshow ?thesis . qed have"sorted_from i (xs2 # xss)" proof(rule "3.IH"[OF _ "3.prems"(2)]) show"cols (xs2 # xss) n"using"3.prems"(1) by(simp add: cols_def) show"sorted_col i (xs2 # xss)"using"3.prems"(3) by simp show"\x. sorted_from (i+1) [ys\xs2 # xss . ys ! i = x]" using"3.prems"(4)
sorted_antimono_suffix[OF map_mono_suffix[OF filter_mono_suffix[OF suffix_ConsI[OF suffix_order.refl]]]] by fastforce qed with * show ?caseby (auto) qed
lemma sorted_from_radix_sort_step: assumes"cols xss n"and"i < n"and"sorted_from (i+1) xss" shows"sorted_from i (sort_col i xss)" proof (rule sorted_from_Suc2[OF cols_sort1[OF assms(1)] assms(2)]) show"sorted_col i (sort_col i xss)"by(simp add: sorted) fix x show"sorted_from (i+1) [ys \ sort_col i xss . ys ! i = x]" proof - from assms(3) have"sorted_from (i+1) (filter (\ys. ys!i = x) xss)" by(rule sorted_filter) thus"sorted (map (drop (i+1)) (filter (\ys. ys!i = x) (sort_col i xss)))" by (metis stable stable_sort_key_def) qed qed
lemma sorted_from_radix_sort: "\ cols xss n; i \ n; sorted_from i xss \ \ sorted_from 0 (radix_sort i xss)" proof(induction i arbitrary: xss) case 0 thus ?caseby simp next case (Suc i) thus ?caseby(simp add: sorted_from_radix_sort_step cols_sort1) qed
corollary sorted_radix_sort: "cols xss n \ sorted (radix_sort n xss)" apply(frule sorted_from_radix_sort[OF _ le_refl]) apply(auto simp add: cols_def sorted_iff_nth_mono) done
end
end
¤ Dauer der Verarbeitung: 0.13 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
