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 \<open>Stably sorted lists\<close>
haftmann@69194
    10
haftmann@69194
    11
abbreviation (input) stable_segment :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@69194
    12
  where "stable_segment cmp x \<equiv> filter (\<lambda>y. compare cmp x y = Equiv)"
haftmann@69194
    13
haftmann@69194
    14
fun sorted :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@69194
    15
  where sorted_Nil: "sorted cmp [] \<longleftrightarrow> True"
haftmann@69194
    16
  | sorted_single: "sorted cmp [x] \<longleftrightarrow> True"
haftmann@69246
    17
  | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> 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 "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> 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 \<noteq> Greater" if "sorted cmp (y # xs)"
haftmann@69246
    30
    and "x \<in> 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 *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P xs
haftmann@69246
    36
      \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)"
haftmann@69194
    37
using \<open>sorted cmp xs\<close> proof (induction xs)
haftmann@69194
    38
  case Nil
haftmann@69194
    39
  show ?case
haftmann@69194
    40
    by (rule \<open>P []\<close>)
haftmann@69194
    41
next
haftmann@69194
    42
  case (Cons x xs)
haftmann@69194
    43
  from \<open>sorted cmp (x # xs)\<close> have "sorted cmp xs"
haftmann@69194
    44
    by (cases xs) simp_all
haftmann@69194
    45
  moreover have "P xs" using \<open>sorted cmp xs\<close>
haftmann@69194
    46
    by (rule Cons.IH)
haftmann@69246
    47
  moreover have "compare cmp x y \<noteq> Greater" if "y \<in> set xs" for y
haftmann@69194
    48
  using that \<open>sorted cmp (x # xs)\<close> 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 \<noteq> Greater" "compare cmp x z \<noteq> Greater"
haftmann@69194
    62
        by auto
haftmann@69246
    63
      then have "compare cmp x w \<noteq> 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 *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs)
haftmann@69246
    76
      \<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater)
haftmann@69194
    77
    \<Longrightarrow> P xs"
haftmann@69194
    78
using \<open>sorted cmp xs\<close> proof (induction xs)
haftmann@69194
    79
  case Nil
haftmann@69194
    80
  show ?case
haftmann@69194
    81
    by (rule \<open>P []\<close>)
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 "\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> 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 \<in> 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 \<open>x \<noteq> y\<close> have "z \<in> set ys"
haftmann@69194
   120
          using notin_set_remove1 [of z ys x] by auto
haftmann@69246
   121
        then show "compare cmp y z \<noteq> 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 \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
haftmann@69194
   145
  where "insort cmp y [] = [y]"
haftmann@69194
   146
  | "insort cmp y (x # xs) = (if compare cmp y x \<noteq> 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 \<Longrightarrow> 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 \<noteq> 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" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> 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 \<noteq> 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 \<noteq> Greater" if "y \<in> 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 \<in> 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 \<noteq> 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) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys
haftmann@69246
   251
     \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. compare cmp x y \<noteq> Greater)" (is "?P \<longleftrightarrow> ?R \<and> ?S \<and> ?Q")
haftmann@69246
   252
proof
haftmann@69246
   253
  assume ?P
haftmann@69246
   254
  have ?R
haftmann@69246
   255
    using \<open>?P\<close> 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 \<open>?P\<close> by (induction xs) (auto dest: sorted_Cons_imp_sorted)
haftmann@69246
   260
  moreover have ?Q
haftmann@69246
   261
    using \<open>?P\<close> 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 \<and> ?S \<and> ?Q"
haftmann@69246
   264
    by simp
haftmann@69246
   265
next
haftmann@69246
   266
  assume "?R \<and> ?S \<and> ?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 \<Rightarrow> 'a list \<Rightarrow> '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: "\<And>y. y \<in> set ys \<Longrightarrow>
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 "\<exists>x\<in>set ys. compare cmp y x = Equiv")
haftmann@69194
   320
    case True
haftmann@69194
   321
    then obtain z where "z \<in> set ys" and "compare cmp y z = Equiv"
haftmann@69194
   322
      by auto
haftmann@69194
   323
    then have "compare cmp y x = Equiv \<longleftrightarrow> 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 \<open>z \<in> set ys\<close> 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 \<open>mset ys = mset xs\<close> have ys: "set ys = set xs"
haftmann@69194
   345
      by (rule mset_eq_setD)
haftmann@69246
   346
    then have "compare cmp x y \<noteq> Greater" if "y \<in> 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 "\<not> 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 \<open>Alternative sorting algorithms\<close>
haftmann@69246
   382
haftmann@69246
   383
subsection \<open>Quicksort\<close>
haftmann@69246
   384
haftmann@69246
   385
definition quicksort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> '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\<leftarrow>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\<leftarrow>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 \<and> compare cmp l x = Equiv
haftmann@69246
   406
    \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp
haftmann@69246
   407
  proof -
haftmann@69246
   408
    have "compare cmp x ?pivot = comp \<longleftrightarrow> 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 \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list"
haftmann@69246
   422
  where "partition cmp pivot xs =
haftmann@69246
   423
    ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> 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 \<Rightarrow> (x # lts, eqs, gts)
haftmann@69246
   431
     | Equiv \<Rightarrow> (lts, x # eqs, gts)
haftmann@69246
   432
     | Greater \<Rightarrow> (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
      [] \<Rightarrow> []
haftmann@69246
   439
    | [x] \<Rightarrow> xs
haftmann@69246
   440
    | [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x])
haftmann@69246
   441
    | _ \<Rightarrow>
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 \<ge> 3")
haftmann@69246
   445
  case False
haftmann@69250
   446
  then have "length xs \<in> {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 \<open>Mergesort\<close>
haftmann@69250
   468
haftmann@69250
   469
definition mergesort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> '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 \<Rightarrow> 'a list \<Rightarrow> '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 \<noteq> [] \<and> z = hd xs \<or> ys \<noteq> [] \<and> 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 "\<not> P x \<and> P y")
haftmann@69250
   519
      case False
haftmann@69250
   520
      with \<open>compare cmp x y = Greater\<close> show ?thesis
haftmann@69250
   521
        by (auto simp add: hyp)
haftmann@69250
   522
    next
haftmann@69250
   523
      case True
haftmann@69250
   524
      from \<open>compare cmp x y = Greater\<close> "3.prems"
haftmann@69250
   525
      have *: "compare cmp z y = Greater" if "z \<in> 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 \<open>compare cmp x y = Greater\<close> 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 \<and> \<not> P y")
haftmann@69250
   537
      case False
haftmann@69250
   538
      with \<open>compare cmp x y \<noteq> Greater\<close> show ?thesis
haftmann@69250
   539
        by (auto simp add: hyp)
haftmann@69250
   540
    next
haftmann@69250
   541
      case True
haftmann@69250
   542
      from \<open>compare cmp x y \<noteq> Greater\<close> "3.prems"
haftmann@69250
   543
      have *: "compare cmp x z \<noteq> Greater" if "z \<in> 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 \<open>compare cmp x y \<noteq> Greater\<close> 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 \<noteq> 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 \<noteq> 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 "\<And>x y. x \<in> set xs \<Longrightarrow> y \<in> set ys \<Longrightarrow> compare cmp x y \<noteq> 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 "\<dots> = 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
      [] \<Rightarrow> []
haftmann@69250
   637
    | [x] \<Rightarrow> xs
haftmann@69250
   638
    | [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x])
haftmann@69250
   639
    | _ \<Rightarrow>
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 \<ge> 3")
haftmann@69250
   646
  case False
haftmann@69250
   647
  then have "length xs \<in> {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