section ‹Sets› theory Set_Extensions imports "HOL-Library.Infinite_Set" begin declare finite_subset[intro] lemma set_not_emptyI[intro 0]: "x ∈ S ⟹ S ≠ {}" by auto lemma sets_empty_iffI[intro 0]: assumes "⋀ a. a ∈ A ⟹ ∃ b. b ∈ B" assumes "⋀ b. b ∈ B ⟹ ∃ a. a ∈ A" shows "A = {} ⟷ B = {}" using assms by auto lemma disjointI[intro 0]: assumes "⋀ x. x ∈ A ⟹ x ∈ B ⟹ False" shows "A ∩ B = {}" using assms by auto lemma range_subsetI[intro 0]: assumes "⋀ x. f x ∈ S" shows "range f ⊆ S" using assms by blast lemma finite_imageI_range: assumes "finite (range f)" shows "finite (f ` A)" using finite_subset image_mono subset_UNIV assms by metis lemma inf_img_fin_domE': assumes "infinite A" assumes "finite (f ` A)" obtains y where "y ∈ f ` A" "infinite (A ∩ f -` {y})" proof (rule ccontr) assume 1: "¬ thesis" have 2: "finite (⋃ y ∈ f ` A. A ∩ f -` {y})" proof (rule finite_UN_I) show "finite (f ` A)" using assms(2) by this show "⋀ y. y ∈ f ` A ⟹ finite (A ∩ f -` {y})" using that 1 by blast qed have 3: "A ⊆ (⋃ y ∈ f ` A. A ∩ f -` {y})" by blast show False using assms(1) 2 3 by blast qed lemma vimage_singleton[simp]: "f -` {y} = {x. f x = y}" unfolding vimage_def by simp lemma these_alt_def: "Option.these S = Some -` S" unfolding Option.these_def by force lemma the_vimage_subset: "the -` {a} ⊆ {None, Some a}" by auto lemma finite_induct_reverse[consumes 1, case_names remove]: assumes "finite S" assumes "⋀ S. finite S ⟹ (⋀ x. x ∈ S ⟹ P (S - {x})) ⟹ P S" shows "P S" using assms(1) proof (induct rule: finite_psubset_induct) case (psubset S) show ?case proof (rule assms(2)) show "finite S" using psubset(1) by this next fix x assume 0: "x ∈ S" show "P (S - {x})" proof (rule psubset(2)) show "S - {x} ⊂ S" using 0 by auto qed qed qed lemma zero_not_in_Suc_image[simp]: "0 ∉ Suc ` A" by auto lemma Collect_split_Suc: "¬ P 0 ⟹ {i. P i} = Suc ` {i. P (Suc i)}" "P 0 ⟹ {i. P i} = {0} ∪ Suc ` {i. P (Suc i)}" proof - assume "¬ P 0" thus "{i. P i} = Suc ` {i. P (Suc i)}" by (auto, metis image_eqI mem_Collect_eq nat.exhaust) next assume "P 0" thus "{i. P i} = {0} ∪ Suc ` {i. P (Suc i)}" by (auto, metis imageI mem_Collect_eq not0_implies_Suc) qed lemma Collect_subsume[simp]: assumes "⋀ x. x ∈ A ⟹ P x" shows "{x ∈ A. P x} = A" using assms unfolding simp_implies_def by auto lemma Max_ge': assumes "finite A" "A ≠ {}" assumes "b ∈ A" "a ≤ b" shows "a ≤ Max A" using assms Max_ge_iff by auto abbreviation "least A ≡ LEAST k. k ∈ A" lemma least_contains[intro?, simp]: fixes A :: "'a :: wellorder set" assumes "k ∈ A" shows "least A ∈ A" using assms by (metis LeastI) lemma least_contains'[intro?, simp]: fixes A :: "'a :: wellorder set" assumes "A ≠ {}" shows "least A ∈ A" using assms by (metis LeastI equals0I) lemma least_least[intro?, simp]: fixes A :: "'a :: wellorder set" assumes "k ∈ A" shows "least A ≤ k" using assms by (metis Least_le) lemma least_unique: fixes A :: "'a :: wellorder set" assumes "k ∈ A" "k ≤ least A" shows "k = least A" using assms by (metis Least_le antisym) lemma least_not_less: fixes A :: "'a :: wellorder set" assumes "k < least A" shows "k ∉ A" using assms by (metis not_less_Least) lemma leastI2_order[simp]: fixes A :: "'a :: wellorder set" assumes "A ≠ {}" "⋀ k. k ∈ A ⟹ (⋀ l. l ∈ A ⟹ k ≤ l) ⟹ P k" shows "P (least A)" proof (rule LeastI2_order) show "least A ∈ A" using assms(1) by rule next fix k assume 1: "k ∈ A" show "least A ≤ k" using 1 by rule next fix k assume 1: "k ∈ A" "∀ l. l ∈ A ⟶ k ≤ l" show "P k" using assms(2) 1 by auto qed lemma least_singleton[simp]: fixes a :: "'a :: wellorder" shows "least {a} = a" by (metis insert_not_empty least_contains' singletonD) lemma least_image[simp]: fixes f :: "'a :: wellorder ⇒ 'b :: wellorder" assumes "A ≠ {}" "⋀ k l. k ∈ A ⟹ l ∈ A ⟹ k ≤ l ⟹ f k ≤ f l" shows "least (f ` A) = f (least A)" proof (rule leastI2_order) show "A ≠ {}" using assms(1) by this next fix k assume 1: "k ∈ A" "⋀ i. i ∈ A ⟹ k ≤ i" show "least (f ` A) = f k" proof (rule leastI2_order) show "f ` A ≠ {}" using assms(1) by simp next fix l assume 2: "l ∈ f ` A" "⋀ i. i ∈ f ` A ⟹ l ≤ i" show "l = f k" using assms(2) 1 2 by force qed qed lemma least_le: fixes A B :: "'a :: wellorder set" assumes "B ≠ {}" assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ B ⟹ i ∈ A" shows "least A ≤ least B" proof (rule ccontr) assume 1: "¬ least A ≤ least B" have 2: "least B ∈ A" using assms(1, 2) 1 by simp have 3: "least A ≤ least B" using 2 by rule show False using 1 3 by rule qed lemma least_eq: fixes A B :: "'a :: wellorder set" assumes "A ≠ {}" "B ≠ {}" assumes "⋀ i. i ≤ least A ⟹ i ≤ least B ⟹ i ∈ A ⟷ i ∈ B" shows "least A = least B" using assms by (auto intro: antisym least_le) lemma least_Suc[simp]: assumes "A ≠ {}" shows "least (Suc ` A) = Suc (least A)" proof (rule antisym) obtain k where 10: "k ∈ A" using assms by blast have 11: "Suc k ∈ Suc ` A" using 10 by auto have 20: "least A ∈ A" using 10 LeastI by metis have 21: "least (Suc ` A) ∈ Suc ` A" using 11 LeastI by metis have 30: "⋀ l. l ∈ A ⟹ least A ≤ l" using 10 Least_le by metis have 31: "⋀ l. l ∈ Suc ` A ⟹ least (Suc ` A) ≤ l" using 11 Least_le by metis show "least (Suc ` A) ≤ Suc (least A)" using 20 31 by auto show "Suc (least A) ≤ least (Suc ` A)" using 21 30 by auto qed lemma least_Suc_diff[simp]: "Suc ` A - {least (Suc ` A)} = Suc ` (A - {least A})" proof (cases "A = {}") case True show ?thesis unfolding True by simp next case False have "Suc ` A - {least (Suc ` A)} = Suc ` A - {Suc (least A)}" using False by simp also have "… = Suc ` A - Suc ` {least A}" by simp also have "… = Suc ` (A - {least A})" by blast finally show ?thesis by this qed lemma Max_diff_least[simp]: fixes A :: "'a :: wellorder set" assumes "finite A" "A - {least A} ≠ {}" shows "Max (A - {least A}) = Max A" proof - have 1: "least A ∈ A" using assms(2) by auto obtain a where 2: "a ∈ A - {least A}" using assms(2) by blast have "Max A = Max (insert (least A) (A - {least A}))" using insert_absorb 1 by force also have "… = max (least A) (Max (A - {least A}))" proof (rule Max_insert) show "finite (A - {least A})" using assms(1) by auto show "A - {least A} ≠ {}" using assms(2) by this qed also have "… = Max (A - {least A})" proof (rule max_absorb2, rule Max_ge') show "finite (A - {least A})" using assms(1) by auto show "A - {least A} ≠ {}" using assms(2) by this show "a ∈ A - {least A}" using 2 by this show "least A ≤ a" using 2 by simp qed finally show ?thesis by rule qed lemma nat_set_card_equality_less: fixes A :: "nat set" assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z < x} = card {z ∈ A. z < y}" shows "x = y" proof (cases x y rule: linorder_cases) case less have 0: "finite {z ∈ A. z < y}" by simp have 1: "{z ∈ A. z < x} ⊂ {z ∈ A. z < y}" using assms(1, 2) less by force have 2: "card {z ∈ A. z < x} < card {z ∈ A. z < y}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp next case equal show ?thesis using equal by this next case greater have 0: "finite {z ∈ A. z < x}" by simp have 1: "{z ∈ A. z < y} ⊂ {z ∈ A. z < x}" using assms(1, 2) greater by force have 2: "card {z ∈ A. z < y} < card {z ∈ A. z < x}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp qed lemma nat_set_card_equality_le: fixes A :: "nat set" assumes "x ∈ A" "y ∈ A" "card {z ∈ A. z ≤ x} = card {z ∈ A. z ≤ y}" shows "x = y" proof (cases x y rule: linorder_cases) case less have 0: "finite {z ∈ A. z ≤ y}" by simp have 1: "{z ∈ A. z ≤ x} ⊂ {z ∈ A. z ≤ y}" using assms(1, 2) less by force have 2: "card {z ∈ A. z ≤ x} < card {z ∈ A. z ≤ y}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp next case equal show ?thesis using equal by this next case greater have 0: "finite {z ∈ A. z ≤ x}" by simp have 1: "{z ∈ A. z ≤ y} ⊂ {z ∈ A. z ≤ x}" using assms(1, 2) greater by force have 2: "card {z ∈ A. z ≤ y} < card {z ∈ A. z ≤ x}" using psubset_card_mono 0 1 by this show ?thesis using assms(3) 2 by simp qed lemma nat_set_card_mono[simp]: fixes A :: "nat set" assumes "x ∈ A" shows "card {z ∈ A. z < x} < card {z ∈ A. z < y} ⟷ x < y" proof assume 1: "card {z ∈ A. z < x} < card {z ∈ A. z < y}" show "x < y" proof (rule ccontr) assume 2: "¬ x < y" have 3: "card {z ∈ A. z < y} ≤ card {z ∈ A. z < x}" using 2 by (auto intro: card_mono) show "False" using 1 3 by simp qed next assume 1: "x < y" show "card {z ∈ A. z < x} < card {z ∈ A. z < y}" proof (intro psubset_card_mono psubsetI) show "finite {z ∈ A. z < y}" by simp show "{z ∈ A. z < x} ⊆ {z ∈ A. z < y}" using 1 by auto show "{z ∈ A. z < x} ≠ {z ∈ A. z < y}" using assms 1 by blast qed qed lemma card_one[elim]: assumes "card A = 1" obtains a where "A = {a}" using assms by (metis One_nat_def card_Suc_eq) lemma image_alt_def: "f ` A = {f x |x. x ∈ A}" by auto lemma supset_mono_inductive[mono]: assumes "⋀ x. x ∈ B ⟶ x ∈ C" shows "A ⊆ B ⟶ A ⊆ C" using assms by auto lemma Collect_mono_inductive[mono]: assumes "⋀ x. P x ⟶ Q x" shows "x ∈ {x. P x} ⟶ x ∈ {x. Q x}" using assms by auto lemma image_union_split: assumes "f ` (A ∪ B) = g ` C" obtains D E where "f ` A = g ` D" "f ` B = g ` E" "D ⊆ C" "E ⊆ C" using assms unfolding image_Un by (metis (erased, lifting) inf_sup_ord(3) inf_sup_ord(4) subset_imageE) lemma image_insert_split: assumes "inj g" "f ` insert a B = g ` C" obtains d E where "f a = g d" "f ` B = g ` E" "d ∈ C" "E ⊆ C" proof - have 1: "f ` ({a} ∪ B) = g ` C" using assms(2) by simp obtain D E where 2: "f ` {a} = g ` D" "f ` B = g ` E" "D ⊆ C" "E ⊆ C" using image_union_split 1 by this obtain d where 3: "D = {d}" using assms(1) 2(1) by (auto, metis (erased, opaque_lifting) imageE image_empty image_insert inj_image_eq_iff singletonI) show ?thesis using that 2 unfolding 3 by simp qed end