[isabelle-dev] Merge-Sort Implementation

[Christian Sternagel]

Hi again,

stability (the third property required by @{thm 
properties_for_sort_key}) did actually cause some difficulties ;)

Hence the attached theory has rough parts in some proofs. But since I 
spent the most part of the weekend on the proof, I decided to post it 
anyway. Finally I can sleep well again ;)

have fun,

chris

On 10/27/2011 03:30 PM, Florian Haftmann wrote:
>> Indeed, that would be the obvious next step. I have not tried yet but
>> would not expect too hard difficulties. If this is of general interest I
>> can try.
>
> Well, if you want to superseed the existing quicksort, you have to
> provide the same generality ;-)
>
> 	Florian
>
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
(*
Copyright 2011 Christian Sternagel, René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
terms of the GNU Lesser General Public License as published by the Free Software
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)
theory Sort_Impl
imports "~~/src/HOL/Library/Multiset"
begin

section {* GHC version of merge sort *}

context linorder
begin

text {*
Split a list into chunks of ascending and descending parts, where
descending parts are reversed. Hence, the result is a list of
sorted lists.
*}
fun sequences :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list list"
  and ascending :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> ('b list \<Rightarrow> 'b list) \<Rightarrow> 'b list \<Rightarrow> 'b list list"
  and descending :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list \<Rightarrow> 'b list list"
