modernized sorting algorithms; quicksort implements sort
authorhaftmann
Sat May 22 10:13:02 2010 +0200 (2010-05-22)
changeset 370764d57f872dc2c
parent 37075 a680ce27aa56
child 37077 3b247fa77c68
modernized sorting algorithms; quicksort implements sort
src/HOL/ex/MergeSort.thy
     1.1 --- a/src/HOL/ex/MergeSort.thy	Sat May 22 10:12:50 2010 +0200
     1.2 +++ b/src/HOL/ex/MergeSort.thy	Sat May 22 10:13:02 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header{*Merge Sort*}
     1.5  
     1.6  theory MergeSort
     1.7 -imports Sorting
     1.8 +imports Multiset
     1.9  begin
    1.10  
    1.11  context linorder
    1.12 @@ -19,23 +19,17 @@
    1.13  | "merge xs [] = xs"
    1.14  | "merge [] ys = ys"
    1.15  
    1.16 -lemma multiset_of_merge[simp]:
    1.17 -     "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
    1.18 -apply(induct xs ys rule: merge.induct)
    1.19 -apply (auto simp: union_ac)
    1.20 -done
    1.21 +lemma multiset_of_merge [simp]:
    1.22 +  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
    1.23 +  by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
    1.24  
    1.25 -lemma set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
    1.26 -apply(induct xs ys rule: merge.induct)
    1.27 -apply auto
    1.28 -done
    1.29 +lemma set_merge [simp]:
    1.30 +  "set (merge xs ys) = set xs \<union> set ys"
    1.31 +  by (induct xs ys rule: merge.induct) auto
    1.32  
    1.33 -lemma sorted_merge[simp]:
    1.34 -     "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
    1.35 -apply(induct xs ys rule: merge.induct)
    1.36 -apply(simp_all add: ball_Un not_le less_le)
    1.37 -apply(blast intro: order_trans)
    1.38 -done
    1.39 +lemma sorted_merge [simp]:
    1.40 +  "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
    1.41 +  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)
    1.42  
    1.43  fun msort :: "'a list \<Rightarrow> 'a list"
    1.44  where
    1.45 @@ -44,16 +38,19 @@
    1.46  | "msort xs = merge (msort (take (size xs div 2) xs))
    1.47                      (msort (drop (size xs div 2) xs))"
    1.48  
    1.49 -theorem sorted_msort: "sorted (op \<le>) (msort xs)"
    1.50 -by (induct xs rule: msort.induct) simp_all
    1.51 +lemma sorted_msort:
    1.52 +  "sorted (msort xs)"
    1.53 +  by (induct xs rule: msort.induct) simp_all
    1.54  
    1.55 -theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
    1.56 -apply (induct xs rule: msort.induct)
    1.57 -  apply simp_all
    1.58 -apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
    1.59 -done
    1.60 +lemma multiset_of_msort:
    1.61 +  "multiset_of (msort xs) = multiset_of xs"
    1.62 +  by (induct xs rule: msort.induct)
    1.63 +    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
    1.64 +
    1.65 +theorem msort_sort:
    1.66 +  "sort = msort"
    1.67 +  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+
    1.68  
    1.69  end
    1.70  
    1.71 -
    1.72  end