Theory Sorting

(*  Title:       An Efficient Generalization of Counting Sort for Large, possibly Infinite Key Ranges
    Author:      Pasquale Noce
                 Software Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Proof of objects' sorting"

theory Sorting
  imports Conservation
begin

text ‹
\null

In this section, it is formally proven that GCsort actually sorts objects.

Here below, steps 5, 6, and 7 of the proof method are accomplished. Predicate @{text sort_inv} is
satisfied just in case, for any bucket delimited by the input counters' list $ns$, the keys of the
corresponding objects within the input objects' list $xs$ are not larger than those of the objects,
if any, to the right of that bucket. The underlying idea is that this predicate:

\begin{itemize}

\item
is trivially satisfied by the output of function @{const gcsort_in}, which places all objects into a
single bucket, and

\item
implies that $xs$ is sorted if every bucket delimited by $ns$ has size one, as happens when function
@{const gcsort_aux} terminates.

\end{itemize}

\null
›

fun sort_inv :: "('a ⇒ 'b::linorder) ⇒ nat × nat list × 'a list ⇒ bool" where
"sort_inv key (u, ns, xs) =
  (∀i < length ns. ∀j < offs ns 0 ! i. ∀k ∈ {offs ns 0 ! i..<length xs}.
    key (xs ! j) ≤ key (xs ! k))"

lemma gcsort_sort_input:
 "sort_inv key (0, [length xs], xs)"
by simp

lemma offs_nth:
  assumes
    A: "find (λn. Suc 0 < n) ns = None" and
    B: "foldl (+) 0 ns = n" and
    C: "k < n"
  shows "∃i < length ns. offs ns 0 ! i = k"
proof (cases ns, insert B C, simp, cases "k = 0", rule exI [of _ 0], simp,
 rule ccontr, simp (no_asm_use))
  fix m ms
  assume
    D: "ns = m # ms" and
    E: "0 < k" and
    F: "∀i < length ns. offs ns 0 ! i ≠ k"
  have G: "∀n ∈ set ns. n ≤ Suc 0"
    using A by (auto simp add: find_None_iff)
  let ?A = "{i. i < length ns ∧ offs ns 0 ! i < k}"
  have H: "Max ?A ∈ ?A"
    using D and E by (rule_tac Max_in, simp_all, rule_tac exI [of _ 0], simp)
  hence I: "Max ?A < length ns"
    by simp
  hence J: "offs ns 0 ! Max ?A = foldl (+) 0 (take (Max ?A) ns)"
    by (rule offs_add)
  have "Max ?A < length ns - Suc 0 ∨ Max ?A = length ns - Suc 0"
    (is "?P ∨ ?Q")
    using H by (simp, arith)
  moreover {
    assume ?P
    hence K: "Suc (Max ?A) < length ns" by simp
    hence "offs ns 0 ! Suc (Max ?A) = foldl (+) 0 (take (Suc (Max ?A)) ns)"
      by (rule offs_add)
    moreover have "take (Suc (Max ?A)) ns = take (Max ?A) ns @ [ns ! Max ?A]"
      using I by (rule take_Suc_conv_app_nth)
    ultimately have "offs ns 0 ! Suc (Max ?A) =
      offs ns 0 ! Max ?A + ns ! Max ?A"
      using J by simp
    moreover have "offs ns 0 ! Max ?A < k"
      using H by simp
    moreover have "ns ! Max ?A ∈ set ns"
      using I by (rule nth_mem)
    with G have "ns ! Max ?A ≤ Suc 0" ..
    ultimately have "offs ns 0 ! Suc (Max ?A) ≤ k" by simp
    moreover have "offs ns 0 ! Suc (Max ?A) ≠ k"
      using F and K by simp
    ultimately have "offs ns 0 ! Suc (Max ?A) < k" by simp
    hence "Suc (Max ?A) ∈ ?A"
      using K by simp
    hence "Suc (Max ?A) ≤ Max ?A"
      by (rule_tac Max_ge, simp)
    hence False by simp
  }
  moreover {
    assume ?Q
    hence "offs ns 0 ! Max ?A = foldl (+) 0 (take (length ns - Suc 0) ns)"
      using J by simp
    moreover have K: "length ns - Suc 0 < length ns"
      using D by simp
    hence "take (Suc (length ns - Suc 0)) ns =
      take (length ns - Suc 0) ns @ [ns ! (length ns - Suc 0)]"
      by (rule take_Suc_conv_app_nth)
    hence "foldl (+) 0 ns =
      foldl (+) 0 (take (length ns - Suc 0) ns @ [ns ! (length ns - Suc 0)])"
      by simp
    ultimately have "n = offs ns 0 ! Max ?A + ns ! (length ns - Suc 0)"
      using B by simp
    moreover have "offs ns 0 ! Max ?A < k"
      using H by simp
    moreover have "ns ! (length ns - Suc 0) ∈ set ns"
      using K by (rule nth_mem)
    with G have "ns ! (length ns - Suc 0) ≤ Suc 0" ..
    ultimately have "n ≤ k" by simp
    with C have False by simp
  }
  ultimately show False ..
qed

lemma gcsort_sort_intro:
 "⟦sort_inv key t; add_inv n t; find (λn. Suc 0 < n) (fst (snd t)) = None⟧ ⟹
    sorted (map key (gcsort_out t))"
proof (cases t, simp add: sorted_iff_nth_mono_less gcsort_out_def,
 erule conjE, (rule allI)+, (rule impI)+)
  fix ns xs j k
  assume "find (λn. Suc 0 < n) ns = None" and "foldl (+) 0 ns = n"
  moreover assume A: "k < n"
  ultimately have "∃i < length ns. offs ns 0 ! i = k"
    by (rule offs_nth)
  then obtain i where "i < length ns ∧ offs ns 0 ! i = k" ..
  moreover assume "∀i < length ns. ∀j < offs ns 0 ! i. ∀k ∈ {offs ns 0 ! i..<n}.
    key (xs ! j) ≤ key (xs ! k)"
  hence "i < length ns ⟶ j < offs ns 0 ! i ⟶ k ∈ {offs ns 0 ! i..<n} ⟶
    key (xs ! j) ≤ key (xs ! k)"
    by simp
  ultimately have "j < k ⟶ k < n ⟶ key (xs ! j) ≤ key (xs ! k)"
    by simp
  moreover assume "j < k"
  ultimately show "key (xs ! j) ≤ key (xs ! k)"
    using A by simp
qed

text ‹
\null

As lemma @{thm [source] gcsort_sort_intro} comprises an additional assumption concerning the form of
the fixed points of function @{const gcsort_aux}, step 8 of the proof method is necessary this time
to prove that such assumption is satisfied.

\null
›

lemma gcsort_sort_form:
 "find (λn. Suc 0 < n) (fst (snd (gcsort_aux index key p t))) = None"
by (induction index key p t rule: gcsort_aux.induct, simp)

text ‹
\null

Here below, step 9 of the proof method is accomplished.

In the most significant case of the proof by recursion induction of lemma @{text round_sort_inv},
namely that of a bucket $B$ with size larger than two and distinct minimum and maximum keys, the
following line of reasoning is adopted. Let $x$ be an object contained in a finer-grained bucket
$B'$ resulting from $B$'s partition, and $y$ an object to the right of $B'$. Then:

\begin{itemize}

\item
If $y$ is contained in some other finer-grained bucket resulting from $B$'s partition, inequality
@{term "key x ≤ key y"} holds because predicate @{const sort_inv} is satisfied by a counters' list
generated by function @{const enum} and an objects' list generated by function @{const fill} in case
@{const fill}'s input offsets' list is computed via the composition of functions @{const offs} and
@{const enum}, as happens within function @{const round}.
\\This is proven beforehand in lemma @{text fill_sort_inv}.

\item
Otherwise, inequality @{term "key x ≤ key y"} holds as well because object $x$ was contained in $B$
by lemma @{thm [source] fill_offs_enum_count_item}, object $y$ occurred to the right of $B$ by lemma
@{thm [source] round_count_inv}, and by hypothesis, the key of any object in $B$ was not larger than
that of any object to the right of $B$.

\end{itemize}

Using lemma @{text round_sort_inv}, the invariance of predicate @{const sort_inv} over inductive set
@{const gcsort_set} is then proven in lemma @{text gcsort_sort_inv}.

\null
›

lemma mini_maxi_keys_le:
 "x ∈ set xs ⟹ key (xs ! mini xs key) ≤ key (xs ! maxi xs key)"
by (frule mini_lb, drule maxi_ub, erule order_trans)

lemma mini_maxi_keys_eq [rule_format]:
 "key (xs ! mini xs key) = key (xs ! maxi xs key) ⟶ x ∈ set xs ⟶
    key x = key (xs ! maxi xs key)"
by (induction xs, simp_all add: Let_def, (rule_tac [!] impI, (rule_tac [!] conjI)?)+,
 rule_tac [2-4] impI, frule_tac [1-3] mini_maxi_keys_le [where key = key], simp_all)

lemma offs_suc:
 "i < length ns ⟹ offs ns (Suc k) ! i = Suc (offs ns k ! i)"
by (simp add: offs_add add_suc)

lemma offs_base_zero:
 "i < length ns ⟹ offs ns k ! i = offs ns 0 ! i + k"
by (simp add: offs_add, subst add_base_zero, simp)

lemma offs_append:
 "offs (ms @ ns) k = offs ms k @ offs ns (foldl (+) k ms)"
by (induction ms arbitrary: k, simp_all)

lemma offs_enum_next_le [rule_format]:
  assumes
    A: "index_less index key" and
    B: "i < j" and
    C: "j < n" and
    D: "∀x ∈ set xs. key x ∈ {mi..ma}"
  shows "offs_next (offs (enum xs index key n mi ma) k) (length xs + k)
    xs index key mi ma i ≤ offs (enum xs index key n mi ma) k ! j"
  (is "_ ≤ offs ?ns _ ! _")
proof (rule ccontr, simp add: not_le)
  assume E: "offs ?ns k ! j <
    offs_next (offs ?ns k) (length xs + k) xs index key mi ma i"
  from B have "offs_set_next (offs ?ns k) xs index key mi ma i =
    offs_set_next (offs ?ns k) xs index key mi ma j"
  proof (rule_tac set_eqI, rule_tac iffI, simp_all, rule_tac ccontr, simp add: not_less)
    fix m
    assume "m < length (offs ?ns k) ∧ i < m ∧
      0 < offs_num (length (offs ?ns k)) xs index key mi ma m"
    hence F: "m ∈ offs_set_next (offs ?ns k) xs index key mi ma i"
      (is "_ ∈ ?A")
      by simp
    hence "Min ?A ≤ m"
      by (rule_tac Min_le, simp)
    moreover assume "m ≤ j"
    ultimately have "offs ?ns k ! Min ?A ≤ offs ?ns k ! j"
      using C by (rule_tac offs_mono, simp_all add: enum_length)
    hence "offs_next (offs ?ns k) (length xs + k) xs index key mi ma i ≤
      offs ?ns k ! j"
      using F by (simp only: offs_next_def split: if_split, rule_tac conjI,
       blast, simp)
    thus False
      using E by simp
  qed
  hence "offs ?ns k ! j <
    offs_next (offs ?ns k) (length xs + k) xs index key mi ma j"
    using E by (simp only: offs_next_def)
  moreover have "offs_num n xs index key mi ma j = 0"
  proof (rule ccontr, simp)
    assume "0 < offs_num n xs index key mi ma j"
    hence "j ∈ offs_set_next (offs ?ns k) xs index key mi ma i"
      (is "_ ∈ ?A")
      using B and C by (simp add: offs_length enum_length)
    moreover from this have "Min ?A ≤ j"
      by (rule_tac Min_le, simp)
    hence "offs ?ns k ! Min ?A ≤ offs ?ns k ! j"
      using C by (erule_tac offs_mono, simp add: enum_length)
    ultimately have "offs_next (offs ?ns k) (length xs + k) xs index key mi ma i ≤
      offs ?ns k ! j"
      by (simp only: offs_next_def split: if_split, rule_tac conjI, blast, simp)
    thus False
      using E by simp
  qed
  hence "offs ?ns k ! j =
    offs_next (offs ?ns k) (length xs + k) xs index key mi ma j"
    using A and C and D by (rule_tac offs_enum_zero, simp_all)
  ultimately show False by simp
qed

lemma offs_pred_ub_less:
 "⟦offs_pred ns ub xs index key mi ma; i < length ns;
   0 < offs_num (length ns) xs index key mi ma i⟧ ⟹
     ns ! i < ub"
by (drule offs_pred_ub, assumption+, simp)

lemma fill_count_none [rule_format]:
  assumes A: "index_less index key"
  shows
   "(∀x ∈ set xs. key x ∈ {mi..ma}) ⟶
    ns ≠ [] ⟶
    offs_pred ns ub xs index key mi ma ⟶
    length xs ≤ ub ⟶
      count (mset (fill xs ns index key ub mi ma)) None = ub - length xs"
  using A
proof (induction xs arbitrary: ns, simp_all add: replicate_count Let_def,
 (rule_tac impI)+, (erule_tac conjE)+, subst mset_update, simp add: fill_length,
 erule_tac offs_pred_ub_less, simp_all add: index_less_def offs_num_cons del:
 not_None_eq, subst conj_commute, rule_tac conjI, rule_tac [!] impI, rotate_tac,
 rotate_tac, erule_tac contrapos_np, rule_tac fill_index_none, simp_all)
  fix x xs and ns :: "nat list"
  let ?i = "index key x (length ns) mi ma"
  let ?ns' = "ns[?i := Suc (ns ! ?i)]"
  assume "⋀ns. ns ≠ [] ⟶ offs_pred ns ub xs index key mi ma ⟶
    count (mset (fill xs ns index key ub mi ma)) None = ub - length xs"
  moreover assume B: "ns ≠ []"
  moreover assume
   "offs_pred ns ub (x # xs) index key mi ma" and
   "mi ≤ key x" and
   "key x ≤ ma"
  hence "offs_pred ?ns' ub xs index key mi ma"
    using A and B by (rule_tac offs_pred_cons, simp_all add: index_less_def)
  ultimately show "count (mset (fill xs ?ns' index key ub mi ma)) None -
    Suc 0 = ub - Suc (length xs)"
    by simp
qed

lemma fill_offs_enum_count_none [rule_format]:
 "⟦index_less index key; ∀x ∈ set xs. key x ∈ {mi..ma}; 0 < n⟧ ⟹
    count (mset (fill xs (offs (enum xs index key n mi ma) 0)
      index key (length xs) mi ma)) None = 0"
by (subst fill_count_none, simp_all, simp only: length_greater_0_conv [symmetric]
 offs_length enum_length, insert offs_enum_pred [of index key xs mi ma n 0], simp)

lemma fill_index [rule_format]:
  assumes A: "index_less index key"
  shows
   "(∀x ∈ set xs. key x ∈ {mi..ma}) ⟶
    offs_pred ns ub xs index key mi ma ⟶
    i < length ns ⟶
    0 < offs_num (length ns) xs index key mi ma i ⟶
    j ∈ {ns ! i..<offs_next ns ub xs index key mi ma i} ⟶
    fill xs ns index key ub mi ma ! j = Some x ⟶
      index key x (length ns) mi ma = i"
proof (induction xs arbitrary: ns, simp add: offs_num_def, simp add: Let_def,
 (rule impI)+, (erule conjE)+, simp)
  fix y xs and ns :: "nat list"
  let ?i = "index key x (length ns) mi ma"
  let ?i' = "index key y (length ns) mi ma"
  let ?ns' = "ns[?i' := Suc (ns ! ?i')]"
  let ?P = "λns.
    offs_pred ns ub xs index key mi ma ⟶
    i < length ns ⟶
    0 < offs_num (length ns) xs index key mi ma i ⟶
    ns ! i ≤ j ∧ j < offs_next ns ub xs index key mi ma i ⟶
    fill xs ns index key ub mi ma ! j = Some x ⟶
      index key x (length ns) mi ma = i"
  assume
    B: "∀x ∈ set xs. mi ≤ key x ∧ key x ≤ ma" and
    C: "mi ≤ key y" and
    D: "key y ≤ ma" and
    E: "offs_pred ns ub (y # xs) index key mi ma" and
    F: "i < length ns" and
    G: "0 < offs_num (length ns) (y # xs) index key mi ma i" and
    H: "ns ! i ≤ j" and
    I: "j < offs_next ns ub (y # xs) index key mi ma i" and
    J: "⋀ns. ?P ns" and
    K: "(fill xs ?ns' index key ub mi ma)[ns ! ?i' := Some y] ! j = Some x"
  have "0 < length ns"
    using F by arith
  hence L: "?i' < length ns"
    using A and C and D by (simp add: index_less_def)
  hence "ns ! ?i' + offs_num (length ns) (y # xs) index key mi ma ?i' ≤ ub"
    by (rule_tac offs_pred_ub [OF E], simp_all add: offs_num_cons)
  hence "ns ! ?i' < ub"
    by (simp add: offs_num_cons)
  with K show "?i = i"
  proof (cases "j = ns ! ?i'", simp, subst (asm) nth_list_update_eq, simp_all
   add: fill_length)
    assume
      M: "j = ns ! ?i" and
      N: "y = x"
    show ?thesis
    proof (rule ccontr, erule neqE)
      assume "?i < i"
      hence "ns ! ?i + offs_num (length ns) (y # xs) index key mi ma ?i ≤ ns ! i"
        using F and G and N by (rule_tac offs_pred_asc [OF E], simp_all
         add: offs_num_cons)
      hence "j < ns ! i"
        using M and N by (simp add: offs_num_cons)
      thus False
        using H by simp
    next
      let ?A = "offs_set_next ns (y # xs) index key mi ma i"
      assume "i < ?i"
      hence O: "?i ∈ ?A"
        using N and L by (simp add: offs_num_cons)
      hence P: "Min ?A ∈ ?A"
        by (rule_tac Min_in, simp, blast)
      have "Min ?A ≤ ?i"
        using O by (rule_tac Min_le, simp)
      moreover have "?A ≠ {}"
        using O by blast
      ultimately have "offs_next ns ub (y # xs) index key mi ma i ≤ j"
      using M proof (simp only: offs_next_def, simp, subst (asm) le_less,
       erule_tac disjE, simp_all)
        assume "Min ?A < ?i"
        hence "ns ! Min ?A + offs_num (length ns) (y # xs) index key mi ma
          (Min ?A) ≤ ns ! ?i"
          using O and P by (rule_tac offs_pred_asc [OF E], simp_all)
        thus "ns ! Min ?A ≤ ns ! ?i" by simp
      qed
      thus False
        using I by simp
    qed
  next
    assume
      M: "j ≠ ns ! ?i'" and
      N: "fill xs ?ns' index key ub mi ma ! j = Some x"
    have "?P ?ns'" using J .
    moreover from D and F have "offs_pred ?ns' ub xs index key mi ma"
      using L by (rule_tac offs_pred_cons [OF E], simp)
    moreover have "i < length ?ns'"
      using F by simp
    moreover have "0 < offs_num (length ?ns') xs index key mi ma i"
    proof (rule ccontr, simp)
      assume O: "offs_num (length ns) xs index key mi ma i = 0"
      hence P: "offs_num (length ns) (y # xs) index key mi ma i = Suc 0"
        using G by (simp add: offs_num_cons split: if_split_asm)
      hence "i = ?i'"
        using O by (simp add: offs_num_cons split: if_split_asm)
      hence "ns ! i < j"
        using H and M by simp
      hence "ns ! i + offs_num (length ns) (y # xs) index key mi ma i ≤ j"
        using P by simp
      with F and G and I have "offs_none ns ub (y # xs) index key mi ma j"
        by (simp add: offs_none_def, rule_tac disjI1, rule_tac exI
         [where x = i], simp)
      with B and C and D and E and F have
       "fill (y # xs) ns index key ub mi ma ! j = None"
        by (rule_tac fill_none [OF A], simp_all, erule_tac disjE, simp_all, auto)
      thus False
        using K by (simp add: Let_def)
    qed
    moreover have "?ns' ! i ≤ j"
      using F and H and M by (cases "?i' = i", simp_all)
    moreover have "offs_next ns ub (y # xs) index key mi ma i ≤
      offs_next ?ns' ub xs index key mi ma i"
      using G and L by (rule_tac offs_pred_next_cons [OF E], simp)
    hence "j < offs_next ?ns' ub xs index key mi ma i"
      using I by simp
    ultimately show ?thesis
      using N by simp
  qed
qed

lemma fill_offs_enum_index [rule_format]:
 "index_less index key ⟹
  ∀x ∈ set xs. key x ∈ {mi..ma} ⟹
  i < n ⟹
  0 < offs_num n xs index key mi ma i ⟹
  j ∈ {offs (enum xs index key n mi ma) 0 ! i..<
    offs_next (offs (enum xs index key n mi ma) 0) (length xs)
      xs index key mi ma i} ⟹
  fill xs (offs (enum xs index key n mi ma) 0) index key (length xs)
    mi ma ! j = Some x ⟹
    index key x n mi ma = i"
by (insert fill_index [of index key xs mi ma "offs (enum xs index key n mi ma) 0"
 "length xs" i j x], insert offs_enum_pred [of index key xs mi ma n 0],
 simp add: offs_length enum_length)

lemma fill_sort_inv [rule_format]:
  assumes
    A: "index_less index key" and
    B: "index_mono index key" and
    C: "∀x ∈ set xs. key x ∈ {mi..ma}"
  shows "sort_inv key (u, enum xs index key n mi ma,
    map the (fill xs (offs (enum xs index key n mi ma) 0)
      index key (length xs) mi ma))"
  (is "sort_inv _ (_, ?ns, _)")
proof (simp, (rule allI, rule impI)+, rule ballI, simp add: enum_length fill_length,
 erule conjE)
  fix i j k
  let ?A = "{i. i < n ∧ 0 < ?ns ! i}"
  let ?B = "{i. i < n ∧ offs ?ns 0 ! i ≤ j ∧ 0 < offs_num n xs index key mi ma i}"
  let ?C = "{i. i < n ∧ offs ?ns 0 ! i ≤ k ∧ 0 < offs_num n xs index key mi ma i}"
  assume
    D: "i < n" and
    E: "j < offs ?ns 0 ! i" and
    F: "offs ?ns 0 ! i ≤ k" and
    G: "k < length xs"
  have H: "∀i < length xs.
    ∃x. fill xs (offs ?ns 0) index key (length xs) mi ma ! i = Some x"
  proof (rule allI, rule impI, rule ccontr, simp)
    fix m
    assume "fill xs (offs ?ns 0) index key (length xs) mi ma ! m = None"
    moreover assume "m < length xs"
    hence "fill xs (offs ?ns 0) index key (length xs) mi ma ! m
      ∈ set (fill xs (offs ?ns 0) index key (length xs) mi ma)"
      by (rule_tac nth_mem, simp add: fill_length)
    ultimately have "None ∈ set (fill xs (offs ?ns 0) index key (length xs) mi ma)"
      by simp
    moreover have
     "count (mset (fill xs (offs ?ns 0) index key (length xs) mi ma)) None = 0"
      using C and D by (rule_tac fill_offs_enum_count_none [OF A], simp_all)
    ultimately show False by simp
  qed
  have "∃y ys. xs = y # ys"
    using G by (rule_tac list.exhaust [of xs], simp_all)
  then obtain z and zs where I: "xs = z # zs" by blast
  hence "index key z n mi ma < n"
    using A and C and D by (simp add: index_less_def)
  moreover from this have "0 < ?ns ! index key z n mi ma"
    using I by (simp add: Let_def, subst nth_list_update_eq, simp_all add:
     enum_length)
  ultimately have "index key z n mi ma ∈ ?A" by simp
  hence J: "Min ?A ∈ ?A"
    by (rule_tac Min_in, simp, blast)
  hence "offs ?ns 0 ! 0 = offs ?ns 0 ! Min ?A"
  proof (cases "Min ?A = 0", simp_all, erule_tac offs_equal, simp_all add:
   enum_length, rule_tac ccontr, erule_tac conjE, simp)
    fix m
    assume "m < Min ?A" and "Min ?A < n" and "0 < ?ns ! m"
    moreover from this have "Min ?A ≤ m"
      by (rule_tac Min_le, simp_all)
    ultimately show False by simp
  qed
  moreover have "∃m ms. ?ns = m # ms"
    using D by (rule_tac list.exhaust [of ?ns], simp_all,
     simp only: length_0_conv [symmetric] enum_length)
  then obtain m and ms where "?ns = m # ms" by blast
  ultimately have "offs ?ns 0 ! Min ?A = 0" by simp
  hence "Min ?A ∈ ?B"
    using J by (simp, subst enum_offs_num [symmetric], simp_all)
  hence K: "Max ?B ∈ ?B"
    by (rule_tac Max_in, simp, blast)
  moreover have "j < offs_next (offs ?ns 0) (length xs)
    xs index key mi ma (Max ?B)"
  proof (simp only: offs_next_def split: if_split, rule conjI, rule_tac [!] impI,
   rule_tac [2] ccontr, simp_all only: not_less)
    show "j < length xs"
      using E and F and G by simp
  next
    assume "offs_set_next (offs ?ns 0) xs index key mi ma (Max ?B) ≠ {}"
      (is "?Z ≠ _")
    hence L: "Min ?Z ∈ ?Z"
      by (rule_tac Min_in, simp)
    moreover assume "offs ?ns 0 ! Min ?Z ≤ j"
    ultimately have "Min ?Z ∈ ?B"
      by (simp add: offs_length enum_length)
    hence "Min ?Z ≤ Max ?B"
      by (rule_tac Max_ge, simp)
    thus False
      using L by simp
  qed
  moreover have
   "∃x. fill xs (offs ?ns 0) index key (length xs) mi ma ! j = Some x"
    using E and F and G and H by simp
  then obtain x where
    L: "fill xs (offs ?ns 0) index key (length xs) mi ma ! j = Some x" ..
  ultimately have M: "index key x n mi ma = Max ?B"
    using C by (rule_tac fill_offs_enum_index [OF A], simp_all)
  have N: "Max ?B ∈ ?C"
    using E and F and K by simp
  hence "Max ?C ∈ ?C"
    by (rule_tac Max_in, simp, blast)
  moreover have O: "k < offs_next (offs ?ns 0) (length xs)
    xs index key mi ma (Max ?C)"
  proof (simp only: offs_next_def split: if_split, rule conjI, rule_tac [!] impI,
   rule_tac [2] ccontr, simp_all only: not_less)
    show "k < length xs" using G .
  next
    assume "offs_set_next (offs ?ns 0) xs index key mi ma (Max ?C) ≠ {}"
      (is "?Z ≠ _")
    hence P: "Min ?Z ∈ ?Z"
      by (rule_tac Min_in, simp)
    moreover assume "offs ?ns 0 ! Min ?Z ≤ k"
    ultimately have "Min ?Z ∈ ?C"
      by (simp add: offs_length enum_length)
    hence "Min ?Z ≤ Max ?C"
      by (rule_tac Max_ge, simp)
    thus False
      using P by simp
  qed
  moreover have
   "∃x. fill xs (offs ?ns 0) index key (length xs) mi ma ! k = Some x"
    using G and H by simp
  then obtain y where
    P: "fill xs (offs ?ns 0) index key (length xs) mi ma ! k = Some y" ..
  ultimately have Q: "index key y n mi ma = Max ?C"
    using C by (rule_tac fill_offs_enum_index [OF A], simp_all)
  have "Max ?B ≤ Max ?C"
    using N by (rule_tac Max_ge, simp)
  hence "Max ?B < Max ?C"
  proof (rule_tac ccontr, simp)
    assume "Max ?B = Max ?C"
    hence "offs ?ns 0 ! i < offs_next (offs ?ns 0) (length xs)
      xs index key mi ma (Max ?B)"
      using F and O by simp
    moreover have "offs ?ns 0 ! Max ?B < offs ?ns 0 ! i"
      using E and K by simp
    with K have "Max ?B < i"
      by (erule_tac contrapos_pp, subst not_less, subst (asm) not_less,
       erule_tac offs_mono, simp add: enum_length)
    hence "offs_next (offs ?ns 0) (length xs + 0) xs index key mi ma (Max ?B) ≤
      offs ?ns 0 ! i"
      using C and D by (rule_tac offs_enum_next_le [OF A], simp_all)
    ultimately show False by simp
  qed
  hence R: "index key x n mi ma < index key y n mi ma"
    using M and Q by simp
  have "count (mset (map the (fill xs (offs ?ns 0) index key
    (length xs) mi ma))) x = count (mset xs) x"
    using C and D by (rule_tac fill_offs_enum_count_item [OF A], simp_all)
  moreover have S: "j < length (map the (fill xs (offs ?ns 0) index key
    (length xs) mi ma))"
    using E and F and G by (simp add: fill_length)
  hence "map the (fill xs (offs ?ns 0) index key (length xs) mi ma) ! j
    ∈ set (map the (fill xs (offs ?ns 0) index key (length xs) mi ma))"
    by (rule nth_mem)
  hence "0 < count (mset (map the (fill xs (offs ?ns 0) index key
    (length xs) mi ma))) x"
    using L and S by simp
  ultimately have T: "x ∈ set xs" by simp
  have "count (mset (map the (fill xs (offs ?ns 0) index key
    (length xs) mi ma))) y = count (mset xs) y"
    using C and D by (rule_tac fill_offs_enum_count_item [OF A], simp_all)
  moreover have U: "k < length (map the (fill xs (offs ?ns 0) index key
    (length xs) mi ma))"
    using G by (simp add: fill_length)
  hence "map the (fill xs (offs ?ns 0) index key (length xs) mi ma) ! k
    ∈ set (map the (fill xs (offs ?ns 0) index key (length xs) mi ma))"
    by (rule nth_mem)
  hence "0 < count (mset (map the (fill xs (offs ?ns 0) index key
    (length xs) mi ma))) y"
    using P and U by simp
  ultimately have V: "y ∈ set xs" by simp
  have "key y ≤ key x ⟶ index key y n mi ma ≤ index key x n mi ma"
    using B and C and T and V by (simp add: index_mono_def)
  hence "key x < key y"
    by (rule_tac contrapos_pp [OF R], simp add: not_less)
  thus "key (the (fill xs (offs ?ns 0) index key (length xs) mi ma ! j)) ≤
    key (the (fill xs (offs ?ns 0) index key (length xs) mi ma ! k))"
    using L and P by simp
