# HG changeset patch
# User nipkow
# Date 1519369376 -3600
# Node ID b39f5bb7d4228e25c595f6c33b74d7c25c558d22
# Parent  34e0e0d5ea7cfa2747d0deaba3034af44cd875d8
simplified Radix_Sort

diff -r 34e0e0d5ea7c -r b39f5bb7d422 src/HOL/ex/Radix_Sort.thy
--- a/src/HOL/ex/Radix_Sort.thy	Thu Feb 22 20:05:30 2018 +0100
+++ b/src/HOL/ex/Radix_Sort.thy	Fri Feb 23 08:02:56 2018 +0100
@@ -2,27 +2,42 @@
 
 theory Radix_Sort
 imports
-  "HOL-Library.Multiset" 
   "HOL-Library.List_lexord" 
   "HOL-Library.Sublist" 
+  "HOL-Library.Multiset" 
+begin
+
+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 stable: "stable_sort_key sort1"
 begin
 
-fun radix_sort :: "nat \<Rightarrow> 'a::linorder list list \<Rightarrow> 'a list list" where
+lemma set_sort1[simp]: "set(sort1 f xs) = set xs"
+by (metis mset set_mset_mset)
+
+abbreviation "sort_col i xss \<equiv> sort1 (\<lambda>xs. xs ! i) xss"
+abbreviation "sorted_col i xss \<equiv> sorted (map (\<lambda>xs. xs ! i) xss)"
+
+fun radix_sort :: "nat \<Rightarrow> 'a list list \<Rightarrow> 'a list list" where
 "radix_sort 0 xss = xss" |
-"radix_sort (Suc n) xss = radix_sort n (sort_key (\<lambda>xs. xs ! n) 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 \<equiv> sorted (map (drop i) xss)"
 
-definition "cols xss k = (\<forall>xs \<in> set xss. length xs = k)"
+definition "cols xss n = (\<forall>xs \<in> set xss. length xs = n)"
 
-lemma mset_radix_sort: "mset (radix_sort k xss) = mset xss"
-by(induction k arbitrary: xss) (auto)
-
-lemma cols_sort_key: "cols xss n \<Longrightarrow> cols (sort_key f xss) n"
+lemma cols_sort1: "cols xss n \<Longrightarrow> cols (sort1 f xss) n"
 by(simp add: cols_def)
 
-lemma sorted_from_Suc2: "\<lbrakk> cols xss n; i < n;
-  sorted (map (\<lambda>xs. xs!i) xss);  \<forall>xs \<in> set xss. sorted_from (i+1) [ys \<leftarrow> xss. ys!i = xs!i] \<rbrakk>
+lemma sorted_from_Suc2:
+  "\<lbrakk> 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 ?case by simp
@@ -36,7 +51,8 @@
   proof -
     have "drop i xs1 = xs1!i # drop (i+1) xs1"
       using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs1)
-    also have "\<dots> \<le> xs2!i # drop (i+1) xs2" using "3.prems"(3,4) by(auto)
+    also have "\<dots> \<le> xs2!i # drop (i+1) xs2"
+      using "3.prems"(3) "3.prems"(4)[of "xs2!i"] by(auto)
     also have "\<dots> = drop i xs2"
       using \<open>i < n\<close> by (simp add: Cons_nth_drop_Suc lxs2)
     finally show ?thesis .
@@ -44,8 +60,8 @@
   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 (map (\<lambda>xs. xs ! i) (xs2 # xss))" using "3.prems"(3) by simp
-    show "\<forall>xs\<in>set (xs2 # xss). sorted_from (i+1) [ys\<leftarrow>xs2 # xss . ys ! i = xs ! i]"
+    show "sorted_col i (xs2 # xss)" using "3.prems"(3) by simp
+    show "\<And>x. sorted_from (i+1) [ys\<leftarrow>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.order.refl]]]]
       by fastforce
@@ -54,21 +70,34 @@
 qed
 
 lemma sorted_from_radix_sort_step:
-  "\<lbrakk> cols xss n; i < n; sorted_from (Suc i) xss \<rbrakk> \<Longrightarrow> sorted_from i (sort_key (\<lambda>xs. xs ! i) xss)"
-apply (rule sorted_from_Suc2)
-apply (auto simp add: sort_key_stable sorted_filter cols_def)
-done
+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 \<leftarrow> sort_col i xss . ys ! i = x]"
+  proof -
+    from assms(3)
+    have "sorted_from (i+1) (filter (\<lambda>ys. ys!i = x) xss)"
+      by(rule sorted_filter)
+    thus "sorted (map (drop (i+1)) (filter (\<lambda>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 \<Longrightarrow> i \<le> n \<Longrightarrow> sorted_from i xss \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
-apply(induction i arbitrary: xss)
- apply(simp add: sort_key_const)
-apply(simp add: sorted_from_radix_sort_step cols_sort_key)
-done
+  "\<lbrakk> cols xss n;  i \<le> n;  sorted_from i xss \<rbrakk> \<Longrightarrow> sorted_from 0 (radix_sort i xss)"
+proof(induction i arbitrary: xss)
+  case 0 thus ?case by simp
+next
+  case (Suc i)
+  thus ?case by(simp add: sorted_from_radix_sort_step cols_sort1)
+qed
 
-lemma sorted_radix_sort: "cols xss n \<Longrightarrow> sorted (radix_sort n xss)"
+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)
 done
 
 end
+
+end