src/HOL/Library/Sorting_Algorithms.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (4 months ago) changeset 69946 494934c30f38 parent 69250 1011f0b46af7 permissions -rw-r--r--
improved code equations taken over from AFP
 haftmann@69194 ` 1` ```(* Title: HOL/Library/Sorting_Algorithms.thy ``` haftmann@69194 ` 2` ``` Author: Florian Haftmann, TU Muenchen ``` haftmann@69194 ` 3` ```*) ``` haftmann@69194 ` 4` haftmann@69194 ` 5` ```theory Sorting_Algorithms ``` haftmann@69194 ` 6` ``` imports Main Multiset Comparator ``` haftmann@69194 ` 7` ```begin ``` haftmann@69194 ` 8` haftmann@69194 ` 9` ```section \Stably sorted lists\ ``` haftmann@69194 ` 10` haftmann@69194 ` 11` ```abbreviation (input) stable_segment :: "'a comparator \ 'a \ 'a list \ 'a list" ``` haftmann@69194 ` 12` ``` where "stable_segment cmp x \ filter (\y. compare cmp x y = Equiv)" ``` haftmann@69194 ` 13` haftmann@69194 ` 14` ```fun sorted :: "'a comparator \ 'a list \ bool" ``` haftmann@69194 ` 15` ``` where sorted_Nil: "sorted cmp [] \ True" ``` haftmann@69194 ` 16` ``` | sorted_single: "sorted cmp [x] \ True" ``` haftmann@69246 ` 17` ``` | sorted_rec: "sorted cmp (y # x # xs) \ compare cmp y x \ Greater \ sorted cmp (x # xs)" ``` haftmann@69194 ` 18` haftmann@69194 ` 19` ```lemma sorted_ConsI: ``` haftmann@69194 ` 20` ``` "sorted cmp (x # xs)" if "sorted cmp xs" ``` haftmann@69246 ` 21` ``` and "\y ys. xs = y # ys \ compare cmp x y \ Greater" ``` haftmann@69246 ` 22` ``` using that by (cases xs) simp_all ``` haftmann@69246 ` 23` haftmann@69246 ` 24` ```lemma sorted_Cons_imp_sorted: ``` haftmann@69246 ` 25` ``` "sorted cmp xs" if "sorted cmp (x # xs)" ``` haftmann@69194 ` 26` ``` using that by (cases xs) simp_all ``` haftmann@69194 ` 27` haftmann@69246 ` 28` ```lemma sorted_Cons_imp_not_less: ``` haftmann@69246 ` 29` ``` "compare cmp y x \ Greater" if "sorted cmp (y # xs)" ``` haftmann@69246 ` 30` ``` and "x \ set xs" ``` haftmann@69246 ` 31` ``` using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater) ``` haftmann@69246 ` 32` haftmann@69194 ` 33` ```lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]: ``` haftmann@69194 ` 34` ``` "P xs" if "sorted cmp xs" and "P []" ``` haftmann@69194 ` 35` ``` and *: "\x xs. sorted cmp xs \ P xs ``` haftmann@69246 ` 36` ``` \ (\y. y \ set xs \ compare cmp x y \ Greater) \ P (x # xs)" ``` haftmann@69194 ` 37` ```using \sorted cmp xs\ proof (induction xs) ``` haftmann@69194 ` 38` ``` case Nil ``` haftmann@69194 ` 39` ``` show ?case ``` haftmann@69194 ` 40` ``` by (rule \P []\) ``` haftmann@69194 ` 41` ```next ``` haftmann@69194 ` 42` ``` case (Cons x xs) ``` haftmann@69194 ` 43` ``` from \sorted cmp (x # xs)\ have "sorted cmp xs" ``` haftmann@69194 ` 44` ``` by (cases xs) simp_all ``` haftmann@69194 ` 45` ``` moreover have "P xs" using \sorted cmp xs\ ``` haftmann@69194 ` 46` ``` by (rule Cons.IH) ``` haftmann@69246 ` 47` ``` moreover have "compare cmp x y \ Greater" if "y \ set xs" for y ``` haftmann@69194 ` 48` ``` using that \sorted cmp (x # xs)\ proof (induction xs) ``` haftmann@69194 ` 49` ``` case Nil ``` haftmann@69194 ` 50` ``` then show ?case ``` haftmann@69194 ` 51` ``` by simp ``` haftmann@69194 ` 52` ``` next ``` haftmann@69194 ` 53` ``` case (Cons z zs) ``` haftmann@69194 ` 54` ``` then show ?case ``` haftmann@69194 ` 55` ``` proof (cases zs) ``` haftmann@69194 ` 56` ``` case Nil ``` haftmann@69194 ` 57` ``` with Cons.prems show ?thesis ``` haftmann@69194 ` 58` ``` by simp ``` haftmann@69194 ` 59` ``` next ``` haftmann@69194 ` 60` ``` case (Cons w ws) ``` haftmann@69246 ` 61` ``` with Cons.prems have "compare cmp z w \ Greater" "compare cmp x z \ Greater" ``` haftmann@69194 ` 62` ``` by auto ``` haftmann@69246 ` 63` ``` then have "compare cmp x w \ Greater" ``` haftmann@69246 ` 64` ``` by (auto dest: compare.trans_not_greater) ``` haftmann@69194 ` 65` ``` with Cons show ?thesis ``` haftmann@69194 ` 66` ``` using Cons.prems Cons.IH by auto ``` haftmann@69194 ` 67` ``` qed ``` haftmann@69194 ` 68` ``` qed ``` haftmann@69194 ` 69` ``` ultimately show ?case ``` haftmann@69194 ` 70` ``` by (rule *) ``` haftmann@69194 ` 71` ```qed ``` haftmann@69194 ` 72` haftmann@69194 ` 73` ```lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]: ``` haftmann@69194 ` 74` ``` "P xs" if "sorted cmp xs" and "P []" ``` haftmann@69194 ` 75` ``` and *: "\x xs. sorted cmp xs \ P (remove1 x xs) ``` haftmann@69246 ` 76` ``` \ x \ set xs \ hd (stable_segment cmp x xs) = x \ (\y. y \ set xs \ compare cmp x y \ Greater) ``` haftmann@69194 ` 77` ``` \ P xs" ``` haftmann@69194 ` 78` ```using \sorted cmp xs\ proof (induction xs) ``` haftmann@69194 ` 79` ``` case Nil ``` haftmann@69194 ` 80` ``` show ?case ``` haftmann@69194 ` 81` ``` by (rule \P []\) ``` haftmann@69194 ` 82` ```next ``` haftmann@69194 ` 83` ``` case (Cons x xs) ``` haftmann@69194 ` 84` ``` then have "sorted cmp (x # xs)" ``` haftmann@69194 ` 85` ``` by (simp add: sorted_ConsI) ``` haftmann@69194 ` 86` ``` moreover note Cons.IH ``` haftmann@69246 ` 87` ``` moreover have "\y. compare cmp x y = Greater \ y \ set xs \ False" ``` haftmann@69194 ` 88` ``` using Cons.hyps by simp ``` haftmann@69194 ` 89` ``` ultimately show ?case ``` haftmann@69194 ` 90` ``` by (auto intro!: * [of "x # xs" x]) blast ``` haftmann@69194 ` 91` ```qed ``` haftmann@69194 ` 92` haftmann@69194 ` 93` ```lemma sorted_remove1: ``` haftmann@69194 ` 94` ``` "sorted cmp (remove1 x xs)" if "sorted cmp xs" ``` haftmann@69194 ` 95` ```proof (cases "x \ set xs") ``` haftmann@69194 ` 96` ``` case False ``` haftmann@69194 ` 97` ``` with that show ?thesis ``` haftmann@69194 ` 98` ``` by (simp add: remove1_idem) ``` haftmann@69194 ` 99` ```next ``` haftmann@69194 ` 100` ``` case True ``` haftmann@69194 ` 101` ``` with that show ?thesis proof (induction xs) ``` haftmann@69194 ` 102` ``` case Nil ``` haftmann@69194 ` 103` ``` then show ?case ``` haftmann@69194 ` 104` ``` by simp ``` haftmann@69194 ` 105` ``` next ``` haftmann@69194 ` 106` ``` case (Cons y ys) ``` haftmann@69194 ` 107` ``` show ?case proof (cases "x = y") ``` haftmann@69194 ` 108` ``` case True ``` haftmann@69194 ` 109` ``` with Cons.hyps show ?thesis ``` haftmann@69194 ` 110` ``` by simp ``` haftmann@69194 ` 111` ``` next ``` haftmann@69194 ` 112` ``` case False ``` haftmann@69194 ` 113` ``` then have "sorted cmp (remove1 x ys)" ``` haftmann@69194 ` 114` ``` using Cons.IH Cons.prems by auto ``` haftmann@69194 ` 115` ``` then have "sorted cmp (y # remove1 x ys)" ``` haftmann@69194 ` 116` ``` proof (rule sorted_ConsI) ``` haftmann@69194 ` 117` ``` fix z zs ``` haftmann@69194 ` 118` ``` assume "remove1 x ys = z # zs" ``` haftmann@69194 ` 119` ``` with \x \ y\ have "z \ set ys" ``` haftmann@69194 ` 120` ``` using notin_set_remove1 [of z ys x] by auto ``` haftmann@69246 ` 121` ``` then show "compare cmp y z \ Greater" ``` haftmann@69194 ` 122` ``` by (rule Cons.hyps(2)) ``` haftmann@69194 ` 123` ``` qed ``` haftmann@69194 ` 124` ``` with False show ?thesis ``` haftmann@69194 ` 125` ``` by simp ``` haftmann@69194 ` 126` ``` qed ``` haftmann@69194 ` 127` ``` qed ``` haftmann@69194 ` 128` ```qed ``` haftmann@69194 ` 129` haftmann@69246 ` 130` ```lemma sorted_stable_segment: ``` haftmann@69246 ` 131` ``` "sorted cmp (stable_segment cmp x xs)" ``` haftmann@69246 ` 132` ```proof (induction xs) ``` haftmann@69246 ` 133` ``` case Nil ``` haftmann@69246 ` 134` ``` show ?case ``` haftmann@69246 ` 135` ``` by simp ``` haftmann@69246 ` 136` ```next ``` haftmann@69246 ` 137` ``` case (Cons y ys) ``` haftmann@69246 ` 138` ``` then show ?case ``` haftmann@69246 ` 139` ``` by (auto intro!: sorted_ConsI simp add: filter_eq_Cons_iff compare.sym) ``` haftmann@69246 ` 140` ``` (auto dest: compare.trans_equiv simp add: compare.sym compare.greater_iff_sym_less) ``` haftmann@69246 ` 141` haftmann@69246 ` 142` ```qed ``` haftmann@69246 ` 143` haftmann@69194 ` 144` ```primrec insort :: "'a comparator \ 'a \ 'a list \ 'a list" ``` haftmann@69194 ` 145` ``` where "insort cmp y [] = [y]" ``` haftmann@69194 ` 146` ``` | "insort cmp y (x # xs) = (if compare cmp y x \ Greater ``` haftmann@69194 ` 147` ``` then y # x # xs ``` haftmann@69194 ` 148` ``` else x # insort cmp y xs)" ``` haftmann@69194 ` 149` haftmann@69194 ` 150` ```lemma mset_insort [simp]: ``` haftmann@69194 ` 151` ``` "mset (insort cmp x xs) = add_mset x (mset xs)" ``` haftmann@69194 ` 152` ``` by (induction xs) simp_all ``` haftmann@69194 ` 153` haftmann@69194 ` 154` ```lemma length_insort [simp]: ``` haftmann@69194 ` 155` ``` "length (insort cmp x xs) = Suc (length xs)" ``` haftmann@69194 ` 156` ``` by (induction xs) simp_all ``` haftmann@69194 ` 157` haftmann@69194 ` 158` ```lemma sorted_insort: ``` haftmann@69194 ` 159` ``` "sorted cmp (insort cmp x xs)" if "sorted cmp xs" ``` haftmann@69194 ` 160` ```using that proof (induction xs) ``` haftmann@69194 ` 161` ``` case Nil ``` haftmann@69194 ` 162` ``` then show ?case ``` haftmann@69194 ` 163` ``` by simp ``` haftmann@69194 ` 164` ```next ``` haftmann@69194 ` 165` ``` case (Cons y ys) ``` haftmann@69194 ` 166` ``` then show ?case by (cases ys) ``` haftmann@69194 ` 167` ``` (auto, simp_all add: compare.greater_iff_sym_less) ``` haftmann@69194 ` 168` ```qed ``` haftmann@69194 ` 169` haftmann@69194 ` 170` ```lemma stable_insort_equiv: ``` haftmann@69194 ` 171` ``` "stable_segment cmp y (insort cmp x xs) = x # stable_segment cmp y xs" ``` haftmann@69194 ` 172` ``` if "compare cmp y x = Equiv" ``` haftmann@69194 ` 173` ```proof (induction xs) ``` haftmann@69194 ` 174` ``` case Nil ``` haftmann@69194 ` 175` ``` from that show ?case ``` haftmann@69194 ` 176` ``` by simp ``` haftmann@69194 ` 177` ```next ``` haftmann@69194 ` 178` ``` case (Cons z xs) ``` haftmann@69194 ` 179` ``` moreover from that have "compare cmp y z = Equiv \ compare cmp z x = Equiv" ``` haftmann@69194 ` 180` ``` by (auto intro: compare.trans_equiv simp add: compare.sym) ``` haftmann@69194 ` 181` ``` ultimately show ?case ``` haftmann@69194 ` 182` ``` using that by (auto simp add: compare.greater_iff_sym_less) ``` haftmann@69194 ` 183` ```qed ``` haftmann@69194 ` 184` haftmann@69194 ` 185` ```lemma stable_insort_not_equiv: ``` haftmann@69194 ` 186` ``` "stable_segment cmp y (insort cmp x xs) = stable_segment cmp y xs" ``` haftmann@69194 ` 187` ``` if "compare cmp y x \ Equiv" ``` haftmann@69194 ` 188` ``` using that by (induction xs) simp_all ``` haftmann@69194 ` 189` haftmann@69194 ` 190` ```lemma remove1_insort_same_eq [simp]: ``` haftmann@69194 ` 191` ``` "remove1 x (insort cmp x xs) = xs" ``` haftmann@69194 ` 192` ``` by (induction xs) simp_all ``` haftmann@69194 ` 193` haftmann@69194 ` 194` ```lemma insort_eq_ConsI: ``` haftmann@69194 ` 195` ``` "insort cmp x xs = x # xs" ``` haftmann@69246 ` 196` ``` if "sorted cmp xs" "\y. y \ set xs \ compare cmp x y \ Greater" ``` haftmann@69194 ` 197` ``` using that by (induction xs) (simp_all add: compare.greater_iff_sym_less) ``` haftmann@69194 ` 198` haftmann@69194 ` 199` ```lemma remove1_insort_not_same_eq [simp]: ``` haftmann@69194 ` 200` ``` "remove1 y (insort cmp x xs) = insort cmp x (remove1 y xs)" ``` haftmann@69194 ` 201` ``` if "sorted cmp xs" "x \ y" ``` haftmann@69194 ` 202` ```using that proof (induction xs) ``` haftmann@69194 ` 203` ``` case Nil ``` haftmann@69194 ` 204` ``` then show ?case ``` haftmann@69194 ` 205` ``` by simp ``` haftmann@69194 ` 206` ```next ``` haftmann@69194 ` 207` ``` case (Cons z zs) ``` haftmann@69194 ` 208` ``` show ?case ``` haftmann@69246 ` 209` ``` proof (cases "compare cmp x z = Greater") ``` haftmann@69194 ` 210` ``` case True ``` haftmann@69194 ` 211` ``` with Cons show ?thesis ``` haftmann@69246 ` 212` ``` by simp ``` haftmann@69194 ` 213` ``` next ``` haftmann@69194 ` 214` ``` case False ``` haftmann@69246 ` 215` ``` then have "compare cmp x y \ Greater" if "y \ set zs" for y ``` haftmann@69246 ` 216` ``` using that Cons.hyps ``` haftmann@69246 ` 217` ``` by (auto dest: compare.trans_not_greater) ``` haftmann@69194 ` 218` ``` with Cons show ?thesis ``` haftmann@69194 ` 219` ``` by (simp add: insort_eq_ConsI) ``` haftmann@69194 ` 220` ``` qed ``` haftmann@69194 ` 221` ```qed ``` haftmann@69194 ` 222` haftmann@69194 ` 223` ```lemma insort_remove1_same_eq: ``` haftmann@69194 ` 224` ``` "insort cmp x (remove1 x xs) = xs" ``` haftmann@69194 ` 225` ``` if "sorted cmp xs" and "x \ set xs" and "hd (stable_segment cmp x xs) = x" ``` haftmann@69194 ` 226` ```using that proof (induction xs) ``` haftmann@69194 ` 227` ``` case Nil ``` haftmann@69194 ` 228` ``` then show ?case ``` haftmann@69194 ` 229` ``` by simp ``` haftmann@69194 ` 230` ```next ``` haftmann@69194 ` 231` ``` case (Cons y ys) ``` haftmann@69194 ` 232` ``` then have "compare cmp x y \ Less" ``` haftmann@69246 ` 233` ``` by (auto simp add: compare.greater_iff_sym_less) ``` haftmann@69194 ` 234` ``` then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv" ``` haftmann@69194 ` 235` ``` by (cases "compare cmp x y") auto ``` haftmann@69194 ` 236` ``` then show ?case proof cases ``` haftmann@69194 ` 237` ``` case 1 ``` haftmann@69194 ` 238` ``` with Cons.prems Cons.IH show ?thesis ``` haftmann@69194 ` 239` ``` by auto ``` haftmann@69194 ` 240` ``` next ``` haftmann@69194 ` 241` ``` case 2 ``` haftmann@69194 ` 242` ``` with Cons.prems have "x = y" ``` haftmann@69194 ` 243` ``` by simp ``` haftmann@69194 ` 244` ``` with Cons.hyps show ?thesis ``` haftmann@69194 ` 245` ``` by (simp add: insort_eq_ConsI) ``` haftmann@69194 ` 246` ``` qed ``` haftmann@69194 ` 247` ```qed ``` haftmann@69194 ` 248` haftmann@69246 ` 249` ```lemma sorted_append_iff: ``` haftmann@69246 ` 250` ``` "sorted cmp (xs @ ys) \ sorted cmp xs \ sorted cmp ys ``` haftmann@69246 ` 251` ``` \ (\x \ set xs. \y \ set ys. compare cmp x y \ Greater)" (is "?P \ ?R \ ?S \ ?Q") ``` haftmann@69246 ` 252` ```proof ``` haftmann@69246 ` 253` ``` assume ?P ``` haftmann@69246 ` 254` ``` have ?R ``` haftmann@69246 ` 255` ``` using \?P\ by (induction xs) ``` haftmann@69246 ` 256` ``` (auto simp add: sorted_Cons_imp_not_less, ``` haftmann@69246 ` 257` ``` auto simp add: sorted_Cons_imp_sorted intro: sorted_ConsI) ``` haftmann@69246 ` 258` ``` moreover have ?S ``` haftmann@69246 ` 259` ``` using \?P\ by (induction xs) (auto dest: sorted_Cons_imp_sorted) ``` haftmann@69246 ` 260` ``` moreover have ?Q ``` haftmann@69246 ` 261` ``` using \?P\ by (induction xs) (auto simp add: sorted_Cons_imp_not_less, ``` haftmann@69246 ` 262` ``` simp add: sorted_Cons_imp_sorted) ``` haftmann@69246 ` 263` ``` ultimately show "?R \ ?S \ ?Q" ``` haftmann@69246 ` 264` ``` by simp ``` haftmann@69246 ` 265` ```next ``` haftmann@69246 ` 266` ``` assume "?R \ ?S \ ?Q" ``` haftmann@69246 ` 267` ``` then have ?R ?S ?Q ``` haftmann@69246 ` 268` ``` by simp_all ``` haftmann@69246 ` 269` ``` then show ?P ``` haftmann@69246 ` 270` ``` by (induction xs) ``` haftmann@69246 ` 271` ``` (auto simp add: append_eq_Cons_conv intro!: sorted_ConsI) ``` haftmann@69246 ` 272` ```qed ``` haftmann@69246 ` 273` haftmann@69194 ` 274` ```definition sort :: "'a comparator \ 'a list \ 'a list" ``` haftmann@69194 ` 275` ``` where "sort cmp xs = foldr (insort cmp) xs []" ``` haftmann@69194 ` 276` haftmann@69194 ` 277` ```lemma sort_simps [simp]: ``` haftmann@69194 ` 278` ``` "sort cmp [] = []" ``` haftmann@69194 ` 279` ``` "sort cmp (x # xs) = insort cmp x (sort cmp xs)" ``` haftmann@69194 ` 280` ``` by (simp_all add: sort_def) ``` haftmann@69194 ` 281` haftmann@69194 ` 282` ```lemma mset_sort [simp]: ``` haftmann@69194 ` 283` ``` "mset (sort cmp xs) = mset xs" ``` haftmann@69194 ` 284` ``` by (induction xs) simp_all ``` haftmann@69194 ` 285` haftmann@69194 ` 286` ```lemma length_sort [simp]: ``` haftmann@69194 ` 287` ``` "length (sort cmp xs) = length xs" ``` haftmann@69194 ` 288` ``` by (induction xs) simp_all ``` haftmann@69194 ` 289` haftmann@69194 ` 290` ```lemma sorted_sort [simp]: ``` haftmann@69194 ` 291` ``` "sorted cmp (sort cmp xs)" ``` haftmann@69194 ` 292` ``` by (induction xs) (simp_all add: sorted_insort) ``` haftmann@69194 ` 293` haftmann@69194 ` 294` ```lemma stable_sort: ``` haftmann@69194 ` 295` ``` "stable_segment cmp x (sort cmp xs) = stable_segment cmp x xs" ``` haftmann@69194 ` 296` ``` by (induction xs) (simp_all add: stable_insort_equiv stable_insort_not_equiv) ``` haftmann@69194 ` 297` haftmann@69194 ` 298` ```lemma sort_remove1_eq [simp]: ``` haftmann@69194 ` 299` ``` "sort cmp (remove1 x xs) = remove1 x (sort cmp xs)" ``` haftmann@69194 ` 300` ``` by (induction xs) simp_all ``` haftmann@69194 ` 301` haftmann@69194 ` 302` ```lemma set_insort [simp]: ``` haftmann@69194 ` 303` ``` "set (insort cmp x xs) = insert x (set xs)" ``` haftmann@69194 ` 304` ``` by (induction xs) auto ``` haftmann@69194 ` 305` haftmann@69194 ` 306` ```lemma set_sort [simp]: ``` haftmann@69194 ` 307` ``` "set (sort cmp xs) = set xs" ``` haftmann@69194 ` 308` ``` by (induction xs) auto ``` haftmann@69194 ` 309` haftmann@69194 ` 310` ```lemma sort_eqI: ``` haftmann@69194 ` 311` ``` "sort cmp ys = xs" ``` haftmann@69194 ` 312` ``` if permutation: "mset ys = mset xs" ``` haftmann@69194 ` 313` ``` and sorted: "sorted cmp xs" ``` haftmann@69194 ` 314` ``` and stable: "\y. y \ set ys \ ``` haftmann@69194 ` 315` ``` stable_segment cmp y ys = stable_segment cmp y xs" ``` haftmann@69194 ` 316` ```proof - ``` haftmann@69194 ` 317` ``` have stable': "stable_segment cmp y ys = ``` haftmann@69194 ` 318` ``` stable_segment cmp y xs" for y ``` haftmann@69194 ` 319` ``` proof (cases "\x\set ys. compare cmp y x = Equiv") ``` haftmann@69194 ` 320` ``` case True ``` haftmann@69194 ` 321` ``` then obtain z where "z \ set ys" and "compare cmp y z = Equiv" ``` haftmann@69194 ` 322` ``` by auto ``` haftmann@69194 ` 323` ``` then have "compare cmp y x = Equiv \ compare cmp z x = Equiv" for x ``` haftmann@69194 ` 324` ``` by (meson compare.sym compare.trans_equiv) ``` haftmann@69194 ` 325` ``` moreover have "stable_segment cmp z ys = ``` haftmann@69194 ` 326` ``` stable_segment cmp z xs" ``` haftmann@69194 ` 327` ``` using \z \ set ys\ by (rule stable) ``` haftmann@69194 ` 328` ``` ultimately show ?thesis ``` haftmann@69194 ` 329` ``` by simp ``` haftmann@69194 ` 330` ``` next ``` haftmann@69194 ` 331` ``` case False ``` haftmann@69194 ` 332` ``` moreover from permutation have "set ys = set xs" ``` haftmann@69194 ` 333` ``` by (rule mset_eq_setD) ``` haftmann@69194 ` 334` ``` ultimately show ?thesis ``` haftmann@69194 ` 335` ``` by simp ``` haftmann@69194 ` 336` ``` qed ``` haftmann@69194 ` 337` ``` show ?thesis ``` haftmann@69194 ` 338` ``` using sorted permutation stable' proof (induction xs arbitrary: ys rule: sorted_induct_remove1) ``` haftmann@69194 ` 339` ``` case Nil ``` haftmann@69194 ` 340` ``` then show ?case ``` haftmann@69194 ` 341` ``` by simp ``` haftmann@69194 ` 342` ``` next ``` haftmann@69194 ` 343` ``` case (minimum x xs) ``` haftmann@69194 ` 344` ``` from \mset ys = mset xs\ have ys: "set ys = set xs" ``` haftmann@69194 ` 345` ``` by (rule mset_eq_setD) ``` haftmann@69246 ` 346` ``` then have "compare cmp x y \ Greater" if "y \ set ys" for y ``` haftmann@69194 ` 347` ``` using that minimum.hyps by simp ``` haftmann@69194 ` 348` ``` from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs" ``` haftmann@69194 ` 349` ``` by simp ``` haftmann@69194 ` 350` ``` have "sort cmp (remove1 x ys) = remove1 x xs" ``` haftmann@69194 ` 351` ``` by (rule minimum.IH) (simp_all add: minimum.prems filter_remove1) ``` haftmann@69194 ` 352` ``` then have "remove1 x (sort cmp ys) = remove1 x xs" ``` haftmann@69194 ` 353` ``` by simp ``` haftmann@69194 ` 354` ``` then have "insort cmp x (remove1 x (sort cmp ys)) = ``` haftmann@69194 ` 355` ``` insort cmp x (remove1 x xs)" ``` haftmann@69194 ` 356` ``` by simp ``` haftmann@69194 ` 357` ``` also from minimum.hyps ys stable have "insort cmp x (remove1 x (sort cmp ys)) = sort cmp ys" ``` haftmann@69194 ` 358` ``` by (simp add: stable_sort insort_remove1_same_eq) ``` haftmann@69194 ` 359` ``` also from minimum.hyps have "insort cmp x (remove1 x xs) = xs" ``` haftmann@69194 ` 360` ``` by (simp add: insort_remove1_same_eq) ``` haftmann@69194 ` 361` ``` finally show ?case . ``` haftmann@69194 ` 362` ``` qed ``` haftmann@69194 ` 363` ```qed ``` haftmann@69194 ` 364` haftmann@69246 ` 365` ```lemma filter_insort: ``` haftmann@69246 ` 366` ``` "filter P (insort cmp x xs) = insort cmp x (filter P xs)" ``` haftmann@69246 ` 367` ``` if "sorted cmp xs" and "P x" ``` haftmann@69246 ` 368` ``` using that by (induction xs) ``` haftmann@69246 ` 369` ``` (auto simp add: compare.trans_not_greater insort_eq_ConsI) ``` haftmann@69246 ` 370` haftmann@69246 ` 371` ```lemma filter_insort_triv: ``` haftmann@69246 ` 372` ``` "filter P (insort cmp x xs) = filter P xs" ``` haftmann@69246 ` 373` ``` if "\ P x" ``` haftmann@69246 ` 374` ``` using that by (induction xs) simp_all ``` haftmann@69246 ` 375` haftmann@69246 ` 376` ```lemma filter_sort: ``` haftmann@69246 ` 377` ``` "filter P (sort cmp xs) = sort cmp (filter P xs)" ``` haftmann@69246 ` 378` ``` by (induction xs) (auto simp add: filter_insort filter_insort_triv) ``` haftmann@69246 ` 379` haftmann@69246 ` 380` haftmann@69246 ` 381` ```section \Alternative sorting algorithms\ ``` haftmann@69246 ` 382` haftmann@69246 ` 383` ```subsection \Quicksort\ ``` haftmann@69246 ` 384` haftmann@69246 ` 385` ```definition quicksort :: "'a comparator \ 'a list \ 'a list" ``` haftmann@69246 ` 386` ``` where quicksort_is_sort [simp]: "quicksort = sort" ``` haftmann@69246 ` 387` haftmann@69246 ` 388` ```lemma sort_by_quicksort: ``` haftmann@69246 ` 389` ``` "sort = quicksort" ``` haftmann@69246 ` 390` ``` by simp ``` haftmann@69246 ` 391` haftmann@69246 ` 392` ```lemma sort_by_quicksort_rec: ``` haftmann@69246 ` 393` ``` "sort cmp xs = sort cmp [x\xs. compare cmp x (xs ! (length xs div 2)) = Less] ``` haftmann@69246 ` 394` ``` @ stable_segment cmp (xs ! (length xs div 2)) xs ``` haftmann@69250 ` 395` ``` @ sort cmp [x\xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "_ = ?rhs") ``` haftmann@69246 ` 396` ```proof (rule sort_eqI) ``` haftmann@69250 ` 397` ``` show "mset xs = mset ?rhs" ``` haftmann@69246 ` 398` ``` by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust) ``` haftmann@69246 ` 399` ```next ``` haftmann@69246 ` 400` ``` show "sorted cmp ?rhs" ``` haftmann@69246 ` 401` ``` by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater) ``` haftmann@69246 ` 402` ```next ``` haftmann@69246 ` 403` ``` let ?pivot = "xs ! (length xs div 2)" ``` haftmann@69246 ` 404` ``` fix l ``` haftmann@69246 ` 405` ``` have "compare cmp x ?pivot = comp \ compare cmp l x = Equiv ``` haftmann@69246 ` 406` ``` \ compare cmp l ?pivot = comp \ compare cmp l x = Equiv" for x comp ``` haftmann@69246 ` 407` ``` proof - ``` haftmann@69246 ` 408` ``` have "compare cmp x ?pivot = comp \ compare cmp l ?pivot = comp" ``` haftmann@69246 ` 409` ``` if "compare cmp l x = Equiv" ``` haftmann@69246 ` 410` ``` using that by (simp add: compare.equiv_subst_left compare.sym) ``` haftmann@69246 ` 411` ``` then show ?thesis by blast ``` haftmann@69246 ` 412` ``` qed ``` haftmann@69250 ` 413` ``` then show "stable_segment cmp l xs = stable_segment cmp l ?rhs" ``` haftmann@69246 ` 414` ``` by (simp add: stable_sort compare.sym [of _ ?pivot]) ``` haftmann@69246 ` 415` ``` (cases "compare cmp l ?pivot", simp_all) ``` haftmann@69246 ` 416` ```qed ``` haftmann@69246 ` 417` haftmann@69246 ` 418` ```context ``` haftmann@69246 ` 419` ```begin ``` haftmann@69246 ` 420` haftmann@69246 ` 421` ```qualified definition partition :: "'a comparator \ 'a \ 'a list \ 'a list \ 'a list \ 'a list" ``` haftmann@69246 ` 422` ``` where "partition cmp pivot xs = ``` haftmann@69246 ` 423` ``` ([x \ xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \ xs. compare cmp x pivot = Greater])" ``` haftmann@69246 ` 424` haftmann@69246 ` 425` ```qualified lemma partition_code [code]: ``` haftmann@69246 ` 426` ``` "partition cmp pivot [] = ([], [], [])" ``` haftmann@69246 ` 427` ``` "partition cmp pivot (x # xs) = ``` haftmann@69246 ` 428` ``` (let (lts, eqs, gts) = partition cmp pivot xs ``` haftmann@69246 ` 429` ``` in case compare cmp x pivot of ``` haftmann@69246 ` 430` ``` Less \ (x # lts, eqs, gts) ``` haftmann@69246 ` 431` ``` | Equiv \ (lts, x # eqs, gts) ``` haftmann@69246 ` 432` ``` | Greater \ (lts, eqs, x # gts))" ``` haftmann@69246 ` 433` ``` using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot]) ``` haftmann@69246 ` 434` haftmann@69246 ` 435` ```lemma quicksort_code [code]: ``` haftmann@69246 ` 436` ``` "quicksort cmp xs = ``` haftmann@69246 ` 437` ``` (case xs of ``` haftmann@69246 ` 438` ``` [] \ [] ``` haftmann@69246 ` 439` ``` | [x] \ xs ``` haftmann@69246 ` 440` ``` | [x, y] \ (if compare cmp x y \ Greater then xs else [y, x]) ``` haftmann@69246 ` 441` ``` | _ \ ``` haftmann@69246 ` 442` ``` let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs ``` haftmann@69246 ` 443` ``` in quicksort cmp lts @ eqs @ quicksort cmp gts)" ``` haftmann@69246 ` 444` ```proof (cases "length xs \ 3") ``` haftmann@69246 ` 445` ``` case False ``` haftmann@69250 ` 446` ``` then have "length xs \ {0, 1, 2}" ``` haftmann@69250 ` 447` ``` by (auto simp add: not_le le_less less_antisym) ``` haftmann@69246 ` 448` ``` then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]" ``` haftmann@69246 ` 449` ``` by (auto simp add: length_Suc_conv numeral_2_eq_2) ``` haftmann@69246 ` 450` ``` then show ?thesis ``` haftmann@69246 ` 451` ``` by cases simp_all ``` haftmann@69246 ` 452` ```next ``` haftmann@69246 ` 453` ``` case True ``` haftmann@69246 ` 454` ``` then obtain x y z zs where "xs = x # y # z # zs" ``` haftmann@69246 ` 455` ``` by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3) ``` haftmann@69246 ` 456` ``` moreover have "quicksort cmp xs = ``` haftmann@69246 ` 457` ``` (let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs ``` haftmann@69246 ` 458` ``` in quicksort cmp lts @ eqs @ quicksort cmp gts)" ``` haftmann@69246 ` 459` ``` using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def) ``` haftmann@69246 ` 460` ``` ultimately show ?thesis ``` haftmann@69246 ` 461` ``` by simp ``` haftmann@69246 ` 462` ```qed ``` haftmann@69246 ` 463` haftmann@69194 ` 464` ```end ``` haftmann@69246 ` 465` haftmann@69250 ` 466` haftmann@69250 ` 467` ```subsection \Mergesort\ ``` haftmann@69250 ` 468` haftmann@69250 ` 469` ```definition mergesort :: "'a comparator \ 'a list \ 'a list" ``` haftmann@69250 ` 470` ``` where mergesort_is_sort [simp]: "mergesort = sort" ``` haftmann@69250 ` 471` haftmann@69250 ` 472` ```lemma sort_by_mergesort: ``` haftmann@69250 ` 473` ``` "sort = mergesort" ``` haftmann@69250 ` 474` ``` by simp ``` haftmann@69250 ` 475` haftmann@69250 ` 476` ```context ``` haftmann@69250 ` 477` ``` fixes cmp :: "'a comparator" ``` haftmann@69250 ` 478` ```begin ``` haftmann@69250 ` 479` haftmann@69250 ` 480` ```qualified function merge :: "'a list \ 'a list \ 'a list" ``` haftmann@69250 ` 481` ``` where "merge [] ys = ys" ``` haftmann@69250 ` 482` ``` | "merge xs [] = xs" ``` haftmann@69250 ` 483` ``` | "merge (x # xs) (y # ys) = (if compare cmp x y = Greater ``` haftmann@69250 ` 484` ``` then y # merge (x # xs) ys else x # merge xs (y # ys))" ``` haftmann@69250 ` 485` ``` by pat_completeness auto ``` haftmann@69250 ` 486` haftmann@69250 ` 487` ```qualified termination by lexicographic_order ``` haftmann@69250 ` 488` haftmann@69250 ` 489` ```lemma mset_merge: ``` haftmann@69250 ` 490` ``` "mset (merge xs ys) = mset xs + mset ys" ``` haftmann@69250 ` 491` ``` by (induction xs ys rule: merge.induct) simp_all ``` haftmann@69250 ` 492` haftmann@69250 ` 493` ```lemma merge_eq_Cons_imp: ``` haftmann@69250 ` 494` ``` "xs \ [] \ z = hd xs \ ys \ [] \ z = hd ys" ``` haftmann@69250 ` 495` ``` if "merge xs ys = z # zs" ``` haftmann@69250 ` 496` ``` using that by (induction xs ys rule: merge.induct) (auto split: if_splits) ``` haftmann@69250 ` 497` haftmann@69250 ` 498` ```lemma filter_merge: ``` haftmann@69250 ` 499` ``` "filter P (merge xs ys) = merge (filter P xs) (filter P ys)" ``` haftmann@69250 ` 500` ``` if "sorted cmp xs" and "sorted cmp ys" ``` haftmann@69250 ` 501` ```using that proof (induction xs ys rule: merge.induct) ``` haftmann@69250 ` 502` ``` case (1 ys) ``` haftmann@69250 ` 503` ``` then show ?case ``` haftmann@69250 ` 504` ``` by simp ``` haftmann@69250 ` 505` ```next ``` haftmann@69250 ` 506` ``` case (2 xs) ``` haftmann@69250 ` 507` ``` then show ?case ``` haftmann@69250 ` 508` ``` by simp ``` haftmann@69250 ` 509` ```next ``` haftmann@69250 ` 510` ``` case (3 x xs y ys) ``` haftmann@69250 ` 511` ``` show ?case ``` haftmann@69250 ` 512` ``` proof (cases "compare cmp x y = Greater") ``` haftmann@69250 ` 513` ``` case True ``` haftmann@69250 ` 514` ``` with 3 have hyp: "filter P (merge (x # xs) ys) = ``` haftmann@69250 ` 515` ``` merge (filter P (x # xs)) (filter P ys)" ``` haftmann@69250 ` 516` ``` by (simp add: sorted_Cons_imp_sorted) ``` haftmann@69250 ` 517` ``` show ?thesis ``` haftmann@69250 ` 518` ``` proof (cases "\ P x \ P y") ``` haftmann@69250 ` 519` ``` case False ``` haftmann@69250 ` 520` ``` with \compare cmp x y = Greater\ show ?thesis ``` haftmann@69250 ` 521` ``` by (auto simp add: hyp) ``` haftmann@69250 ` 522` ``` next ``` haftmann@69250 ` 523` ``` case True ``` haftmann@69250 ` 524` ``` from \compare cmp x y = Greater\ "3.prems" ``` haftmann@69250 ` 525` ``` have *: "compare cmp z y = Greater" if "z \ set (filter P xs)" for z ``` haftmann@69250 ` 526` ``` using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less) ``` haftmann@69250 ` 527` ``` from \compare cmp x y = Greater\ show ?thesis ``` haftmann@69250 ` 528` ``` by (cases "filter P xs") (simp_all add: hyp *) ``` haftmann@69250 ` 529` ``` qed ``` haftmann@69250 ` 530` ``` next ``` haftmann@69250 ` 531` ``` case False ``` haftmann@69250 ` 532` ``` with 3 have hyp: "filter P (merge xs (y # ys)) = ``` haftmann@69250 ` 533` ``` merge (filter P xs) (filter P (y # ys))" ``` haftmann@69250 ` 534` ``` by (simp add: sorted_Cons_imp_sorted) ``` haftmann@69250 ` 535` ``` show ?thesis ``` haftmann@69250 ` 536` ``` proof (cases "P x \ \ P y") ``` haftmann@69250 ` 537` ``` case False ``` haftmann@69250 ` 538` ``` with \compare cmp x y \ Greater\ show ?thesis ``` haftmann@69250 ` 539` ``` by (auto simp add: hyp) ``` haftmann@69250 ` 540` ``` next ``` haftmann@69250 ` 541` ``` case True ``` haftmann@69250 ` 542` ``` from \compare cmp x y \ Greater\ "3.prems" ``` haftmann@69250 ` 543` ``` have *: "compare cmp x z \ Greater" if "z \ set (filter P ys)" for z ``` haftmann@69250 ` 544` ``` using that by (auto dest: compare.trans_not_greater sorted_Cons_imp_not_less) ``` haftmann@69250 ` 545` ``` from \compare cmp x y \ Greater\ show ?thesis ``` haftmann@69250 ` 546` ``` by (cases "filter P ys") (simp_all add: hyp *) ``` haftmann@69250 ` 547` ``` qed ``` haftmann@69250 ` 548` ``` qed ``` haftmann@69250 ` 549` ```qed ``` haftmann@69246 ` 550` haftmann@69250 ` 551` ```lemma sorted_merge: ``` haftmann@69250 ` 552` ``` "sorted cmp (merge xs ys)" if "sorted cmp xs" and "sorted cmp ys" ``` haftmann@69250 ` 553` ```using that proof (induction xs ys rule: merge.induct) ``` haftmann@69250 ` 554` ``` case (1 ys) ``` haftmann@69250 ` 555` ``` then show ?case ``` haftmann@69250 ` 556` ``` by simp ``` haftmann@69250 ` 557` ```next ``` haftmann@69250 ` 558` ``` case (2 xs) ``` haftmann@69250 ` 559` ``` then show ?case ``` haftmann@69250 ` 560` ``` by simp ``` haftmann@69250 ` 561` ```next ``` haftmann@69250 ` 562` ``` case (3 x xs y ys) ``` haftmann@69250 ` 563` ``` show ?case ``` haftmann@69250 ` 564` ``` proof (cases "compare cmp x y = Greater") ``` haftmann@69250 ` 565` ``` case True ``` haftmann@69250 ` 566` ``` with 3 have "sorted cmp (merge (x # xs) ys)" ``` haftmann@69250 ` 567` ``` by (simp add: sorted_Cons_imp_sorted) ``` haftmann@69250 ` 568` ``` then have "sorted cmp (y # merge (x # xs) ys)" ``` haftmann@69250 ` 569` ``` proof (rule sorted_ConsI) ``` haftmann@69250 ` 570` ``` fix z zs ``` haftmann@69250 ` 571` ``` assume "merge (x # xs) ys = z # zs" ``` haftmann@69250 ` 572` ``` with 3(4) True show "compare cmp y z \ Greater" ``` haftmann@69250 ` 573` ``` by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp) ``` haftmann@69250 ` 574` ``` (auto simp add: compare.asym_greater sorted_Cons_imp_not_less) ``` haftmann@69250 ` 575` ``` qed ``` haftmann@69250 ` 576` ``` with True show ?thesis ``` haftmann@69250 ` 577` ``` by simp ``` haftmann@69250 ` 578` ``` next ``` haftmann@69250 ` 579` ``` case False ``` haftmann@69250 ` 580` ``` with 3 have "sorted cmp (merge xs (y # ys))" ``` haftmann@69250 ` 581` ``` by (simp add: sorted_Cons_imp_sorted) ``` haftmann@69250 ` 582` ``` then have "sorted cmp (x # merge xs (y # ys))" ``` haftmann@69250 ` 583` ``` proof (rule sorted_ConsI) ``` haftmann@69250 ` 584` ``` fix z zs ``` haftmann@69250 ` 585` ``` assume "merge xs (y # ys) = z # zs" ``` haftmann@69250 ` 586` ``` with 3(3) False show "compare cmp x z \ Greater" ``` haftmann@69250 ` 587` ``` by (clarsimp simp add: sorted_Cons_imp_sorted dest!: merge_eq_Cons_imp) ``` haftmann@69250 ` 588` ``` (auto simp add: compare.asym_greater sorted_Cons_imp_not_less) ``` haftmann@69250 ` 589` ``` qed ``` haftmann@69250 ` 590` ``` with False show ?thesis ``` haftmann@69250 ` 591` ``` by simp ``` haftmann@69250 ` 592` ``` qed ``` haftmann@69250 ` 593` ```qed ``` haftmann@69250 ` 594` haftmann@69250 ` 595` ```lemma merge_eq_appendI: ``` haftmann@69250 ` 596` ``` "merge xs ys = xs @ ys" ``` haftmann@69250 ` 597` ``` if "\x y. x \ set xs \ y \ set ys \ compare cmp x y \ Greater" ``` haftmann@69250 ` 598` ``` using that by (induction xs ys rule: merge.induct) simp_all ``` haftmann@69250 ` 599` haftmann@69250 ` 600` ```lemma merge_stable_segments: ``` haftmann@69250 ` 601` ``` "merge (stable_segment cmp l xs) (stable_segment cmp l ys) = ``` haftmann@69250 ` 602` ``` stable_segment cmp l xs @ stable_segment cmp l ys" ``` haftmann@69250 ` 603` ``` by (rule merge_eq_appendI) (auto dest: compare.trans_equiv_greater) ``` haftmann@69250 ` 604` haftmann@69250 ` 605` ```lemma sort_by_mergesort_rec: ``` haftmann@69250 ` 606` ``` "sort cmp xs = ``` haftmann@69250 ` 607` ``` merge (sort cmp (take (length xs div 2) xs)) ``` haftmann@69250 ` 608` ``` (sort cmp (drop (length xs div 2) xs))" (is "_ = ?rhs") ``` haftmann@69250 ` 609` ```proof (rule sort_eqI) ``` haftmann@69250 ` 610` ``` have "mset (take (length xs div 2) xs) + mset (drop (length xs div 2) xs) = ``` haftmann@69250 ` 611` ``` mset (take (length xs div 2) xs @ drop (length xs div 2) xs)" ``` haftmann@69250 ` 612` ``` by (simp only: mset_append) ``` haftmann@69250 ` 613` ``` then show "mset xs = mset ?rhs" ``` haftmann@69250 ` 614` ``` by (simp add: mset_merge) ``` haftmann@69250 ` 615` ```next ``` haftmann@69250 ` 616` ``` show "sorted cmp ?rhs" ``` haftmann@69250 ` 617` ``` by (simp add: sorted_merge) ``` haftmann@69250 ` 618` ```next ``` haftmann@69250 ` 619` ``` fix l ``` haftmann@69250 ` 620` ``` have "stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs) ``` haftmann@69250 ` 621` ``` = stable_segment cmp l xs" ``` haftmann@69250 ` 622` ``` by (simp only: filter_append [symmetric] append_take_drop_id) ``` haftmann@69250 ` 623` ``` have "merge (stable_segment cmp l (take (length xs div 2) xs)) ``` haftmann@69250 ` 624` ``` (stable_segment cmp l (drop (length xs div 2) xs)) = ``` haftmann@69250 ` 625` ``` stable_segment cmp l (take (length xs div 2) xs) @ stable_segment cmp l (drop (length xs div 2) xs)" ``` haftmann@69250 ` 626` ``` by (rule merge_eq_appendI) (auto simp add: compare.trans_equiv_greater) ``` haftmann@69250 ` 627` ``` also have "\ = stable_segment cmp l xs" ``` haftmann@69250 ` 628` ``` by (simp only: filter_append [symmetric] append_take_drop_id) ``` haftmann@69250 ` 629` ``` finally show "stable_segment cmp l xs = stable_segment cmp l ?rhs" ``` haftmann@69250 ` 630` ``` by (simp add: stable_sort filter_merge) ``` haftmann@69250 ` 631` ```qed ``` haftmann@69250 ` 632` haftmann@69250 ` 633` ```lemma mergesort_code [code]: ``` haftmann@69250 ` 634` ``` "mergesort cmp xs = ``` haftmann@69250 ` 635` ``` (case xs of ``` haftmann@69250 ` 636` ``` [] \ [] ``` haftmann@69250 ` 637` ``` | [x] \ xs ``` haftmann@69250 ` 638` ``` | [x, y] \ (if compare cmp x y \ Greater then xs else [y, x]) ``` haftmann@69250 ` 639` ``` | _ \ ``` haftmann@69250 ` 640` ``` let ``` haftmann@69250 ` 641` ``` half = length xs div 2; ``` haftmann@69250 ` 642` ``` ys = take half xs; ``` haftmann@69250 ` 643` ``` zs = drop half xs ``` haftmann@69250 ` 644` ``` in merge (mergesort cmp ys) (mergesort cmp zs))" ``` haftmann@69250 ` 645` ```proof (cases "length xs \ 3") ``` haftmann@69250 ` 646` ``` case False ``` haftmann@69250 ` 647` ``` then have "length xs \ {0, 1, 2}" ``` haftmann@69250 ` 648` ``` by (auto simp add: not_le le_less less_antisym) ``` haftmann@69250 ` 649` ``` then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]" ``` haftmann@69250 ` 650` ``` by (auto simp add: length_Suc_conv numeral_2_eq_2) ``` haftmann@69250 ` 651` ``` then show ?thesis ``` haftmann@69250 ` 652` ``` by cases simp_all ``` haftmann@69250 ` 653` ```next ``` haftmann@69250 ` 654` ``` case True ``` haftmann@69250 ` 655` ``` then obtain x y z zs where "xs = x # y # z # zs" ``` haftmann@69250 ` 656` ``` by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3) ``` haftmann@69250 ` 657` ``` moreover have "mergesort cmp xs = ``` haftmann@69250 ` 658` ``` (let ``` haftmann@69250 ` 659` ``` half = length xs div 2; ``` haftmann@69250 ` 660` ``` ys = take half xs; ``` haftmann@69250 ` 661` ``` zs = drop half xs ``` haftmann@69250 ` 662` ``` in merge (mergesort cmp ys) (mergesort cmp zs))" ``` haftmann@69250 ` 663` ``` using sort_by_mergesort_rec [of xs] by (simp add: Let_def) ``` haftmann@69250 ` 664` ``` ultimately show ?thesis ``` haftmann@69250 ` 665` ``` by simp ``` haftmann@69250 ` 666` ```qed ``` haftmann@69246 ` 667` haftmann@69246 ` 668` ```end ``` haftmann@69250 ` 669` haftmann@69250 ` 670` ```end ```