Theory Stability

(*  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 algorithm's stability"

theory Stability
  imports Sorting
begin

text ‹
\null

In this section, it is formally proven that GCsort is \emph{stable}, viz. that the sublist of the
output of function @{const gcsort} built by picking out the objects having a given key matches the
sublist of the input objects' list built in the same way.

Here below, steps 5, 6, and 7 of the proof method are accomplished. Particularly, @{text stab_inv}
is the predicate that will be shown to be invariant over inductive set @{const gcsort_set}.

\null
›

fun stab_inv :: "('b ⇒ 'a list) ⇒ ('a ⇒ 'b) ⇒ nat × nat list × 'a list ⇒
  bool" where
"stab_inv f key (u, ns, xs) = (∀k. [x←xs. key x = k] = f k)"

lemma gcsort_stab_input:
 "stab_inv (λk. [x←xs. key x = k]) key (0, [length xs], xs)"
by simp

lemma gcsort_stab_intro:
 "stab_inv f key t ⟹ [x←gcsort_out t. key x = k] = f k"
by (cases t, simp add: gcsort_out_def)

text ‹
\null

In what follows, step 9 of the proof method is accomplished.

First, lemma @{text fill_offs_enum_stable} proves that function @{const fill}, if its input offsets'
list is computed via the composition of functions @{const offs} and @{const enum}, does not modify
the sublist of its input objects' list formed by the objects having a given key. Moreover, lemmas
@{text mini_stable} and @{text maxi_stable} prove that the extraction of the leftmost minimum and
the rightmost maximum from an objects' list through functions @{const mini} and @{const maxi} is
endowed with the same property.

These lemmas are then used to prove lemma @{text gcsort_stab_inv}, which states that the sublist of
the objects having a given key within the objects' list is still the same after any recursive round.

\null
›

lemma fill_stable [rule_format]:
  assumes
    A: "index_less index key" and
    B: "index_same index key"
  shows
   "(∀x ∈ set xs. key x ∈ {mi..ma}) ⟶
    ns ≠ [] ⟶
    offs_pred ns ub xs index key mi ma ⟶
      map the [w←fill xs ns index key ub mi ma. ∃x. w = Some x ∧ key x = k] =
        [x←xs. k = key x]"
proof (induction xs arbitrary: ns, simp_all add: Let_def, rule conjI,
 (rule_tac [!] impI)+, (erule_tac [!] conjE)+, 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)]"
  let ?ws = "[w←fill xs ?ns' index key ub mi ma.
    ∃y. w = Some y ∧ key y = key x]"
  let ?ws' = "[w←(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x].
    ∃y. w = Some y ∧ key y = key x]"
  assume
    C: "∀x ∈ set xs. mi ≤ key x ∧ key x ≤ ma" and
    D: "mi ≤ key x" and
    E: "key x ≤ ma" and
    F: "ns ≠ []" and
    G: "offs_pred ns ub (x # xs) index key mi ma"
  have H: "?i < length ns"
    using A and D and E and F by (simp add: index_less_def)
  assume "⋀ns. ns ≠ [] ⟶ offs_pred ns ub xs index key mi ma ⟶
    map the [w←fill xs ns index key ub mi ma.
      ∃y. w = Some y ∧ key y = key x] =
    [y←xs. key x = key y]"
  moreover have I: "offs_pred ?ns' ub xs index key mi ma"
    using G and H by (rule_tac offs_pred_cons, simp_all)
  ultimately have J: "map the ?ws = [y←xs. key x = key y]"
    using F by simp
  have "ns ! ?i + offs_num (length ns) (x # xs) index key mi ma ?i ≤ ub"
    using G and H by (rule offs_pred_ub, simp add: offs_num_cons)
  hence K: "ns ! ?i < ub"
    by (simp add: offs_num_cons)
  moreover from this have
    L: "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (ns ! ?i) = Some x"
    by (subst nth_list_update_eq, simp_all add: fill_length)
  ultimately have "0 < length ?ws'"
    by (simp add: length_filter_conv_card card_gt_0_iff,
     rule_tac exI [where x = "ns ! ?i"], simp add: fill_length)
  hence "∃w ws. ?ws' = w # ws"
    by (rule_tac list.exhaust [of ?ws'], simp_all)
  then obtain w and ws where "?ws' = w # ws" by blast
  hence "∃us vs y.
    (fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] = us @ w # vs ∧
    (∀u ∈ set us. ∀y. u = Some y ⟶ key y ≠ key x) ∧
    w = Some y ∧ key y = key x ∧
    ws = [w←vs. ∃y. w = Some y ∧ key y = key x]"
    (is "∃us vs y. ?P us vs y")
    by (simp add: filter_eq_Cons_iff, blast)
  then obtain us and vs and y where M: "?P us vs y" by blast
  let ?A = "{i. i < length ns ∧ 0 < offs_num (length ns) xs index key mi ma i ∧
    ns ! i ≤ length us}"
  have "length us = ns ! ?i"
  proof (rule ccontr, erule neqE, cases "?A = {}",
   cases "0 < offs_num (length ns) xs index key mi ma 0", simp_all only: not_gr0)
    assume
      N: "length us < ns ! ?i" and
      O: "?A = {}" and
      P: "0 < offs_num (length ns) xs index key mi ma 0"
    have "length us < ns ! 0"
    proof (rule ccontr, simp add: not_less)
      assume "ns ! 0 ≤ length us"
      with F and P have "0 ∈ ?A" by simp
      with O show False by blast
    qed
    hence "length us < ?ns' ! 0"
      using F by (cases ?i, simp_all)
    hence "offs_none ?ns' ub xs index key mi ma (length us)"
      using P by (simp add: offs_none_def)
    hence "fill xs ?ns' index key ub mi ma ! (length us) = None"
      using C and F and I by (rule_tac fill_none [OF A], simp_all)
    hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (length us) = None"
      using N by simp
    thus False
      using M by simp
  next
    assume
      N: "length us < ns ! ?i" and
      O: "?A = {}" and
      P: "offs_num (length ns) xs index key mi ma 0 = 0"
    from K and N have "length us < offs_next ?ns' ub xs index key mi ma 0"
    proof (rule_tac ccontr, simp only: not_less offs_next_def split: if_split_asm)
      assume "offs_set_next ?ns' xs index key mi ma 0 ≠ {}"
        (is "?B ≠ _")
      hence "Min ?B ∈ ?B"
        by (rule_tac Min_in, simp)
      moreover assume "?ns' ! Min ?B ≤ length us"
      hence "ns ! Min ?B ≤ length us"
        using H by (cases "Min ?B = ?i", simp_all)
      ultimately have "Min ?B ∈ ?A" by simp
      with O show False by blast
    qed
    hence "offs_none ?ns' ub xs index key mi ma (length us)"
      using P by (simp add: offs_none_def)
    hence "fill xs ?ns' index key ub mi ma ! (length us) = None"
      using C and F and I by (rule_tac fill_none [OF A], simp_all)
    hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (length us) = None"
      using N by simp
    thus False
      using M by simp
  next
    assume N: "length us < ns ! ?i"
    assume "?A ≠ {}"
    hence "Max ?A ∈ ?A"
      by (rule_tac Max_in, simp)
    moreover from this have O: "Max ?A ≠ ?i"
      using N by (rule_tac notI, simp)
    ultimately have "index key y (length ?ns') mi ma = Max ?A"
    using C proof (rule_tac fill_index [OF A _ I, where j = "length us"], simp_all,
     rule_tac ccontr, simp only: not_less not_le offs_next_def split: if_split_asm)
      assume "ub ≤ length us"
      with N have "ub < ns ! ?i" by simp
      with K show False by simp
    next
      let ?B = "offs_set_next ?ns' xs index key mi ma (Max ?A)"
      assume "?ns' ! Min ?B ≤ length us"
      hence "ns ! Min ?B ≤ length us"
        using H by (cases "Min ?B = ?i", simp_all)
      moreover assume "?B ≠ {}"
      hence P: "Min ?B ∈ ?B"
        by (rule_tac Min_in, simp)
      ultimately have "Min ?B ∈ ?A" by simp
      hence "Min ?B ≤ Max ?A"
        by (rule_tac Max_ge, simp)
      thus False
        using P by simp
    next
      have "fill xs ?ns' index key ub mi ma ! length us =
        (fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! length us"
        using N by simp
      thus "fill xs ?ns' index key ub mi ma ! length us = Some y"
        using M by simp
    qed
    moreover have "index key y (length ?ns') mi ma = ?i"
      using B and D and E and M by (cases "y = x", simp_all add:
       index_same_def)
    ultimately show False
      using O by simp
  next
    assume N: "ns ! ?i < length us"
    hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (ns ! ?i) =
      us ! (ns ! ?i)"
      using M by (simp add: nth_append)
    hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] ! (ns ! ?i) ∈ set us"
      using N by simp
    thus False
      using L and M by blast
  qed
  hence "take (ns ! ?i) ((fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x]) = us"
    using M by simp
  hence N: "take (ns ! ?i) (fill xs ?ns' index key ub mi ma) = us" by simp
  have "fill xs ?ns' index key ub mi ma =
    take (ns ! ?i) (fill xs ?ns' index key ub mi ma) @
    fill xs ?ns' index key ub mi ma ! (ns ! ?i) #
    drop (Suc (ns ! ?i)) (fill xs ?ns' index key ub mi ma)"
    (is "_ = ?ts @ _ # ?ds")
    using K by (rule_tac id_take_nth_drop, simp add: fill_length)
  moreover have "fill xs ?ns' index key ub mi ma ! (ns ! ?i) = None"
    using C and D and E and F and G by (rule_tac fill_index_none [OF A],
     simp_all)
  ultimately have O: "fill xs ?ns' index key ub mi ma = us @ None # ?ds"
    using N by simp
  have "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] =
    ?ts @ Some x # ?ds"
    using K by (rule_tac upd_conv_take_nth_drop, simp add: fill_length)
  hence "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] =
    us @ Some x # ?ds"
    using N by simp
  hence "?ws' = Some x # [w←?ds. ∃y. w = Some y ∧ key y = key x]"
    using M by simp
  also have "… = Some x # ?ws"
    using M by (subst (2) O, simp)
  finally show "map the ?ws' = x # [y←xs. key x = key y]"
    using J by simp
next
  fix x xs and ns :: "nat list"
  let ?i = "index key x (length ns) mi ma"
  let ?ns' = "ns[?i := Suc (ns ! ?i)]"
  let ?ws = "[w←fill xs ?ns' index key ub mi ma. ∃y. w = Some y ∧ key y = k]"
  let ?ws' = "[w←(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x].
    ∃y. w = Some y ∧ key y = k]"
  assume
    C: "∀x ∈ set xs. mi ≤ key x ∧ key x ≤ ma" and
    D: "mi ≤ key x" and
    E: "key x ≤ ma" and
    F: "ns ≠ []" and
    G: "offs_pred ns ub (x # xs) index key mi ma" and
    H: "k ≠ key x"
  have I: "?i < length ns"
    using A and D and E and F by (simp add: index_less_def)
  assume "⋀ns. ns ≠ [] ⟶ offs_pred ns ub xs index key mi ma ⟶
    map the [w←fill xs ns index key ub mi ma.
      ∃y. w = Some y ∧ key y = k] =
    [y←xs. k = key y]"
  moreover have "offs_pred ?ns' ub xs index key mi ma"
    using G and I by (rule_tac offs_pred_cons, simp_all)
  ultimately have J: "map the ?ws = [y←xs. k = key y]"
    using F by simp
  have "ns ! ?i + offs_num (length ns) (x # xs) index key mi ma ?i ≤ ub"
    using G and I by (rule offs_pred_ub, simp add: offs_num_cons)
  hence K: "ns ! ?i < ub"
    by (simp add: offs_num_cons)
  have "fill xs ?ns' index key ub mi ma =
    take (ns ! ?i) (fill xs ?ns' index key ub mi ma) @
    fill xs ?ns' index key ub mi ma ! (ns ! ?i) #
    drop (Suc (ns ! ?i)) (fill xs ?ns' index key ub mi ma)"
    (is "_ = ?ts @ _ # ?ds")
    using K by (rule_tac id_take_nth_drop, simp add: fill_length)
  moreover have "fill xs ?ns' index key ub mi ma ! (ns ! ?i) = None"
    using C and D and E and F and G by (rule_tac fill_index_none [OF A],
     simp_all)
  ultimately have L: "fill xs ?ns' index key ub mi ma = ?ts @ None # ?ds"
    by simp
  have "(fill xs ?ns' index key ub mi ma)[ns ! ?i := Some x] =
    ?ts @ Some x # ?ds"
    using K by (rule_tac upd_conv_take_nth_drop, simp add: fill_length)
  moreover have "?ws = [w←?ts. ∃y. w = Some y ∧ key y = k] @
    [w←?ds. ∃y. w = Some y ∧ key y = k]"
    by (subst L, simp)
  ultimately have "?ws' = ?ws"
    using H by simp
  thus "map the ?ws' = [y←xs. k = key y]"
    using J by simp
qed

lemma fill_offs_enum_stable [rule_format]:
  assumes
    A: "index_less index key" and
    B: "index_same index key"
  shows
   "∀x ∈ set xs. key x ∈ {mi..ma} ⟹
    0 < n ⟹
      [x←map the (fill xs (offs (enum xs index key n mi ma) 0)
        index key (length xs) mi ma). key x = k] = [x←xs. k = key x]"
  (is "_ ⟹ _ ⟹ [_←map the ?ys. _] = _"
   is "_ ⟹ _ ⟹ [_←map the (fill _ ?ns _ _ _ _ _). _] = _")
proof (subst fill_stable [symmetric, OF A B, of xs mi ma ?ns], simp,
 simp only: length_greater_0_conv [symmetric] offs_length enum_length,
 rule offs_enum_pred [OF A], simp, subst filter_map,
 simp add: filter_eq_nths fill_length)
  assume
    C: "∀x ∈ set xs. mi ≤ key x ∧ key x ≤ ma" and
    D: "0 < n"
  have "{i. i < length xs ∧ key (the (?ys ! i)) = k} =
    {i. i < length xs ∧ (∃x. ?ys ! i = Some x ∧ key x = k)}"
    (is "?A = ?B")
  proof (rule set_eqI, rule iffI, simp_all, erule_tac [!] conjE, erule_tac [2] exE,
   erule_tac [2] conjE, simp_all)
    fix i
    assume E: "i < length xs" and F: "key (the (?ys ! i)) = k"
    have "∃x. ?ys ! i = Some x"
    proof (cases "?ys ! i", simp_all)
      assume "?ys ! i = None"
      moreover have "?ys ! i ∈ set ?ys"
        using E by (rule_tac nth_mem, simp add: fill_length)
      ultimately have "None ∈ set ?ys" by simp
      moreover have "count (mset ?ys) None = 0"
        using C and D by (rule_tac fill_offs_enum_count_none [OF A], simp)
      ultimately show False by simp
    qed
    then obtain x where "?ys ! i = Some x" ..
    moreover from this have "key x = k"
      using F by simp
    ultimately show "∃x. ?ys ! i = Some x ∧ key x = k" by simp
  qed
  thus "map the (nths ?ys ?A) = map the (nths ?ys ?B)" by simp
qed

lemma mini_first [rule_format]:
 "xs ≠ [] ⟶ i < mini xs key ⟶
    key (xs ! mini xs key) < key (xs ! i)"
by (induction xs arbitrary: i, simp_all add: Let_def, (rule impI)+,
 erule conjE, simp add: not_le nth_Cons split: nat.split)

lemma maxi_last [rule_format]:
 "xs ≠ [] ⟶ maxi xs key < i ⟶ i < length xs ⟶
    key (xs ! i) < key (xs ! maxi xs key)"
by (induction xs arbitrary: i, simp_all add: Let_def, (rule impI)+,
 rule le_less_trans, rule maxi_ub, rule nth_mem, simp)

lemma nths_range:
 "nths xs A = nths xs (A ∩ {..<length xs})"
proof (induction xs arbitrary: A, simp_all add: nths_Cons)
  fix xs :: "'a list" and A
  assume "⋀A. nths xs A = nths xs (A ∩ {..<length xs})"
  hence "nths xs {i. Suc i ∈ A} = nths xs ({i. Suc i ∈ A} ∩ {..<length xs})" .
  moreover have
   "{i. Suc i ∈ A} ∩ {..<length xs} = {i. Suc i ∈ A ∧ i < length xs}"
    by blast
  ultimately show
   "nths xs {i. Suc i ∈ A} = nths xs {i. Suc i ∈ A ∧ i < length xs}"
    by simp
qed

lemma filter_nths_diff:
  assumes
    A: "i < length xs" and
    B: "¬ P (xs ! i)"
  shows "[x←nths xs (A - {i}). P x] = [x←nths xs A. P x]"
proof (cases "i ∈ A", simp_all)
  case True
  have C: "xs = take i xs @ xs ! i # drop (Suc i) xs"
    (is "_ = ?ts @ _ # ?ds")
    using A by (rule id_take_nth_drop)
  have "nths xs A = nths ?ts A @ nths (xs ! i # ?ds) {j. j + length ?ts ∈ A}"
    by (subst C, simp add: nths_append)
  moreover have D: "length ?ts = i"
    using A by simp
  ultimately have E: "nths xs A = nths ?ts (A ∩ {..<i}) @ xs ! i #
    nths ?ds {j. Suc j + i ∈ A}"
    (is "_ = ?vs @ _ # ?ws")
    using True by (simp add: nths_Cons, subst nths_range, simp)
  have "nths xs (A - {i}) = nths ?ts (A - {i}) @
    nths (xs ! i # ?ds) {j. j + length ?ts ∈ A - {i}}"
    by (subst C, simp add: nths_append)
  moreover have "(A - {i}) ∩ {..<i} = A ∩ {..<i}"
    by (rule set_eqI, rule iffI, simp_all)
  ultimately have "nths xs (A - {i}) = ?vs @ ?ws"
    using D by (simp add: nths_Cons, subst nths_range, simp)
  thus ?thesis
    using B and E by simp
qed

lemma mini_stable:
  assumes
    A: "xs ≠ []" and
    B: "mini xs key ∈ A"
      (is "?nmi ∈ _")
  shows "[x←[xs ! ?nmi] @ nths xs (A - {?nmi}). key x = k] =
    [x←nths xs A. key x = k]"
    (is "[x←[?xmi] @ _. _] = _")
proof (simp, rule conjI, rule_tac [!] impI, rule_tac [2] filter_nths_diff,
 rule_tac [2] mini_less, simp_all add: A)
  assume C: "key ?xmi = k"
  moreover have "?nmi < length xs"
    using A by (rule_tac mini_less, simp)
  ultimately have "0 < length [x←xs. key x = k]"
    by (simp add: length_filter_conv_card card_gt_0_iff, rule_tac exI, rule_tac conjI)
  hence "∃y ys. [x←xs. key x = k] = y # ys"
    by (rule_tac list.exhaust [of "[x←xs. key x = k]"], simp_all)
  then obtain y and ys where "[x←xs. key x = k] = y # ys" by blast
  hence "∃us vs. xs = us @ y # vs ∧
    (∀u ∈ set us. key u ≠ k) ∧ key y = k ∧ ys = [x←vs. key x = k]"
    (is "∃us vs. ?P us vs")
    by (simp add: filter_eq_Cons_iff)
  then obtain us and vs where D: "?P us vs" by blast
  have E: "length us = ?nmi"
  proof (rule ccontr, erule neqE)
    assume "length us < ?nmi"
    with A have "key ?xmi < key (xs ! length us)"
      by (rule mini_first)
    also have "… = k"
      using D by simp
    finally show False
      using C by simp
  next
    assume F: "?nmi < length us"
    hence "?xmi = us ! ?nmi"
      using D by (simp add: nth_append)
    hence "?xmi ∈ set us"
      using F by simp
    thus False
      using C and D by simp
  qed
  moreover have "xs ! length us = y"
    using D by simp
  ultimately have F: "?xmi = y" by simp
  have "nths xs A = nths us A @ nths (y # vs) {i. i + ?nmi ∈ A}"
    using D and E by (simp add: nths_append)
  also have "… = nths us A @ y # nths vs {i. Suc i + ?nmi ∈ A}"
    (is "_ = _ @ _ # ?ws")
    using B by (simp add: nths_Cons)
  finally have G: "[x←nths xs A. key x = k] = y # [x←?ws. key x = k]"
    using D by (simp add: filter_empty_conv, rule_tac ballI,
     drule_tac in_set_nthsD, simp)
  have "nths xs (A - {?nmi}) = nths us (A - {?nmi}) @
    nths (y # vs) {i. i + ?nmi ∈ A - {?nmi}}"
    using D and E by (simp add: nths_append)
  also have "… = nths us (A - {?nmi}) @ ?ws"
    by (simp add: nths_Cons)
  finally have H: "[x←nths xs (A - {?nmi}). key x = k] = [x←?ws. key x = k]"
    using D by (simp add: filter_empty_conv, rule_tac ballI,
     drule_tac in_set_nthsD, simp)
  show "?xmi # [x←nths xs (A - {?nmi}). key x = k] =
    [x←nths xs A. key x = k]"
    using F and G and H by simp
qed

lemma maxi_stable:
  assumes
    A: "xs ≠ []" and
    B: "maxi xs key ∈ A"
      (is "?nma ∈ _")
  shows "[x←nths xs (A - {?nma}) @ [xs ! ?nma]. key x = k] =
    [x←nths xs A. key x = k]"
    (is "[x←_ @ [?xma]. _] = _")
proof (simp, rule conjI, rule_tac [!] impI, rule_tac [2] filter_nths_diff,
 rule_tac [2] maxi_less, simp_all add: A)
  assume C: "key ?xma = k"
  moreover have D: "?nma < length xs"
    using A by (rule_tac maxi_less, simp)
  ultimately have "0 < length [x←rev xs. key x = k]"
    by (simp add: length_filter_conv_card card_gt_0_iff,
     rule_tac exI [where x = "length xs - Suc ?nma"], simp add: rev_nth)
  hence "∃y ys. [x←rev xs. key x = k] = y # ys"
    by (rule_tac list.exhaust [of "[x←rev xs. key x = k]"], simp_all)
  then obtain y and ys where "[x←rev xs. key x = k] = y # ys" by blast
  hence "∃us vs. rev xs = us @ y # vs ∧
    (∀u ∈ set us. key u ≠ k) ∧ key y = k ∧ ys = [x←vs. key x = k]"
    (is "∃us vs. ?P us vs")
    by (simp add: filter_eq_Cons_iff)
  then obtain us and vs where E: "?P us vs" by blast
  hence F: "xs = rev vs @ y # rev us"
    by (simp add: rev_swap)
  have G: "length us = length xs - Suc ?nma"
  proof (rule ccontr, erule neqE)
    assume "length us < length xs - Suc ?nma"
    hence "?nma < length xs - Suc (length us)" by simp
    moreover have "length xs - Suc (length us) < length xs"
      using D by simp
    ultimately have "key (xs ! (length xs - Suc (length us))) < key ?xma"
      by (rule maxi_last [OF A])
    moreover have "length us < length xs"
      using F by simp
    ultimately have "key (rev xs ! length us) < key ?xma"
      by (simp add: rev_nth)
    moreover have "key (rev xs ! length us) = k"
      using E by simp
    ultimately show False
      using C by simp
  next
    assume H: "length xs - Suc ?nma < length us"
    hence "rev xs ! (length xs - Suc ?nma) = us ! (length xs - Suc ?nma)"
      using E by (simp add: nth_append)
    hence "rev xs ! (length xs - Suc ?nma) ∈ set us"
      using H by simp
    hence "?xma ∈ set us"
      using D by (simp add: rev_nth)
    thus False
      using C and E by simp
  qed
  moreover have "rev xs ! length us = y"
    using E by simp
  ultimately have H: "?xma = y"
    using D by (simp add: rev_nth)
  have "length xs = length us + Suc ?nma"
    using D and G by simp
  hence I: "length vs = ?nma"
    using F by simp
  hence "nths xs A = nths (rev vs) A @ nths (y # rev us) {i. i + ?nma ∈ A}"
    using F by (simp add: nths_append)
  also have "… = nths (rev vs) (A ∩ {..<?nma}) @ y #
    nths (rev us) {i. Suc i + ?nma ∈ A}"
    (is "_ = ?ws @ _ # _")
    using B and I by (simp add: nths_Cons, subst nths_range, simp)
  finally have J: "[x←nths xs A. key x = k] = [x←?ws. key x = k] @ [y]"
    using E by (simp add: filter_empty_conv, rule_tac ballI,
     drule_tac in_set_nthsD, simp)
  have "nths xs (A - {?nma}) = nths (rev vs) (A - {?nma}) @
    nths (y # rev us) {i. i + ?nma ∈ A - {?nma}}"
    using F and I by (simp add: nths_append)
  hence "nths xs (A - {?nma}) = nths (rev vs) ((A - {?nma}) ∩ {..<?nma}) @
    nths (rev us) {i. Suc i + ?nma ∈ A}"
    using I by (simp add: nths_Cons, subst nths_range, simp)
  moreover have "(A - {?nma}) ∩ {..<?nma} = A ∩ {..<?nma}"
    by (rule set_eqI, rule iffI, simp_all)
  ultimately have K: "[x←nths xs (A - {?nma}). key x = k] =
    [x←?ws. key x = k]"
    using E by (simp add: filter_empty_conv, rule_tac ballI,
     drule_tac in_set_nthsD, simp)
  show "[x←nths xs (A - {?nma}). key x = k] @ [?xma] =
    [x←nths xs A. key x = k]"
    using H and J and K by simp
qed

lemma round_stab_inv [rule_format]:
 "index_less index key ⟶ index_same index key ⟶ bn_inv p q t ⟶
    add_inv n t ⟶ stab_inv f key t ⟶ stab_inv f key (round index key p q r t)"
proof (induction index key p q r t arbitrary: n f rule: round.induct,
 (rule_tac [!] impI)+, simp, simp, simp_all only: simp_thms)
  fix index p q r u ns xs n f and key :: "'a ⇒ 'b"
  let ?t = "round index key p q r (u, ns, tl xs)"
  assume
   "⋀n f. bn_inv p q (u, ns, tl xs) ⟶ add_inv n (u, ns, tl xs) ⟶
      stab_inv f key (u, ns, tl xs) ⟶ stab_inv f key ?t" and
   "bn_inv p q (u, Suc 0 # ns, xs)" and
   "add_inv n (u, Suc 0 # ns, xs)" and
   "stab_inv f key (u, Suc 0 # ns, xs)"
  thus "stab_inv f key (round index key p q r (u, Suc 0 # ns, xs))"
  proof (cases ?t, cases xs, simp_all add: add_suc, arith, erule_tac conjE,
   rule_tac allI, simp)
    fix k y ys xs'
    let ?f' = "f(key y := tl (f (key y)))"
    assume "⋀n' f'. foldl (+) 0 ns = n' ∧ length ys = n' ⟶
      (∀k'. [x←ys. key x = k'] = f' k') ⟶ (∀k'. [x←xs'. key x = k'] = f' k')"
    moreover assume "Suc (foldl (+) 0 ns) = n" and "Suc (length ys) = n"
    ultimately have "(∀k'. [x←ys. key x = k'] = ?f' k') ⟶
      (∀k'. [x←xs'. key x = k'] = ?f' k')"
      by blast
    moreover assume A: "∀k'. (if key y = k'
      then y # [x←ys. key x = k'] else [x←ys. key x = k']) = f k'"
    hence B: "f (key y) = y # [x←ys. key x = key y]"
      by (drule_tac spec [where x = "key y"], simp)
    hence "∀k'. [x←ys. key x = k'] = ?f' k'"
    proof (rule_tac allI, simp, rule_tac impI)
      fix k'
      assume "k' ≠ key y"
      thus "[x←ys. key x = k'] = f k'"
        using A by (drule_tac spec [where x = k'], simp)
    qed
    ultimately have C: "∀k'. [x←xs'. key x = k'] = ?f' k'" ..
    show "(key y = k ⟶ y # [x←xs'. key x = k] = f k) ∧
      (key y ≠ k ⟶ [x←xs'. key x = k] = f k)"
    proof (rule conjI, rule_tac [!] impI)
      assume "key y = k"
      moreover have "tl (f (key y)) = [x←xs'. key x = key y]"
        using C by simp
      hence "f (key y) = y # [x←xs'. key x = key y]"
        using B by (subst hd_Cons_tl [symmetric], simp_all)
      ultimately show "y # [x←xs'. key x = k] = f k" by simp
    next
      assume "key y ≠ k"
      thus "[x←xs'. key x = k] = f k"
        using C by simp
    qed
  qed
next
  fix index p q r u m ns n f 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_same index key"
  assume
   "⋀ws a b c d e g h i n f.
      ws = ?ws ⟹ a = bn_comp m p q r ⟹ (b, c) = bn_comp m p q r ⟹
      d = ?r b ⟹ (e, g) = ?r b ⟹ (h, i) = g ⟹
        bn_inv p q (e, ns, ?ys) ⟶ add_inv n (e, ns, ?ys) ⟶
          stab_inv f key (e, ns, ?ys) ⟶ stab_inv f key (?t c e)" and
   "bn_inv p q (u, Suc (Suc m) # ns, xs)" and
   "add_inv n (u, Suc (Suc m) # ns, xs)" and
   "stab_inv f key (u, Suc (Suc m) # ns, xs)"
  thus "stab_inv f 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)+)?)+,
   (erule_tac conjE)+, subst (asm) (2) add_base_zero, simp)
    fix m' r' v ms' ws' xs' k
    let ?f = "λk. [x←?ys. key x = k]"
    let ?P = "λf. ∀k. [x←?ys. key x = k] = f k"
    let ?Q = "λf. ∀k. [x←xs'. key x = k] = f k"
    assume
      C: "?r m' = (v, ms', ws')" and
      D: "bn_comp m p q r = (m', r')" and
      E: "bn_valid m p q" and
      F: "Suc (Suc (foldl (+) 0 ns + m)) = n" and
      G: "length xs = n"
    assume "⋀ws a b c d e g h i n' f.
      ws = ?ws ⟹ a = (m', r') ⟹ b = m' ∧ c = r' ⟹
      d = (v, ms', ws') ⟹ e = v ∧ g = (ms', ws') ⟹ h = ms' ∧ i = ws' ⟹
        foldl (+) 0 ns = n' ∧ n - Suc (Suc m) = n' ⟶ ?P f ⟶ ?Q f"
    hence "⋀f. foldl (+) 0 ns = n - Suc (Suc m) ⟶ ?P f ⟶ ?Q f"
      by simp
    hence "⋀f. ?P f ⟶ ?Q f"
      using F by simp
    hence "?P ?f ⟶ ?Q ?f" .
    hence "[x←xs'. key x = k] = [x←?ys. key x = k]" by simp
    moreover assume "∀k. [x←xs. key x = k] = f k"
    hence "f k = [x←?ws @ ?ys. key x = k]" by simp
    ultimately have "f k = [x←?ws. key x = k] @ [x←xs'. key x = k]"
      by (subst (asm) filter_append, simp)
    with C [symmetric] show "[x←ws'. key x = k] @ [x←xs'. key x = k] = f k"
    proof (simp add: round_suc_suc_def Let_def del: filter.simps
     split: if_split_asm)
      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"
      have H: "length ?ws = Suc (Suc m)"
        using F and G by simp
      hence I: "?nmi ≠ ?nma"
        by (rule_tac mini_maxi_neq, simp)
      have "[x←(([?xmi] @ map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma))
        @ [?xma]). key x = k] = [x←?ws. key x = k]"
      proof (cases "m = 0")
        case True
        have "?nmi < length ?ws"
          using H by (rule_tac mini_less, simp)
        hence J: "?nmi < Suc (Suc 0)"
          using True by simp
        moreover have "?nma < length ?ws"
          using H by (rule_tac maxi_less, simp)
        hence K: "?nma < Suc (Suc 0)"
          using True by simp
        ultimately have "card ({..<Suc (Suc 0)} - {?nma} - {?nmi}) = 0"
          using I by auto
        hence L: "{..<Suc (Suc 0)} - {?nma} - {?nmi} = {}" by simp
        have "length (fill ?zs (offs ?ms 0) index key m ?mi ?ma) = 0"
          using True by (simp add: fill_length)
        hence M: "map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma) =
          nths ?ws ({..<Suc (Suc 0)} - {?nma} - {?nmi})"
          by (subst L, simp)
        show ?thesis
        proof (subst M, subst filter_append)
          show "[x←[?xmi] @ nths ?ws ({..<Suc (Suc 0)} - {?nma} - {?nmi}).
            key x = k] @ [x←[?xma]. key x = k] = [x←?ws. key x = k]"
          proof (subst mini_stable, simp only: length_greater_0_conv
           [symmetric] H, simp add: I J, subst filter_append [symmetric])
            show "[x←nths ?ws ({..<Suc (Suc 0)} - {?nma}) @ [?xma].
              key x = k] = [x←?ws. key x = k]"
              by (subst maxi_stable, simp only: length_greater_0_conv
               [symmetric] H, simp add: K, simp add: True)
          qed
        qed
      next
        case False
        hence "0 < ?k"
          by (simp, drule_tac bn_comp_fst_nonzero [OF E], subst (asm) D,
           simp split: nat.split)
        hence "[x←map the (fill ?zs (offs ?ms 0) index key (length ?zs) ?mi ?ma).
          key x = k] = [x←?zs. k = key x]"
          by (rule_tac fill_offs_enum_stable [OF A B], simp, rule_tac conjI,
           ((rule_tac mini_lb | rule_tac maxi_ub), erule_tac in_set_nthsD)+)
        moreover have "[x←?zs. k = key x] = [x←?zs. key x = k]"
          by (rule filter_cong, simp, blast)
        ultimately have
          J: "[x←map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma).
            key x = k] = [x←?zs. key x = k]"
          using H by (simp add: mini_maxi_nths)
        show ?thesis
        proof (simp only: filter_append J, subst Compl_eq_Diff_UNIV,
         subst Diff_insert, subst filter_append [symmetric])
          show "[x←[?xmi] @ nths ?ws (UNIV - {?nma} - {?nmi}). key x = k]
            @ [x←[?xma]. key x = k] = [x←?ws. key x = k]"
          proof (subst mini_stable, simp only: length_greater_0_conv
           [symmetric] H, simp add: I, subst filter_append [symmetric])
            show "[x←nths ?ws (UNIV - {?nma}) @ [?xma]. key x = k] =
              [x←?ws. key x = k]"
              by (subst maxi_stable, simp only: length_greater_0_conv
               [symmetric] H, simp, subst nths_range, subst H, simp)
          qed
        qed
      qed
      thus "[x←?xmi # map the (fill ?zs (offs ?ms 0) index key m ?mi ?ma) @
        [?xma]. key x = k] = [x←?ws. key x = k]"
        by simp
    qed
  qed
qed

lemma gcsort_stab_inv:
  assumes
    A: "index_less index key" and
    B: "index_same index key" and
    C: "add_inv n t" and
    D: "n ≤ p"
  shows "⟦t' ∈ gcsort_set index key p t; stab_inv f key t⟧ ⟹
    stab_inv f key t'"
by (erule gcsort_set.induct, simp, drule gcsort_add_inv [OF A _ C D],
 rule round_stab_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_stable}. 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_same}, and states that function @{const gcsort} leaves unchanged the sublist of the
objects having a given key within the input objects' list.

\null
›

theorem gcsort_stable:
  assumes
    A: "index_less index key" and
    B: "index_same index key" and
    C: "length xs ≤ p"
  shows "[x←gcsort index key p xs. key x = k] = [x←xs. key x = k]"
proof -
  let ?t = "(0, [length xs], xs)"
  have "stab_inv (λk. [x←xs. key x = k]) key (gcsort_aux index key p ?t)"
    by (rule gcsort_stab_inv [OF A B _ C], rule gcsort_add_input,
     rule gcsort_aux_set, rule gcsort_stab_input)
  hence "[x←gcsort_out (gcsort_aux index key p ?t). key x = k] =
    [x←xs. key x = k]"
    by (rule gcsort_stab_intro)
  moreover have "?t = gcsort_in xs"
    by (simp add: gcsort_in_def)
  ultimately show ?thesis
    by (simp add: gcsort_def)
qed

end