where
  "sequences key (a#b#xs) = (if key a > key b
    then descending key b [a] xs
    else ascending key b (op # a) xs)"
| "sequences key xs = [xs]"

| "ascending key a f (b#bs) = (if \<not> key a > key b
    then ascending key b (f \<circ> op # a) bs
    else f [a] # sequences key (b#bs))"
| "ascending key a f bs = f [a] # sequences key bs"

| "descending key a as (b#bs) = (if key a > key b
    then descending key b (a#as) bs
    else (a#as) # sequences key (b#bs))"
| "descending key a as bs = (a#as) # sequences key bs"

fun merge :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list \<Rightarrow> 'b list \<Rightarrow> 'b list" where
  "merge key (a#as) (b#bs) = (if key a > key b
    then b # merge key (a#as) bs
    else a # merge key as (b#bs))"
| "merge key [] bs = bs"
| "merge key as [] = as"

fun merge_pairs :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list list \<Rightarrow> 'b list list" where
  "merge_pairs key (a#b#xs) = merge key a b # merge_pairs key xs"
| "merge_pairs key xs = xs"

lemma length_merge[simp]:
  "length (merge key xs ys) = length xs + length ys"
  by (induct xs ys rule: merge.induct) simp_all

lemma merge_pairs_length[simp]:
  "length (merge_pairs key xs) \<le> length xs"
  by (induct xs rule: merge_pairs.induct) simp_all

fun merge_all :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b list list \<Rightarrow> 'b list" where
  "merge_all key [] = []"
| "merge_all key [x] = x"
| "merge_all key xs = merge_all key (merge_pairs key xs)"

lemma set_merge[simp]:
  "set (merge key xs ys) = set xs \<union> set ys"
  by (induct xs ys rule: merge.induct) auto

lemma sorted_merge[simp]:
  assumes "sorted (map key xs)" and "sorted (map key ys)"
  shows "sorted (map key (merge key xs ys))"
  using assms by (induct xs ys rule: merge.induct) (auto simp: sorted_Cons)

lemma multiset_of_merge[simp]:
  "multiset_of (merge key xs ys) = multiset_of xs + multiset_of ys"
  by (induct xs ys rule: merge.induct) (auto simp: ac_simps)

lemma sorted_merge_pairs[simp]:
  assumes "\<forall>x\<in>set xs. sorted (map key x)"
  shows "\<forall>x\<in>set (merge_pairs key xs). sorted (map key x)"
  using assms by (induct xs rule: merge_pairs.induct) simp_all

lemma multiset_of_merge_pairs[simp]:
  "multiset_of (concat (merge_pairs key xs)) = multiset_of (concat xs)"
  by (induct xs rule: merge_pairs.induct) (auto simp: ac_simps)

lemma sorted_merge_all:
  assumes "\<forall>x\<in>set xs. sorted (map key x)"
  shows "sorted (map key (merge_all key xs))"
  using assms by (induct xs rule: merge_all.induct) simp_all

lemma multiset_of_merge_all[simp]:
  "multiset_of (merge_all key xs) = multiset_of (concat xs)"
  by (induct xs rule: merge_all.induct) (auto simp: ac_simps)

lemma
  shows sorted_sequences: "\<forall>x\<in>set (sequences key xs). sorted (map key x)"
  and "\<lbrakk>\<forall>x\<in>set (f []). key x \<le> key a; sorted (map key (f [])); \<forall>xs ys. f (xs at ys) = f xs @ ys;
    \<forall>x. f [x] = f [] @ [x]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (ascending key a f xs). sorted (map key x)"
  and "\<lbrakk>\<forall>x\<in>set bs. key a \<le> key x; sorted (map key bs)\<rbrakk>
    \<Longrightarrow> \<forall>x\<in>set (descending key a bs xs). sorted (map key x)"
  by (induct xs and a f xs and a bs xs rule: sequences_ascending_descending.induct)
     (simp_all add: sorted_append sorted_Cons,
      metis append_Cons append_Nil le_less_linear order_trans,
      metis less_le less_trans)

lemma
  shows multiset_of_sequences[simp]:
    "multiset_of (concat (sequences key xs)) = multiset_of xs"
  and "(\<And>x xs. multiset_of (f (x#xs)) = {#x#} + multiset_of (f []) + multiset_of xs)
    \<Longrightarrow> multiset_of (concat (ascending key a f xs)) = {#a#} + multiset_of (f []) + multiset_of xs"
  and "multiset_of (concat (descending key a bs xs)) = {#a#} + multiset_of bs + multiset_of xs"
by (induct xs and a f xs and a bs xs rule: sequences_ascending_descending.induct)
   (simp_all add: ac_simps)

lemma sort_merge_all_sequences:
  "sort = merge_all (\<lambda>x. x) \<circ> sequences (\<lambda>x. x)"
  by (intro ext properties_for_sort)
     (insert sorted_merge_all[OF sorted_sequences, of "\<lambda>x. x"], simp_all)

lemma set_concat_merge_pairs[simp]:
  "set (concat (merge_pairs key xs)) = set (concat xs)"
  by (induct xs rule: merge_pairs.induct) (simp_all add: ac_simps)

fun take_desc :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
  "take_desc key a [] = [a]"
| "take_desc key a (x#xs) = (if key x < key a
    then a # take_desc key x xs
    else [a])"

fun drop_desc :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
  "drop_desc key a [] = []"
| "drop_desc key a (x#xs) = (if key x < key a
    then drop_desc key x xs
    else x#xs)"

lemma descending_take_desc_drop_desc_conv[simp]:
  "descending key a bs xs
    = (rev (take_desc key a xs) @ bs) # sequences key (drop_desc key a xs)"
proof (induct xs arbitrary: a bs)
  case (Cons x xs) thus ?case by (cases "key a < key x") simp_all
qed simp

lemma set_take_desc_append_drop_desc[simp]:
  "set (take_desc key a xs @ drop_desc key a xs) = set (a#xs)"
  by (induct xs arbitrary: a) auto

lemma multiset_of_take_desc_append_drop_desc[simp]:
  "multiset_of (take_desc key a xs @ drop_desc key a xs) =
    multiset_of (a#xs)"
  by (induct xs arbitrary: a) (auto simp: ac_simps)

fun take_asc :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
  "take_asc key a [] = []"
| "take_asc key a (x#xs) = (if \<not> key a > key x
    then x # take_asc key x xs
    else [])"

fun drop_asc :: "('b \<Rightarrow> 'a) \<Rightarrow> 'b \<Rightarrow> 'b list \<Rightarrow> 'b list" where
  "drop_asc key a [] = []"
| "drop_asc key a (x#xs) = (if \<not> key a > key x
    then drop_asc key x xs
    else x#xs)"

lemma take_asc_append_drop_asc[simp]:
  "take_asc key a xs @ drop_asc key a xs = xs"
  by (induct xs arbitrary: a) simp_all

lemma ascending_take_asc_drop_asc_conv_gen:
  assumes "\<And>xs ys. f (xs at ys) = f xs @ ys"
  shows "ascending key a (f \<circ> op @ as) xs
    = (f as @ a # take_asc key a xs) # sequences key (drop_asc key a xs)"
using assms
proof (induct xs arbitrary: as a)
  case Nil thus ?case by simp
next
  case (Cons x xs)
  show ?case
  proof (cases "key x < key a")
    case True with Cons show ?thesis by simp
  next
    case False
    with Cons(1)[of "x" "as@[a]"] and Cons(2)
      show ?thesis by (simp add: o_def)
  qed
qed

lemma ascending_take_asc_drop_asc_conv[simp]:
  "ascending key b (op # a) xs
    = (a # b # take_asc key b xs) # sequences key (drop_asc key b xs)"
proof -
  let ?f = "op # a"
  have "\<And>xs ys. (op # a) (xs at ys) = (op # a) xs @ ys" by simp
  from ascending_take_asc_drop_asc_conv_gen[of ?f key b "[]" xs, OF this]
    show ?thesis by (simp add: o_def)
qed

lemma sequences_simp:
  "sequences key (a#b#xs) = (if key b < key a
    then (rev (take_desc key b xs)@[a]) # sequences key (drop_desc key b xs)
    else (a # b # take_asc key b xs) # sequences key (drop_asc key b xs))"
  by simp

lemma take_desc_drop_desc[simp]:
  "take_desc key x xs @ drop_desc key x xs = x#xs"
  by (induct xs arbitrary: x) simp_all

lemma length_drop_desc[simp]:
  fixes xs::"'b list"
  shows "length (drop_desc key b xs) < length (a#b#xs)" (is "?P b xs")
proof (induct xs arbitrary: b rule: length_induct)
  fix xs::"'b list" and b
  assume IH: "\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. ?P x ys)"
  show "?P b xs"
  proof (cases xs)
    case Nil thus ?thesis by simp
  next
    case (Cons y ys) with IH[rule_format, of ys y]
      show ?thesis by simp
  qed
qed

lemma length_drop_asc[simp]:
  fixes xs::"'b list"
  shows "length (drop_asc key b xs) < length (a#b#xs)" (is "?P b xs")
proof (induct xs arbitrary: b rule: length_induct)
  fix xs::"'b list" and b
  assume IH: "\<forall>ys. length ys < length xs \<longrightarrow> (\<forall>x. ?P x ys)"
  show "?P b xs"
  proof (cases xs)
    case Nil thus ?thesis by simp
  next
    case (Cons y ys) with IH[rule_format, of ys y]
      show ?thesis by simp
  qed
qed

lemma sequences_induct[case_names Nil singleton IH]:
  fixes xs::"'b list"
  assumes "P key []" and "\<And>x. P key [x]"
    and "\<And>a b xs.
    (key b < key a \<Longrightarrow> P key (drop_desc key b xs))
    \<Longrightarrow> (\<not> key b < key a \<Longrightarrow> P key (drop_asc key b xs))
    \<Longrightarrow> P key (a#b#xs)"
  shows "P key xs"
proof (induct xs rule: length_induct)
  fix xs::"'b list"
  assume IH[rule_format]: "\<forall>ys. length ys < length xs \<longrightarrow> P key ys"
  show "P key xs"
  proof (cases xs)
    case Nil with assms show ?thesis by simp
  next
    case (Cons a ys)
    show ?thesis
    proof (cases ys)
      case Nil with assms and Cons show ?thesis by simp
    next
      note Cons' = Cons
      case (Cons b zs)
      have "length (drop_desc key b zs) < length xs"
        unfolding Cons Cons' using length_drop_desc[of key b zs] by simp
      moreover have "length (drop_asc key b zs) < length xs"
        unfolding Cons Cons' using length_drop_asc[of key b zs] by simp
      ultimately show ?thesis
        using IH and assms(3)[of b a zs]
        unfolding Cons Cons' by (cases "key b < key a") simp_all
    qed
  qed
qed

lemma take_desc_less:
  assumes "key x < key y"
  shows "\<forall>z\<in>set (take_desc key x xs). key z < key y"
  using assms
  by (induct xs arbitrary: x y) (auto, force)

lemma take_desc_less':
  assumes "key x < key y"
  shows "\<forall>z\<in>set (rev (take_desc key x xs)). key y \<noteq> key z"
  using take_desc_less[of key x y, OF assms]
  unfolding less_le by force

lemma take_desc_le:
  "\<forall>x\<in>set (take_desc key b xs). key x \<le> key b"
  by (induct xs arbitrary: b) (auto, force)

lemma filter_by_key_drop_desc[simp]:
  assumes "key b \<le> key x"
  shows "[y\<leftarrow>drop_desc key b xs . key x = key y] = [y\<leftarrow>xs . key x = key y]"
  using assms by (induct xs arbitrary: b) auto

lemma filter_by_key_rev_take_desc[simp]:
  "[y\<leftarrow>rev (take_desc key b xs). key b = key y] = [b]"
proof (cases xs)
  case Nil thus ?thesis by simp
next
  case (Cons y ys)
  {
    assume "key y < key b"
    from filter_False[OF take_desc_less'[of key y b ys], OF this]
      have "[z\<leftarrow>rev (take_desc key y ys). key b = key z] = []" .
  }
  thus ?thesis by (simp add: Cons)
qed

lemma filter_by_key_take_desc'[simp]:
  assumes "key b < key a"
  shows "[y\<leftarrow>rev (take_desc key b xs). key a = key y] = []"
  using filter_False[OF take_desc_less'[of key b a, OF assms]] .

lemma length_rev_take_desc:
  "length [y\<leftarrow>rev (take_desc key b xs). key x = key y] \<le> Suc 0"
  by (induct xs arbitrary: b) simp_all

lemma rev_take_desc_fiter_key_conv[simp]: 
  "[y\<leftarrow>rev (take_desc key b xs). key x = key y]
    = [y\<leftarrow>take_desc key b xs. key x = key y]"
    (is "?xs = ?ys")
proof -
  from length_rev_take_desc[of key x b xs]
    have "length ?xs = 0 \<or> length ?xs = Suc 0" by arith
  thus ?thesis
  proof
    assume "length ?xs = 0"
    hence "?xs = []" by simp
    thus ?thesis unfolding rev_filter[symmetric] rev_is_Nil_conv by simp
  next
    assume "length ?xs = Suc 0"
    then obtain a where a: "?xs = [a]" by (cases "?xs") simp_all
    show ?thesis
      using a[unfolded rev_filter[symmetric],
        unfolded rev_singleton_conv, unfolded a[symmetric], symmetric] .
  qed
qed

lemma filter_by_key_take_desc[simp]:
  "[y\<leftarrow>take_desc key b xs. key b = key y] = [b]"
proof -
  from filter_by_key_rev_take_desc[of key b xs]
    show ?thesis unfolding rev_filter[symmetric]
    unfolding rev_singleton_conv by simp
qed

lemmas [simp] = filter_by_key_take_desc'[simplified]

lemma help1:
  assumes "key b < key a"
  shows
    "[y\<leftarrow>(rev (take_desc key b xs) @ [a]) @ drop_desc key b xs. key x = key y]
    = [y\<leftarrow>a # b # xs . key x = key y]"
  using assms by (auto simp: filter_append[symmetric])

lemma help2:
  assumes "\<not> key b < key a"
  shows "[y\<leftarrow>(a # b # take_asc key b xs) @ drop_asc key b xs. key x = key y]
    = [y\<leftarrow>a # b # xs . key x = key y]"
  by simp

lemma if_P_not: "~ P \<Longrightarrow> (if P then x else y) = y" by simp

lemma filter_by_key_sequences[simp]:
  "[y\<leftarrow>concat (sequences key xs). key x = key y] = [y\<leftarrow>xs. key x = key y]" (is "?P key xs")
proof (induct key xs rule: sequences_induct)
  case Nil show ?case by simp
next
  case (singleton x) show ?case by simp
next
  case (IH a b xs)
  thus ?case
  apply (unfold sequences_simp)
  apply (cases "key b < key a")
    apply (unfold if_P concat.simps)
    apply (insert help1[of key b a x xs])
    apply (unfold filter_append)
    apply simp
  apply (unfold if_P_not concat.simps)
  apply (insert help2[of key b a x xs])
  apply (unfold filter_append)
  apply simp
  done
qed

lemma set_merge_all[simp]: "set (merge_all key xs) = set (concat xs)"
  by (induct xs rule: merge_all.induct)
     (simp_all del: set_concat merge_pairs.simps)

lemma merge_Nil2[simp]: "merge key xs [] = xs" by (cases xs) simp_all
declare merge.simps(3)[simp del]

lemma merge_filter_True:
  "\<forall>x\<in>set (merge key (filter P xs) (filter P ys)). P x"
  by (induct xs ys rule: list_induct2')
     (simp, simp, simp, unfold set_merge set_filter, blast)

lemma filter_merge_filter[simp]:
  "filter P (merge key (filter P xs) (filter P ys))
    = merge key (filter P xs) (filter P ys)"
  using filter_True[OF merge_filter_True] .

lemma merge_simp:
  assumes "sorted (map key xs)"
  shows "merge key xs (y#ys)
    = takeWhile (\<lambda>x. key x \<le> key y) xs
    @ y#merge key (dropWhile (\<lambda>x. key x \<le> key y) xs) ys"
  using assms by (induct xs arbitrary: y ys) (auto simp: sorted_Cons)

lemma sorted_merge_induct[consumes 1, case_names Nil IH]:
  fixes key::"'b \<Rightarrow> 'a"
  assumes sorted: "sorted (map key xs)"
    and "\<And>xs. P key xs []"
    and "\<And>xs y ys. sorted (map key xs) \<Longrightarrow>
    P key (dropWhile (\<lambda>x. key x \<le> key y) xs) ys
    \<Longrightarrow> P key xs (y#ys)"
  shows "P key xs ys"
using assms(1)
proof (induct "xs at ys" arbitrary: xs ys rule: length_induct)
  fix xs ys::"'b list"
  assume IH[rule_format]: "\<forall>zs. length zs < length (xs at ys) \<longrightarrow>
    (\<forall>us vs. zs = us @ vs \<longrightarrow> sorted (map key us) \<longrightarrow> P key us vs)"
    and sorted: "sorted (map key xs)"
  let ?f = "\<lambda>y xs. dropWhile (\<lambda>x. key x \<le> key y) xs"
  show "P key xs ys"
  proof (cases ys)
    case Nil thus ?thesis using assms(2) by simp
  next
    case (Cons v vs)
    show ?thesis unfolding Cons
    proof (rule assms(3)[OF sorted])
      show "P key (?f v xs) vs"
      proof (rule IH)
        show "length (?f v xs @ vs) < length (xs at ys)"
        unfolding Cons using length_dropWhile_le[of "\<lambda>x. key x \<le> key v" xs]
        unfolding length_append list.size by simp
      next
        show "?f v xs @ vs = ?f v xs @ vs" by simp
      next
        show "sorted (map key (?f v xs))"
          using sorted_dropWhile[OF sorted, of "\<lambda>x. x \<le> key v"]
          unfolding dropWhile_map o_def .
      qed
    qed
  qed
qed

lemma filter_by_key_dropWhile[simp]:
  assumes "sorted (map key xs)"
  shows "[y\<leftarrow>dropWhile (\<lambda>x. key x \<le> key z) xs. key z = key y] = []"
    (is "[y\<leftarrow>dropWhile ?P xs. key z = key y] = []")
using assms
proof (induct xs rule: rev_induct)
  case Nil thus ?case by simp
next
  case (snoc x xs)
  hence IH: "[y\<leftarrow>dropWhile ?P xs. key z = key y] = []"
    by (auto simp: sorted_append)
  show ?case
  proof (cases "\<forall>z\<in>set xs. ?P z")
    case True
    show ?thesis
      using dropWhile_append2[of xs ?P "[x]"] and True by simp
  next
    case False
    then obtain a where a: "a \<in> set xs" "\<not> ?P a" by auto
    show ?thesis
      unfolding dropWhile_append1[of a xs ?P, OF a]
      using snoc and False by (auto simp: IH sorted_append)
  qed
qed

lemma filter_by_key_takeWhile[simp]:
  assumes "sorted (map key xs)"
  shows "[y\<leftarrow>takeWhile (\<lambda>x. key x \<le> key z) xs. key z = key y]
    = [y\<leftarrow>xs. key z = key y]"
    (is "[y\<leftarrow>takeWhile ?P xs. key z = key y] = _")
using assms
proof (induct xs rule: rev_induct)
  case Nil thus ?case by simp
next
  case (snoc x xs)
  hence IH: "[y\<leftarrow>takeWhile ?P xs. key z = key y] = [y\<leftarrow>xs. key z = key y]"
    by (auto simp: sorted_append)
  show ?case
  proof (cases "\<forall>z\<in>set xs. ?P z")
    case True
    show ?thesis
      using takeWhile_append2[of xs ?P "[x]"] and True by simp
  next
    case False
    then obtain a where a: "a \<in> set xs" "\<not> ?P a" by auto
    show ?thesis
      unfolding takeWhile_append1[of a xs ?P, OF a]
      using snoc and False by (auto simp: IH sorted_append)
  qed
qed

lemma filter_by_key_merge_is_append[simp]:
  assumes "sorted (map key xs)"
  shows "[y\<leftarrow>merge key xs ys. key x = key y]
    = [y\<leftarrow>xs. key x = key y] @ [y\<leftarrow>ys. key x = key y]"
    (is "?P xs ys")
using assms
proof (induct key xs ys rule: sorted_merge_induct)
  case Nil thus ?case by simp
next
  case (IH xs y ys)
  show ?case
  proof (cases "key x = key y")
    case False
    thus ?thesis
      by (simp add: merge_simp[OF IH(1)] IH(2))
         (simp only: filter_append[symmetric] takeWhile_dropWhile_id)
  next
    case True
    show ?thesis
      unfolding filter_append[symmetric]
      unfolding merge_simp[OF IH(1)]
      unfolding filter.simps filter_append
      unfolding if_P[OF True]
      unfolding IH(2) unfolding True
      using IH(1)
      by simp
  qed
qed

lemma filter_by_key_merge_pairs[simp]:
  assumes "\<forall>xs\<in>set xss. sorted (map key xs)"
  shows "[y\<leftarrow>concat (merge_pairs key xss). key x = key y]
    = [y\<leftarrow>concat xss. key x = key y]"
  using assms by (induct xss rule: merge_pairs.induct) simp_all

lemma filter_by_key_merge_all[simp]:
  assumes "\<forall>xs\<in>set xss. sorted (map key xs)"
  shows "[y\<leftarrow>merge_all key xss. key x = key y]
    = [y\<leftarrow>concat xss. key x = key y]"
  using assms by (induct xss rule: merge_all.induct) simp_all

lemma filter_by_key_merge_all_sequences[simp]:
  "[x\<leftarrow>merge_all key (sequences key xs) . key y = key x]
    = [x\<leftarrow>xs . key y = key x]"
  using sorted_sequences[of key xs] by simp

lemma sort_key_merge_all_sequences:
  "sort_key key = merge_all key \<circ> sequences key"
  by (intro ext properties_for_sort_key)
     (simp_all add: sorted_merge_all[OF sorted_sequences])

end

end