Theory Mergesort_Complexity
theory Mergesort_Complexity
imports
Efficient_Sort
Complex_Main
begin
lemma log2_mono:
"x > 0 ⟹ x ≤ y ⟹ log 2 x ≤ log 2 y"
by auto
section ‹Counting the Number of Comparisons›
context
fixes key :: "'a ⇒ 'k::linorder"
begin
fun c_merge :: "'a list ⇒ 'a list ⇒ nat"
where
"c_merge (x # xs) (y # ys) =
1 + (if key y < key x then c_merge (x # xs) ys else c_merge xs (y # ys))"
| "c_merge [] ys = 0"
| "c_merge xs [] = 0"
fun c_merge_pairs :: "'a list list ⇒ nat"
where
"c_merge_pairs (xs # ys # zss) = c_merge xs ys + c_merge_pairs zss"
| "c_merge_pairs [] = 0"
| "c_merge_pairs [x] = 0"
fun c_merge_all :: "'a list list ⇒ nat"
where
"c_merge_all [] = 0"
| "c_merge_all [x] = 0"
| "c_merge_all xss = c_merge_pairs xss + c_merge_all (merge_pairs key xss)"
fun c_sequences :: "'a list ⇒ nat"
and c_asc :: "'a ⇒ 'a list ⇒ nat"
and c_desc :: "'a ⇒ 'a list ⇒ nat"
where
"c_sequences (x # y # zs) = 1 + (if key y < key x then c_desc y zs else c_asc y zs)"
| "c_sequences [] = 0"
| "c_sequences [x] = 0"
| "c_asc x (y # ys) = 1 + (if ¬ key y < key x then c_asc y ys else c_sequences (y # ys))"
| "c_asc x [] = 0"
| "c_desc x (y # ys) = 1 + (if key y < key x then c_desc y ys else c_sequences (y # ys))"
| "c_desc x [] = 0"
fun c_msort :: "'a list ⇒ nat"
where
"c_msort xs = c_sequences xs + c_merge_all (sequences key xs)"
lemma c_merge:
"c_merge xs ys ≤ length xs + length ys"
by (induct xs ys rule: c_merge.induct) simp_all
lemma c_merge_pairs:
"c_merge_pairs xss ≤ length (concat xss)"
proof (induct xss rule: c_merge_pairs.induct)
case (1 xs ys zss)
then show ?case using c_merge [of xs ys] by simp
qed simp_all
lemma c_merge_all:
"c_merge_all xss ≤ length (concat xss) * ⌈log 2 (length xss)⌉"
proof (induction xss rule: c_merge_all.induct)
case (3 xs ys zss)
let ?clen = "λxs. length (concat xs)"
let ?xss = "xs # ys # zss"
let ?xss2 = "merge_pairs key ?xss"
have *: "⌈log 2 (real n + 2)⌉ = ⌈log 2 (Suc n div 2 + 1)⌉ + 1" for n :: nat
using ceiling_log2_div2 [of "n + 2"] by (simp add: algebra_simps)
have "c_merge_all ?xss = c_merge_pairs ?xss + c_merge_all ?xss2" by simp
also have "… ≤ ?clen ?xss + c_merge_all ?xss2"
using c_merge [of xs ys] and c_merge_pairs [of ?xss] by auto
also have "… ≤ ?clen ?xss + ?clen ?xss2 * ⌈log 2 (length ?xss2)⌉"
using "3.IH" by simp
also have "… ≤ ?clen ?xss * ⌈log 2 (length ?xss)⌉"
by (auto simp: * algebra_simps)
finally show ?case by simp
qed simp_all
lemma
shows c_sequences: "c_sequences xs ≤ length xs - 1"
and c_asc: "c_asc x ys ≤ length ys"
and c_desc: "c_desc x ys ≤ length ys"
by (induct xs and x ys and x ys rule: c_sequences_c_asc_c_desc.induct) simp_all
lemma
shows length_concat_sequences [simp]: "length (concat (sequences key xs)) = length xs"
and length_concat_asc: "ascP f ⟹ length (concat (asc key a f ys)) = 1 + length (f []) + length ys"
and length_concat_desc: "length (concat (desc key a xs ys)) = 1 + length xs + length ys"
by (induct xs and a f ys and a xs ys rule: sequences_asc_desc.induct)
(auto simp: ascP_f_singleton)
lemma
shows sequences_ne: "xs ≠ [] ⟹ sequences key xs ≠ []"
and asc_ne: "ascP f ⟹ asc key a f ys ≠ []"
and desc_ne: "desc key a xs ys ≠ []"
by (induct xs and a f ys and a xs ys taking: key rule: sequences_asc_desc.induct) simp_all
lemma c_msort:
assumes [simp]: "length xs = n"
shows "c_msort xs ≤ n + n * ⌈log 2 n⌉"
proof -
have [simp]: "xs = [] ⟷ length xs = 0" by blast
have "int (c_merge_all (sequences key xs)) ≤ int n * ⌈log 2 (length (sequences key xs))⌉"
using c_merge_all [of "sequences key xs"] by simp
also have "… ≤ int n * ⌈log 2 n⌉"
using length_sequences [of key xs]
by (cases n) (auto intro!: sequences_ne mult_mono ceiling_mono log2_mono)
finally have "int (c_merge_all (sequences key xs)) ≤ int n * ⌈log 2 n⌉" .
moreover have "c_sequences xs ≤ n" using c_sequences [of xs] by auto
ultimately show ?thesis by (auto intro: add_mono)
qed
end
end