# Theory K_Smallest

```section ‹Ranks, \$k\$ smallest element and elements›

theory K_Smallest
imports
Frequency_Moments_Preliminary_Results
Interpolation_Polynomials_HOL_Algebra.Interpolation_Polynomial_Cardinalities
begin

text ‹This section contains definitions and results for the selection of the \$k\$ smallest elements, the \$k\$-th smallest element, rank of an element in an ordered set.›

definition rank_of :: "'a :: linorder ⇒ 'a set ⇒ nat" where "rank_of x S = card {y ∈ S. y < x}"
text ‹The function @{term "rank_of"} returns the rank of an element within a set.›

lemma rank_mono:
assumes "finite S"
shows "x ≤ y ⟹ rank_of x S ≤ rank_of y S"
unfolding rank_of_def using assms by (intro card_mono, auto)

lemma rank_mono_2:
assumes "finite S"
shows "S' ⊆ S ⟹ rank_of x S' ≤ rank_of x S"
unfolding rank_of_def using assms by (intro card_mono, auto)

lemma rank_mono_commute:
assumes "finite S"
assumes "S ⊆ T"
assumes "strict_mono_on T f"
assumes "x ∈ T"
shows "rank_of x S = rank_of (f x) (f ` S)"
proof -
have a: "inj_on f T"
by (metis assms(3) strict_mono_on_imp_inj_on)

have "rank_of (f x) (f ` S) = card (f ` {y ∈ S. f y < f x})"
unfolding rank_of_def by (intro arg_cong[where f="card"], auto)
also have "... = card (f ` {y ∈ S. y < x})"
using assms by (intro arg_cong[where f="card"] arg_cong[where f="(`) f"])
(meson in_mono linorder_not_le strict_mono_onD strict_mono_on_leD set_eq_iff)
also have "... = card {y ∈ S. y < x}"
using assms by (intro card_image  inj_on_subset[OF a], blast)
also have "... = rank_of x S"
finally show ?thesis
by simp
qed

definition least where "least k S = {y ∈ S. rank_of y S < k}"
text ‹The function @{term "least"} returns the k smallest elements of a finite set.›

lemma rank_strict_mono:
assumes "finite S"
shows "strict_mono_on S (λx. rank_of x S)"
proof -
have "⋀x y. x ∈ S ⟹ y ∈ S ⟹ x < y ⟹ rank_of x S < rank_of y S"
unfolding rank_of_def using assms
by (intro psubset_card_mono, auto)

thus ?thesis
qed

lemma rank_of_image:
assumes "finite S"
shows "(λx. rank_of x S) ` S = {0..<card S}"
proof (rule card_seteq)
show "finite {0..<card S}" by simp

have "⋀x. x ∈ S ⟹ card {y ∈ S. y < x} < card S"
by (rule psubset_card_mono, metis assms, blast)
thus "(λx. rank_of x S) ` S ⊆ {0..<card S}"

have "inj_on (λx. rank_of x S) S"
by (metis strict_mono_on_imp_inj_on rank_strict_mono assms)
thus "card {0..<card S} ≤ card ((λx. rank_of x S) ` S)"
qed

lemma card_least:
assumes "finite S"
shows "card (least k S) = min k (card S)"
proof (cases "card S < k")
case True
have "⋀t. rank_of t S ≤ card S"
unfolding rank_of_def using assms
by (intro card_mono, auto)
hence "⋀t. rank_of t S < k"
by (metis True not_less_iff_gr_or_eq order_less_le_trans)
hence "least k S = S"
then show ?thesis using True by simp
next
case False
hence a:"card S ≥ k" using leI by blast
hence "card ((λx. rank_of x S) -` {0..<k} ∩ S) = card {0..<k}"
using assms
by (intro card_vimage_inj_on strict_mono_on_imp_inj_on rank_strict_mono)
hence "card (least k S) = k"
by (simp add: Collect_conj_eq Int_commute least_def vimage_def)
then show ?thesis using a by linarith
qed

lemma least_subset: "least k S ⊆ S"

