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