section ‹Sets and Extended Natural Numbers› theory ESet_Extensions imports "../Basics/Functions" Basic_Extensions CCPO_Extensions begin lemma card_lessThan_enat[simp]: "card {..< enat k} = card {..< k}" proof - have 1: "{..< enat k} = enat ` {..< k}" unfolding lessThan_def image_Collect using enat_iless by force have "card {..< enat k} = card (enat ` {..< k})" unfolding 1 by rule also have "… = card {..< k}" using card_image inj_enat by metis finally show ?thesis by this qed lemma card_atMost_enat[simp]: "card {.. enat k} = card {.. k}" proof - have 1: "{.. enat k} = enat ` {.. k}" unfolding atMost_def image_Collect using enat_ile by force have "card {.. enat k} = card (enat ` {.. k})" unfolding 1 by rule also have "… = card {.. k}" using card_image inj_enat by metis finally show ?thesis by this qed lemma enat_Collect: assumes "∞ ∉ A" shows "{i. enat i ∈ A} = the_enat ` A" using assms by (safe, force) (metis enat_the_enat) lemma Collect_lessThan: "{i. enat i < n} = the_enat ` {..< n}" proof - have 1: "∞ ∉ {..< n}" by simp have "{i. enat i < n} = {i. enat i ∈ {..< n}}" by simp also have "… = the_enat ` {..< n}" using enat_Collect 1 by this finally show ?thesis by this qed instantiation set :: (type) esize_ccpo begin function esize_set where "finite A ⟹ esize A = enat (card A)" | "infinite A ⟹ esize A = ∞" by auto termination by lexicographic_order lemma esize_iff_empty[iff]: "esize A = 0 ⟷ A = {}" by (cases "finite A", auto) lemma esize_iff_infinite[iff]: "esize A = ∞ ⟷ infinite A" by force lemma esize_singleton[simp]: "esize {a} = eSuc 0" by simp lemma esize_infinite_enat[dest, simp]: "infinite A ⟹ enat k < esize A" by force instance proof fix A :: "'a set" assume 1: "esize A ≠ ∞" show "finite {B. B ⊆ A}" using 1 by simp next fix A B :: "'a set" assume 1: "A ⊆ B" show "esize A ≤ esize B" proof (cases "finite B") case False show ?thesis using False by auto next case True have 2: "finite A" using True 1 by auto show ?thesis using card_mono True 1 2 by auto qed next fix A B :: "'a set" assume 1: "esize A ≠ ∞" "A ⊂ B" show "esize A < esize B" using psubset_card_mono 1 by (cases "finite B", auto) qed end lemma esize_image[simp, intro]: assumes "inj_on f A" shows "esize (f ` A) = esize A" using card_image finite_imageD assms by (cases "finite A", auto) lemma esize_insert1[simp]: "a ∉ A ⟹ esize (insert a A) = eSuc (esize A)" by (cases "finite A", force+) lemma esize_insert2[simp]: "a ∈ A ⟹ esize (insert a A) = esize A" using insert_absorb by metis lemma esize_remove1[simp]: "a ∉ A ⟹ esize (A - {a}) = esize A" by (cases "finite A", force+) lemma esize_remove2[simp]: "a ∈ A ⟹ esize (A - {a}) = epred (esize A)" by (cases "finite A", force+) lemma esize_union_disjoint[simp]: assumes "A ∩ B = {}" shows "esize (A ∪ B) = esize A + esize B" proof (cases "finite (A ∪ B)") case True show ?thesis using card_Un_disjoint assms True by auto next case False show ?thesis using False by (cases "finite A", auto) qed lemma esize_lessThan[simp]: "esize {..< n} = n" proof (cases n) case (enat k) have 1: "finite {..< n}" unfolding enat by (metis finite_lessThan_enat_iff not_enat_eq) show ?thesis using 1 unfolding enat by simp next case (infinity) have 1: "infinite {..< n}" unfolding infinity using infinite_lessThan_infty by simp show ?thesis using 1 unfolding infinity by simp qed lemma esize_atMost[simp]: "esize {.. n} = eSuc n" proof (cases n) case (enat k) have 1: "finite {.. n}" unfolding enat by (metis atMost_iff finite_enat_bounded) show ?thesis using 1 unfolding enat by simp next case (infinity) have 1: "infinite {.. n}" unfolding infinity by (metis atMost_iff enat_ord_code(3) infinite_lessThan_infty infinite_super subsetI) show ?thesis using 1 unfolding infinity by simp qed lemma least_eSuc[simp]: assumes "A ≠ {}" shows "least (eSuc ` A) = eSuc (least A)" proof (rule antisym) obtain k where 10: "k ∈ A" using assms by blast have 11: "eSuc k ∈ eSuc ` A" using 10 by auto have 20: "least A ∈ A" using 10 LeastI by metis have 21: "least (eSuc ` A) ∈ eSuc ` A" using 11 LeastI by metis have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis have 31: "⋀ l. l ∈ eSuc ` A ⟹ least (eSuc ` A) ≤ l" using 11 Least_le by metis show "least (eSuc ` A) ≤ eSuc (least A)" using 20 31 by auto show "eSuc (least A) ≤ least (eSuc ` A)" using 21 30 by auto qed lemma Inf_enat_eSuc[simp]: "⨅ (eSuc ` A) = eSuc (⨅ A)" unfolding Inf_enat_def by simp definition lift :: "nat set ⇒ nat set" where "lift A ≡ insert 0 (Suc ` A)" lemma liftI_0[intro, simp]: "0 ∈ lift A" unfolding lift_def by auto lemma liftI_Suc[intro]: "a ∈ A ⟹ Suc a ∈ lift A" unfolding lift_def by auto lemma liftE[elim]: assumes "b ∈ lift A" obtains (0) "b = 0" | (Suc) a where "b = Suc a" "a ∈ A" using assms unfolding lift_def by auto lemma lift_esize[simp]: "esize (lift A) = eSuc (esize A)" unfolding lift_def by auto lemma lift_least[simp]: "least (lift A) = 0" unfolding lift_def by auto primrec nth_least :: "'a set ⇒ nat ⇒ 'a :: wellorder" where "nth_least A 0 = least A" | "nth_least A (Suc n) = nth_least (A - {least A}) n" lemma nth_least_wellformed[intro?, simp]: assumes "enat n < esize A" shows "nth_least A n ∈ A" using assms proof (induct n arbitrary: A) case 0 show ?case using 0 by simp next case (Suc n) have 1: "A ≠ {}" using Suc(2) by auto have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp have 3: "nth_least (A - {least A}) n ∈ A - {least A}" using Suc(1) 2 by this show ?case using 3 by simp qed lemma card_wellformed[intro?, simp]: fixes k :: "'a :: wellorder" assumes "k ∈ A" shows "enat (card {i ∈ A. i < k}) < esize A" proof (cases "finite A") case False show ?thesis using False by simp next case True have 1: "esize {i ∈ A. i < k} < esize A" using True assms by fastforce show ?thesis using True 1 by simp qed lemma nth_least_strict_mono: assumes "enat l < esize A" "k < l" shows "nth_least A k < nth_least A l" using assms proof (induct k arbitrary: A l) case 0 obtain l' where 1: "l = Suc l'" using 0(2) by (metis gr0_conv_Suc) have 2: "A ≠ {}" using 0(1) by auto have 3: "enat l' < esize (A - {least A})" using 0(1) 2 unfolding 1 by simp have 4: "nth_least (A - {least A}) l' ∈ A - {least A}" using 3 by rule show ?case using 1 4 by (auto intro: le_neq_trans) next case (Suc k) obtain l' where 1: "l = Suc l'" using Suc(3) by (metis Suc_lessE) have 2: "A ≠ {}" using Suc(2) by auto show ?case using Suc 2 unfolding 1 by simp qed lemma nth_least_mono[intro, simp]: assumes "enat l < esize A" "k ≤ l" shows "nth_least A k ≤ nth_least A l" using nth_least_strict_mono le_less assms by metis lemma card_nth_least[simp]: assumes "enat n < esize A" shows "card {k ∈ A. k < nth_least A n} = n" using assms proof (induct n arbitrary: A) case 0 have 1: "{k ∈ A. k < least A} = {}" using least_not_less by auto show ?case using nth_least.simps(1) card.empty 1 by metis next case (Suc n) have 1: "A ≠ {}" using Suc(2) by auto have 2: "enat n < esize (A - {least A})" using Suc(2) 1 by simp have 3: "nth_least A 0 < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast have 4: "{k ∈ A. k < nth_least A (Suc n)} = {least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 1 3 by auto have 5: "card {k ∈ A - {least A}. k < nth_least (A - {least A}) n} = n" using Suc(1) 2 by this have 6: "finite {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 5 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1) by (metis (no_types, lifting)) have "card {k ∈ A. k < nth_least A (Suc n)} = card ({least A} ∪ {k ∈ A - {least A}. k < nth_least (A - {least A}) n})" using 4 by simp also have "… = card {least A} + card {k ∈ A - {least A}. k < nth_least (A - {least A}) n}" using 6 by simp also have "… = Suc n" using 5 by simp finally show ?case by this qed lemma card_nth_least_le[simp]: assumes "enat n < esize A" shows "card {k ∈ A. k ≤ nth_least A n} = Suc n" proof - have 1: "{k ∈ A. k ≤ nth_least A n} = {nth_least A n} ∪ {k ∈ A. k < nth_least A n}" using assms by auto have 2: "card {k ∈ A. k < nth_least A n} = n" using assms by simp have 3: "finite {k ∈ A. k < nth_least A n}" using 2 Collect_empty_eq card.infinite infinite_imp_nonempty least_not_less nth_least.simps(1) by (metis (no_types, lifting)) have "card {k ∈ A. k ≤ nth_least A n} = card ({nth_least A n} ∪ {k ∈ A. k < nth_least A n})" unfolding 1 by rule also have "… = card {nth_least A n} + card {k ∈ A. k < nth_least A n}" using 3 by simp also have "… = Suc n" using assms by simp finally show ?thesis by this qed lemma nth_least_card: fixes k :: nat assumes "k ∈ A" shows "nth_least A (card {i ∈ A. i < k}) = k" proof (rule nat_set_card_equality_less) have 1: "enat (card {l ∈ A. l < k}) < esize A" proof (cases "finite A") case False show ?thesis using False by simp next case True have 1: "{l ∈ A. l < k} ⊂ A" using assms by blast have 2: "card {l ∈ A. l < k} < card A" using psubset_card_mono True 1 by this show ?thesis using True 2 by simp qed show "nth_least A (card {l ∈ A. l < k}) ∈ A" using 1 by rule show "k ∈ A" using assms by this show "card {z ∈ A. z < nth_least A (card {i ∈ A. i < k})} = card {z ∈ A. z < k}" using 1 by simp qed interpretation nth_least: bounded_function_pair "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" using nth_least_wellformed card_wellformed by (unfold_locales, blast+) interpretation nth_least: injection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" using card_nth_least by (unfold_locales, blast) interpretation nth_least: surjection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" for A :: "nat set" using nth_least_card by (unfold_locales, blast) interpretation nth_least: bijection "{i. enat i < esize A}" "A" "nth_least A" "λ k. card {i ∈ A. i < k}" for A :: "nat set" by unfold_locales lemma nth_least_strict_mono_inverse: fixes A :: "nat set" assumes "enat k < esize A" "enat l < esize A" "nth_least A k < nth_least A l" shows "k < l" using assms by (metis not_less_iff_gr_or_eq nth_least_strict_mono) lemma nth_least_less_card_less: fixes k :: nat shows "enat n < esize A ∧ nth_least A n < k ⟷ n < card {i ∈ A. i < k}" proof safe assume 1: "enat n < esize A" "nth_least A n < k" have 2: "nth_least A n ∈ A" using 1(1) by rule have "n = card {i ∈ A. i < nth_least A n}" using 1 by simp also have "… < card {i ∈ A. i < k}" using 1(2) 2 by simp finally show "n < card {i ∈ A. i < k}" by this next assume 1: "n < card {i ∈ A. i < k}" have "enat n < enat (card {i ∈ A. i < k})" using 1 by simp also have "… = esize {i ∈ A. i < k}" by simp also have "… ≤ esize A" by blast finally show 2: "enat n < esize A" by this have 3: "n = card {i ∈ A. i < nth_least A n}" using 2 by simp have 4: "card {i ∈ A. i < nth_least A n} < card {i ∈ A. i < k}" using 1 2 by simp have 5: "nth_least A n ∈ A" using 2 by rule show "nth_least A n < k" using 4 5 by simp qed lemma nth_least_less_esize_less: "enat n < esize A ∧ enat (nth_least A n) < k ⟷ enat n < esize {i ∈ A. enat i < k}" using nth_least_less_card_less by (cases k, simp+) lemma nth_least_le: assumes "enat n < esize A" shows "n ≤ nth_least A n" using assms proof (induct n) case 0 show ?case using 0 by simp next case (Suc n) have "n ≤ nth_least A n" using Suc by (metis Suc_ile_eq less_imp_le) also have "… < nth_least A (Suc n)" using nth_least_strict_mono Suc(2) by blast finally show ?case by simp qed lemma nth_least_eq: assumes "enat n < esize A" "enat n < esize B" assumes "⋀ i. i ≤ nth_least A n ⟹ i ≤ nth_least B n ⟹ i ∈ A ⟷ i ∈ B" shows "nth_least A n = nth_least B n" using assms proof (induct n arbitrary: A B) case 0 have 1: "least A = least B" proof (rule least_eq) show "A ≠ {}" using 0(1) by simp show "B ≠ {}" using 0(2) by simp next fix i assume 2: "i ≤ least A" "i ≤ least B" show "i ∈ A ⟷ i ∈ B" using 0(3) 2 unfolding nth_least.simps by this qed show ?case using 1 by simp next case (Suc n) have 1: "A ≠ {}" "B ≠ {}" using Suc(2, 3) by auto have 2: "least A = least B" proof (rule least_eq) show "A ≠ {}" using 1(1) by this show "B ≠ {}" using 1(2) by this next fix i assume 3: "i ≤ least A" "i ≤ least B" have 4: "nth_least A 0 ≤ nth_least A (Suc n)" using Suc(2) by blast have 5: "nth_least B 0 ≤ nth_least B (Suc n)" using Suc(3) by blast have 6: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 4 5 by auto show "i ∈ A ⟷ i ∈ B" using Suc(4) 6 by this qed have 3: "nth_least (A - {least A}) n = nth_least (B - {least B}) n" proof (rule Suc(1)) show "enat n < esize (A - {least A})" using Suc(2) 1(1) by simp show "enat n < esize (B - {least B})" using Suc(3) 1(2) by simp next fix i assume 3: "i ≤ nth_least (A - {least A}) n" "i ≤ nth_least (B - {least B}) n" have 4: "i ≤ nth_least A (Suc n)" "i ≤ nth_least B (Suc n)" using 3 by simp+ have 5: "i ∈ A ⟷ i ∈ B" using Suc(4) 4 by this show "i ∈ A - {least A} ⟷ i ∈ B - {least B}" using 2 5 by auto qed show ?case using 3 by simp qed lemma nth_least_restrict[simp]: assumes "enat i < esize {i ∈ s. enat i < k}" shows "nth_least {i ∈ s. enat i < k} i = nth_least s i" proof (rule nth_least_eq) show "enat i < esize {i ∈ s. enat i < k}" using assms by this show "enat i < esize s" using nth_least_less_esize_less assms by auto next fix l assume 1: "l ≤ nth_least {i ∈ s. enat i < k} i" have 2: "nth_least {i ∈ s. enat i < k} i ∈ {i ∈ s. enat i < k}" using assms by rule have "enat l ≤ enat (nth_least {i ∈ s. enat i < k} i)" using 1 by simp also have "… < k" using 2 by simp finally show "l ∈ {i ∈ s. enat i < k} ⟷ l ∈ s" by auto qed lemma least_nth_least[simp]: assumes "A ≠ {}" "⋀ i. i ∈ A ⟹ enat i < esize B" shows "least (nth_least B ` A) = nth_least B (least A)" using assms by simp lemma nth_least_nth_least[simp]: assumes "enat n < esize A" "⋀ i. i ∈ A ⟹ enat i < esize B" shows "nth_least B (nth_least A n) = nth_least (nth_least B ` A) n" using assms proof (induct n arbitrary: A) case 0 show ?case using 0 by simp next case (Suc n) have 1: "A ≠ {}" using Suc(2) by auto have 2: "nth_least B ` (A - {least A}) = nth_least B ` A - nth_least B ` {least A}" proof (rule inj_on_image_set_diff) show "inj_on (nth_least B) {i. enat i < esize B}" using nth_least.inj_on by this show "A - {least A} ⊆ {i. enat i < esize B}" using Suc(3) by blast show "{least A} ⊆ {i. enat i < esize B}" using Suc(3) 1 by force qed have "nth_least B (nth_least A (Suc n)) = nth_least B (nth_least (A - {least A}) n)" by simp also have "… = nth_least (nth_least B ` (A - {least A})) n" using Suc 1 by force also have "… = nth_least (nth_least B ` A - nth_least B ` {least A}) n" unfolding 2 by rule also have "… = nth_least (nth_least B ` A - {nth_least B (least A)}) n" by simp also have "… = nth_least (nth_least B ` A - {least (nth_least B ` A)}) n" using Suc(3) 1 by auto also have "… = nth_least (nth_least B ` A) (Suc n)" by simp finally show ?case by this qed lemma nth_least_Max[simp]: assumes "finite A" "A ≠ {}" shows "nth_least A (card A - 1) = Max A" using assms proof (induct "card A - 1" arbitrary: A) case 0 have 1: "card A = 1" using 0 by (metis One_nat_def Suc_diff_1 card_gt_0_iff) obtain a where 2: "A = {a}" using 1 by rule show ?case unfolding 2 by (simp del: insert_iff) next case (Suc n) have 1: "least A ∈ A" using Suc(4) by rule have 2: "card (A - {least A}) = Suc n" using Suc(2, 3) 1 by simp have 3: "A - {least A} ≠ {}" using 2 Suc(3) by fastforce have "nth_least A (card A - 1) = nth_least A (Suc n)" unfolding Suc(2) by rule also have "… = nth_least (A - {least A}) n" by simp also have "… = nth_least (A - {least A}) (card (A - {least A}) - 1)" unfolding 2 by simp also have "… = Max (A - {least A})" proof (rule Suc(1)) show "n = card (A - {least A}) - 1" unfolding 2 by simp show "finite (A - {least A})" using Suc(3) by simp show "A - {least A} ≠ {}" using 3 by this qed also have "… = Max A" using Suc(3) 3 by simp finally show ?case by this qed lemma nth_least_le_Max: assumes "finite A" "A ≠ {}" "enat n < esize A" shows "nth_least A n ≤ Max A" proof - have "nth_least A n ≤ nth_least A (card A - 1)" proof (rule nth_least_mono) show "enat (card A - 1) < esize A" by (metis Suc_diff_1 Suc_ile_eq assms(1) assms(2) card_eq_0_iff esize_set.simps(1) not_gr0 order_refl) show "n ≤ card A - 1" by (metis Suc_diff_1 Suc_leI antisym_conv assms(1) assms(3) enat_ord_simps(2) esize_set.simps(1) le_less neq_iff not_gr0) qed also have "… = Max A" using nth_least_Max assms(1, 2) by this finally show ?thesis by this qed lemma nth_least_not_contains: fixes k :: nat assumes "enat (Suc n) < esize A" "nth_least A n < k" "k < nth_least A (Suc n)" shows "k ∉ A" proof assume 1: "k ∈ A" have 2: "nth_least A (card {i ∈ A. i < k}) = k" using nth_least.right_inverse 1 by this have 3: "n < card {i ∈ A. i < k}" proof (rule nth_least_strict_mono_inverse) show "enat n < esize A" using assms(1) by auto show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp show "nth_least A n < nth_least A (card {i ∈ A. i < k})" using assms(2) 2 by simp qed have 4: "card {i ∈ A. i < k} < Suc n" proof (rule nth_least_strict_mono_inverse) show "enat (card {i ∈ A. i < k}) < esize A" using nth_least.g.wellformed 1 by simp show "enat (Suc n) < esize A" using assms(1) by this show "nth_least A (card {i ∈ A. i < k}) < nth_least A (Suc n)" using assms(3) 2 by simp qed show "False" using 3 4 by auto qed lemma nth_least_Suc[simp]: assumes "enat n < esize A" shows "nth_least (Suc ` A) n = Suc (nth_least A n)" using assms proof (induct n arbitrary: A) case (0) have 1: "A ≠ {}" using 0 by auto show ?case using 1 by simp next case (Suc n) have 1: "enat n < esize (A - {least A})" proof - have 2: "A ≠ {}" using Suc(2) by auto have 3: "least A ∈ A" using LeastI 2 by fast have 4: "A = insert (least A) A" using 3 by auto have "eSuc (enat n) = enat (Suc n)" by simp also have "… < esize A" using Suc(2) by this also have "… = esize (insert (least A) A)" using 4 by simp also have "… = eSuc (esize (A - {least A}))" using 3 2 by simp finally show ?thesis using Extended_Nat.eSuc_mono by metis qed have "nth_least (Suc ` A) (Suc n) = nth_least (Suc ` A - {least (Suc ` A)}) n" by simp also have "… = nth_least (Suc ` (A - {least A})) n" by simp also have "… = Suc (nth_least (A - {least A}) n)" using Suc(1) 1 by this also have "… = Suc (nth_least A (Suc n))" by simp finally show ?case by this qed lemma nth_least_lift[simp]: "nth_least (lift A) 0 = 0" "enat n < esize A ⟹ nth_least (lift A) (Suc n) = Suc (nth_least A n)" unfolding lift_def by simp+ lemma nth_least_list_card[simp]: assumes "enat n ≤ esize A" shows "card {k ∈ A. k < nth_least (lift A) n} = n" using less_Suc_eq_le assms by (cases n, auto simp del: nth_least.simps) end