# HG changeset patch
# User haftmann
# Date 1274515982 -7200
# Node ID 4d57f872dc2cd73dce1c55dbb9a450abee074927
# Parent  a680ce27aa562fbe1f18962ee725a1dbc04e1bf1
modernized sorting algorithms; quicksort implements sort

diff -r a680ce27aa56 -r 4d57f872dc2c src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Sat May 22 10:12:50 2010 +0200
+++ b/src/HOL/ex/MergeSort.thy	Sat May 22 10:13:02 2010 +0200
@@ -6,7 +6,7 @@
 header{*Merge Sort*}
 
 theory MergeSort
-imports Sorting
+imports Multiset
 begin
 
 context linorder
@@ -19,23 +19,17 @@
 | "merge xs [] = xs"
 | "merge [] ys = ys"
 
-lemma multiset_of_merge[simp]:
-     "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
-apply(induct xs ys rule: merge.induct)
-apply (auto simp: union_ac)
-done
+lemma multiset_of_merge [simp]:
+  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
+  by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
 
-lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
-apply(induct xs ys rule: merge.induct)
-apply auto
-done
+lemma set_merge [simp]:
+  "set (merge xs ys) = set xs \<union> set ys"
+  by (induct xs ys rule: merge.induct) auto
 
-lemma sorted_merge[simp]:
-     "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
-apply(induct xs ys rule: merge.induct)
-apply(simp_all add: ball_Un not_le less_le)
-apply(blast intro: order_trans)
-done
+lemma sorted_merge [simp]:
+  "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
+  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)
 
 fun msort :: "'a list \<Rightarrow> 'a list"
 where
@@ -44,16 +38,19 @@
 | "msort xs = merge (msort (take (size xs div 2) xs))
                     (msort (drop (size xs div 2) xs))"
 
-theorem sorted_msort: "sorted (op \<le>) (msort xs)"
-by (induct xs rule: msort.induct) simp_all
+lemma sorted_msort:
+  "sorted (msort xs)"
+  by (induct xs rule: msort.induct) simp_all
 
-theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
-apply (induct xs rule: msort.induct)
-  apply simp_all
-apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
-done
+lemma multiset_of_msort:
+  "multiset_of (msort xs) = multiset_of xs"
+  by (induct xs rule: msort.induct)
+    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
+
+theorem msort_sort:
+  "sort = msort"
+  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
 
 end
 
-
 end