Theory InfiniteSet2

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

header {* Set operations with results of type inat *}

theory InfiniteSet2
imports SetInterval2
begin

subsection {* Set operations with @{typ inat} *} 

subsubsection {* Basic definitions *}

definition
  icard :: "'a set => inat"
where
  "icard A ≡ if finite A then Fin (card A) else ∞"

subsection {* Results for @{text icard} *}

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

lemma icard_finite_conv: "(icard A = Fin (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 = Fin (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_Fin_imp: "icard A = Fin 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_Fin: "finite A ==> the_Fin (icard A) = card A"
by (simp add: icard_def)

lemma icard_eq_Fin_imp_card: "icard A = Fin n ==> card A = n"
by (frule icard_eq_Fin_imp, simp add: icard_finite)

lemma icard_eq_Fin_card_conv: "0 < n ==> (icard A = Fin n) = (card A = n)"
apply (rule iffI)
 apply (simp add: icard_eq_Fin_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_inat_def)
apply (rule iffI)
 apply (frule icard_eq_Fin_imp)
 apply (simp add: icard_finite)
apply simp
done
lemmas icard_empty_iff_Fin = icard_empty_iff[unfolded zero_inat_def]

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

lemma icard_singleton: "icard {a} = iSuc 0"
by (simp add: icard_finite iSuc_Fin)
lemmas icard_singleton_Fin[simp] = icard_singleton[unfolded zero_inat_def]
lemma icard_1_imp_singleton: "icard A = iSuc 0 ==> ∃a. A = {a}"
apply (simp add: iSuc_Fin)
apply (frule icard_eq_Fin_imp)
apply (simp add: icard_finite card_1_imp_singleton)
done
lemma icard_1_singleton_conv: "(icard A = iSuc 0) = (∃a. A = {a})"
apply (rule iffI)
 apply (simp add: icard_1_imp_singleton)
apply fastsimp
done



thm Finite_Set.card_insert_disjoint
lemma icard_insert_disjoint: "x ∉ A ==> icard (insert x A) = iSuc (icard A)"
apply (case_tac "finite A")
 apply (simp add: icard_finite iSuc_Fin card_insert_disjoint)
apply (simp add: infinite_insert)
done
thm Finite_Set.card_insert_if
lemma icard_insert_if: "icard (insert x A) = (if x ∈ A then icard A else iSuc (icard A))"
apply (case_tac "x ∈ A")
 apply (simp add: insert_absorb)
apply (simp add: icard_insert_disjoint)
done
thm Finite_Set.card_0_eq
lemmas icard_0_eq = icard_empty_iff

thm Finite_Set.card_Suc_Diff1
lemma icard_Suc_Diff1: "x ∈ A ==> iSuc (icard (A - {x})) = icard A"
apply (case_tac "finite A")
 apply (simp add: icard_finite iSuc_Fin in_imp_not_empty not_empty_card_gr0_conv[THEN iffD1])
apply (simp add: Diff_infinite_finite[OF singleton_finite])
done

thm Finite_Set.card_Diff_singleton
lemma icard_Diff_singleton: "x ∈ A ==> icard (A - {x}) = icard A - 1"
apply (rule iSuc_inject[THEN iffD1])
apply (frule in_imp_not_empty, drule icard_not_empty_iff[THEN iffD2])
apply (simp add: icard_Suc_Diff1 iSuc_pred_Fin one_iSuc)
done

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

thm Finite_Set.card_insert
lemma icard_insert: "icard (insert x A) = iSuc (icard (A - {x}))"
by (metis icard_Diff_singleton_if icard_Suc_Diff1 icard_insert_disjoint insert_absorb)

thm Finite_Set.card_insert_le
lemma icard_insert_le: "icard A ≤ icard (insert x A)"
by (simp add: icard_insert_if)

thm Finite_Set.card_mono
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

thm Finite_Set.card_seteq
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 (fastsimp simp add: infinite_atLeast)
done

thm Finite_Set.psubset_card_mono
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 (fastsimp simp add: infinite_atLeast)
done

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

