concrecte sorting algorithms beyond insertion sort
authorhaftmann
Sun Nov 04 15:00:30 2018 +0000 (6 months ago)
changeset 69246c1fe9dcc274a
parent 69245 3e9f812c308c
child 69249 27423819534c
concrecte sorting algorithms beyond insertion sort
src/HOL/Library/Comparator.thy
src/HOL/Library/Sorting_Algorithms.thy
     1.1 --- a/src/HOL/Library/Comparator.thy	Mon Nov 05 23:15:58 2018 +0100
     1.2 +++ b/src/HOL/Library/Comparator.thy	Sun Nov 04 15:00:30 2018 +0000
     1.3 @@ -76,6 +76,24 @@
     1.4    "asymp (\<lambda>a b. cmp a b = Greater)"
     1.5    using irreflp_greater by (auto intro!: asympI dest: asym_greater)
     1.6  
     1.7 +lemma trans_equiv_less:
     1.8 +  "cmp a c = Less" if "cmp a b = Equiv" and "cmp b c = Less"
     1.9 +  using that
    1.10 +  by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
    1.11 +
    1.12 +lemma trans_less_equiv:
    1.13 +  "cmp a c = Less" if "cmp a b = Less" and "cmp b c = Equiv"
    1.14 +  using that
    1.15 +  by (metis (full_types) comp.exhaust greater_iff_sym_less trans_equiv trans_less)
    1.16 +
    1.17 +lemma trans_equiv_greater:
    1.18 +  "cmp a c = Greater" if "cmp a b = Equiv" and "cmp b c = Greater"
    1.19 +  using that by (simp add: sym [of a b] greater_iff_sym_less trans_less_equiv)
    1.20 +
    1.21 +lemma trans_greater_equiv:
    1.22 +  "cmp a c = Greater" if "cmp a b = Greater" and "cmp b c = Equiv"
    1.23 +  using that by (simp add: sym [of b c] greater_iff_sym_less trans_equiv_less)
    1.24 +
    1.25  lemma transp_less:
    1.26    "transp (\<lambda>a b. cmp a b = Less)"
    1.27    by (rule transpI) (fact trans_less)
    1.28 @@ -118,6 +136,26 @@
    1.29    "transp (\<lambda>a b. cmp a b \<noteq> Greater)"
    1.30    by (rule transpI) (fact trans_not_greater)
    1.31  
    1.32 +text \<open>Substitution under equivalences\<close>
    1.33 +
    1.34 +lemma equiv_subst_left:
    1.35 +  "cmp z y = comp \<longleftrightarrow> cmp x y = comp" if "cmp z x = Equiv" for comp
    1.36 +proof -
    1.37 +  from that have "cmp x z = Equiv"
    1.38 +    by (simp add: sym)
    1.39 +  with that show ?thesis
    1.40 +    by (cases comp) (auto intro: trans_equiv trans_equiv_less trans_equiv_greater)
    1.41 +qed
    1.42 +
    1.43 +lemma equiv_subst_right:
    1.44 +  "cmp x z = comp \<longleftrightarrow> cmp x y = comp" if "cmp z y = Equiv" for comp
    1.45 +proof -
    1.46 +  from that have "cmp y z = Equiv"
    1.47 +    by (simp add: sym)
    1.48 +  with that show ?thesis
    1.49 +    by (cases comp) (auto intro: trans_equiv trans_less_equiv trans_greater_equiv)
    1.50 +qed
    1.51 +
    1.52  end
    1.53  
    1.54  typedef 'a comparator = "{cmp :: 'a \<Rightarrow> 'a \<Rightarrow> comp. comparator cmp}"
     2.1 --- a/src/HOL/Library/Sorting_Algorithms.thy	Mon Nov 05 23:15:58 2018 +0100
     2.2 +++ b/src/HOL/Library/Sorting_Algorithms.thy	Sun Nov 04 15:00:30 2018 +0000
     2.3 @@ -6,11 +6,6 @@
     2.4    imports Main Multiset Comparator
     2.5  begin
     2.6  
     2.7 -text \<open>Prelude\<close>
     2.8 -
     2.9 -hide_const (open) sorted insort sort
    2.10 -
    2.11 -
    2.12  section \<open>Stably sorted lists\<close>
    2.13  
    2.14  abbreviation (input) stable_segment :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
    2.15 @@ -19,17 +14,26 @@
    2.16  fun sorted :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> bool"
    2.17    where sorted_Nil: "sorted cmp [] \<longleftrightarrow> True"
    2.18    | sorted_single: "sorted cmp [x] \<longleftrightarrow> True"
    2.19 -  | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp x y \<noteq> Less \<and> sorted cmp (x # xs)"
    2.20 +  | sorted_rec: "sorted cmp (y # x # xs) \<longleftrightarrow> compare cmp y x \<noteq> Greater \<and> sorted cmp (x # xs)"
    2.21  
    2.22  lemma sorted_ConsI:
    2.23    "sorted cmp (x # xs)" if "sorted cmp xs"
    2.24 -    and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp y x \<noteq> Less"
    2.25 +    and "\<And>y ys. xs = y # ys \<Longrightarrow> compare cmp x y \<noteq> Greater"
    2.26 +  using that by (cases xs) simp_all
    2.27 +
    2.28 +lemma sorted_Cons_imp_sorted:
    2.29 +  "sorted cmp xs" if "sorted cmp (x # xs)"
    2.30    using that by (cases xs) simp_all
    2.31  
    2.32 +lemma sorted_Cons_imp_not_less:
    2.33 +  "compare cmp y x \<noteq> Greater" if "sorted cmp (y # xs)"
    2.34 +    and "x \<in> set xs"
    2.35 +  using that by (induction xs arbitrary: y) (auto dest: compare.trans_not_greater)
    2.36 +
    2.37  lemma sorted_induct [consumes 1, case_names Nil Cons, induct pred: sorted]:
    2.38    "P xs" if "sorted cmp xs" and "P []"
    2.39      and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P xs
    2.40 -      \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp y x \<noteq> Less) \<Longrightarrow> P (x # xs)"
    2.41 +      \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater) \<Longrightarrow> P (x # xs)"
    2.42  using \<open>sorted cmp xs\<close> proof (induction xs)
    2.43    case Nil
    2.44    show ?case
    2.45 @@ -40,7 +44,7 @@
    2.46      by (cases xs) simp_all
    2.47    moreover have "P xs" using \<open>sorted cmp xs\<close>
    2.48      by (rule Cons.IH)
    2.49 -  moreover have "compare cmp y x \<noteq> Less" if "y \<in> set xs" for y
    2.50 +  moreover have "compare cmp x y \<noteq> Greater" if "y \<in> set xs" for y
    2.51    using that \<open>sorted cmp (x # xs)\<close> proof (induction xs)
    2.52      case Nil
    2.53      then show ?case
    2.54 @@ -54,10 +58,10 @@
    2.55          by simp
    2.56      next
    2.57        case (Cons w ws)
    2.58 -      with Cons.prems have "compare cmp w z \<noteq> Less" "compare cmp z x \<noteq> Less"
    2.59 +      with Cons.prems have "compare cmp z w \<noteq> Greater" "compare cmp x z \<noteq> Greater"
    2.60          by auto
    2.61 -      then have "compare cmp w x \<noteq> Less"
    2.62 -        by (auto dest: compare.trans_not_less)
    2.63 +      then have "compare cmp x w \<noteq> Greater"
    2.64 +        by (auto dest: compare.trans_not_greater)
    2.65        with Cons show ?thesis
    2.66          using Cons.prems Cons.IH by auto
    2.67      qed
    2.68 @@ -69,7 +73,7 @@
    2.69  lemma sorted_induct_remove1 [consumes 1, case_names Nil minimum]:
    2.70    "P xs" if "sorted cmp xs" and "P []"
    2.71      and *: "\<And>x xs. sorted cmp xs \<Longrightarrow> P (remove1 x xs)
    2.72 -      \<Longrightarrow> x \<in> set xs \<Longrightarrow> hd (stable_segment cmp x xs) = x \<Longrightarrow> (\<And>y. y \<in> set xs \<Longrightarrow> compare cmp y x \<noteq> Less)
    2.73 +      \<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)
    2.74      \<Longrightarrow> P xs"
    2.75  using \<open>sorted cmp xs\<close> proof (induction xs)
    2.76    case Nil
    2.77 @@ -80,7 +84,7 @@
    2.78    then have "sorted cmp (x # xs)"
    2.79      by (simp add: sorted_ConsI)
    2.80    moreover note Cons.IH
    2.81 -  moreover have "\<And>y. compare cmp y x = Less \<Longrightarrow> y \<in> set xs \<Longrightarrow> False"
    2.82 +  moreover have "\<And>y. compare cmp x y = Greater \<Longrightarrow> y \<in> set xs \<Longrightarrow> False"
    2.83      using Cons.hyps by simp
    2.84    ultimately show ?case
    2.85      by (auto intro!: * [of "x # xs" x]) blast
    2.86 @@ -114,7 +118,7 @@
    2.87          assume "remove1 x ys = z # zs"
    2.88          with \<open>x \<noteq> y\<close> have "z \<in> set ys"
    2.89            using notin_set_remove1 [of z ys x] by auto
    2.90 -        then show "compare cmp z y \<noteq> Less"
    2.91 +        then show "compare cmp y z \<noteq> Greater"
    2.92            by (rule Cons.hyps(2))
    2.93        qed
    2.94        with False show ?thesis
    2.95 @@ -123,6 +127,20 @@
    2.96    qed
    2.97  qed
    2.98  
    2.99 +lemma sorted_stable_segment:
   2.100 +  "sorted cmp (stable_segment cmp x xs)"
   2.101 +proof (induction xs)
   2.102 +  case Nil
   2.103 +  show ?case
   2.104 +    by simp
   2.105 +next
   2.106 +  case (Cons y ys)
   2.107 +  then show ?case
   2.108 +    by (auto intro!: sorted_ConsI simp add: filter_eq_Cons_iff compare.sym)
   2.109 +      (auto dest: compare.trans_equiv simp add: compare.sym compare.greater_iff_sym_less)
   2.110 +
   2.111 +qed
   2.112 +
   2.113  primrec insort :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
   2.114    where "insort cmp y [] = [y]"
   2.115    | "insort cmp y (x # xs) = (if compare cmp y x \<noteq> Greater
   2.116 @@ -175,7 +193,7 @@
   2.117  
   2.118  lemma insort_eq_ConsI:
   2.119    "insort cmp x xs = x # xs"
   2.120 -    if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp y x \<noteq> Less"
   2.121 +    if "sorted cmp xs" "\<And>y. y \<in> set xs \<Longrightarrow> compare cmp x y \<noteq> Greater"
   2.122    using that by (induction xs) (simp_all add: compare.greater_iff_sym_less)
   2.123  
   2.124  lemma remove1_insort_not_same_eq [simp]:
   2.125 @@ -188,14 +206,15 @@
   2.126  next
   2.127    case (Cons z zs)
   2.128    show ?case
   2.129 -  proof (cases "compare cmp z x = Less")
   2.130 +  proof (cases "compare cmp x z = Greater")
   2.131      case True
   2.132      with Cons show ?thesis
   2.133 -      by (simp add: compare.greater_iff_sym_less)
   2.134 +      by simp
   2.135    next
   2.136      case False
   2.137 -    have "compare cmp y x \<noteq> Less" if "y \<in> set zs" for y
   2.138 -      using that False Cons.hyps by (auto dest: compare.trans_not_less)
   2.139 +    then have "compare cmp x y \<noteq> Greater" if "y \<in> set zs" for y
   2.140 +      using that Cons.hyps
   2.141 +      by (auto dest: compare.trans_not_greater)
   2.142      with Cons show ?thesis
   2.143        by (simp add: insort_eq_ConsI)
   2.144    qed
   2.145 @@ -211,7 +230,7 @@
   2.146  next
   2.147    case (Cons y ys)
   2.148    then have "compare cmp x y \<noteq> Less"
   2.149 -    by auto
   2.150 +    by (auto simp add: compare.greater_iff_sym_less)
   2.151    then consider "compare cmp x y = Greater" | "compare cmp x y = Equiv"
   2.152      by (cases "compare cmp x y") auto
   2.153    then show ?case proof cases
   2.154 @@ -227,6 +246,31 @@
   2.155    qed
   2.156  qed
   2.157  
   2.158 +lemma sorted_append_iff:
   2.159 +  "sorted cmp (xs @ ys) \<longleftrightarrow> sorted cmp xs \<and> sorted cmp ys
   2.160 +     \<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")
   2.161 +proof
   2.162 +  assume ?P
   2.163 +  have ?R
   2.164 +    using \<open>?P\<close> by (induction xs)
   2.165 +      (auto simp add: sorted_Cons_imp_not_less,
   2.166 +        auto simp add: sorted_Cons_imp_sorted intro: sorted_ConsI)
   2.167 +  moreover have ?S
   2.168 +    using \<open>?P\<close> by (induction xs) (auto dest: sorted_Cons_imp_sorted)
   2.169 +  moreover have ?Q
   2.170 +    using \<open>?P\<close> by (induction xs) (auto simp add: sorted_Cons_imp_not_less,
   2.171 +      simp add: sorted_Cons_imp_sorted)
   2.172 +  ultimately show "?R \<and> ?S \<and> ?Q"
   2.173 +    by simp
   2.174 +next
   2.175 +  assume "?R \<and> ?S \<and> ?Q"
   2.176 +  then have ?R ?S ?Q
   2.177 +    by simp_all
   2.178 +  then show ?P
   2.179 +    by (induction xs)
   2.180 +      (auto simp add: append_eq_Cons_conv intro!: sorted_ConsI)
   2.181 +qed
   2.182 +
   2.183  definition sort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
   2.184    where "sort cmp xs = foldr (insort cmp) xs []"
   2.185  
   2.186 @@ -299,7 +343,7 @@
   2.187      case (minimum x xs)
   2.188      from \<open>mset ys = mset xs\<close> have ys: "set ys = set xs"
   2.189        by (rule mset_eq_setD)
   2.190 -    then have "compare cmp y x \<noteq> Less" if "y \<in> set ys" for y
   2.191 +    then have "compare cmp x y \<noteq> Greater" if "y \<in> set ys" for y
   2.192        using that minimum.hyps by simp
   2.193      from minimum.prems have stable: "stable_segment cmp x ys = stable_segment cmp x xs"
   2.194        by simp
   2.195 @@ -318,4 +362,113 @@
   2.196    qed
   2.197  qed
   2.198  
   2.199 +lemma filter_insort:
   2.200 +  "filter P (insort cmp x xs) = insort cmp x (filter P xs)"
   2.201 +    if "sorted cmp xs" and "P x"
   2.202 +  using that by (induction xs)
   2.203 +    (auto simp add: compare.trans_not_greater insort_eq_ConsI)
   2.204 +
   2.205 +lemma filter_insort_triv:
   2.206 +  "filter P (insort cmp x xs) = filter P xs"
   2.207 +    if "\<not> P x"
   2.208 +  using that by (induction xs) simp_all
   2.209 +
   2.210 +lemma filter_sort:
   2.211 +  "filter P (sort cmp xs) = sort cmp (filter P xs)"
   2.212 +  by (induction xs) (auto simp add: filter_insort filter_insort_triv)
   2.213 +
   2.214 +
   2.215 +section \<open>Alternative sorting algorithms\<close>
   2.216 +
   2.217 +subsection \<open>Quicksort\<close>
   2.218 +
   2.219 +definition quicksort :: "'a comparator \<Rightarrow> 'a list \<Rightarrow> 'a list"
   2.220 +  where quicksort_is_sort [simp]: "quicksort = sort"
   2.221 +
   2.222 +lemma sort_by_quicksort:
   2.223 +  "sort = quicksort"
   2.224 +  by simp
   2.225 +
   2.226 +lemma sort_by_quicksort_rec:
   2.227 +  "sort cmp xs = sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Less]
   2.228 +    @ stable_segment cmp (xs ! (length xs div 2)) xs
   2.229 +    @ sort cmp [x\<leftarrow>xs. compare cmp x (xs ! (length xs div 2)) = Greater]" (is "sort cmp ?lhs = ?rhs")
   2.230 +proof (rule sort_eqI)
   2.231 +  show "mset ?lhs = mset ?rhs"
   2.232 +    by (rule multiset_eqI) (auto simp add: compare.sym intro: comp.exhaust)
   2.233 +next
   2.234 +  show "sorted cmp ?rhs"
   2.235 +    by (auto simp add: sorted_append_iff sorted_stable_segment compare.equiv_subst_right dest: compare.trans_greater)
   2.236 +next
   2.237 +  let ?pivot = "xs ! (length xs div 2)"
   2.238 +  fix l
   2.239 +  assume "l \<in> set xs"
   2.240 +  have "compare cmp x ?pivot = comp \<and> compare cmp l x = Equiv
   2.241 +    \<longleftrightarrow> compare cmp l ?pivot = comp \<and> compare cmp l x = Equiv" for x comp
   2.242 +  proof -
   2.243 +    have "compare cmp x ?pivot = comp \<longleftrightarrow> compare cmp l ?pivot = comp"
   2.244 +      if "compare cmp l x = Equiv"
   2.245 +      using that by (simp add: compare.equiv_subst_left compare.sym)
   2.246 +    then show ?thesis by blast
   2.247 +  qed
   2.248 +  then show "stable_segment cmp l ?lhs = stable_segment cmp l ?rhs"
   2.249 +    by (simp add: stable_sort compare.sym [of _ ?pivot])
   2.250 +      (cases "compare cmp l ?pivot", simp_all)
   2.251 +qed
   2.252 +
   2.253 +context
   2.254 +begin
   2.255 +
   2.256 +qualified definition partition :: "'a comparator \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list \<times> 'a list \<times> 'a list"
   2.257 +  where "partition cmp pivot xs =
   2.258 +    ([x \<leftarrow> xs. compare cmp x pivot = Less], stable_segment cmp pivot xs, [x \<leftarrow> xs. compare cmp x pivot = Greater])"
   2.259 +
   2.260 +qualified lemma partition_code [code]:
   2.261 +  "partition cmp pivot [] = ([], [], [])"
   2.262 +  "partition cmp pivot (x # xs) =
   2.263 +    (let (lts, eqs, gts) = partition cmp pivot xs
   2.264 +     in case compare cmp x pivot of
   2.265 +       Less \<Rightarrow> (x # lts, eqs, gts)
   2.266 +     | Equiv \<Rightarrow> (lts, x # eqs, gts)
   2.267 +     | Greater \<Rightarrow> (lts, eqs, x # gts))"
   2.268 +  using comp.exhaust by (auto simp add: partition_def Let_def compare.sym [of _ pivot])
   2.269 +
   2.270 +lemma quicksort_code [code]:
   2.271 +  "quicksort cmp xs =
   2.272 +    (case xs of
   2.273 +      [] \<Rightarrow> []
   2.274 +    | [x] \<Rightarrow> xs
   2.275 +    | [x, y] \<Rightarrow> (if compare cmp x y \<noteq> Greater then xs else [y, x])
   2.276 +    | _ \<Rightarrow>
   2.277 +        let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs
   2.278 +        in quicksort cmp lts @ eqs @ quicksort cmp gts)"
   2.279 +proof (cases "length xs \<ge> 3")
   2.280 +  case False
   2.281 +  then have "length xs \<le> 2"
   2.282 +    by simp
   2.283 +  then have "length xs = 0 \<or> length xs = 1 \<or> length xs = 2"
   2.284 +    using le_neq_trans less_2_cases by auto
   2.285 +  then consider "xs = []" | x where "xs = [x]" | x y where "xs = [x, y]"
   2.286 +    by (auto simp add: length_Suc_conv numeral_2_eq_2)
   2.287 +  then show ?thesis
   2.288 +    by cases simp_all
   2.289 +next
   2.290 +  case True
   2.291 +  then obtain x y z zs where "xs = x # y # z # zs"
   2.292 +    by (metis le_0_eq length_0_conv length_Cons list.exhaust not_less_eq_eq numeral_3_eq_3)
   2.293 +  moreover have "quicksort cmp xs =
   2.294 +    (let (lts, eqs, gts) = partition cmp (xs ! (length xs div 2)) xs
   2.295 +    in quicksort cmp lts @ eqs @ quicksort cmp gts)"
   2.296 +    using sort_by_quicksort_rec [of cmp xs] by (simp add: partition_def)
   2.297 +  ultimately show ?thesis
   2.298 +    by simp
   2.299 +qed
   2.300 +
   2.301  end
   2.302 +
   2.303 +text \<open>Evaluation example\<close>
   2.304 +
   2.305 +value "let cmp = key abs (reversed default)
   2.306 +  in quicksort cmp [65, 1705, -2322, 734, 4, (-17::int)]"
   2.307 +
   2.308 +end