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" by (simp add:rank_of_def) 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 by (simp add:rank_of_def strict_mono_on_def) 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}" by (intro image_subsetI, simp add:rank_of_def) 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)" by (simp add:card_image) 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" by (simp add:least_def) 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) (simp_all add: rank_of_image) 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" by (simp add:least_def) 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) (simp add:least_def rank_mono_commute[symmetric, where T="S"]) 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 by (simp add:least_def, blast) moreover have "card (least k B) ≥ card (least k A)" using assms finite_subset[OF assms(2,1)] card_mono[OF assms(1,2)] by (simp add: card_least min_le_iff_disj) 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 thus ?thesis by (simp add:least_def) 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" by (simp add:count_less_def M_xs) 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" by (simp add:count_le_def M_xs) 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" by (simp add:nth_mset_def xs_def[symmetric]) 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))" by (simp add:count_le_def M_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" by (simp add:A_def count_mset) 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))" by (simp add:nth_mset_def xs_def[symmetric]) also have "... = Max (least (k+1) (set_mset A))" by (simp add:A_def) 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