src/HOL/ex/MergeSort.thy
 changeset 15732 faa48c5b1402 parent 15631 cbee04ce413b child 15815 62854cac5410
```     1.1 --- a/src/HOL/ex/MergeSort.thy	Thu Apr 14 17:57:04 2005 +0200
1.2 +++ b/src/HOL/ex/MergeSort.thy	Thu Apr 14 17:57:23 2005 +0200
1.3 @@ -16,17 +16,18 @@
1.4  "merge(xs,[]) = xs"
1.5  "merge([],ys) = ys"
1.6
1.7 -lemma [simp]: "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
1.8 +lemma multiset_of_merge[simp]:
1.9 + "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
1.10  apply(induct xs ys rule: merge.induct)
1.11  apply (auto simp: union_ac)
1.12  done
1.13
1.14 -lemma [simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
1.15 +lemma set_merge[simp]: "set(merge(xs,ys)) = set xs \<union> set ys"
1.16  apply(induct xs ys rule: merge.induct)
1.17  apply auto
1.18  done
1.19
1.20 -lemma [simp]:
1.21 +lemma sorted_merge[simp]:
1.22   "sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
1.23  apply(induct xs ys rule: merge.induct)
1.24  apply(simp_all add:ball_Un linorder_not_le order_less_le)
1.25 @@ -40,10 +41,10 @@
1.26  "msort xs = merge(msort(take (size xs div 2) xs),
1.27                    msort(drop (size xs div 2) xs))"
1.28
1.29 -lemma "sorted op <= (msort xs)"
1.30 +lemma sorted_msort: "sorted op <= (msort xs)"
1.31  by (induct xs rule: msort.induct) simp_all
1.32
1.33 -lemma "multiset_of (msort xs) = multiset_of xs"
1.34 +lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
1.35  apply (induct xs rule: msort.induct)
1.36    apply simp
1.37   apply simp
```