# HG changeset patch
# User nipkow
# Date 1023089813 -7200
# Node ID 3cc108872aca78edf8c54c14f8a2780acf1637ac
# Parent  7618f289c9c12da809c626016c718c03384c681d
*** empty log message ***

diff -r 7618f289c9c1 -r 3cc108872aca src/HOL/ex/MergeSort.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/MergeSort.thy	Mon Jun 03 09:36:53 2002 +0200
@@ -0,0 +1,53 @@
+(*  Title:      HOL/ex/Merge.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow
+    Copyright   2002 TU Muenchen
+
+Merge sort
+*)
+
+theory MergeSort = Sorting:
+
+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"
+
+lemma [simp]: "multiset(merge(xs,ys)) x = multiset xs x + multiset ys x"
+apply(induct xs ys rule: merge.induct)
+apply auto
+done
+
+lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
+apply(induct xs ys rule: merge.induct)
+apply auto
+done
+
+lemma [simp]:
+ "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
+apply(induct xs ys rule: merge.induct)
+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))"
+
+lemma "sorted op <= (msort xs)"
+by (induct xs rule: msort.induct) simp_all
+
+lemma "multiset(msort xs) x = multiset xs x"
+apply (induct xs rule: msort.induct)
+  apply simp
+ apply simp
+apply (simp del:multiset_append add:multiset_append[symmetric])
+done
+
+end