src/HOL/ex/MergeSort.thy
changeset 15815 62854cac5410
parent 15732 faa48c5b1402
child 19860 6e44610bdd76
     1.1 --- a/src/HOL/ex/MergeSort.thy	Fri Apr 22 15:10:42 2005 +0200
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Fri Apr 22 17:32:03 2005 +0200
     1.3 @@ -2,22 +2,26 @@
     1.4      ID:         $Id$
     1.5      Author:     Tobias Nipkow
     1.6      Copyright   2002 TU Muenchen
     1.7 -
     1.8 -Merge sort
     1.9  *)
    1.10  
    1.11 -theory MergeSort = Sorting:
    1.12 +header{*Merge Sort*}
    1.13 +
    1.14 +theory MergeSort
    1.15 +imports Sorting
    1.16 +begin
    1.17  
    1.18  consts merge :: "('a::linorder)list * 'a list \<Rightarrow> 'a list"
    1.19  
    1.20  recdef merge "measure(%(xs,ys). size xs + size ys)"
    1.21 -"merge(x#xs,y#ys) =
    1.22 - (if x <= y then x # merge(xs,y#ys) else y # merge(x#xs,ys))"
    1.23 -"merge(xs,[]) = xs"
    1.24 -"merge([],ys) = ys"
    1.25 +    "merge(x#xs, y#ys) =
    1.26 +         (if x \<le> y then x # merge(xs, y#ys) else y # merge(x#xs, ys))"
    1.27 +
    1.28 +    "merge(xs,[]) = xs"
    1.29 +
    1.30 +    "merge([],ys) = ys"
    1.31  
    1.32  lemma multiset_of_merge[simp]:
    1.33 - "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
    1.34 +     "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
    1.35  apply(induct xs ys rule: merge.induct)
    1.36  apply (auto simp: union_ac)
    1.37  done
    1.38 @@ -28,27 +32,25 @@
    1.39  done
    1.40  
    1.41  lemma sorted_merge[simp]:
    1.42 - "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
    1.43 +     "sorted (op \<le>) (merge(xs,ys)) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
    1.44  apply(induct xs ys rule: merge.induct)
    1.45 -apply(simp_all add:ball_Un linorder_not_le order_less_le)
    1.46 +apply(simp_all add: ball_Un linorder_not_le order_less_le)
    1.47  apply(blast intro: order_trans)
    1.48  done
    1.49  
    1.50  consts msort :: "('a::linorder) list \<Rightarrow> 'a list"
    1.51  recdef msort "measure size"
    1.52 -"msort [] = []"
    1.53 -"msort [x] = [x]"
    1.54 -"msort xs = merge(msort(take (size xs div 2) xs),
    1.55 -                  msort(drop (size xs div 2) xs))"
    1.56 +    "msort [] = []"
    1.57 +    "msort [x] = [x]"
    1.58 +    "msort xs = merge(msort(take (size xs div 2) xs),
    1.59 +		      msort(drop (size xs div 2) xs))"
    1.60  
    1.61 -lemma sorted_msort: "sorted op <= (msort xs)"
    1.62 +theorem sorted_msort: "sorted (op \<le>) (msort xs)"
    1.63  by (induct xs rule: msort.induct) simp_all
    1.64  
    1.65 -lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    1.66 +theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    1.67  apply (induct xs rule: msort.induct)
    1.68 -  apply simp
    1.69 - apply simp
    1.70 -apply simp
    1.71 +  apply simp_all
    1.72  apply (subst union_commute)
    1.73  apply (simp del:multiset_of_append add:multiset_of_append[symmetric] union_assoc)
    1.74  apply (simp add: union_ac)