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.7 -
1.8 -Merge sort
1.9  *)
1.10
1.11 -theory MergeSort = Sorting:
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.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)