Theory Card_Lemmas

(*  Title:      Card_Lemmas.thy
    Author:     Ata Keskin, TU München
*)

section "Lemmas involving the cardinality of sets"

text ‹In this section, we prove some lemmas that make use of the term @{term card} or provide bounds for it.›

theory Card_Lemmas
  imports Main
begin

lemma card_Int_copy:
  assumes "finite X" and "A ∪ B ⊆ X" and "∃f. inj_on f (A ∩ B) ∧ (A ∪ B) ∩ (f ` (A ∩ B)) = {} ∧ f ` (A ∩ B) ⊆ X"
  shows "card A + card B ≤ card X"
proof -
  from rev_finite_subset[OF assms(1), of A] rev_finite_subset[OF assms(1), of B] assms(2) 
  have finite_A: "finite A" and finite_B: "finite B" by blast+
  then have finite_A_Un_B: "finite (A ∪ B)" and finite_A_Int_B: "finite (A ∩ B)" by blast+
  from assms(3) obtain f where f_inj_on: "inj_on f (A ∩ B)" 
                           and f_disjnt: "(A ∪ B) ∩ (f ` (A ∩ B)) = {}" 
                           and f_imj_in: "f ` (A ∩ B) ⊆ X" by blast
  from finite_A_Int_B have finite_f_img: "finite (f ` (A ∩ B))" by blast
  from assms(2) f_imj_in have union_in: "(A ∪ B) ∪ f ` (A ∩ B) ⊆ X" by blast
  
  from card_Un_Int[OF finite_A finite_B] have "card A + card B = card (A ∪ B) + card (A ∩ B)" .
  also from card_image[OF f_inj_on] have "... = card (A ∪ B) + card (f ` (A ∩ B))" by presburger
  also from card_Un_disjoint[OF finite_A_Un_B finite_f_img f_disjnt] have "... = card ((A ∪ B) ∪ f ` (A ∩ B))" by argo
  also from card_mono[OF assms(1) union_in] have "... ≤ card X" by blast
  finally show ?thesis .
qed

lemma finite_diff_not_empty: 
  assumes "finite Y" and "card Y < card X"
  shows "X - Y ≠ {}"
proof
  assume "X - Y = {}"
  hence "X ⊆ Y" by simp
  from card_mono[OF assms(1) this] assms(2) show False by linarith
qed

lemma obtain_difference_element:
  fixes F :: "'a set set"
  assumes "2 ≤ card F"
  obtains "x" where "x∈ ⋃F" "x ∉ ⋂F"
proof -
  from assms card_le_Suc_iff[of 1 F] obtain A F' where 0: "F = insert A F'" and 1: "A ∉ F'" and 2: "1 ≤ card F'" by auto
  from 2 card_le_Suc_iff[of 0 F'] obtain B F'' where 3: "F' = insert B F''" by auto
  from 1 3 have A_noteq_B: "A ≠ B" by blast
  from 0 3 have A_in_F: "A ∈ F" and B_in_F: "B ∈ F" by blast+
  from A_noteq_B have "(A - B) ∪ (B - A) ≠ {}" by simp
  with A_in_F B_in_F that show thesis by blast
qed

end