Theory Buckets

theory Buckets
  imports 
    "../../util/Continuous_Interval" 
    List_Type
begin
section ‹Buckets›

subsection ‹Entire Bucket›

definition bucket :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat set"
  where
"bucket α T b ≡ {k |k. k < length T ∧ α (T ! k) = b}"

definition bucket_size :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"bucket_size α T b ≡ card (bucket α T b)"

definition bucket_upt :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat set"
  where
"bucket_upt α T b = {k |k. k < length T ∧ α (T ! k) < b}"

definition bucket_start :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"bucket_start α T b ≡ card (bucket_upt α T b)"

definition bucket_end :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"bucket_end α T b ≡ card (bucket_upt α T (Suc b))"

lemma bucket_upt_subset:
  "bucket_upt α T b ⊆ {0..<length T}"
  by (rule subsetI, simp add: bucket_upt_def)

lemma bucket_upt_subset_Suc:
  "bucket_upt α T b ⊆ bucket_upt α T (Suc b)"
  by (rule subsetI, simp add: bucket_upt_def)

lemma bucket_upt_un_bucket:
  "bucket_upt α T b ∪ bucket α T b = bucket_upt α T (Suc b)"
  apply (clarsimp simp: bucket_upt_def bucket_def)
  apply (intro equalityI subsetI; clarsimp)
  apply (erule disjE; clarsimp)
  done

lemma bucket_0:
  assumes "valid_list T" "α bot = 0" "strict_mono α" "length T = Suc k"
  shows "bucket α T 0 = {k}"
proof safe
  fix x
  assume "x ∈ bucket α T 0"
  then show "x = k"
    by (metis (mono_tags, lifting) assms bucket_def diff_Suc_1 le_neq_trans le_simps(2)
                                   mem_Collect_eq strict_mono_eq valid_list_def)
next
  show "k ∈ bucket α T 0"
    by (metis (mono_tags, lifting) assms(1,2,4) bucket_def diff_Suc_1 last_conv_nth lessI
                                   list.size(3) mem_Collect_eq order_less_irrefl valid_list_def)
qed

lemma finite_bucket:
  "finite (bucket α T x)"
  by (clarsimp simp: bucket_def)

lemma finite_bucket_upt:
  "finite (bucket_upt α T b)"
  by (meson bucket_upt_subset subset_eq_atLeast0_lessThan_finite)