lemma least_mono_commute:
assumes "finite S"
assumes "strict_mono_on S f"
shows "f ` least k S = least k (f ` S)"
proof -
have a:"inj_on f S"
using strict_mono_on_imp_inj_on[OF assms(2)] by simp

have "card (least k (f ` S)) = min k (card (f ` S))"
by (subst card_least, auto simp add:assms)
also have "... = min k (card S)"
by (subst card_image, metis a, auto)
also have "... = card (least k S)"
by (subst card_least, auto simp add:assms)
also have "... = card (f ` least k S)"
by (subst card_image[OF inj_on_subset[OF a]], simp_all add:least_def)
finally have b: "card (least k (f ` S)) ≤ card (f ` least k S)" by simp

have c: "f ` least k S ⊆least k (f ` S)"
using assms by (intro image_subsetI)

show ?thesis
using b c assms by (intro card_seteq, simp_all add:least_def)
qed

lemma least_eq_iff:
assumes "finite B"
assumes "A ⊆ B"
assumes "⋀x. x ∈ B ⟹ rank_of x B < k ⟹ x ∈ A"
shows "least k A = least k B"
proof -
have "least k B ⊆ least k A"
using assms rank_mono_2[OF assms(1,2)] order_le_less_trans
moreover have "card (least k B) ≥ card (least k A)"
using assms finite_subset[OF assms(2,1)] card_mono[OF assms(1,2)]
moreover have "finite (least k A)"
using finite_subset least_subset assms(1,2) by metis
ultimately show ?thesis
by (intro card_seteq[symmetric], simp_all)
qed

lemma least_insert:
assumes "finite S"
shows "least k (insert x (least k S)) = least k (insert x S)" (is "?lhs = ?rhs")
proof (rule least_eq_iff)
show "finite (insert x S)"
using assms(1) by simp
show "insert x (least k S) ⊆ insert x S"
using least_subset by blast
show "y ∈ insert x (least k S)" if a: "y ∈ insert x S" and b: "rank_of y (insert x S) < k" for y
proof -
have "rank_of y S ≤ rank_of y (insert x S)"
using assms by (intro rank_mono_2, auto)
also have "... < k" using b by simp
finally have "rank_of y S < k" by simp
hence "y = x ∨ (y ∈ S ∧ rank_of y S < k)"
using a by simp
qed
qed

definition count_le where "count_le x M = size {#y ∈# M. y ≤ x#}"
definition count_less where "count_less x M = size {#y ∈# M. y < x#}"

definition nth_mset :: "nat ⇒ ('a :: linorder) multiset ⇒ 'a" where
"nth_mset k M = sorted_list_of_multiset M ! k"

lemma nth_mset_bound_left:
assumes "k < size M"
assumes "count_less x M ≤ k"
shows "x ≤ nth_mset k M"
proof (rule ccontr)
define xs where "xs = sorted_list_of_multiset M"
have s_xs: "sorted xs" by (simp add:xs_def sorted_sorted_list_of_multiset)
have l_xs: "k < length xs"
using  assms(1) by (simp add:xs_def size_mset[symmetric])
have M_xs: "M = mset xs" by (simp add:xs_def)
hence a:"⋀i. i ≤ k ⟹ xs ! i ≤ xs ! k"
using s_xs l_xs sorted_iff_nth_mono by blast

assume "¬(x ≤ nth_mset k M)"
hence "x > nth_mset k M" by simp
hence b:"x > xs ! k" by (simp add:nth_mset_def xs_def[symmetric])

have "k < card {0..k}" by simp
also have "... ≤ card {i. i < length xs ∧ xs ! i < x}"
using a b l_xs order_le_less_trans
by (intro card_mono subsetI) auto
also have "... = length (filter (λy. y < x) xs)"
by (subst length_filter_conv_card, simp)
also have "... = size (mset (filter (λy. y < x) xs))"
by (subst size_mset, simp)
also have "... = count_less x M"
also have "... ≤ k"
using assms by simp
finally show "False" by simp
qed

