src/HOL/ex/MergeSort.thy

--- a/src/HOL/ex/MergeSort.thy	Fri Apr 22 15:10:42 2005 +0200
+++ b/src/HOL/ex/MergeSort.thy	Fri Apr 22 17:32:03 2005 +0200
@@ -2,22 +2,26 @@
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2002 TU Muenchen
-
-Merge sort
 *)
 
-theory MergeSort = Sorting:
+header{*Merge Sort*}
+
+theory MergeSort
+imports Sorting
+begin
 
 consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
 
 recdef merge "measure(%(xs,ys). size xs + size ys)"
-"merge(x#xs,y#ys) =
- (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
-"merge(xs,[]) = xs"
-"merge([],ys) = ys"
+    "merge(x#xs, y#ys) =
+         (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
+
+    "merge(xs,[]) = xs"
+
+    "merge([],ys) = ys"
 
 lemma multiset_of_merge[simp]:
- "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
+     "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
 apply(induct xs ys rule: merge.induct)
 apply (auto simp: union_ac)
 done
@@ -28,27 +32,25 @@
 done
 
 lemma sorted_merge[simp]:
- "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
+     "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 linorder_not_le order_less_le)
+apply(simp_all add: ball_Un linorder_not_le order_less_le)
 apply(blast intro: order_trans)
 done
 
 consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
 recdef msort "measure size"
-"msort [] = []"
-"msort [x] = [x]"
-"msort xs = merge(msort(take (size xs div 2) xs),
-                  msort(drop (size xs div 2) xs))"
+    "msort [] = []"
+    "msort [x] = [x]"
+    "msort xs = merge(msort(take (size xs div 2) xs),
+		      msort(drop (size xs div 2) xs))"
 
-lemma sorted_msort: "sorted op <= (msort xs)"
+theorem sorted_msort: "sorted (op \<le>) (msort xs)"
 by (induct xs rule: msort.induct) simp_all
 
-lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
+theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
 apply (induct xs rule: msort.induct)
-  apply simp
- apply simp
-apply simp
+  apply simp_all
 apply (subst union_commute)
 apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
 apply (simp add: union_ac)