--- a/src/HOL/ex/MergeSort.thy Thu Apr 14 17:57:04 2005 +0200
+++ b/src/HOL/ex/MergeSort.thy Thu Apr 14 17:57:23 2005 +0200
@@ -16,17 +16,18 @@
"merge(xs,[]) = xs"
"merge([],ys) = ys"
-lemma [simp]: "multiset_of (merge(xs,ys)) = multiset_of xs + multiset_of ys"
+lemma multiset_of_merge[simp]:
+ "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 [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 [simp]:
+lemma sorted_merge[simp]:
"sorted (op <=) (merge(xs,ys)) = (sorted (op <=) xs & sorted (op <=) ys)"
apply(induct xs ys rule: merge.induct)
apply(simp_all add:ball_Un linorder_not_le order_less_le)
@@ -40,10 +41,10 @@
"msort xs = merge(msort(take (size xs div 2) xs),
msort(drop (size xs div 2) xs))"
-lemma "sorted op <= (msort xs)"
+lemma sorted_msort: "sorted op <= (msort xs)"
by (induct xs rule: msort.induct) simp_all
-lemma "multiset_of (msort xs) = multiset_of xs"
+lemma multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
apply (induct xs rule: msort.induct)
apply simp
apply simp