lemma nth_mset_bound_left_excl:
assumes "k < size M"
assumes "count_le x M ≤ k"
shows "x < nth_mset k M"
proof (rule ccontr)
define xs where "xs = sorted_list_of_multiset M"
have s_xs: "sorted xs" by (simp add:xs_def sorted_sorted_list_of_multiset)
have l_xs: "k < length xs"
using  assms(1) by (simp add:xs_def size_mset[symmetric])
have M_xs: "M = mset xs" by (simp add:xs_def)
hence a:"⋀i. i ≤ k ⟹ xs ! i ≤ xs ! k"
using s_xs l_xs sorted_iff_nth_mono by blast

assume "¬(x < nth_mset k M)"
hence "x ≥ nth_mset k M" by simp
hence b:"x ≥ xs ! k" by (simp add:nth_mset_def xs_def[symmetric])

have "k+1 ≤ card {0..k}" by simp
also have "... ≤ card {i. i < length xs ∧ xs ! i ≤ xs ! k}"
using a b l_xs order_le_less_trans
by (intro card_mono subsetI, auto)
also have "... ≤ card {i. i < length xs ∧ xs ! i ≤ x}"
using b by (intro card_mono subsetI, auto)
also have "... = length (filter (λy. y ≤ x) xs)"
by (subst length_filter_conv_card, simp)
also have "... = size (mset (filter (λy. y ≤ x) xs))"
by (subst size_mset, simp)
also have "... = count_le x M"
also have "... ≤ k"
using assms by simp
finally show "False" by simp
qed

lemma nth_mset_bound_right:
assumes "k < size M"
assumes "count_le x M > k"
shows "nth_mset k M ≤ x"
proof (rule ccontr)
define xs where "xs = sorted_list_of_multiset M"
have s_xs: "sorted xs" by (simp add:xs_def sorted_sorted_list_of_multiset)
have l_xs: "k < length xs"
using  assms(1) by (simp add:xs_def size_mset[symmetric])
have M_xs: "M = mset xs" by (simp add:xs_def)

assume "¬(nth_mset k M ≤ x)"
hence "x < nth_mset k M" by simp
hence "x < xs ! k"
hence a:"⋀i. i < length xs ∧ xs ! i ≤ x ⟹ i < k"
using s_xs l_xs sorted_iff_nth_mono leI by fastforce
have "count_le x M = size (mset (filter (λy. y ≤ x) xs))"
also have "... = length (filter (λy. y ≤ x) xs)"
by (subst size_mset, simp)
also have "... = card {i. i < length xs ∧ xs ! i ≤ x}"
by (subst length_filter_conv_card, simp)
also have "... ≤ card {i. i < k}"
using a by (intro card_mono subsetI, auto)
also have "... = k" by simp
finally have "count_le x M ≤ k" by simp
thus "False" using assms by simp
qed

lemma nth_mset_commute_mono:
assumes "mono f"
assumes "k < size M"
shows "f (nth_mset k M) = nth_mset k (image_mset f M)"
proof -
have a:"k < length (sorted_list_of_multiset M)"
by (metis assms(2) mset_sorted_list_of_multiset size_mset)
show ?thesis
using a by (simp add:nth_mset_def sorted_list_of_multiset_image_commute[OF assms(1)])
qed

lemma nth_mset_max:
assumes "size A > k"
assumes "⋀x. x ≤ nth_mset k A ⟹ count A x ≤ 1"
shows "nth_mset k A = Max (least (k+1) (set_mset A))" and "card (least (k+1) (set_mset A)) = k+1"
proof -
define xs where "xs = sorted_list_of_multiset A"
have k_bound: "k < length xs" unfolding xs_def
by (metis size_mset mset_sorted_list_of_multiset assms(1))

have A_def: "A = mset xs" by (simp add:xs_def)
have s_xs: "sorted xs" by (simp add:xs_def sorted_sorted_list_of_multiset)
have "⋀x. x ≤ xs ! k ⟹ count A x ≤ Suc 0"
using assms(2) by (simp add:xs_def[symmetric] nth_mset_def)
hence no_col: "⋀x. x ≤ xs ! k ⟹ count_list xs x ≤ 1"