qed

lemma round_sort_inv [rule_format]:
 "index_less index key ⟶ index_mono index key ⟶ bn_inv p q t ⟶
    add_inv n t ⟶ sort_inv key t ⟶ sort_inv key (round index key p q r t)"
proof (induction index key p q r t arbitrary: n rule: round.induct,
 (rule_tac [!] impI)+, simp, simp_all only: simp_thms)
  fix index p q r u ns xs n and key :: "'a ⇒ 'b"
  let ?t = "round index key p q r (u, ns, xs)"
  assume "⋀n. bn_inv p q (u, ns, xs) ⟶ add_inv n (u, ns, xs) ⟶
    sort_inv key (u, ns, xs) ⟶ sort_inv key ?t"
  hence "bn_inv p q (u, ns, xs) ⟶ add_inv n (u, ns, xs) ⟶
    sort_inv key (u, ns, xs) ⟶ sort_inv key ?t" .
  moreover assume
   "bn_inv p q (u, 0 # ns, xs)"
   "add_inv n (u, 0 # ns, xs)" and
   "sort_inv key (u, 0 # ns, xs)"
  ultimately show "sort_inv key (round index key p q r (u, 0 # ns, xs))"
    by auto
next
  fix index p q r u ns xs n and key :: "'a ⇒ 'b"
  let ?t = "round index key p q r (u, ns, tl xs)"
  assume
    A: "index_less index key" and
    B: "bn_inv p q (u, Suc 0 # ns, xs)"
  moreover assume
   "⋀n. bn_inv p q (u, ns, tl xs) ⟶ add_inv n (u, ns, tl xs) ⟶
      sort_inv key (u, ns, tl xs) ⟶ sort_inv key ?t" and
   "add_inv n (u, Suc 0 # ns, xs)" and
   "sort_inv key (u, Suc 0 # ns, xs)"
  ultimately show "sort_inv key (round index key p q r (u, Suc 0 # ns, xs))"
  proof (cases ?t, cases xs, simp_all add: add_suc, (rule_tac allI, rule_tac impI)+,
   rule_tac ballI, simp, (erule_tac conjE)+, simp)
    fix i j k y ys u' ns' xs'
    assume
      C: "round index key p q r (u, ns, ys) = (u', ns', xs')" and
      D: "Suc (foldl (+) 0 ns) = n" and
      E: "Suc (length ys) = n" and
      F: "∀i < Suc (length ns).
        ∀j < (0 # offs ns (Suc 0)) ! i. ∀k ∈ {(0 # offs ns (Suc 0)) ! i..<n}.
          key ((y # ys) ! j) ≤ key (ys ! (k - Suc 0))"
    assume A': "j < (0 # offs ns' (Suc 0)) ! i"
    hence "∃i'. i = Suc i'"
      by (rule_tac nat.exhaust [of i], simp_all)
    then obtain i' where B': "i = Suc i'" ..
    assume "i < Suc (length ns')"
    hence G: "i' < length ns'"
      using B' by simp
    hence H: "j < Suc (offs ns' 0 ! i')"
      using A' and B' by (simp add: offs_suc)
    assume "(0 # offs ns' (Suc 0)) ! i ≤ k"
    hence "Suc (offs ns' 0 ! i') ≤ k"
      using B' and G by (simp add: offs_suc)
    moreover from this have "∃k'. k = Suc k'"
      by (rule_tac nat.exhaust [of k], simp_all)
    then obtain k' where I: "k = Suc k'" ..
    ultimately have J: "offs ns' 0 ! i' ≤ k'" by simp
    assume "k < Suc (length xs')"
    hence K: "k' < length xs'"
      using I by simp
    let ?P = "λn. foldl (+) 0 ns = n ∧ length ys = n"
    let ?Q = "λn. ∀i < length ns.
      ∀j < offs ns 0 ! i. ∀k ∈ {offs ns 0 ! i..<n}.
        key (ys ! j) ≤ key (ys ! k)"
    let ?R = "∀i < length ns'.
      ∀j < offs ns' 0 ! i. ∀k ∈ {offs ns' 0 ! i..<length xs'}.
        key (xs' ! j) ≤ key (xs' ! k)"
    assume "⋀n. ?P n ⟶ ?Q n ⟶ ?R"
    hence "?P (n - Suc 0) ⟶ ?Q (n - Suc 0) ⟶ ?R" .
    hence "?Q (n - Suc 0) ⟶ ?R"
      using D and E by auto
    moreover have "?Q (n - Suc 0)"
    proof ((rule allI, rule impI)+, rule ballI, simp, erule conjE)
      fix i j k
      have "Suc i < Suc (length ns) ⟶ (∀j < (0 # offs ns (Suc 0)) ! Suc i.
        ∀k ∈ {(0 # offs ns (Suc 0)) ! Suc i..<n}.
          key ((y # ys) ! j) ≤ key (ys ! (k - Suc 0)))"
        using F ..
      moreover assume "i < length ns"
      ultimately have "Suc j < Suc (offs ns 0 ! i) ⟶
        (∀k ∈ {Suc (offs ns 0 ! i)..<n}.
          key ((y # ys) ! Suc j) ≤ key (ys ! (k - Suc 0)))"
        by (auto simp add: offs_suc)
      moreover assume "j < offs ns 0 ! i"
      ultimately have "∀k ∈ {Suc (offs ns 0 ! i)..<n}.
        key (ys ! j) ≤ key (ys ! (k - Suc 0))"
        by simp
      moreover assume "offs ns 0 ! i ≤ k" and "k < n - Suc 0"
      hence "Suc k ∈ {Suc (offs ns 0 ! i)..<n}" by simp
      ultimately have "key (ys ! j) ≤ key (ys ! (Suc k - Suc 0))" ..
      thus "key (ys ! j) ≤ key (ys ! k)" by simp
    qed
    ultimately have ?R ..
    from I show "key ((y # xs') ! j) ≤ key (xs' ! (k - Suc 0))"
    proof (cases j, simp_all)
      have "bn_inv p q (u, ns, ys)"
        using B by simp
      moreover have "add_inv (n - Suc 0) (u, ns, ys)"
        using D and E by auto
      moreover have "count_inv (λx. count (mset ys) x) (u, ns, ys)" by simp
      ultimately have "count_inv (λx. count (mset ys) x)
        (round index key p q r (u, ns, ys))"
        by (rule round_count_inv [OF A])
      hence "count (mset xs') (xs' ! k') = count (mset ys) (xs' ! k')"
        using C by simp
      moreover have "0 < count (mset xs') (xs' ! k')"
        using K by simp
      ultimately have "xs' ! k' ∈ set ys" by simp
      hence "∃m < length ys. ys ! m = xs' ! k'"
        by (simp add: in_set_conv_nth)
      then obtain m where L: "m < length ys ∧ ys ! m = xs' ! k'" ..
      have "Suc 0 < Suc (length ns) ⟶ (∀j < (0 # offs ns (Suc 0)) ! Suc 0.
        ∀k ∈ {(0 # offs ns (Suc 0)) ! Suc 0..<n}.
          key ((y # ys) ! j) ≤ key (ys ! (k - Suc 0)))"
        using F ..
      moreover have M: "0 < length ns"
        using D [symmetric] and E and L by (rule_tac ccontr, simp)
      ultimately have "∀k ∈ {Suc (offs ns 0 ! 0)..<n}.
        key y ≤ key (ys ! (k - Suc 0))"
        by (auto simp add: offs_suc)
      hence "∀k ∈ {Suc 0..<n}. key y ≤ key (ys ! (k - Suc 0))"
        using M by (cases ns, simp_all)
      moreover have "Suc m ∈ {Suc 0..<n}"
        using E and L by simp
      ultimately have "key y ≤ key (ys ! (Suc m - Suc 0))" ..
      thus "key y ≤ key (xs' ! k')"
        using L by simp
    next
      case (Suc j')
      moreover have "i' < length ns' ⟶ (∀j < offs ns' 0 ! i'.
        ∀k ∈ {offs ns' 0 ! i'..<length xs'}. key (xs' ! j) ≤ key (xs' ! k))"
        using ‹?R› ..
      hence "j' < offs ns' 0 ! i' ⟶
        (∀k ∈ {offs ns' 0 ! i'..<length xs'}. key (xs' ! j') ≤ key (xs' ! k))"
        using G by simp
      ultimately have "∀k ∈ {offs ns' 0 ! i'..<length xs'}.
        key (xs' ! j') ≤ key (xs' ! k)"
        using H by simp
      moreover have "k' ∈ {offs ns' 0 ! i'..<length xs'}"
        using J and K by simp
      ultimately show "key (xs' ! j') ≤ key (xs' ! k')" ..
    qed
  qed
next
  fix index p q r u m ns n and key :: "'a ⇒ 'b" and xs :: "'a list"
  let ?ws = "take (Suc (Suc m)) xs"
  let ?ys = "drop (Suc (Suc m)) xs"
  let ?r = "λm'. round_suc_suc index key ?ws m m' u"
  let ?t = "λr' v. round index key p q r' (v, ns, ?ys)"
  assume
    A: "index_less index key" and
    B: "index_mono index key" and
    C: "bn_inv p q (u, Suc (Suc m) # ns, xs)"
  assume
   "⋀ws a b c d e f g h n.
      ws = ?ws ⟹ a = bn_comp m p q r ⟹ (b, c) = bn_comp m p q r ⟹
      d = ?r b ⟹ (e, f) = ?r b ⟹ (g, h) = f ⟹
        bn_inv p q (e, ns, ?ys) ⟶ add_inv n (e, ns, ?ys) ⟶
          sort_inv key (e, ns, ?ys) ⟶ sort_inv key (?t c e)" and
   "add_inv n (u, Suc (Suc m) # ns, xs)" and
   "sort_inv key (u, Suc (Suc m) # ns, xs)"
  with C show "sort_inv key (round index key p q r (u, Suc (Suc m) # ns, xs))"
  using [[simproc del: defined_all]]
  proof (simp split: prod.split, ((rule_tac allI)+, (rule_tac impI)+)+,
   rule_tac ballI, simp, (erule_tac conjE)+, subst (asm) (2) add_base_zero, simp)
    fix m' r' v ms' ws' u' ns' xs' i j k
    let ?nmi = "mini ?ws key"
    let ?nma = "maxi ?ws key"
    let ?xmi = "?ws ! ?nmi"
    let ?xma = "?ws ! ?nma"
    let ?mi = "key ?xmi"
    let ?ma = "key ?xma"
    let ?k = "case m of 0 ⇒ m | Suc 0 ⇒ m | Suc (Suc i) ⇒ u + m'"
    let ?zs = "nths ?ws (- {?nmi, ?nma})"
    let ?ms = "enum ?zs index key ?k ?mi ?ma"
    let ?P = "λn'. foldl (+) 0 ns = n' ∧ n - Suc (Suc m) = n'"
    let ?Q = "λn'. ∀i < length ns.
      ∀j < offs ns 0 ! i. ∀k ∈ {offs ns 0 ! i..<n'}.
        key (xs ! Suc (Suc (m + j))) ≤ key (xs ! Suc (Suc (m + k)))"
    let ?R = "∀i < length ns'.
      ∀j < offs ns' 0 ! i. ∀k ∈ {offs ns' 0 ! i..<length xs'}.
        key (xs' ! j) ≤ key (xs' ! k)"
    assume
      D: "?r m' = (v, ms', ws')" and
      E: "?t r' v = (u', ns', xs')" and
      F: "bn_comp m p q r = (m', r')" and
      G: "bn_valid m p q" and
      H: "Suc (Suc (foldl (+) 0 ns + m)) = n" and
      I: "length xs = n" and
      J: "∀i < Suc (length ns). ∀j < (0 # offs ns (Suc (Suc m))) ! i.
        ∀k ∈ {(0 # offs ns (Suc (Suc m))) ! i..<n}.
          key (xs ! j) ≤ key (xs ! k)" and
      K: "i < length ms' + length ns'" and
      L: "j < offs (ms' @ ns') 0 ! i" and
      M: "offs (ms' @ ns') 0 ! i ≤ k" and
      N: "k < length ws' + length xs'"
    have O: "length ?ws = Suc (Suc m)"
      using H and I by simp
    with D [symmetric] have P: "length ws' = Suc (Suc m)"
      by (simp add: round_suc_suc_def Let_def fill_length split: if_split_asm)
    have Q: "⋀i. i < m ⟹
      the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! i) ∈ set ?ws"
    proof -
      fix i
      let ?x = "the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! i)"
      assume R: "i < m"
      hence "0 < m" by simp
      hence "0 < ?k"
        by (drule_tac bn_comp_fst_nonzero [OF G], subst (asm) F,
         simp split: nat.split)
      hence "count (mset (map the (fill ?zs (offs ?ms 0)
        index key (length ?zs) ?mi ?ma))) ?x = count (mset ?zs) ?x"
        by (rule_tac fill_offs_enum_count_item [OF A], simp, rule_tac conjI,
         ((rule_tac mini_lb | rule_tac maxi_ub), erule_tac in_set_nthsD)+)
      hence "count (mset (map the (fill ?zs (offs ?ms 0)
        index key m ?mi ?ma))) ?x = count (mset ?zs) ?x"
        using O by (simp add: mini_maxi_nths)
      moreover have "0 < count (mset (map the (fill ?zs (offs ?ms 0)
        index key m ?mi ?ma))) ?x"
        using R by (simp add: fill_length)
      ultimately have "?x ∈ set ?zs" by simp
      thus "?x ∈ set ?ws"
        by (rule in_set_nthsD)
    qed
    have R: "⋀i. i < Suc (Suc m) ⟹ Suc (Suc m) ≤ k ⟹
      key (?ws ! i) ≤ key (xs' ! (k - Suc (Suc m)))"
    proof -
      fix i
      have "bn_inv p q (v, ns, ?ys)"
        using C by simp
      moreover have "add_inv (n - Suc (Suc m)) (v, ns, ?ys)"
        using H and I by simp
      moreover have "count_inv (λx. count (mset ?ys) x) (v, ns, ?ys)"
        by simp
      ultimately have "count_inv (λx. count (mset ?ys) x) (?t r' v)"
        by (rule round_count_inv [OF A])
      hence S: "count (mset xs') (xs' ! (k - Suc (Suc m))) =
        count (mset ?ys) (xs' ! (k - Suc (Suc m)))"
        using E by simp
      have "k < Suc (Suc (m + length xs'))"
        using N and P by simp
      moreover assume "Suc (Suc m) ≤ k"
      ultimately have "0 < count (mset xs') (xs' ! (k - Suc (Suc m)))"
        by simp
      hence "xs' ! (k - Suc (Suc m)) ∈ set ?ys"
        using S by simp
      hence "∃p < length ?ys. ?ys ! p = xs' ! (k - Suc (Suc m))"
        by (simp add: in_set_conv_nth)
      then obtain p where
        T: "p < length ?ys ∧ ?ys ! p = xs' ! (k - Suc (Suc m))" ..
      have "Suc 0 < Suc (length ns) ⟶
        (∀j < (0 # offs ns (Suc (Suc m))) ! Suc 0.
         ∀k ∈ {(0 # offs ns (Suc (Suc m))) ! Suc 0..<n}.
           key (xs ! j) ≤ key (xs ! k))"
        using J ..
      moreover have U: "0 < length ns"
        using H [symmetric] and I and T by (rule_tac ccontr, simp)
      ultimately have "∀j < offs ns (Suc (Suc m)) ! 0.
        ∀k ∈ {offs ns (Suc (Suc m)) ! 0..<n}. key (xs ! j) ≤ key (xs ! k)"
        by simp
      moreover assume "i < Suc (Suc m)"
      moreover have "offs ns (Suc (Suc m)) ! 0 = Suc (Suc m)"
        using U by (subst offs_base_zero, simp, cases ns, simp_all)
      ultimately have "∀k ∈ {Suc (Suc m)..<n}. key (?ws ! i) ≤ key (xs ! k)"
        by simp
      moreover have "Suc (Suc m) + p ∈ {Suc (Suc m)..<n}"
        using I and T by (simp, arith)
      ultimately have "key (?ws ! i) ≤ key (xs ! (Suc (Suc m) + p))" ..
      thus "key (?ws ! i) ≤ key (xs' ! (k - Suc (Suc m)))"
        using O and T by simp
    qed
    assume "⋀ws a b c d e f g h n'.
      ws = ?ws ⟹ a = (m', r') ⟹ b = m' ∧ c = r' ⟹
      d = (v, ms', ws') ⟹ e = v ∧ f = (ms', ws') ⟹ g = ms' ∧ h = ws' ⟹
        ?P n' ⟶ ?Q n' ⟶ ?R"
    hence "?P (n - Suc (Suc m)) ⟶ ?Q (n - Suc (Suc m)) ⟶ ?R"
      by simp
    hence "?Q (n - Suc (Suc m)) ⟶ ?R"
      using H by simp
    moreover have "?Q (n - Suc (Suc m))"
    proof ((rule allI, rule impI)+, rule ballI, simp, erule conjE,
     subst (1 2) append_take_drop_id [of "Suc (Suc m)", symmetric],
     simp only: nth_append O, simp)
      fix i j k
      have "Suc i < Suc (length ns) ⟶
        (∀j < (0 # offs ns (Suc (Suc m))) ! Suc i.
         ∀k ∈ {(0 # offs ns (Suc (Suc m))) ! Suc i..<n}.
           key ((xs) ! j) ≤ key (xs ! k))"
        using J ..
      moreover assume "i < length ns"
      ultimately have "j < offs ns 0 ! i ⟶
        (∀k ∈ {offs ns 0 ! i + Suc (Suc m)..<n}.
          key (xs ! (Suc (Suc m) + j)) ≤ key (xs ! k))"
        by (simp, subst (asm) offs_base_zero, simp,
         subst (asm) (2) offs_base_zero, simp_all)
      moreover assume "j < offs ns 0 ! i"
      ultimately have "∀k ∈ {offs ns 0 ! i + Suc (Suc m)..<n}.
        key (?ys ! j) ≤ key (xs ! k)"
        using O by simp
      moreover assume "offs ns 0 ! i ≤ k" and "k < n - Suc (Suc m)"
      hence "Suc (Suc m) + k ∈ {offs ns 0 ! i + Suc (Suc m)..<n}"
        by simp
      ultimately have "key (?ys ! j) ≤ key (xs ! (Suc (Suc m) + k))" ..
      thus "key (?ys ! j) ≤ key (?ys ! k)"
        using O by simp
    qed
    ultimately have ?R ..
    show "key ((ws' @ xs') ! j) ≤ key ((ws' @ xs') ! k)"
    proof (simp add: nth_append not_less P, (rule_tac [!] conjI,
     rule_tac [!] impI)+, rule_tac [3] FalseE)
      assume
        S: "j < Suc (Suc m)" and
        T: "k < Suc (Suc m)"
      from D [symmetric] show "key (ws' ! j) ≤ key (ws' ! k)"
      proof (simp add: round_suc_suc_def Let_def split: if_split_asm,
       (erule_tac [2] conjE)+, simp_all)
        assume U: "?mi = ?ma"
        have "j < length ?ws"
          using S and O by simp
        hence "?ws ! j ∈ set ?ws"
          by (rule nth_mem)
        with U have "key (?ws ! j) = ?ma"
          by (rule mini_maxi_keys_eq)
        moreover have "k < length ?ws"
          using T and O by simp
        hence "?ws ! k ∈ set ?ws"
          by (rule nth_mem)
        with U have "key (?ws ! k) = ?ma"
          by (rule mini_maxi_keys_eq)
        ultimately show "key (?ws ! j) ≤ key (?ws ! k)" by simp
      next
        assume U: "ms' = Suc 0 # ?ms @ [Suc 0]"
        hence V: "j < (0 # offs (?ms @ Suc 0 # ns') (Suc 0)) ! i"
          using L by simp
        hence "∃i'. i = Suc i'"
          by (rule_tac nat.exhaust [of i], simp_all)
        then obtain i' where W: "i = Suc i'" ..
        have "i < Suc (Suc (?k + length ns'))"
          using K and U by (simp add: enum_length)
        hence X: "i' < Suc (?k + length ns')"
          using W by simp
        hence Y: "j < Suc (offs (?ms @ Suc 0 # ns') 0 ! i')"
          using V and W by (simp add: enum_length offs_suc)
        have "(0 # offs (?ms @ Suc 0 # ns') (Suc 0)) ! i ≤ k"
          using M and U by simp
        hence "Suc (offs (?ms @ Suc 0 # ns') 0 ! i') ≤ k"
          using W and X by (simp add: enum_length offs_suc)
        moreover from this have "∃k'. k = Suc k'"
          by (rule_tac nat.exhaust [of k], simp_all)
        then obtain k' where Z: "k = Suc k'" ..
        ultimately have AA: "offs (?ms @ Suc 0 # ns') 0 ! i' ≤ k'"
          by simp
        have AB: "j ≤ k'"
          using Y and AA by simp
        with Z show
         "key ((?xmi # map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma) @
            [?xma]) ! j) ≤
          key ((?xmi # map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma) @
            [?xma]) ! k)"
        proof (cases j, case_tac [2] "j < Suc m", simp_all add: nth_append
         not_less fill_length, rule_tac [1-2] conjI, rule_tac [1-4] impI,
         rule_tac [5] FalseE, simp_all)
          assume "k' < m"
          hence "the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! k') ∈ set ?ws"
            by (rule Q)
          thus "?mi ≤ key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! k'))"
            by (rule mini_lb)
        next
          assume "m ≤ k'"
          hence "k' = m"
            using T and Z by simp
          thus "?mi ≤ key ([?xma] ! (k' - m))"
            by (simp, rule_tac mini_maxi_keys_le, rule_tac nth_mem [of 0],
             subst O, simp)
        next
          fix j'
          have "sort_inv key (0, ?ms, map the (fill ?zs (offs ?ms 0) index key
            (length ?zs) ?mi ?ma))"
            by (rule fill_sort_inv [OF A B], simp, rule conjI,
             ((rule mini_lb | rule maxi_ub), erule in_set_nthsD)+)
          hence "sort_inv key (0, ?ms, map the (fill ?zs (offs ?ms 0) index key
            m ?mi ?ma))"
            using O by (simp add: mini_maxi_nths)
          hence "∀i < ?k. ∀j < offs ?ms 0 ! i. ∀k ∈ {offs ?ms 0 ! i..<m}.
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j)) ≤
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! k))"
            by (simp add: enum_length fill_length)
          moreover assume AC: "k' < m"
          hence AD: "offs (?ms @ Suc 0 # ns') 0 ! i' < m"
            using AA by simp
          have AE: "i' < ?k"
          proof (rule contrapos_pp [OF AD], simp add: not_less offs_append
           nth_append offs_length enum_length)
            have "0 < m"
              using AC by simp
            hence "0 < ?k"
              by (drule_tac bn_comp_fst_nonzero [OF G], subst (asm) F,
               simp split: nat.split)
            with A have "foldl (+) 0 ?ms = length ?zs"
              by (rule enum_add, simp, rule_tac conjI,
               ((rule_tac mini_lb | rule_tac maxi_ub), erule_tac in_set_nthsD)+)
            hence "foldl (+) 0 ?ms = m"
              using O by (simp add: mini_maxi_nths)
            with X show "m ≤ (foldl (+) 0 ?ms #
              offs ns' (Suc (foldl (+) 0 ?ms))) ! (i' - ?k)"
              by (cases "i' - ?k", simp_all, subst offs_base_zero, simp_all)
          qed
          ultimately have "∀j < offs ?ms 0 ! i'. ∀k ∈ {offs ?ms 0 ! i'..<m}.
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j)) ≤
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! k))"
            by simp
          moreover assume "j = Suc j'"
          with Y and AE have "j' < offs ?ms 0 ! i'"
            by (simp add: offs_append nth_append offs_length enum_length)
          ultimately have "∀k ∈ {offs ?ms 0 ! i'..<m}.
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j')) ≤
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! k))"
            by simp
          moreover from AA and AE have "offs ?ms 0 ! i' ≤ k'"
            by (simp add: offs_append nth_append offs_length enum_length)
          hence "k' ∈ {offs ?ms 0 ! i'..<m}"
            using AC by simp
          ultimately show
           "key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j')) ≤
            key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! k'))" ..
        next
          fix j'
          assume "j' < m"
          hence "the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j') ∈ set ?ws"
            (is "?x ∈ _")
            by (rule Q)
          moreover assume "m ≤ k'"
          hence "k' = m"
            using T and Z by simp
          ultimately show "key ?x ≤ key ([?xma] ! (k' - m))"
            by (simp, rule_tac maxi_ub)
        next
          fix j'
          assume "j = Suc j'" and "m ≤ j'"
          hence "Suc m ≤ j" by simp
          hence "Suc (Suc m) ≤ k"
            using Z and AB by simp
          thus False
            using T by simp
        qed
      qed
    next
      assume
        S: "j < Suc (Suc m)" and
        T: "Suc (Suc m) ≤ k"
      from D [symmetric] show "key (ws' ! j) ≤ key (xs' ! (k - Suc (Suc m)))"
      proof (simp add: round_suc_suc_def Let_def split: if_split_asm,
       rule_tac R [OF S T], cases j, case_tac [2] "j < Suc m",
       simp_all add: nth_append not_less fill_length)
        have "?nmi < length ?ws"
          using O by (rule_tac mini_less, simp)
        hence "?nmi < Suc (Suc m)"
          using O by simp
        thus "?mi ≤ key (xs' ! (k - Suc (Suc m)))"
          using T by (rule R)
      next
        fix j'
        assume "j' < m"
        hence U: "the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j') ∈ set ?ws"
          by (rule Q)
        have "∃p < Suc (Suc m). ?ws ! p =
          the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j')"
          using O and U by (simp add: in_set_conv_nth)
        then obtain p where V: "p < Suc (Suc m) ∧ ?ws ! p =
          the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j')" ..
        hence "key (?ws ! p) ≤ key (xs' ! (k - Suc (Suc m)))"
          using T by (rule_tac R, simp)
        thus "key (the (fill ?zs (offs ?ms 0) index key m ?mi ?ma ! j')) ≤
          key (xs' ! (k - Suc (Suc m)))"
          using V by simp
      next
        fix j'
        assume "j = Suc j'" and "m ≤ j'"
        moreover from this have "Suc m ≤ j" by simp
        hence "j = Suc m"
          using S by simp
        ultimately have "j' = m" by simp
        thus "key ([?xma] ! (j' - m)) ≤ key (xs' ! (k - Suc (Suc m)))"
        proof simp
          have "?nma < length ?ws"
            using O by (rule_tac maxi_less, simp)
          hence "?nma < Suc (Suc m)"
            using O by simp
          thus "?ma ≤ key (xs' ! (k - Suc (Suc m)))"
            using T by (rule R)
        qed
      qed
    next
      assume "k < Suc (Suc m)" and "Suc (Suc m) ≤ j"
      hence "k < j" by simp
      moreover have "j < k"
        using L and M by simp
      ultimately show False by simp
    next
      assume
        S: "Suc (Suc m) ≤ j" and
        T: "Suc (Suc m) ≤ k"
      have U: "0 < length ns' ∧ 0 < length xs'"
      proof (rule ccontr, simp, erule disjE)
        have "bn_inv p q (v, ns, ?ys)"
          using C by simp
        moreover have "add_inv (n - Suc (Suc m)) (v, ns, ?ys)"
          using H and I by simp
        ultimately have "add_inv (n - Suc (Suc m)) (?t r' v)"
          by (rule round_add_inv [OF A])
        hence "length xs' = foldl (+) 0 ns'"
          using E by simp
        moreover assume "ns' = []"
        ultimately have "length xs' = 0" by simp
        hence "k < Suc (Suc m)"
          using N and P by simp
        thus False
          using T by simp
      next
        assume "xs' = []"
        hence "k < Suc (Suc m)"
          using N and P by simp
        thus False
          using T by simp
      qed
      hence V: "i - length ms' < length ns'"
        using K by arith
      hence W: "∀j < offs ns' 0 ! (i - length ms').
        ∀k ∈ {offs ns' 0 ! (i - length ms')..<length xs'}.
          key (xs' ! j) ≤ key (xs' ! k)"
        using ‹?R› by simp
      from D [symmetric] have X: "foldl (+) 0 ms' = Suc (Suc m)"
      proof (simp add: round_suc_suc_def Let_def add_replicate add_suc
       split: if_split_asm, cases "m = 0")
        case True
        hence "?k = 0" by simp
        hence "length ?ms = 0"
          by (simp add: enum_length)
        thus "foldl (+) 0 ?ms = m"
          using True by simp
      next
        case False
        hence "0 < ?k"
          by (simp, drule_tac bn_comp_fst_nonzero [OF G], subst (asm) F,
           simp split: nat.split)
        with A have "foldl (+) 0 ?ms = length ?zs"
          by (rule enum_add, simp, rule_tac conjI,
           ((rule_tac mini_lb | rule_tac maxi_ub), erule_tac in_set_nthsD)+)
        thus "foldl (+) 0 ?ms = m"
          using O by (simp add: mini_maxi_nths)
      qed
      have "length ms' < i"
      proof (rule ccontr, simp add: not_less)
        assume "i ≤ length ms'"
        moreover have "length ms' < length (ms' @ ns')"
          using U by simp
        ultimately have "offs (ms' @ ns') 0 ! i ≤
          offs (ms' @ ns') 0 ! (length ms')"
          by (rule offs_mono)
        also have "… = Suc (Suc m)"
          using U and X by (simp add: offs_append nth_append offs_length,
           cases ns', simp_all)
        finally have "offs (ms' @ ns') 0 ! i ≤ Suc (Suc m)" .
        hence "j < Suc (Suc m)"
          using L by simp
        thus False
          using S by simp
      qed
      hence Y: "offs (ms' @ ns') 0 ! i =
        Suc (Suc m) + offs ns' 0 ! (i - length ms')"
        using X by (simp add: offs_append nth_append offs_length,
         subst offs_base_zero [OF V], simp)
      hence "j < Suc (Suc m) + offs ns' 0 ! (i - length ms')"
        using L by simp
      moreover from this have "0 < offs ns' 0 ! (i - length ms')"
        using S by (rule_tac ccontr, simp)
      ultimately have "j - Suc (Suc m) < offs ns' 0 ! (i - length ms')"
        by simp
      hence Z: "∀k ∈ {offs ns' 0 ! (i - length ms')..<length xs'}.
        key (xs' ! (j - Suc (Suc m))) ≤ key (xs' ! k)"
        using W by simp
      have "offs ns' 0 ! (i - length ms') ≤ k - Suc (Suc m)"
        using M and Y by simp
      moreover have "k - Suc (Suc m) < length xs'"
        using N and P and U by arith
      ultimately have "k - Suc (Suc m) ∈
        {offs ns' 0 ! (i - length ms')..<length xs'}"
        by simp
      with Z show "key (xs' ! (j - Suc (Suc m))) ≤
        key (xs' ! (k - Suc (Suc m)))" ..
    qed
  qed
qed

lemma gcsort_sort_inv:
  assumes
    A: "index_less index key" and
    B: "index_mono index key" and
    C: "add_inv n t" and
    D: "n ≤ p"
  shows "⟦t' ∈ gcsort_set index key p t; sort_inv key t⟧ ⟹
    sort_inv key t'"
by (erule gcsort_set.induct, simp, drule gcsort_add_inv [OF A _ C D],
 rule round_sort_inv [OF A B], simp_all del: bn_inv.simps, erule conjE,
 frule sym, erule subst, rule bn_inv_intro, insert D, simp)

text ‹
\null

The only remaining task is to address step 10 of the proof method, which is done by proving theorem
@{text gcsort_sorted}. It holds under the conditions that the objects' number is not larger than the
counters' upper bound and function @{text index} satisfies both predicates @{const index_less} and
@{const index_mono}, and states that function @{const gcsort} is successful in sorting the input
objects' list.

\null
›

theorem gcsort_sorted:
  assumes
    A: "index_less index key" and
    B: "index_mono index key" and
    C: "length xs ≤ p"
  shows "sorted (map key (gcsort index key p xs))"
proof -
  let ?t = "(0, [length xs], xs)"
  have "sort_inv key (gcsort_aux index key p ?t)"
    by (rule gcsort_sort_inv [OF A B _ C], rule gcsort_add_input,
     rule gcsort_aux_set, rule gcsort_sort_input)
  moreover have "add_inv (length xs) (gcsort_aux index key p ?t)"
    by (rule gcsort_add_inv [OF A _ _ C],
     rule gcsort_aux_set, rule gcsort_add_input)
  ultimately have "sorted (map key (gcsort_out (gcsort_aux index key p ?t)))"
    by (rule gcsort_sort_intro, simp add: gcsort_sort_form)
  moreover have "?t = gcsort_in xs"
    by (simp add: gcsort_in_def)
  ultimately show ?thesis
    by (simp add: gcsort_def)
qed

end