lemma bucket_start_Suc:
  "bucket_start α T (Suc b) = bucket_start α T b + bucket_size α T b"
  apply (clarsimp simp: bucket_start_def bucket_size_def)
  apply (subst card_Un_disjoint[symmetric])
     apply (meson bucket_upt_subset subset_eq_atLeast0_lessThan_finite)
    apply (simp add: finite_bucket)
   apply (rule disjointI')
  apply (metis (mono_tags, lifting) bucket_def bucket_upt_def less_irrefl_nat mem_Collect_eq)
  apply (simp add: bucket_upt_un_bucket)
  done

lemma bucket_start_le:
  "b ≤ b' ⟹ bucket_start α T b ≤ bucket_start α T b'"
  apply (clarsimp simp: bucket_start_def)
  by (meson bucket_upt_subset bucket_upt_subset_Suc card_mono lift_Suc_mono_le
        subset_eq_atLeast0_lessThan_finite)

lemma bucket_start_Suc_eq_bucket_end:
  "bucket_start α T (Suc b) = bucket_end α T b"
  by (simp add: bucket_end_def bucket_start_def)

lemma bucket_end_le_length:
  "bucket_end α T b ≤ length T"
  apply (clarsimp simp: bucket_end_def)
  apply (insert card_mono[OF _  bucket_upt_subset[of α T "Suc b"]])
  apply (erule meta_impE, simp)
  apply (erule order.trans)
  apply simp
  done

lemma bucket_start_le_end:
  "bucket_start α T b ≤ bucket_end α T b"
  by (metis Suc_n_not_le_n bucket_start_Suc_eq_bucket_end bucket_start_le nat_le_linear)

lemma le_bucket_start_le_end:
  "b ≤ b' ⟹ bucket_start α T b ≤ bucket_end α T b'"
  using bucket_start_le bucket_start_le_end le_trans by blast

lemma bucket_end_le:
  "b ≤ b' ⟹ bucket_end α T b ≤ bucket_end α T b'"
  by (metis bucket_start_Suc_eq_bucket_end bucket_start_le_end lift_Suc_mono_le)

lemma less_bucket_end_le_start:
  "b < b' ⟹ bucket_end α T b ≤ bucket_start α T b'"
  by (metis Suc_leI bucket_start_Suc_eq_bucket_end bucket_start_le)

lemma bucket_end_def':
  "bucket_end α T b = bucket_start α T b + bucket_size α T b"
  by (metis bucket_start_Suc bucket_start_Suc_eq_bucket_end)

lemma valid_list_bucket_start_0:
  "⟦valid_list T; strict_mono α; α bot = 0⟧ ⟹
   bucket_start α T 0 = 0"
  by (clarsimp simp: bucket_start_def bucket_upt_def)

lemma bucket_upt_0:
  "bucket_upt α T 0 = {}"
  by (clarsimp simp: bucket_upt_def)

lemma bucket_start_0:
  "bucket_start α T 0 = 0"
  by (clarsimp simp: bucket_start_def bucket_upt_def)

lemma valid_list_bucket_upt_Suc_0:
  "⟦valid_list T; strict_mono α; α bot = 0; length T = Suc n⟧ ⟹
   bucket_upt α T (Suc 0) = {n}"
  apply (clarsimp simp: bucket_upt_def)
  apply (intro equalityI subsetI)
   apply (clarsimp simp: valid_list_def)
   apply (metis less_antisym strict_mono_eq)
  apply (clarsimp simp: valid_list_ex_def)
  done

lemma valid_list_bucket_end_0:
  "⟦valid_list T; strict_mono α; α bot = 0⟧ ⟹
   bucket_end α T 0 = 1"
  apply (clarsimp simp: bucket_end_def)
  apply (frule valid_list_length_ex)
  apply clarsimp
  apply (frule (3) valid_list_bucket_upt_Suc_0)
  apply simp
  done

lemma nth_Max:
  "T ≠ [] ⟹ ∃i < length T. T ! i = Max (set T)"
  by (metis List.finite_set Max_in in_set_conv_nth set_empty)

lemma bucket_upt_Suc_Max:
  "strict_mono α ⟹ bucket_upt α T (Suc (α (Max (set T)))) = {0..<length T}"
  apply (intro equalityI subsetI)
   apply (erule bucket_upt_subset[THEN subsetD])
  by (clarsimp simp: bucket_upt_def less_Suc_eq_le strict_mono_less_eq)

lemma bucket_end_Max:
  "strict_mono α ⟹ bucket_end α T (α (Max (set T))) = length T"
  apply (clarsimp simp: bucket_end_def)
  apply (drule bucket_upt_Suc_Max[where T = T])
  apply clarsimp
  done

lemma bucket_end_eq_length:
  "⟦strict_mono α; b ≤ α (Max (set T)); T ≠ []; bucket_end α T b = length T⟧ ⟹
   b = α (Max (set T))"
proof -
  assume "strict_mono α" "b ≤ α (Max (set T))" "bucket_end α T b = length T" "T ≠ []"
  show "b = α (Max (set T))"
  proof (rule ccontr)
    assume "b ≠ α (Max (set T))"
    with ‹b ≤ _›
    have "b < α (Max (set T))"
      by simp
    hence "∃b'. b' = α (Max (set T))"
      by blast
    then obtain b' where
      "b' = α (Max (set T))"
      by blast
    with ‹b < _›
    have "b < b'"
      by blast
    hence "bucket_end α T b ≤ bucket_start α T b'"
      by (simp add: less_bucket_end_le_start)
    moreover
    from nth_Max[OF ‹T ≠ []›]
    obtain i where
      "i < length T"
      "T ! i = Max (set T)"
      by blast
    with ‹b' = α (Max (set T))› ‹strict_mono α›
    have "i ∈ bucket α T b'"
      by (simp add: bucket_def)
    hence "bucket_start α T b' < bucket_end α T b'"
      by (metis add_diff_cancel_left' bucket_end_def' bucket_size_def bucket_start_le_end
            card_gt_0_iff diff_is_0_eq' empty_iff finite_bucket nat_less_le)
    moreover
    have "bucket_end α T b' ≤ length T"
      using bucket_end_le_length by blast
    ultimately
    show False
      using ‹bucket_end α T b = length T›
      by linarith
  qed
qed

subsection ‹L-types›

definition l_bucket :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat set"
  where
"l_bucket α T b = {k |k. k ∈ bucket α T b ∧ suffix_type T k = L_type}"

definition l_bucket_size :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"l_bucket_size α T b ≡ card (l_bucket α T b)"

definition l_bucket_end :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"l_bucket_end α T b = bucket_start α T b + l_bucket_size α T b"

lemma l_bucket_subset_bucket:
  "l_bucket α T b ⊆ bucket α T b"
  by (rule subsetI, simp add: l_bucket_def)

lemma bucket_upt_int_l_bucket:
  "strict_mono α ⟹ bucket_upt α T b ∩ l_bucket α T b = {}"
  apply (rule disjoint_subset2[where B = "bucket α T b"])
   apply (simp add: l_bucket_def)
  apply (simp add: bucket_def bucket_upt_def)
  apply (rule disjointI')
  apply clarsimp
  done

lemma subset_l_bucket:
  "⟦∀k < length ls. ls ! k < length T ∧ suffix_type T (ls ! k) = L_type ∧ α (T ! (ls ! k)) = x;
    distinct ls⟧ ⟹
   set ls ⊆ l_bucket α T x"
  apply (rule subsetI)
  apply (clarsimp simp: l_bucket_def bucket_def in_set_conv_nth)
  done

lemma finite_l_bucket:
  "finite (l_bucket α T x)"
  apply (clarsimp simp: finite_bucket l_bucket_def)
  done

lemma l_bucket_list_eq:
  "⟦∀k < length ls. ls ! k < length T ∧ suffix_type T (ls ! k) = L_type ∧ α (T ! (ls ! k)) = x;
    distinct ls; length ls = l_bucket_size α T x⟧ ⟹
   set ls = l_bucket α T x"
  apply (frule (1) subset_l_bucket)
  apply (frule distinct_card)
  apply (insert finite_l_bucket[of α T x])
  by (simp add: card_subset_eq l_bucket_size_def)

lemma l_bucket_le_bucket_size:
  "l_bucket_size α T b ≤ bucket_size α T b"
  apply (clarsimp simp: l_bucket_size_def bucket_size_def)
  apply (rule card_mono[OF finite_bucket l_bucket_subset_bucket])
  done

lemma l_bucket_not_empty:
  "⟦i < length T; suffix_type T i = L_type⟧ ⟹ 0 < l_bucket_size α T (α (T ! i))"
  apply (clarsimp simp: l_bucket_size_def)
  apply (subst card_gt_0_iff)
  apply (intro conjI finite_l_bucket)
  apply (clarsimp simp: l_bucket_def bucket_def)
  apply blast
  done

lemma l_bucket_end_le_bucket_end:
  "l_bucket_end α T b ≤ bucket_end α T b"
  apply (clarsimp simp: l_bucket_end_def)
  apply (rule order.trans[where b = "bucket_start α T b + bucket_size α T b"])
   apply (simp add: l_bucket_le_bucket_size)
  by (metis bucket_start_Suc bucket_start_Suc_eq_bucket_end le_refl)

lemma l_bucket_Max:
  assumes "valid_list T"
  and     "Suc 0 < length T"
  and     "strict_mono α"
  shows "l_bucket α T (α (Max (set T))) = bucket α T (α (Max (set T)))"
proof (intro subsetI equalityI)
  let ?b = "α (Max (set T))"
  fix x
  assume "x ∈ l_bucket α T ?b"
  then show "x ∈ bucket α T ?b"
    using l_bucket_subset_bucket by blast
next
  let ?b = "α (Max (set T))"
  fix x
  assume "x ∈ bucket α T ?b"
  hence "x < length T" "α (T ! x) = ?b"
    using bucket_def by blast+
  with suffix_max_hd_is_l_type[OF assms(1) _ assms(2)]
  have "suffix_type T x = L_type"
    by (metis Cons_nth_drop_Suc assms(3) list.sel(1) strict_mono_eq)
  then show "x ∈ l_bucket α T ?b"
    using ‹x ∈ bucket α T (α (Max (set T)))› l_bucket_def by blast
qed

subsection ‹LMS-types›

definition lms_bucket :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat set"
  where
"lms_bucket α T b = {k |k. k ∈ bucket α T b ∧ abs_is_lms T k}"

definition lms_bucket_size :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"lms_bucket_size α T b ≡ card (lms_bucket α T b)"

lemma lms_bucket_subset_bucket:
  "lms_bucket α T b ⊆ bucket α T b"
  by (simp add: lms_bucket_def)

lemma finite_lms_bucket:
  "finite (lms_bucket α T b)"
  by (clarsimp simp: lms_bucket_def finite_bucket)

lemma disjoint_l_lms_bucket:
 "l_bucket α T b ∩ lms_bucket α T b = {}"
  apply (rule disjointI')
  by (clarsimp simp: l_bucket_def lms_bucket_def abs_is_lms_def)

subsection ‹S-types›

definition s_bucket :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat set"
  where
"s_bucket α T b = {k |k. k ∈ bucket α T b ∧ suffix_type T k = S_type}"

definition s_bucket_size :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"s_bucket_size α T b ≡ card (s_bucket α T b)"

definition s_bucket_start :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"s_bucket_start α T b ≡ bucket_start α T b + l_bucket_size α T b"

lemma finite_s_bucket:
 "finite (s_bucket α T b)"
  by (clarsimp simp: s_bucket_def finite_bucket)

lemma disjoint_l_s_bucket:
 "l_bucket α T b ∩ s_bucket α T b = {}"
  apply (rule disjointI')
  by (clarsimp simp: l_bucket_def s_bucket_def)

lemma lms_subset_s_bucket:
  "lms_bucket α T b ⊆ s_bucket α T b"
  by (clarsimp simp: s_bucket_def lms_bucket_def abs_is_lms_def)

lemma l_un_s_bucket:
  "bucket α T b = l_bucket α T b ∪ s_bucket α T b"
  apply (rule equalityI; clarsimp simp: l_bucket_def s_bucket_def)
  by (meson suffix_type_def)

lemma s_bucket_Max:
  assumes "valid_list T"
  and     "length T > Suc 0"
  and     "strict_mono α"
shows "s_bucket α T (α (Max (set T))) = {}"
proof -
  let ?b = "α (Max (set T))"
  from l_bucket_Max[OF assms]
  have "l_bucket α T ?b = bucket α T ?b" .
  moreover
  from l_un_s_bucket
  have "bucket α T ?b = l_bucket α T ?b ∪ s_bucket α T ?b" .
  hence "s_bucket α T ?b ⊆ bucket α T ?b"
    by blast
  moreover
  from disjoint_l_s_bucket
  have "l_bucket α T ?b ∩ s_bucket α T ?b = {}" .
  ultimately
  show ?thesis
    by blast
qed

lemma s_bucket_0:
  assumes "valid_list T"
  and     "strict_mono α"
  and     "α bot = 0"
  and     "length T = Suc n"
shows "s_bucket α T 0 = {n}"
proof -
  have "suffix_type T n = S_type"
    using assms(4) suffix_type_last by blast
  moreover
  have "T ! n = bot"
    by (metis assms(1) assms(4) diff_Suc_1 last_conv_nth length_greater_0_conv valid_list_def)
  hence "α (T ! n) = 0"
    by (simp add: assms(3))
  ultimately have "n ∈ s_bucket α T 0"
    by (simp add: assms(4) bucket_def s_bucket_def)
  hence "{n} ⊆ s_bucket α T 0"
    by blast
  moreover
  have "s_bucket α T 0 ⊆ {n}"
    unfolding s_bucket_def
  proof safe
    fix k
    assume "k ∈ bucket α T 0" "suffix_type T k = S_type"
    hence "k ≤ n"
      by (simp add: assms(4) bucket_def)
    have "α (T ! k) = 0"
      using ‹k ∈ bucket α T 0› bucket_def by blast
    hence "T ! k = bot"
      by (metis assms(2) assms(3) strict_mono_eq)
    show "k = n"
    proof (rule ccontr)
      assume "k ≠ n"
      hence "k < n"
        by (simp add: ‹k ≤ n› le_neq_implies_less)
      then show False
        using ‹k ∈ bucket α T 0› ‹k ≠ n› assms bucket_0 by blast
    qed
  qed
  ultimately show ?thesis
    by blast
qed

lemma s_bucket_successor:
  "⟦valid_list T; strict_mono α; α bot = 0; b ≠ 0; x ∈ s_bucket α T b⟧ ⟹
    Suc x ∈ s_bucket α T b ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')"
proof -
  assume "valid_list T" "strict_mono α" "α bot = 0" "b ≠ 0" "x ∈ s_bucket α T b"
  hence "suffix_type T x = S_type"
    by (simp add: s_bucket_def)

  from valid_list_length_ex[OF ‹valid_list _›]
  obtain n where
    "length T = Suc n"
    by blast
  moreover
  from ‹x ∈ s_bucket α T b›
  have "x < length T" "α (T ! x) = b"
    by (simp add: s_bucket_def bucket_def)+
  ultimately have "Suc x < length T"
    by (metis Suc_lessI ‹α bot = 0› ‹b ≠ 0› ‹valid_list T› diff_Suc_1 last_conv_nth list.size(3)
          valid_list_def)

  have "T ! x ≤ T ! Suc x"
    by (simp add: ‹Suc x < length T› ‹suffix_type T x = S_type› s_type_letter_le_Suc)
  hence "T ! x < T ! Suc x ∨ T ! x = T ! Suc x"
    using le_neq_trans by blast
  moreover
  have "T ! x < T ! Suc x ⟹ ?thesis"
  proof -
    assume "T ! x < T ! Suc x"
    hence "α (T ! x) < α (T ! Suc x)"
      by (simp add: ‹strict_mono α› strict_mono_less)
    hence "b < α (T ! Suc x)"
      by (simp add: ‹α (T ! x) = b›)
    with ‹Suc x < length T›
    have "Suc x ∈ bucket α T (α (T ! Suc x))"
      by (simp add: bucket_def)
    with ‹b < α (T ! Suc x)›
    show ?thesis
      by blast
  qed
  moreover
  have "T ! x = T ! Suc x ⟹ ?thesis"
  proof -
    assume "T ! x = T ! Suc x"
    hence "α (T ! Suc x) = b"
      using ‹α (T ! x) = b› by auto
    moreover
    from ‹Suc x < length T› ‹T ! x = T ! Suc x› ‹suffix_type T x = S_type›
    have "suffix_type T (Suc x) = S_type"
      using suffix_type_neq by force
    ultimately show ?thesis
      by (simp add: ‹Suc x < length T› bucket_def s_bucket_def)
  qed
  ultimately show ?thesis
    by blast
qed

lemma subset_s_bucket_successor:
  "⟦valid_list T; strict_mono α; α bot = 0; b ≠ 0; A ⊆ s_bucket α T b; A ≠ {}⟧ ⟹
    ∃x ∈ A. Suc x ∈ s_bucket α T b - A ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')"
proof -
  assume "valid_list T" "strict_mono α" "α bot = 0" "b ≠ 0" "A ⊆ s_bucket α T b" "A ≠ {}"

  have "finite A"
    using ‹A ⊆ s_bucket α T b› finite_s_bucket finite_subset by blast

  let ?B = "s_bucket α T b - A"

  have "∃x ∈ A. Suc x ∉ A"
  proof (rule ccontr)
    assume "¬ (∃x∈A. Suc x ∉ A)"
    hence "∀x∈A. Suc x ∈ A"
      by clarsimp
    hence "¬ finite A"
      using Max.coboundedI Max_in Suc_n_not_le_n ‹A ≠ {}› by blast
    with ‹finite A›
    show False
      by blast
  qed
  then obtain x where
    "x ∈ A"
    "Suc x ∉ A"
    by blast
  with s_bucket_successor[OF ‹valid_list _› ‹strict_mono _› ‹α _ = _› ‹b ≠ _›, of x]
       ‹A ⊆ s_bucket α T b›
  have "Suc x ∈ s_bucket α T b ∨ (∃b'. b < b' ∧ Suc x ∈ bucket α T b')"
    by blast
  moreover
  have "Suc x ∈ s_bucket α T b ⟹ ?thesis"
  proof -
    assume "Suc x ∈ s_bucket α T b"
    with ‹Suc x ∉ A›
    show ?thesis
      using ‹x ∈ A› by blast
  qed
  moreover
  have "(∃b'. b < b' ∧ Suc x ∈ bucket α T b') ⟹ ?thesis"
    using ‹x ∈ A› by blast
  ultimately show ?thesis
    by blast
qed

lemma valid_list_s_bucket_start_0:
  "⟦valid_list T; strict_mono α; α bot = 0⟧ ⟹
   s_bucket_start α T 0 = 0"
  apply (clarsimp simp: s_bucket_start_def bucket_start_0)
  apply (frule valid_list_length_ex)
  apply clarsimp
  apply (frule (3) bucket_0)
  apply (frule suffix_type_last)
  apply (clarsimp simp: l_bucket_size_def l_bucket_def)
  done

definition pure_s_bucket :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat set"
  where
"pure_s_bucket α T b = {k |k. k ∈ s_bucket α T b ∧ k ∉ lms_bucket α T b}"

definition pure_s_bucket_size :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"pure_s_bucket_size α T b ≡ card (pure_s_bucket α T b)"

lemma finite_pure_s_bucket:
 "finite (pure_s_bucket α T b)"
  by (clarsimp simp: pure_s_bucket_def finite_s_bucket)

lemma pure_s_subset_s_bucket:
  "pure_s_bucket α T b ⊆ s_bucket α T b"
  by (clarsimp simp: s_bucket_def pure_s_bucket_def)

lemma disjoint_lms_pure_s_bucket:
 "lms_bucket α T b ∩ pure_s_bucket α T b = {}"
  apply (rule disjointI')
  by (clarsimp simp: lms_bucket_def pure_s_bucket_def)

lemma disjoint_pure_s_lms_bucket:
  "pure_s_bucket α T b ∩ lms_bucket α T b = {}"
  apply (subst Int_commute)
  by (rule disjoint_lms_pure_s_bucket)

lemma s_eq_pure_s_un_lms_bucket:
  "s_bucket α T b = pure_s_bucket α T b ∪ lms_bucket α T b"
  apply (intro equalityI; clarsimp simp: pure_s_subset_s_bucket lms_subset_s_bucket)
  apply (clarsimp simp: s_bucket_def lms_bucket_def pure_s_bucket_def)
  done

lemma l_pl_pure_s_pl_lms_size:
  "bucket_size α T b = l_bucket_size α T b + pure_s_bucket_size α T b + lms_bucket_size α T b"
  apply (clarsimp simp: bucket_size_def l_bucket_size_def pure_s_bucket_size_def
                        lms_bucket_size_def)
  apply (subst add.assoc)
  apply (subst card_Un_disjoint[symmetric,
          OF finite_pure_s_bucket finite_lms_bucket disjoint_pure_s_lms_bucket])
  apply (subst s_eq_pure_s_un_lms_bucket[symmetric])
  apply (subst card_Un_disjoint[symmetric,
          OF finite_l_bucket finite_s_bucket disjoint_l_s_bucket])
  apply (clarsimp simp: l_un_s_bucket)
  done

lemma s_bucket_start_eq_l_bucket_end:
  "s_bucket_start α T b = l_bucket_end α T b"
  by (simp add: l_bucket_end_def s_bucket_start_def)

lemma s_eq_pure_pl_lms_size:
  "s_bucket_size α T b = pure_s_bucket_size α T b + lms_bucket_size α T b"
  by (simp add: card_Un_disjoint disjoint_pure_s_lms_bucket finite_lms_bucket finite_pure_s_bucket
        lms_bucket_size_def pure_s_bucket_size_def s_bucket_size_def s_eq_pure_s_un_lms_bucket)

lemma bucket_end_eq_s_start_pl_size:
  "bucket_end α T b = s_bucket_start α T b + s_bucket_size α T b"
  by (simp add: bucket_end_def' l_bucket_end_def l_pl_pure_s_pl_lms_size
        s_bucket_start_eq_l_bucket_end s_eq_pure_pl_lms_size)

lemma bucket_start_le_s_bucket_start:
  "bucket_start α T b ≤ s_bucket_start α T b"
  by (simp add: s_bucket_start_def)

lemma bucket_0_size1:
  assumes "valid_list T"
  and     "strict_mono α"
  and     "α bot = 0"
shows "bucket_size α T 0 = Suc 0 ∧ l_bucket_size α T 0 = 0"
proof -
  from valid_list_length_ex[OF assms(1)]
  obtain n where
    "length T = Suc n"
    by blast
  with bucket_0[OF assms(1,3,2)]
  have "bucket α T 0 = {n}"
    by blast
  hence "bucket_size α T 0 = Suc 0"
    by (simp add: bucket_size_def)
  moreover
  have "suffix_type T n = S_type"
    by (simp add: ‹length T = Suc n› suffix_type_last)
  hence "n ∉ l_bucket α T 0"
    by (simp add: l_bucket_def)
  hence "l_bucket_size α T 0 = 0"
  proof -
    have "l_bucket α T 0 ⊆ {n}"
      by (metis ‹bucket α T 0 = {n}› l_bucket_subset_bucket)
    hence "∀n. n ∉ l_bucket α T 0"
      using ‹n ∉ l_bucket α T 0› by blast
    then show ?thesis
      by (simp add: l_bucket_size_def)
  qed
  ultimately
  show ?thesis
    by blast
qed

lemma bucket_0_size2:
  assumes "valid_list T"
  and     "strict_mono α"
  and     "α bot = 0"
  and     "length T = Suc (Suc n)"
shows "bucket_size α T 0 = Suc 0 ∧ l_bucket_size α T 0 = 0 ∧ lms_bucket_size α T 0 = Suc 0 ∧
       pure_s_bucket_size α T 0 = 0"
proof -
  from bucket_0[OF assms(1,3,2,4)]
  have "bucket α T 0 = {Suc n}" .

  have "abs_is_lms T (Suc n)"
    using assms(1,4) abs_is_lms_last by blast
  hence "lms_bucket α T 0 = {Suc n}"
    using lms_bucket_subset_bucket[of α T 0] ‹bucket α T 0 = {Suc n}›
    by (simp add: lms_bucket_def subset_antisym)
  hence "lms_bucket_size α T 0 = Suc 0"
    by (simp add: lms_bucket_size_def)
  moreover
  from ‹bucket α T 0 = {Suc n}› ‹lms_bucket α T 0 = {Suc n}›
  have "pure_s_bucket α T 0 = {}"
    by (metis disjoint_insert(1) disjoint_l_lms_bucket disjoint_lms_pure_s_bucket
          l_bucket_subset_bucket l_un_s_bucket pure_s_subset_s_bucket singletonI
          subset_singletonD sup_bot.left_neutral)
  hence "pure_s_bucket_size α T 0 = 0"
    by (simp add: pure_s_bucket_size_def)
  moreover
  from bucket_0_size1[OF assms(1-3)]
  have "bucket_size α T 0 = Suc 0 ∧ l_bucket_size α T 0 = 0" .
  ultimately
  show ?thesis
    by blast
qed

definition lms_bucket_start :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat ⇒ nat"
  where
"lms_bucket_start α T b = bucket_start α T b + l_bucket_size α T b + pure_s_bucket_size α T b"

lemma l_bucket_end_le_lms_bucket_start:
  "l_bucket_end α T b ≤ lms_bucket_start α T b"
  by (simp add: l_bucket_end_def lms_bucket_start_def)

lemma lms_bucket_start_le_bucket_end:
  "lms_bucket_start α T b ≤ bucket_end α T b"
  by (simp add: bucket_end_def' lms_bucket_start_def l_pl_pure_s_pl_lms_size)

lemma lms_bucket_pl_size_eq_end:
  "lms_bucket_start α T b + lms_bucket_size α T b = bucket_end α T b"
  by (simp add: bucket_end_def' l_pl_pure_s_pl_lms_size lms_bucket_start_def)

section ‹Continuous Buckets›

lemma continuous_buckets:
  "continuous_list (map (λb. (bucket_start α T b, bucket_end α T b)) [i..<j])"
  by (clarsimp simp: continuous_list_def bucket_start_Suc_eq_bucket_end)

lemma index_in_bucket_interval_gen:
  "⟦i < length T; strict_mono α⟧ ⟹
    ∃b ≤ α (Max (set T)). bucket_start α T b ≤ i ∧ i < bucket_end α T b"
  apply (insert continuous_buckets[of α T 0 "Suc (α (Max (set T)))"])
  apply (drule continuous_list_interval_2[where n = "α (Max (set T))" and i = i])
     apply clarsimp
    apply (subst nth_map)
     apply clarsimp
    apply (clarsimp split: prod.split simp: upt_rec bucket_start_0)
    apply (subst nth_map)
    apply clarsimp
   apply (clarsimp split: prod.split simp: nth_append bucket_end_Max)
  apply clarsimp
  apply (clarsimp simp: nth_append split: if_splits prod.splits)
  apply (meson dual_order.order_iff_strict)
  by blast

lemma index_in_bucket_interval:
  "⟦i < length T; valid_list T; α bot = 0; strict_mono α⟧ ⟹
    ∃b ≤ α (Max (set T)). bucket_start α T b ≤ i ∧ i < bucket_end α T b"
  using index_in_bucket_interval_gen by blast

section ‹Bucket Initialisation›

definition lms_bucket_init :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ bool"
  where
"lms_bucket_init α T B =
  (α (Max (set T)) < length B ∧
   (∀b ≤ α (Max (set T)). B ! b = bucket_end α T b))"

lemma lms_bucket_init_length:
  "lms_bucket_init α T B ⟹ α (Max (set T)) < length B"
  using lms_bucket_init_def by blast

lemma lms_bucket_initD:
  "⟦lms_bucket_init α T B; b ≤ α (Max (set T))⟧ ⟹ B ! b = bucket_end α T b"
  using lms_bucket_init_def by blast

definition l_bucket_init :: "('a :: {linorder,order_bot} ⇒ nat) ⇒ 'a list ⇒ nat list ⇒ bool"
  where
"l_bucket_init α T B =
  (α (Max (set T)) < length B ∧
   (∀b ≤ α (Max (set T)). B ! b = bucket_start α T b))"

lemma l_bucket_init_length:
  "l_bucket_init α T B ⟹ α (Max (set T)) < length B"
  using l_bucket_init_def by blast

lemma l_bucket_initD:
  "⟦l_bucket_init α T B; b ≤ α (Max (set T))⟧ ⟹ B ! b = bucket_start α T b"
  using l_bucket_init_def by blast

definition s_bucket_init
  where
"s_bucket_init α T B =
  (α (Max (set T)) < length B ∧
   (∀b≤α (Max (set T)).
    (b > 0 ⟶ B ! b = bucket_end α T b) ∧
    (b = 0 ⟶ B ! b = 0)
   )
  )"

lemma s_bucket_init_length:
  "s_bucket_init α T B ⟹ α (Max (set T)) < length B"
  using s_bucket_init_def by blast

lemma s_bucket_initD:
  "⟦s_bucket_init α T B; b ≤ α (Max (set T)); b > 0⟧ ⟹ B ! b = bucket_end α T b"
  "⟦s_bucket_init α T B; b ≤ α (Max (set T)); b = 0⟧ ⟹ B ! b = 0"
  using s_bucket_init_def by auto

section ‹Bucket Range›

definition in_s_current_bucket
  where
"in_s_current_bucket α T B b i ≡ (b ≤ α (Max (set T)) ∧ B ! b ≤ i ∧ i < bucket_end α T b)"

lemma in_s_current_bucketD:
  "in_s_current_bucket α T B b i ⟹ b ≤ α (Max (set T))"
  "in_s_current_bucket α T B b i ⟹ B ! b ≤ i"
  "in_s_current_bucket α T B b i ⟹ i < bucket_end α T b"
  by (simp_all add: in_s_current_bucket_def)

definition in_s_current_buckets
  where
"in_s_current_buckets α T B i ≡ (∃b. in_s_current_bucket α T B b i)"

lemma in_s_current_bucket_list_slice:
  assumes "length SA = length T"
  and     "in_s_current_bucket α T B b i"
  and     "SA ! i = x"
shows "x ∈ set (list_slice SA (B ! b) (bucket_end α T b))"
  by (metis assms bucket_end_le_length in_s_current_bucket_def list_slice_nth_mem)

definition in_l_bucket
  where
"in_l_bucket α T b i ≡ (b ≤ α (Max (set T)) ∧ bucket_start α T b ≤ i ∧ i < l_bucket_end α T b)"

end