# HG changeset patch
# User nipkow
# Date 1526314775 -7200
# Node ID 3e4af46a6f6aaa903aff33ae6ca83825d74cca2d
# Parent  e0bd5089eabf244cbeec92abcbc21dc14486eb73
more sorted cleaning

diff -r e0bd5089eabf -r 3e4af46a6f6a src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 14 15:37:26 2018 +0200
+++ b/src/HOL/List.thy	Mon May 14 18:19:35 2018 +0200
@@ -5056,15 +5056,7 @@
 using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
       rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
 by auto
-(*
-lemma sorted_nth_monoI:
-  "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
-by (simp add: sorted_iff_nth_less)
-
-lemma sorted_equals_nth_mono:
-  "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
-by (auto simp: sorted_iff_nth_less nat_less_le)
-*)
+
 lemma sorted_map_remove1:
   "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
 by (induct xs) (auto)
diff -r e0bd5089eabf -r 3e4af46a6f6a src/HOL/ex/Radix_Sort.thy
--- a/src/HOL/ex/Radix_Sort.thy	Mon May 14 15:37:26 2018 +0200
+++ b/src/HOL/ex/Radix_Sort.thy	Mon May 14 18:19:35 2018 +0200
@@ -7,14 +7,21 @@
   "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"\<lambda>xs. xs ! n"} 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 \<Rightarrow> 'a::linorder) \<Rightarrow> 'a list list \<Rightarrow> 'a list list"
-assumes sorted: "sorted (map f (sort1 f xs))"
-assumes mset: "mset (sort1 f xs) = mset xs"
+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 xs) = set xs"
+lemma set_sort1[simp]: "set(sort1 f xss) = set xss"
 by (metis mset set_mset_mset)
 
 abbreviation "sort_col i xss \<equiv> sort1 (\<lambda>xs. xs ! i) xss"
@@ -95,7 +102,7 @@
 
 corollary sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
 apply(frule sorted_from_radix_sort[OF _ le_refl])
- apply(auto simp add: cols_def sorted_equals_nth_mono)
+ apply(auto simp add: cols_def sorted_iff_nth_mono)
 done
 
 end