<commit_before>(*  Title:      HOL/ex/MergeSort.thy
    Author:     <NAME>
    Copyright   2002 TU Muenchen
*)

header{*Merge Sort*}

theory MergeSort
imports Sorting
begin

context linorder
begin

fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "merge (x#xs) (y#ys) =
         (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
| "merge xs [] = xs"
| "merge [] ys = 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 set_merge[simp]: "set (merge xs ys) = set xs \<union> set ys"
apply(induct xs ys rule: merge.induct)
apply auto
done

lemma sorted_merge[simp]:
     "sorted (op \<le>) (merge xs ys) = (sorted (op \<le>) xs & sorted (op \<le>) ys)"
apply(induct xs ys rule: merge.induct)
apply(simp_all add: ball_Un not_le less_le)
apply(blast intro: order_trans)
done

fun msort :: "'a list \<Rightarrow> 'a list"
where
  "msort [] = []"
| "msort [x] = [x]"
| "msort xs = merge (msort (take (size xs div 2) xs))
                    (msort (drop (size xs div 2) xs))"

theorem sorted_msort: "sorted (op \<le>) (msort xs)"
by (induct xs rule: msort.induct) simp_all

theorem multiset_of_msort: "multiset_of (msort xs) = multiset_of xs"
apply (induct xs rule: msort.induct)
  apply simp_all
apply (metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)
done

end


end
<commit_msg>modernized sorting algorithms; quicksort implements sort<commit_after>(*  Title:      HOL/ex/MergeSort.thy
    Author:     <NAME>
    Copyright   2002 <NAME>
*)

header{*Merge Sort*}

theory MergeSort
imports Multiset
begin

context linorder
begin

fun merge :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
where
  "merge (x#xs) (y#ys) =
         (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)"
| "merge xs [] = xs"
| "merge [] ys = ys"

lemma multiset_of_merge [simp]:
  "multiset_of (merge xs ys) = multiset_of xs + multiset_of ys"
  by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)

lemma set_merge [simp]:
  "set (merge xs ys) = set xs \<union> set ys"
  by (induct xs ys rule: merge.induct) auto

lemma sorted_merge [simp]:
  "sorted (merge xs ys) \<longleftrightarrow> sorted xs \<and> sorted ys"
  by (induct xs ys rule: merge.induct) (auto simp add: ball_Un not_le less_le sorted_Cons)

fun msort :: "'a list \<Rightarrow> 'a list"
where
  "msort [] = []"
| "msort [x] = [x]"
| "msort xs = merge (msort (take (size xs div 2) xs))
                    (msort (drop (size xs div 2) xs))"

lemma sorted_msort:
  "sorted (msort xs)"
  by (induct xs rule: msort.induct) simp_all

lemma multiset_of_msort:
  "multiset_of (msort xs) = multiset_of xs"
  by (induct xs rule: msort.induct)
    (simp_all, metis append_take_drop_id drop_Suc_Cons multiset_of.simps(2) multiset_of_append take_Suc_Cons)

theorem msort_sort:
  "sort = msort"
  by (rule ext, rule properties_for_sort) (fact multiset_of_msort sorted_msort)+

end

end

{'fraction_non_alphanumeric': 0.12916939175931982, 'fraction_numerical': 0.004578155657292348, 'mean_word_length': 3.78716744913928, 'pattern_counts': {'":': 0, '<': 22, '<?xml version=': 0, '>': 22, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1648424', 'n_tokens_mistral': 1296, 'n_tokens_neox': 1186, 'n_words': 383}