1(* Author: Tobias Nipkow *) 2 3theory Sorting 4imports 5 Complex_Main 6 "HOL-Library.Multiset" 7begin 8 9hide_const List.insort 10 11declare Let_def [simp] 12 13 14subsection "Insertion Sort" 15 16fun insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where 17"insort x [] = [x]" | 18"insort x (y#ys) = 19 (if x \<le> y then x#y#ys else y#(insort x ys))" 20 21fun isort :: "'a::linorder list \<Rightarrow> 'a list" where 22"isort [] = []" | 23"isort (x#xs) = insort x (isort xs)" 24 25 26subsubsection "Functional Correctness" 27 28lemma mset_insort: "mset (insort x xs) = add_mset x (mset xs)" 29apply(induction xs) 30apply auto 31done 32 33lemma mset_isort: "mset (isort xs) = mset xs" 34apply(induction xs) 35apply simp 36apply (simp add: mset_insort) 37done 38 39lemma set_insort: "set (insort x xs) = insert x (set xs)" 40by (metis mset_insort set_mset_add_mset_insert set_mset_mset) 41 42lemma sorted_insort: "sorted (insort a xs) = sorted xs" 43apply(induction xs) 44apply(auto simp add: set_insort) 45done 46 47lemma "sorted (isort xs)" 48apply(induction xs) 49apply(auto simp: sorted_insort) 50done 51 52 53subsubsection "Time Complexity" 54 55text \<open>We count the number of function calls.\<close> 56 57text\<open> 58\<open>insort x [] = [x]\<close> 59\<open>insort x (y#ys) = 60 (if x \<le> y then x#y#ys else y#(insort x ys))\<close> 61\<close> 62fun t_insort :: "'a::linorder \<Rightarrow> 'a list \<Rightarrow> nat" where 63"t_insort x [] = 1" | 64"t_insort x (y#ys) = 65 (if x \<le> y then 0 else t_insort x ys) + 1" 66 67text\<open> 68\<open>isort [] = []\<close> 69\<open>isort (x#xs) = insort x (isort xs)\<close> 70\<close> 71fun t_isort :: "'a::linorder list \<Rightarrow> nat" where 72"t_isort [] = 1" | 73"t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1" 74 75 76lemma t_insort_length: "t_insort x xs \<le> length xs + 1" 77apply(induction xs) 78apply auto 79done 80 81lemma length_insort: "length (insort x xs) = length xs + 1" 82apply(induction xs) 83apply auto 84done 85 86lemma length_isort: "length (isort xs) = length xs" 87apply(induction xs) 88apply (auto simp: length_insort) 89done 90 91lemma t_isort_length: "t_isort xs \<le> (length xs + 1) ^ 2" 92proof(induction xs) 93 case Nil show ?case by simp 94next 95 case (Cons x xs) 96 have "t_isort (x#xs) = t_isort xs + t_insort x (isort xs) + 1" by simp 97 also have "\<dots> \<le> (length xs + 1) ^ 2 + t_insort x (isort xs) + 1" 98 using Cons.IH by simp 99 also have "\<dots> \<le> (length xs + 1) ^ 2 + length xs + 1 + 1" 100 using t_insort_length[of x "isort xs"] by (simp add: length_isort) 101 also have "\<dots> \<le> (length(x#xs) + 1) ^ 2" 102 by (simp add: power2_eq_square) 103 finally show ?case . 104qed 105 106 107subsection "Merge Sort" 108 109fun merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 110"merge [] ys = ys" | 111"merge xs [] = xs" | 112"merge (x#xs) (y#ys) = (if x \<le> y then x # merge xs (y#ys) else y # merge (x#xs) ys)" 113 114fun msort :: "'a::linorder list \<Rightarrow> 'a list" where 115"msort xs = (let n = length xs in 116 if n \<le> 1 then xs 117 else merge (msort (take (n div 2) xs)) (msort (drop (n div 2) xs)))" 118 119declare msort.simps [simp del] 120 121 122subsubsection "Functional Correctness" 123 124lemma mset_merge: "mset(merge xs ys) = mset xs + mset ys" 125by(induction xs ys rule: merge.induct) auto 126 127lemma "mset (msort xs) = mset xs" 128proof(induction xs rule: msort.induct) 129 case (1 xs) 130 let ?n = "length xs" 131 let ?xs1 = "take (?n div 2) xs" 132 let ?xs2 = "drop (?n div 2) xs" 133 show ?case 134 proof cases 135 assume "?n \<le> 1" 136 thus ?thesis by(simp add: msort.simps[of xs]) 137 next 138 assume "\<not> ?n \<le> 1" 139 hence "mset (msort xs) = mset (msort ?xs1) + mset (msort ?xs2)" 140 by(simp add: msort.simps[of xs] mset_merge) 141 also have "\<dots> = mset ?xs1 + mset ?xs2" 142 using \<open>\<not> ?n \<le> 1\<close> by(simp add: "1.IH") 143 also have "\<dots> = mset (?xs1 @ ?xs2)" by (simp del: append_take_drop_id) 144 also have "\<dots> = mset xs" by simp 145 finally show ?thesis . 146 qed 147qed 148 149lemma set_merge: "set(merge xs ys) = set xs \<union> set ys" 150by(induction xs ys rule: merge.induct) (auto) 151 152lemma sorted_merge: "sorted (merge xs ys) \<longleftrightarrow> (sorted xs \<and> sorted ys)" 153by(induction xs ys rule: merge.induct) (auto simp: set_merge) 154 155lemma "sorted (msort xs)" 156proof(induction xs rule: msort.induct) 157 case (1 xs) 158 let ?n = "length xs" 159 show ?case 160 proof cases 161 assume "?n \<le> 1" 162 thus ?thesis by(simp add: msort.simps[of xs] sorted01) 163 next 164 assume "\<not> ?n \<le> 1" 165 thus ?thesis using "1.IH" 166 by(simp add: sorted_merge msort.simps[of xs] mset_merge) 167 qed 168qed 169 170 171subsubsection "Time Complexity" 172 173text \<open>We only count the number of comparisons between list elements.\<close> 174 175fun c_merge :: "'a::linorder list \<Rightarrow> 'a list \<Rightarrow> nat" where 176"c_merge [] ys = 0" | 177"c_merge xs [] = 0" | 178"c_merge (x#xs) (y#ys) = 1 + (if x \<le> y then c_merge xs (y#ys) else c_merge (x#xs) ys)" 179 180lemma c_merge_ub: "c_merge xs ys \<le> length xs + length ys" 181by (induction xs ys rule: c_merge.induct) auto 182 183fun c_msort :: "'a::linorder list \<Rightarrow> nat" where 184"c_msort xs = 185 (let n = length xs; 186 ys = take (n div 2) xs; 187 zs = drop (n div 2) xs 188 in if n \<le> 1 then 0 189 else c_msort ys + c_msort zs + c_merge (msort ys) (msort zs))" 190 191declare c_msort.simps [simp del] 192 193lemma length_merge: "length(merge xs ys) = length xs + length ys" 194apply (induction xs ys rule: merge.induct) 195apply auto 196done 197 198lemma length_msort: "length(msort xs) = length xs" 199proof (induction xs rule: msort.induct) 200 case (1 xs) 201 thus ?case by (auto simp: msort.simps[of xs] length_merge) 202qed 203text \<open>Why structured proof? 204 To have the name "xs" to specialize msort.simps with xs 205 to ensure that msort.simps cannot be used recursively. 206Also works without this precaution, but that is just luck.\<close> 207 208lemma c_msort_le: "length xs = 2^k \<Longrightarrow> c_msort xs \<le> k * 2^k" 209proof(induction k arbitrary: xs) 210 case 0 thus ?case by (simp add: c_msort.simps) 211next 212 case (Suc k) 213 let ?n = "length xs" 214 let ?ys = "take (?n div 2) xs" 215 let ?zs = "drop (?n div 2) xs" 216 show ?case 217 proof (cases "?n \<le> 1") 218 case True 219 thus ?thesis by(simp add: c_msort.simps) 220 next 221 case False 222 have "c_msort(xs) = 223 c_msort ?ys + c_msort ?zs + c_merge (msort ?ys) (msort ?zs)" 224 by (simp add: c_msort.simps msort.simps) 225 also have "\<dots> \<le> c_msort ?ys + c_msort ?zs + length ?ys + length ?zs" 226 using c_merge_ub[of "msort ?ys" "msort ?zs"] length_msort[of ?ys] length_msort[of ?zs] 227 by arith 228 also have "\<dots> \<le> k * 2^k + c_msort ?zs + length ?ys + length ?zs" 229 using Suc.IH[of ?ys] Suc.prems by simp 230 also have "\<dots> \<le> k * 2^k + k * 2^k + length ?ys + length ?zs" 231 using Suc.IH[of ?zs] Suc.prems by simp 232 also have "\<dots> = 2 * k * 2^k + 2 * 2 ^ k" 233 using Suc.prems by simp 234 finally show ?thesis by simp 235 qed 236qed 237 238(* Beware of conversions: *) 239lemma "length xs = 2^k \<Longrightarrow> c_msort xs \<le> length xs * log 2 (length xs)" 240using c_msort_le[of xs k] apply (simp add: log_nat_power algebra_simps) 241by (metis (mono_tags) numeral_power_eq_of_nat_cancel_iff of_nat_le_iff of_nat_mult) 242 243 244subsection "Bottom-Up Merge Sort" 245 246(* Exercise: make tail recursive *) 247fun merge_adj :: "('a::linorder) list list \<Rightarrow> 'a list list" where 248"merge_adj [] = []" | 249"merge_adj [xs] = [xs]" | 250"merge_adj (xs # ys # zss) = merge xs ys # merge_adj zss" 251 252text \<open>For the termination proof of \<open>merge_all\<close> below.\<close> 253lemma length_merge_adjacent[simp]: "length (merge_adj xs) = (length xs + 1) div 2" 254by (induction xs rule: merge_adj.induct) auto 255 256fun merge_all :: "('a::linorder) list list \<Rightarrow> 'a list" where 257"merge_all [] = undefined" | 258"merge_all [xs] = xs" | 259"merge_all xss = merge_all (merge_adj xss)" 260 261definition msort_bu :: "('a::linorder) list \<Rightarrow> 'a list" where 262"msort_bu xs = (if xs = [] then [] else merge_all (map (\<lambda>x. [x]) xs))" 263 264 265subsubsection "Functional Correctness" 266 267lemma mset_merge_adj: 268 "\<Union># image_mset mset (mset (merge_adj xss)) = \<Union># image_mset mset (mset xss)" 269by(induction xss rule: merge_adj.induct) (auto simp: mset_merge) 270 271lemma msec_merge_all: 272 "xss \<noteq> [] \<Longrightarrow> mset (merge_all xss) = (\<Union># (mset (map mset xss)))" 273by(induction xss rule: merge_all.induct) (auto simp: mset_merge mset_merge_adj) 274 275lemma sorted_merge_adj: 276 "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). sorted xs" 277by(induction xss rule: merge_adj.induct) (auto simp: sorted_merge) 278 279lemma sorted_merge_all: 280 "\<forall>xs \<in> set xss. sorted xs \<Longrightarrow> xss \<noteq> [] \<Longrightarrow> sorted (merge_all xss)" 281apply(induction xss rule: merge_all.induct) 282using [[simp_depth_limit=3]] by (auto simp add: sorted_merge_adj) 283 284lemma sorted_msort_bu: "sorted (msort_bu xs)" 285by(simp add: msort_bu_def sorted_merge_all) 286 287lemma mset_msort: "mset (msort_bu xs) = mset xs" 288by(simp add: msort_bu_def msec_merge_all comp_def) 289 290 291subsubsection "Time Complexity" 292 293fun c_merge_adj :: "('a::linorder) list list \<Rightarrow> nat" where 294"c_merge_adj [] = 0" | 295"c_merge_adj [xs] = 0" | 296"c_merge_adj (xs # ys # zss) = c_merge xs ys + c_merge_adj zss" 297 298fun c_merge_all :: "('a::linorder) list list \<Rightarrow> nat" where 299"c_merge_all [] = undefined" | 300"c_merge_all [xs] = 0" | 301"c_merge_all xss = c_merge_adj xss + c_merge_all (merge_adj xss)" 302 303definition c_msort_bu :: "('a::linorder) list \<Rightarrow> nat" where 304"c_msort_bu xs = (if xs = [] then 0 else c_merge_all (map (\<lambda>x. [x]) xs))" 305 306lemma length_merge_adj: 307 "\<lbrakk> even(length xss); \<forall>x \<in> set xss. length x = m \<rbrakk> \<Longrightarrow> \<forall>xs \<in> set (merge_adj xss). length xs = 2*m" 308by(induction xss rule: merge_adj.induct) (auto simp: length_merge) 309 310lemma c_merge_adj: "\<forall>xs \<in> set xss. length xs = m \<Longrightarrow> c_merge_adj xss \<le> m * length xss" 311proof(induction xss rule: c_merge_adj.induct) 312 case 1 thus ?case by simp 313next 314 case 2 thus ?case by simp 315next 316 case (3 x y) thus ?case using c_merge_ub[of x y] by (simp add: algebra_simps) 317qed 318 319lemma c_merge_all: "\<lbrakk> \<forall>xs \<in> set xss. length xs = m; length xss = 2^k \<rbrakk> 320 \<Longrightarrow> c_merge_all xss \<le> m * k * 2^k" 321proof (induction xss arbitrary: k m rule: c_merge_all.induct) 322 case 1 thus ?case by simp 323next 324 case 2 thus ?case by simp 325next 326 case (3 xs ys xss) 327 let ?xss = "xs # ys # xss" 328 let ?xss2 = "merge_adj ?xss" 329 obtain k' where k': "k = Suc k'" using "3.prems"(2) 330 by (metis length_Cons nat.inject nat_power_eq_Suc_0_iff nat.exhaust) 331 have "even (length xss)" using "3.prems"(2) even_Suc_Suc_iff by fastforce 332 from "3.prems"(1) length_merge_adj[OF this] 333 have *: "\<forall>x \<in> set(merge_adj ?xss). length x = 2*m" by(auto simp: length_merge) 334 have **: "length ?xss2 = 2 ^ k'" using "3.prems"(2) k' by auto 335 have "c_merge_all ?xss = c_merge_adj ?xss + c_merge_all ?xss2" by simp 336 also have "\<dots> \<le> m * 2^k + c_merge_all ?xss2" 337 using "3.prems"(2) c_merge_adj[OF "3.prems"(1)] by (auto simp: algebra_simps) 338 also have "\<dots> \<le> m * 2^k + (2*m) * k' * 2^k'" 339 using "3.IH"[OF * **] by simp 340 also have "\<dots> = m * k * 2^k" 341 using k' by (simp add: algebra_simps) 342 finally show ?case . 343qed 344 345corollary c_msort_bu: "length xs = 2 ^ k \<Longrightarrow> c_msort_bu xs \<le> k * 2 ^ k" 346using c_merge_all[of "map (\<lambda>x. [x]) xs" 1] by (simp add: c_msort_bu_def) 347 348end 349