src/HOL/ex/MergeSort.thy
changeset 29780 1df0e5af40b9
parent 19872 1b53b196f85f
child 30661 54858c8ad226
     1.1 --- a/src/HOL/ex/MergeSort.thy	Tue Feb 03 11:16:28 2009 +0100
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Tue Feb 03 11:16:28 2009 +0100
     1.3 @@ -10,40 +10,40 @@
     1.4  imports Sorting
     1.5  begin
     1.6  
     1.7 -consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
     1.8 +context linorder
     1.9 +begin
    1.10  
    1.11 -recdef merge "measure(%(xs,ys). size xs + size ys)"
    1.12 -    "merge(x#xs, y#ys) =
    1.13 -         (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
    1.14 -
    1.15 -    "merge(xs,[]) = xs"
    1.16 -
    1.17 -    "merge([],ys) = ys"
    1.18 +fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
    1.19 +where
    1.20 +  "merge (x#xs) (y#ys) =
    1.21 +         (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
    1.22 +| "merge xs [] = xs"
    1.23 +| "merge [] ys = ys"
    1.24  
    1.25  lemma multiset_of_merge[simp]:
    1.26 -     "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
    1.27 +     "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
    1.28  apply(induct xs ys rule: merge.induct)
    1.29  apply (auto simp: union_ac)
    1.30  done
    1.31  
    1.32 -lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
    1.33 +lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
    1.34  apply(induct xs ys rule: merge.induct)
    1.35  apply auto
    1.36  done
    1.37  
    1.38  lemma sorted_merge[simp]:
    1.39 -     "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
    1.40 +     "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
    1.41  apply(induct xs ys rule: merge.induct)
    1.42 -apply(simp_all add: ball_Un linorder_not_le order_less_le)
    1.43 +apply(simp_all add: ball_Un not_le less_le)
    1.44  apply(blast intro: order_trans)
    1.45  done
    1.46  
    1.47 -consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
    1.48 -recdef msort "measure size"
    1.49 -    "msort [] = []"
    1.50 -    "msort [x] = [x]"
    1.51 -    "msort xs = merge(msort(take (size xs div 2) xs),
    1.52 -		      msort(drop (size xs div 2) xs))"
    1.53 +fun msort :: "'a list \<Rightarrow> 'a list"
    1.54 +where
    1.55 +  "msort [] = []"
    1.56 +| "msort [x] = [x]"
    1.57 +| "msort xs = merge (msort (take (size xs div 2) xs))
    1.58 +	                  (msort (drop (size xs div 2) xs))"
    1.59  
    1.60  theorem sorted_msort: "sorted (op \<le>) (msort xs)"
    1.61  by (induct xs rule: msort.induct) simp_all
    1.62 @@ -57,3 +57,6 @@
    1.63  done
    1.64  
    1.65  end
    1.66 +
    1.67 +
    1.68 +end