# HG changeset patch
# User krauss
# Date 1233656188 -3600
# Node ID 1df0e5af40b9e3b8e90b1d8c99187ea2c8cbb35e
# Parent  2786b348c376d0c88e6de889827f49cbcf0df68c
mergesort example: recdef->fun, localized

diff -r 2786b348c376 -r 1df0e5af40b9 src/HOL/ex/MergeSort.thy
--- a/src/HOL/ex/MergeSort.thy	Tue Feb 03 11:16:28 2009 +0100
+++ b/src/HOL/ex/MergeSort.thy	Tue Feb 03 11:16:28 2009 +0100
@@ -10,40 +10,40 @@
 imports Sorting
 begin
 
-consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
+context linorder
+begin
 
-recdef merge "measure(%(xs,ys). size xs + size 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"
+fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
+where
+  "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
 
-lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
+lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
 apply(induct xs ys rule: merge.induct)
 apply auto
 done
 
 lemma sorted_merge[simp]:
-     "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) 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 not_le 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))"
+fun msort :: "'a list \<Rightarrow> 'a list"
+where
+  "msort [] = []"
+| "msort [x] = [x]"
+| "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
@@ -57,3 +57,6 @@
 done
 
 end
+
+
+end