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