Theory InfiniteSet2

(*  Title:      InfiniteSet2.thy
    Date:       Aug 2008
    Author:     David Trachtenherz
*)

section ‹Set operations with results of type enat›

theory InfiniteSet2
imports SetInterval2
begin

subsection ‹Set operations with @{typ enat}›

subsubsection ‹Basic definitions›

definition icard :: "'a set ⇒ enat"
  where "icard A ≡ if finite A then enat (card A) else ∞"


subsection ‹Results for ‹icard››

lemma icard_UNIV_nat: "icard (UNIV::nat set) = ∞"
by (simp add: icard_def)

lemma icard_finite_conv: "(icard A = enat (card A)) = finite A"
by (case_tac "finite A", simp_all add: icard_def)
lemma icard_infinite_conv: "(icard A = ∞) = infinite A"
by (case_tac "finite A", simp_all add: icard_def)

corollary icard_finite: "finite A ⟹ icard A = enat (card A)"
by (rule icard_finite_conv[THEN iffD2])
corollary icard_infinite[simp]: "infinite A ⟹ icard A = ∞"
by (rule icard_infinite_conv[THEN iffD2])

lemma icard_eq_enat_imp: "icard A = enat n ⟹ finite A"
by (case_tac "finite A", simp_all)
lemma icard_eq_Infty_imp: "icard A = ∞ ⟹ infinite A"
by (rule icard_infinite_conv[THEN iffD1])

lemma icard_the_enat: "finite A ⟹ the_enat (icard A) = card A"
by (simp add: icard_def)

lemma icard_eq_enat_imp_card: "icard A = enat n ⟹ card A = n"
by (frule icard_eq_enat_imp, simp add: icard_finite)

lemma icard_eq_enat_card_conv: "0 < n ⟹ (icard A = enat n) = (card A = n)"
apply (rule iffI)
 apply (simp add: icard_eq_enat_imp_card)
apply (drule sym, simp)
apply (frule card_gr0_imp_finite)
apply (rule icard_finite, assumption)
done

lemma icard_empty[simp]: "icard {} = 0"
by (simp add: icard_finite[OF finite.emptyI])
lemma icard_empty_iff: "(icard A = 0) = (A = {})"
apply (unfold zero_enat_def)
apply (rule iffI)
 apply (frule icard_eq_enat_imp)
 apply (simp add: icard_finite)
apply simp
done
lemmas icard_empty_iff_enat = icard_empty_iff[unfolded zero_enat_def]

lemma icard_not_empty_iff: "(0 < icard A) = (A ≠ {})"
by (simp add: icard_empty_iff[symmetric])
lemmas icard_not_empty_iff_enat = icard_not_empty_iff[unfolded zero_enat_def]

lemma icard_singleton: "icard {a} = eSuc 0"
by (simp add: icard_finite eSuc_enat)
lemmas icard_singleton_enat[simp] = icard_singleton[unfolded zero_enat_def]
lemma icard_1_imp_singleton: "icard A = eSuc 0 ⟹ ∃a. A = {a}"
apply (simp add: eSuc_enat)
apply (frule icard_eq_enat_imp)
apply (simp add: icard_finite card_1_imp_singleton)
done
lemma icard_1_singleton_conv: "(icard A = eSuc 0) = (∃a. A = {a})"
apply (rule iffI)
 apply (simp add: icard_1_imp_singleton)
apply fastforce
done

lemma icard_insert_disjoint: "x ∉ A ⟹ icard (insert x A) = eSuc (icard A)"
apply (case_tac "finite A")
 apply (simp add: icard_finite eSuc_enat card_insert_disjoint)
apply (simp add: infinite_insert)
done

lemma icard_insert_if: "icard (insert x A) = (if x ∈ A then icard A else eSuc (icard A))"
apply (case_tac "x ∈ A")
 apply (simp add: insert_absorb)
apply (simp add: icard_insert_disjoint)
done

lemmas icard_0_eq = icard_empty_iff

lemma icard_Suc_Diff1: "x ∈ A ⟹ eSuc (icard (A - {x})) = icard A"
apply (case_tac "finite A")
 apply (simp add: icard_finite eSuc_enat in_imp_not_empty not_empty_card_gr0_conv[THEN iffD1])
apply (simp add: Diff_infinite_finite[OF singleton_finite])
done

