author haftmann Sat, 22 May 2010 11:01:59 +0200 changeset 37077 3b247fa77c68 parent 37057 e70f9230c608 (current diff) parent 37076 4d57f872dc2c (diff) child 37086 3a7c2c949320
merged
```--- a/src/HOL/Library/Multiset.thy	Fri May 21 23:48:48 2010 +0200
+++ b/src/HOL/Library/Multiset.thy	Sat May 22 11:01:59 2010 +0200
@@ -826,7 +826,8 @@
This lemma shows which properties suffice to show that a function
@{text "f"} with @{text "f xs = ys"} behaves like sort.
*}
-lemma properties_for_sort:
+
+lemma (in linorder) properties_for_sort:
"multiset_of ys = multiset_of xs \<Longrightarrow> sorted ys \<Longrightarrow> sort xs = ys"
proof (induct xs arbitrary: ys)
case Nil then show ?case by simp```
```--- a/src/HOL/Library/Quicksort.thy	Fri May 21 23:48:48 2010 +0200
+++ b/src/HOL/Library/Quicksort.thy	Sat May 22 11:01:59 2010 +0200
@@ -2,7 +2,7 @@
*)

theory Quicksort
imports Main Multiset
@@ -12,22 +12,27 @@
begin

fun quicksort :: "'a list \<Rightarrow> 'a list" where
-"quicksort []     = []" |
-"quicksort (x#xs) = quicksort([y\<leftarrow>xs. ~ x\<le>y]) @ [x] @ quicksort([y\<leftarrow>xs. x\<le>y])"
+  "quicksort []     = []"
+| "quicksort (x#xs) = quicksort [y\<leftarrow>xs. \<not> x\<le>y] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"
+
+lemma [code]:
+  "quicksort []     = []"
+  "quicksort (x#xs) = quicksort [y\<leftarrow>xs. y<x] @ [x] @ quicksort [y\<leftarrow>xs. x\<le>y]"

lemma quicksort_permutes [simp]:
"multiset_of (quicksort xs) = multiset_of xs"
-by (induct xs rule: quicksort.induct) (auto simp: union_ac)
+  by (induct xs rule: quicksort.induct) (simp_all add: ac_simps)

lemma set_quicksort [simp]: "set (quicksort xs) = set xs"

-lemma sorted_quicksort: "sorted(quicksort xs)"
-apply (induct xs rule: quicksort.induct)
- apply simp
-apply (simp add:sorted_Cons sorted_append not_le less_imp_le)
-apply (metis leD le_cases le_less_trans)
-done
+lemma sorted_quicksort: "sorted (quicksort xs)"
+  by (induct xs rule: quicksort.induct) (auto simp add: sorted_Cons sorted_append not_le less_imp_le)
+
+theorem quicksort_sort [code_unfold]:
+  "sort = quicksort"
+  by (rule ext, rule properties_for_sort) (fact quicksort_permutes sorted_quicksort)+

end
```
```--- a/src/HOL/ex/MergeSort.thy	Fri May 21 23:48:48 2010 +0200
+++ b/src/HOL/ex/MergeSort.thy	Sat May 22 11:01:59 2010 +0200
@@ -6,7 +6,7 @@

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(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```