more sorted cleaning
authornipkow
Mon May 14 18:19:35 2018 +0200 (12 months ago)
changeset 681763e4af46a6f6a
parent 68175 e0bd5089eabf
child 68185 c80b0a35eb54
child 68186 56fcf7e980e3
more sorted cleaning
src/HOL/List.thy
src/HOL/ex/Radix_Sort.thy
     1.1 --- a/src/HOL/List.thy	Mon May 14 15:37:26 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Mon May 14 18:19:35 2018 +0200
     1.3 @@ -5056,15 +5056,7 @@
     1.4  using sorted_nth_mono[ of "rev xs" "length xs - j - 1" "length xs - i - 1"]
     1.5        rev_nth[of "length xs - i - 1" "xs"] rev_nth[of "length xs - j - 1" "xs"]
     1.6  by auto
     1.7 -(*
     1.8 -lemma sorted_nth_monoI:
     1.9 -  "(\<And> i j. \<lbrakk> i \<le> j ; j < length xs \<rbrakk> \<Longrightarrow> xs ! i \<le> xs ! j) \<Longrightarrow> sorted xs"
    1.10 -by (simp add: sorted_iff_nth_less)
    1.11 -
    1.12 -lemma sorted_equals_nth_mono:
    1.13 -  "sorted xs = (\<forall>j < length xs. \<forall>i \<le> j. xs ! i \<le> xs ! j)"
    1.14 -by (auto simp: sorted_iff_nth_less nat_less_le)
    1.15 -*)
    1.16 +
    1.17  lemma sorted_map_remove1:
    1.18    "sorted (map f xs) \<Longrightarrow> sorted (map f (remove1 x xs))"
    1.19  by (induct xs) (auto)
     2.1 --- a/src/HOL/ex/Radix_Sort.thy	Mon May 14 15:37:26 2018 +0200
     2.2 +++ b/src/HOL/ex/Radix_Sort.thy	Mon May 14 18:19:35 2018 +0200
     2.3 @@ -7,14 +7,21 @@
     2.4    "HOL-Library.Multiset" 
     2.5  begin
     2.6  
     2.7 +text \<open>The \<open>Radix_Sort\<close> locale provides a sorting function \<open>radix_sort\<close> that sorts
     2.8 +lists of lists. It is parameterized by a sorting function \<open>sort1 f\<close> that also sorts
     2.9 +lists of lists, but only w.r.t. the column selected by \<open>f\<close>.
    2.10 +Working with lists, \<open>f\<close> is instantiated with @{term"\<lambda>xs. xs ! n"} to select the \<open>n\<close>-th element.
    2.11 +A more efficient implementation would sort lists of arrays because arrays support
    2.12 +constant time access to every element.\<close>
    2.13 +
    2.14  locale Radix_Sort =
    2.15  fixes sort1 :: "('a list \<Rightarrow> 'a::linorder) \<Rightarrow> 'a list list \<Rightarrow> 'a list list"
    2.16 -assumes sorted: "sorted (map f (sort1 f xs))"
    2.17 -assumes mset: "mset (sort1 f xs) = mset xs"
    2.18 +assumes sorted: "sorted (map f (sort1 f xss))"
    2.19 +assumes mset: "mset (sort1 f xss) = mset xss"
    2.20  assumes stable: "stable_sort_key sort1"
    2.21  begin
    2.22  
    2.23 -lemma set_sort1[simp]: "set(sort1 f xs) = set xs"
    2.24 +lemma set_sort1[simp]: "set(sort1 f xss) = set xss"
    2.25  by (metis mset set_mset_mset)
    2.26  
    2.27  abbreviation "sort_col i xss \<equiv> sort1 (\<lambda>xs. xs ! i) xss"
    2.28 @@ -95,7 +102,7 @@
    2.29  
    2.30  corollary sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
    2.31  apply(frule sorted_from_radix_sort[OF _ le_refl])
    2.32 - apply(auto simp add: cols_def sorted_equals_nth_mono)
    2.33 + apply(auto simp add: cols_def sorted_iff_nth_mono)
    2.34  done
    2.35  
    2.36  end