Theory Countable

section ‹Countable Sets›

theory Countable
  imports Nats Axiom_Of_Choice Nat_Parity Cardinality
begin

text ‹The definition below corresponds to Definition 2.6.9 in Halvorson.›
definition epi_countable :: "cset ⇒ bool" where
  "epi_countable X ⟷ (∃ f. f : ℕ⇩c → X ∧ epimorphism f)"

lemma emptyset_is_not_epi_countable:
  "¬ epi_countable ∅"
  using comp_type emptyset_is_empty epi_countable_def zero_type by blast

text ‹The fact that the empty set is not countable according to the definition from Halvorson
  (@{thm epi_countable_def}) motivated the following definition.›
definition countable :: "cset ⇒ bool" where
  "countable X ⟷ (∃ f. f : X → ℕ⇩c ∧ monomorphism f)"

lemma epi_countable_is_countable: 
  assumes "epi_countable X"
  shows "countable X"
  using assms countable_def epi_countable_def epis_give_monos by blast

lemma emptyset_is_countable:
  "countable ∅"
  using countable_def empty_subset subobject_of_def2 by blast

lemma natural_numbers_are_countably_infinite:
  "countable ℕ⇩c ∧ is_infinite ℕ⇩c"
  by (meson CollectI Peano's_Axioms countable_def injective_imp_monomorphism is_infinite_def successor_type)

lemma iso_to_N_is_countably_infinite:
  assumes "X ≅ ℕ⇩c"
  shows "countable X ∧ is_infinite X"
  by (meson assms countable_def is_isomorphic_def is_smaller_than_def iso_imp_epi_and_monic isomorphic_is_symmetric larger_than_infinite_is_infinite natural_numbers_are_countably_infinite)

lemma smaller_than_countable_is_countable:
  assumes "X ≤⇩c Y" "countable Y"
  shows "countable X"
  by (smt assms cfunc_type_def comp_type composition_of_monic_pair_is_monic countable_def is_smaller_than_def)

lemma iso_pres_countable:
  assumes "X ≅ Y" "countable Y"
  shows "countable X"
  using assms is_isomorphic_def is_smaller_than_def iso_imp_epi_and_monic smaller_than_countable_is_countable by blast

lemma NuN_is_countable:
  "countable(ℕ⇩c ∐ ℕ⇩c)"
  using countable_def epis_give_monos halve_with_parity_iso halve_with_parity_type iso_imp_epi_and_monic by smt

text ‹The lemma below corresponds to Exercise 2.6.11 in Halvorson.›
lemma coproduct_of_countables_is_countable:
  assumes "countable X" "countable Y"
  shows "countable(X ∐ Y)"
  unfolding countable_def
proof-
  obtain x where x_def:  "x : X  → ℕ⇩c ∧ monomorphism x"
    using assms(1) countable_def by blast
  obtain y where y_def:  "y : Y  → ℕ⇩c ∧ monomorphism y"
    using assms(2) countable_def by blast
  obtain n where n_def: " n : ℕ⇩c ∐ ℕ⇩c → ℕ⇩c ∧ monomorphism n"
    using NuN_is_countable countable_def by blast
  have xy_type: "x ⨝⇩f y : X ∐ Y → ℕ⇩c ∐ ℕ⇩c"
    using x_def y_def by (typecheck_cfuncs, auto)
  then have nxy_type: "n ∘⇩c (x ⨝⇩f y) : X ∐ Y → ℕ⇩c"
    using comp_type n_def by blast
  have "injective(x ⨝⇩f y)"
    using cfunc_bowtieprod_inj monomorphism_imp_injective x_def y_def by blast
  then have "monomorphism(x ⨝⇩f y)"
    using injective_imp_monomorphism by auto
  then have "monomorphism(n ∘⇩c (x ⨝⇩f y))"
    using cfunc_type_def composition_of_monic_pair_is_monic n_def xy_type by auto
  then show "∃f. f : X ∐ Y → ℕ⇩c ∧ monomorphism f"
    using nxy_type by blast
qed

end