lemma icard_Diff_singleton: "x ∈ A ⟹ icard (A - {x}) = icard A - 1"
apply (rule eSuc_inject[THEN iffD1])
apply (frule in_imp_not_empty, drule icard_not_empty_iff[THEN iffD2])
apply (simp add: icard_Suc_Diff1 eSuc_pred_enat one_eSuc)
done

lemma icard_Diff_singleton_if: "icard (A - {x}) = (if x ∈ A then icard A - 1 else icard A)"
by (simp add: icard_Diff_singleton)

lemma icard_insert: "icard (insert x A) = eSuc (icard (A - {x}))"
by (metis icard_Diff_singleton_if icard_Suc_Diff1 icard_insert_disjoint insert_absorb)

lemma icard_insert_le: "icard A ≤ icard (insert x A)"
by (simp add: icard_insert_if)

lemma icard_mono: "A ⊆ B ⟹ icard A ≤ icard B"
apply (case_tac "finite B")
 apply (frule subset_finite_imp_finite, simp)
 apply (simp add: icard_finite card_mono)
apply simp
done

lemma not_icard_seteq: "∃(A::nat set) B. (A ⊆ B ∧ icard B ≤ icard A ∧ ¬ A = B)"
apply (rule_tac x="{1..}" in exI)
apply (rule_tac x="{0..}" in exI)
apply (fastforce simp add: infinite_atLeast)
done

lemma not_psubset_icard_mono: "∃(A::nat set) B. A ⊂ B ∧ ¬ icard A < icard B"
apply (rule_tac x="{1..}" in exI)
apply (rule_tac x="{0..}" in exI)
apply (fastforce simp add: infinite_atLeast)
done

lemma icard_Un_Int: "icard A + icard B = icard (A ∪ B) + icard (A ∩ B)"
apply (case_tac "finite A", case_tac "finite B")
 apply (simp add: icard_finite card_Un_Int[of A])
apply simp_all
done

lemma icard_Un_disjoint: "A ∩ B = {} ⟹ icard (A ∪ B) = icard A + icard B"
by (simp add: icard_Un_Int[of A])

lemma not_icard_Diff_subset: "∃(A::nat set) B. B ⊆ A ∧ ¬ icard (A - B) = icard A - icard B"
apply (rule_tac x="{0..}" in exI)
apply (rule_tac x="{1..}" in exI)
apply (simp add: set_diff_eq linorder_not_le icard_UNIV_nat eSuc_enat)
done

lemma not_icard_Diff1_less: "∃(A::nat set)x. x ∈ A ∧ ¬ icard (A - {x}) < icard A"
by (rule_tac x="{0..}" in exI, simp)

lemma not_icard_Diff2_less: "∃(A::nat set)x y. x ∈ A ∧ y ∈ A ∧ ¬ icard (A - {x} - {y}) < icard A"
by (rule_tac x="{0..}" in exI, simp)

lemma icard_Diff1_le: "icard (A - {x}) ≤ icard A"
by (rule icard_mono, rule Diff_subset)

lemma icard_psubset: "⟦ A ⊆ B; icard A < icard B ⟧ ⟹ A ⊂ B"
by (metis less_le psubset_eq)

lemma icard_partition: "
  ⟦ ⋀c. c ∈ C ⟹ icard c = k; ⋀c1 c2. ⟦c1 ∈ C; c2 ∈ C; c1 ≠ c2⟧ ⟹ c1 ∩ c2 = {} ⟧ ⟹
  icard (⋃C) = k * icard C"
apply (case_tac "C = {}", simp)
apply (case_tac "k = 0")
 apply (simp add: icard_empty_iff_enat)
apply simp
apply (case_tac k, rename_tac k1)
 apply (subgoal_tac "0 < k1")
  prefer 2
  apply simp
 apply (case_tac "finite C")
  apply (simp add: icard_finite)
  apply (subgoal_tac "⋀c. c ∈ C ⟹ card c = k1")
   prefer 2
   apply (rule icard_eq_enat_imp_card, simp)
  apply (frule_tac C=C and k=k1 in SetInterval2.card_partition, simp+)
  apply (subgoal_tac "finite (⋃C)")
   prefer 2
   apply (rule card_gr0_imp_finite)
   apply (simp add: not_empty_card_gr0_conv)
  apply (simp add: icard_finite)
 apply simp
 apply (rule icard_infinite)
 apply (rule ccontr, simp)
 apply (drule finite_UnionD, simp)
apply (frule icard_not_empty_iff[THEN iffD2])
apply (simp add: icard_infinite_conv)
apply (frule not_empty_imp_ex, erule exE, rename_tac c)
apply (frule Union_upper)
apply (rule infinite_super, assumption)
apply simp
done