thm Finite_Set.card_Un_disjoint
lemma icard_Un_disjoint: "A ∩ B = {} ==> icard (A ∪ B) = icard A + icard B"
by (simp add: icard_Un_Int[of A])

thm Finite_Set.card_Diff_subset
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 iSuc_Fin)
done


thm 
  Finite_Set.card_Diff1_less
  Finite_Set.card_Diff2_less
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)

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

thm Finite_Set.card_psubset
lemma icard_psubset: "[| A ⊆ B; icard A < icard B |] ==> A ⊂ B"
by (metis iless_ile psubset_eq)

thm SetInterval2.card_partition
lemma icard_partition: "
  [| !!c. c ∈ C ==> icard c = k; !!c1 c2. [|c1 ∈ C; c2 ∈ C; c1 ≠ c2|] ==> c1 ∩ c2 = {} |] ==> 
  icard (\<Union>C) = k * icard C"
apply (case_tac "C = {}", simp)
apply (case_tac "k = 0")
 apply (simp add: icard_empty_iff_Fin)
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)
  thm SetInterval2.card_partition
  thm icard_eq_Fin_imp_card
  apply (subgoal_tac "!!c. c ∈ C ==> card c = k1")
   prefer 2
   apply (rule icard_eq_Fin_imp_card, simp)
  thm SetInterval2.card_partition
  apply (frule_tac C=C and k=k1 in SetInterval2.card_partition, simp+)
  apply (subgoal_tac "finite (\<Union>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)
 thm finite_UnionD
 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)
thm Union_upper
apply (frule Union_upper)
thm infinite_super
apply (rule infinite_super, assumption)
apply simp
done
 
thm Big_Operators.setsum_constant

thm Big_Operators.setprod_constant

thm Big_Operators.setsum_bounded

thm Big_Operators.card_UN_disjoint

thm Big_Operators.card_Union_disjoint

thm Finite_Set.card_image_le
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
 
thm Finite_Set.card_image
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

thm Finite_Set.eq_card_imp_inj_on
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

thm Finite_Set.inj_on_iff_eq_card
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)

thm Finite_Set.card_inj_on_le
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


thm Finite_Set.card_bij_eq
thm Finite_Set.card_bij_eq[no_vars]
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)

thm Big_Operators.card_SigmaI

thm Big_Operators.card_cartesian_product
lemma icard_cartesian_product: "icard (A × B) = icard A * icard B"
apply (case_tac "A = {} ∨ B = {}", fastsimp)
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

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

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



thm Finite_Set.card_Pow

thm Finite_Set.dvd_partition

thm Equiv_Relations.equiv_imp_dvd_card

thm Equiv_Relations.card_quotient_disjoint



thm
  SetInterval.card_lessThan
  SetInterval.card_atMost
  SetInterval.card_atLeastLessThan
  SetInterval.card_atLeastAtMost
  SetInterval.card_greaterThanAtMost
  SetInterval.card_greaterThanLessThan
lemma 
  icard_lessThan: "icard {..<u} = Fin u" and
  icard_atMost: "icard {..u} = Fin (Suc u)" and
  icard_atLeastLessThan: "icard {l..<u} = Fin (u - l)" and
  icard_atLeastAtMost: "icard {l..u} = Fin (Suc u - l)" and
  icard_greaterThanAtMost: "icard {l<..u} = Fin (u - l)" and
  icard_greaterThanLessThan: "icard {l<..<u} = Fin (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)



thm 
  SetInterval.card_atLeastZeroLessThan_int
  SetInterval.card_atLeastLessThan_int
  SetInterval.card_atLeastAtMost_int
  SetInterval.card_greaterThanAtMost_int
lemma 
  icard_atLeastZeroLessThan_int: "icard {0..<u} = Fin (nat u)" and
  icard_atLeastLessThan_int: "icard {l..<u} = Fin (nat (u - l))" and
  icard_atLeastAtMost_int: "icard {l..u} = Fin (nat (u - l + 1))" and
  icard_greaterThanAtMost_int: "icard {l<..u} = Fin (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