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