lemma icard_image_le: "icard (f ` A) ≤ icard A"
apply (case_tac "finite A")
 apply (simp add: icard_finite card_image_le)
apply simp
done

lemma icard_image: "inj_on f A ⟹ icard (f ` A) = icard A"
apply (case_tac "finite A")
 apply (simp add: icard_finite card_image)
apply (simp add: icard_infinite_conv inj_on_imp_infinite_image)
done

lemma not_eq_icard_imp_inj_on: "∃(f::nat⇒nat) (A::nat set). icard (f ` A) = icard A ∧ ¬ inj_on f A"
apply (rule_tac x="λn. (if n = 0 then Suc 0 else n)" in exI)
apply (rule_tac x="{0..}" in exI)
apply (rule conjI)
 apply (rule subst[of "{1..}" "((λn. if n = 0 then Suc 0 else n) ` {0..})"])
  apply (simp add: set_eq_iff)
  apply (rule allI, rename_tac n)
  apply (case_tac "n = 0", simp)
  apply simp
 apply (simp only: icard_infinite[OF infinite_atLeast])
apply (simp add: inj_on_def)
apply blast
done

lemma not_inj_on_iff_eq_icard: "∃(f::nat⇒nat) (A::nat set). ¬ (inj_on f A = (icard (f ` A) = icard A))"
by (insert not_eq_icard_imp_inj_on, blast)

lemma icard_inj_on_le: "⟦ inj_on f A; f ` A ⊆ B ⟧ ⟹ icard A ≤ icard B"
apply (case_tac "finite B")
 apply (metis icard_image icard_mono)
apply simp
done

lemma icard_bij_eq: "
  ⟦ inj_on f A; f ` A ⊆ B; inj_on g B; g ` B ⊆ A ⟧ ⟹
  icard A = icard B"
by (simp add: order_eq_iff icard_inj_on_le)

lemma icard_cartesian_product: "icard (A × B) = icard A * icard B"
apply (case_tac "A = {} ∨ B = {}", fastforce)
apply clarsimp
apply (case_tac "finite A ∧ finite B")
 apply (simp add: icard_finite)
apply (simp only: de_Morgan_conj, erule disjE)
apply (simp_all add:
  icard_not_empty_iff[symmetric]
  cartesian_product_infiniteL_imp_infinite cartesian_product_infiniteR_imp_infinite)
done

lemma icard_cartesian_product_singleton: "icard ({x} × A) = icard A"
by (simp add: icard_cartesian_product mult_eSuc)

lemma icard_cartesian_product_singleton_right: "icard (A × {x}) = icard A"
by (simp add: icard_cartesian_product mult_eSuc_right)

lemma
  icard_lessThan: "icard {..<u} = enat u" and
  icard_atMost: "icard {..u} = enat (Suc u)" and
  icard_atLeastLessThan: "icard {l..<u} = enat (u - l)" and
  icard_atLeastAtMost: "icard {l..u} = enat (Suc u - l)" and
  icard_greaterThanAtMost: "icard {l<..u} = enat (u - l)" and
  icard_greaterThanLessThan: "icard {l<..<u} = enat (u - Suc l)"
by (simp_all add: icard_finite)

lemma icard_atLeast: "icard {(u::nat)..} = ∞"
by (simp add: infinite_atLeast)

lemma icard_greaterThan: "icard {(u::nat)<..} = ∞"
by (simp add: infinite_greaterThan)

lemma
  icard_atLeastZeroLessThan_int: "icard {0..<u} = enat (nat u)" and
  icard_atLeastLessThan_int: "icard {l..<u} = enat (nat (u - l))" and
  icard_atLeastAtMost_int: "icard {l..u} = enat (nat (u - l + 1))" and
  icard_greaterThanAtMost_int: "icard {l<..u} = enat (nat (u - l))"
by (simp_all add: icard_finite)

lemma icard_atLeast_int: "icard {(u::int)..} = ∞"
by (simp add: infinite_atLeast_int)

lemma icard_greaterThan_int: "icard {(u::int)<..} = ∞"
by (simp add: infinite_greaterThan_int)

lemma icard_atMost_int: "icard {..(u::int)} = ∞"
by (simp add: infinite_atMost_int)

lemma icard_lessThan_int: "icard {..<(u::int)} = ∞"
by (simp add: infinite_lessThan_int)

end