have inj_xs: "inj_on (λk. xs ! k) {0..k}"
by (rule inj_onI, simp) (metis (full_types) count_list_ge_2_iff k_bound no_col
le_neq_implies_less linorder_not_le order_le_less_trans s_xs sorted_iff_nth_mono)

have "⋀y. y < length xs ⟹ rank_of (xs ! y) (set xs) < k+1 ⟹ y < k+1"
proof (rule ccontr)
fix y
assume b:"y < length xs"
assume "¬y < k +1"
hence a:"k + 1 ≤ y" by simp

have d:"Suc k < length xs" using a b by simp

have "k+1 = card ((!) xs ` {0..k})"
by (subst card_image[OF inj_xs], simp)
also have "... ≤ rank_of (xs ! (k+1)) (set xs)"
unfolding rank_of_def using k_bound
by (intro card_mono image_subsetI conjI, simp_all) (metis count_list_ge_2_iff no_col not_le le_imp_less_Suc s_xs
sorted_iff_nth_mono d order_less_le)
also have "... ≤ rank_of (xs ! y) (set xs)"
unfolding rank_of_def
by (intro card_mono subsetI, simp_all)
(metis Suc_eq_plus1 a b s_xs order_less_le_trans sorted_iff_nth_mono)
also assume "... < k+1"
finally show "False" by force
qed

moreover have "rank_of (xs ! y) (set xs) < k+1" if a:"y < k + 1" for y
proof -
have "rank_of (xs ! y) (set xs) ≤ card ((λk. xs ! k) ` {k. k < length xs ∧ xs ! k < xs ! y})"
unfolding rank_of_def
by (intro card_mono subsetI, simp)
(metis (no_types, lifting) imageI in_set_conv_nth mem_Collect_eq)
also have "... ≤ card {k. k < length xs ∧ xs ! k < xs ! y}"
by (rule card_image_le, simp)
also have "... ≤ card {k. k < y}"
by (intro card_mono subsetI, simp_all add:not_less)
(metis sorted_iff_nth_mono s_xs linorder_not_less)
also have "... = y" by simp
also have "... < k + 1" using a by simp
finally show "rank_of (xs ! y) (set xs) < k+1" by simp
qed

ultimately have rank_conv: "⋀y. y < length xs ⟹ rank_of (xs ! y) (set xs) < k+1 ⟷ y < k+1"
by blast

have "y ≤ xs ! k"  if a:"y ∈ least (k+1) (set xs)"  for y
proof -
have "y ∈ set xs" using a least_subset by blast
then obtain i where i_bound: "i < length xs" and y_def: "y = xs ! i" using in_set_conv_nth by metis
hence "rank_of (xs ! i) (set xs) < k+1"
using a y_def i_bound by (simp add: least_def)
hence "i < k+1"
using rank_conv i_bound by blast
hence "i ≤ k" by linarith
hence "xs ! i ≤ xs ! k"
using s_xs i_bound k_bound sorted_nth_mono by blast
thus "y ≤ xs ! k" using y_def by simp
qed

moreover have "xs ! k ∈ least (k+1) (set xs)"
using k_bound rank_conv by (simp add:least_def)

ultimately have "Max (least (k+1) (set xs)) = xs ! k"
by (intro Max_eqI finite_subset[OF least_subset], auto)

hence "nth_mset k A = Max (K_Smallest.least (Suc k) (set xs))"
also have "... = Max (least (k+1) (set_mset A))"
finally show "nth_mset k A = Max (least (k+1) (set_mset A))"  by simp

have "k + 1 = card ((λi. xs ! i) ` {0..k})"
by (subst card_image[OF inj_xs], simp)
also have "... ≤ card (least (k+1) (set xs))"
using rank_conv k_bound
by (intro card_mono image_subsetI finite_subset[OF least_subset], simp_all add:least_def)
finally have "card (least (k+1) (set xs)) ≥ k+1" by simp
moreover have "card (least (k+1) (set xs)) ≤ k+1"
by (subst card_least, simp, simp)
ultimately have "card (least (k+1) (set xs)) = k+1" by simp
thus "card (least (k+1) (set_mset A)) = k+1"  by (simp add:A_def)
qed

end
```