hoelzl@50134: (* Title: HOL/Library/Countable_Set.thy hoelzl@50134: Author: Johannes Hölzl hoelzl@50134: Author: Andrei Popescu hoelzl@50134: *) hoelzl@50134: hoelzl@50134: header {* Countable sets *} hoelzl@50134: hoelzl@50134: theory Countable_Set hoelzl@50134: imports "~~/src/HOL/Library/Countable" "~~/src/HOL/Library/Infinite_Set" hoelzl@50134: begin hoelzl@50134: hoelzl@50134: subsection {* Predicate for countable sets *} hoelzl@50134: hoelzl@50134: definition countable :: "'a set \ bool" where hoelzl@50134: "countable S \ (\f::'a \ nat. inj_on f S)" hoelzl@50134: hoelzl@50134: lemma countableE: hoelzl@50134: assumes S: "countable S" obtains f :: "'a \ nat" where "inj_on f S" hoelzl@50134: using S by (auto simp: countable_def) hoelzl@50134: hoelzl@50134: lemma countableI: "inj_on (f::'a \ nat) S \ countable S" hoelzl@50134: by (auto simp: countable_def) hoelzl@50134: hoelzl@50134: lemma countableI': "inj_on (f::'a \ 'b::countable) S \ countable S" hoelzl@50134: using comp_inj_on[of f S to_nat] by (auto intro: countableI) hoelzl@50134: hoelzl@50134: lemma countableE_bij: hoelzl@50134: assumes S: "countable S" obtains f :: "nat \ 'a" and C :: "nat set" where "bij_betw f C S" hoelzl@50134: using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv) hoelzl@50134: hoelzl@50134: lemma countableI_bij: "bij_betw f (C::nat set) S \ countable S" hoelzl@50134: by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on) hoelzl@50134: hoelzl@50134: lemma countable_finite: "finite S \ countable S" hoelzl@50134: by (blast dest: finite_imp_inj_to_nat_seg countableI) hoelzl@50134: hoelzl@50134: lemma countableI_bij1: "bij_betw f A B \ countable A \ countable B" hoelzl@50134: by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij) hoelzl@50134: hoelzl@50134: lemma countableI_bij2: "bij_betw f B A \ countable A \ countable B" hoelzl@50134: by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij) hoelzl@50134: hoelzl@50134: lemma countable_iff_bij[simp]: "bij_betw f A B \ countable A \ countable B" hoelzl@50134: by (blast intro: countableI_bij1 countableI_bij2) hoelzl@50134: hoelzl@50134: lemma countable_subset: "A \ B \ countable B \ countable A" hoelzl@50134: by (auto simp: countable_def intro: subset_inj_on) hoelzl@50134: hoelzl@50134: lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)" hoelzl@50134: using countableI[of to_nat A] by auto hoelzl@50134: hoelzl@50134: subsection {* Enumerate a countable set *} hoelzl@50134: hoelzl@50134: lemma countableE_infinite: hoelzl@50134: assumes "countable S" "infinite S" hoelzl@50134: obtains e :: "'a \ nat" where "bij_betw e S UNIV" hoelzl@50134: proof - hoelzl@50134: from `countable S`[THEN countableE] guess f . hoelzl@50134: then have "bij_betw f S (f`S)" hoelzl@50134: unfolding bij_betw_def by simp hoelzl@50134: moreover hoelzl@50134: from `inj_on f S` `infinite S` have inf_fS: "infinite (f`S)" hoelzl@50134: by (auto dest: finite_imageD) hoelzl@50134: then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV" hoelzl@50134: by (intro bij_betw_the_inv_into bij_enumerate) hoelzl@50134: ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \ f) S UNIV" hoelzl@50134: by (rule bij_betw_trans) hoelzl@50134: then show thesis .. hoelzl@50134: qed hoelzl@50134: hoelzl@50134: lemma countable_enum_cases: hoelzl@50134: assumes "countable S" hoelzl@50134: obtains (finite) f :: "'a \ nat" where "finite S" "bij_betw f S {.. nat" where "infinite S" "bij_betw f S UNIV" hoelzl@50134: using ex_bij_betw_finite_nat[of S] countableE_infinite `countable S` hoelzl@50134: by (cases "finite S") (auto simp add: atLeast0LessThan) hoelzl@50134: hoelzl@50134: definition to_nat_on :: "'a set \ 'a \ nat" where hoelzl@50134: "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)" hoelzl@50134: hoelzl@50134: definition from_nat_into :: "'a set \ nat \ 'a" where hoelzl@50144: "from_nat_into S n = (if n \ to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\S)" hoelzl@50134: hoelzl@50134: lemma to_nat_on_finite: "finite S \ bij_betw (to_nat_on S) S {..< card S}" hoelzl@50134: using ex_bij_betw_finite_nat unfolding to_nat_on_def hoelzl@50134: by (intro someI2_ex[where Q="\f. bij_betw f S {.. infinite S \ bij_betw (to_nat_on S) S UNIV" hoelzl@50134: using countableE_infinite unfolding to_nat_on_def hoelzl@50134: by (intro someI2_ex[where Q="\f. bij_betw f S UNIV"]) auto hoelzl@50134: hoelzl@50148: lemma bij_betw_from_nat_into_finite: "finite S \ bij_betw (from_nat_into S) {..< card S} S" hoelzl@50144: unfolding from_nat_into_def[abs_def] hoelzl@50144: using to_nat_on_finite[of S] hoelzl@50144: apply (subst bij_betw_cong) hoelzl@50144: apply (split split_if) hoelzl@50144: apply (simp add: bij_betw_def) hoelzl@50144: apply (auto cong: bij_betw_cong hoelzl@50144: intro: bij_betw_inv_into to_nat_on_finite) hoelzl@50144: done hoelzl@50134: hoelzl@50148: lemma bij_betw_from_nat_into: "countable S \ infinite S \ bij_betw (from_nat_into S) UNIV S" hoelzl@50144: unfolding from_nat_into_def[abs_def] hoelzl@50144: using to_nat_on_infinite[of S, unfolded bij_betw_def] hoelzl@50144: by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) hoelzl@50134: hoelzl@50134: lemma inj_on_to_nat_on[intro]: "countable A \ inj_on (to_nat_on A) A" hoelzl@50134: using to_nat_on_infinite[of A] to_nat_on_finite[of A] hoelzl@50134: by (cases "finite A") (auto simp: bij_betw_def) hoelzl@50134: hoelzl@50134: lemma to_nat_on_inj[simp]: hoelzl@50134: "countable A \ a \ A \ b \ A \ to_nat_on A a = to_nat_on A b \ a = b" hoelzl@50134: using inj_on_to_nat_on[of A] by (auto dest: inj_onD) hoelzl@50134: hoelzl@50144: lemma from_nat_into_to_nat_on[simp]: "countable A \ a \ A \ from_nat_into A (to_nat_on A a) = a" hoelzl@50134: by (auto simp: from_nat_into_def intro!: inv_into_f_f) hoelzl@50134: hoelzl@50134: lemma subset_range_from_nat_into: "countable A \ A \ range (from_nat_into A)" hoelzl@50134: by (auto intro: from_nat_into_to_nat_on[symmetric]) hoelzl@50134: hoelzl@50144: lemma from_nat_into: "A \ {} \ from_nat_into A n \ A" hoelzl@50144: unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex) hoelzl@50144: hoelzl@50144: lemma range_from_nat_into_subset: "A \ {} \ range (from_nat_into A) \ A" hoelzl@50144: using from_nat_into[of A] by auto hoelzl@50144: hoelzl@50148: lemma range_from_nat_into[simp]: "A \ {} \ countable A \ range (from_nat_into A) = A" hoelzl@50144: by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into) hoelzl@50144: hoelzl@50144: lemma image_to_nat_on: "countable A \ infinite A \ to_nat_on A ` A = UNIV" hoelzl@50144: using to_nat_on_infinite[of A] by (simp add: bij_betw_def) hoelzl@50144: hoelzl@50144: lemma to_nat_on_surj: "countable A \ infinite A \ \a\A. to_nat_on A a = n" hoelzl@50144: by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on) hoelzl@50144: hoelzl@50144: lemma to_nat_on_from_nat_into[simp]: "n \ to_nat_on A ` A \ to_nat_on A (from_nat_into A n) = n" hoelzl@50144: by (simp add: f_inv_into_f from_nat_into_def) hoelzl@50144: hoelzl@50148: lemma to_nat_on_from_nat_into_infinite[simp]: hoelzl@50144: "countable A \ infinite A \ to_nat_on A (from_nat_into A n) = n" hoelzl@50144: by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into) hoelzl@50144: hoelzl@50144: lemma from_nat_into_inj: hoelzl@50148: "countable A \ m \ to_nat_on A ` A \ n \ to_nat_on A ` A \ hoelzl@50148: from_nat_into A m = from_nat_into A n \ m = n" hoelzl@50148: by (subst to_nat_on_inj[symmetric, of A]) auto hoelzl@50148: hoelzl@50148: lemma from_nat_into_inj_infinite[simp]: hoelzl@50148: "countable A \ infinite A \ from_nat_into A m = from_nat_into A n \ m = n" hoelzl@50148: using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp hoelzl@50148: hoelzl@50148: lemma eq_from_nat_into_iff: hoelzl@50148: "countable A \ x \ A \ i \ to_nat_on A ` A \ x = from_nat_into A i \ i = to_nat_on A x" hoelzl@50148: by auto hoelzl@50144: hoelzl@50144: lemma from_nat_into_surj: "countable A \ a \ A \ \n. from_nat_into A n = a" hoelzl@50144: by (rule exI[of _ "to_nat_on A a"]) simp hoelzl@50144: hoelzl@50144: lemma from_nat_into_inject[simp]: hoelzl@50148: "A \ {} \ countable A \ B \ {} \ countable B \ from_nat_into A = from_nat_into B \ A = B" hoelzl@50148: by (metis range_from_nat_into) hoelzl@50144: hoelzl@50148: lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \ {} \ countable A})" hoelzl@50148: unfolding inj_on_def by auto hoelzl@50144: hoelzl@50134: subsection {* Closure properties of countability *} hoelzl@50134: hoelzl@50134: lemma countable_SIGMA[intro, simp]: hoelzl@50134: "countable I \ (\i. i \ I \ countable (A i)) \ countable (SIGMA i : I. A i)" hoelzl@50134: by (intro countableI'[of "\(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def) hoelzl@50134: hoelzl@50134: lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)" hoelzl@50134: proof - hoelzl@50134: from A guess g by (rule countableE) hoelzl@50134: moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \ A" hoelzl@50134: by (auto intro: inj_on_inv_into inv_into_into) hoelzl@50134: ultimately show ?thesis hoelzl@50134: by (blast dest: comp_inj_on subset_inj_on intro: countableI) hoelzl@50134: qed hoelzl@50134: hoelzl@50134: lemma countable_UN[intro, simp]: hoelzl@50134: fixes I :: "'i set" and A :: "'i => 'a set" hoelzl@50134: assumes I: "countable I" hoelzl@50134: assumes A: "\i. i \ I \ countable (A i)" hoelzl@50134: shows "countable (\i\I. A i)" hoelzl@50134: proof - hoelzl@50134: have "(\i\I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff) hoelzl@50134: then show ?thesis by (simp add: assms) hoelzl@50134: qed hoelzl@50134: hoelzl@50134: lemma countable_Un[intro]: "countable A \ countable B \ countable (A \ B)" hoelzl@50134: by (rule countable_UN[of "{True, False}" "\True \ A | False \ B", simplified]) hoelzl@50134: (simp split: bool.split) hoelzl@50134: hoelzl@50134: lemma countable_Un_iff[simp]: "countable (A \ B) \ countable A \ countable B" hoelzl@50134: by (metis countable_Un countable_subset inf_sup_ord(3,4)) hoelzl@50134: hoelzl@50134: lemma countable_Plus[intro, simp]: hoelzl@50134: "countable A \ countable B \ countable (A <+> B)" hoelzl@50134: by (simp add: Plus_def) hoelzl@50134: hoelzl@50134: lemma countable_empty[intro, simp]: "countable {}" hoelzl@50134: by (blast intro: countable_finite) hoelzl@50134: hoelzl@50134: lemma countable_insert[intro, simp]: "countable A \ countable (insert a A)" hoelzl@50134: using countable_Un[of "{a}" A] by (auto simp: countable_finite) hoelzl@50134: hoelzl@50134: lemma countable_Int1[intro, simp]: "countable A \ countable (A \ B)" hoelzl@50134: by (force intro: countable_subset) hoelzl@50134: hoelzl@50134: lemma countable_Int2[intro, simp]: "countable B \ countable (A \ B)" hoelzl@50134: by (blast intro: countable_subset) hoelzl@50134: hoelzl@50134: lemma countable_INT[intro, simp]: "i \ I \ countable (A i) \ countable (\i\I. A i)" hoelzl@50134: by (blast intro: countable_subset) hoelzl@50134: hoelzl@50134: lemma countable_Diff[intro, simp]: "countable A \ countable (A - B)" hoelzl@50134: by (blast intro: countable_subset) hoelzl@50134: hoelzl@50134: lemma countable_vimage: "B \ range f \ countable (f -` B) \ countable B" hoelzl@50134: by (metis Int_absorb2 assms countable_image image_vimage_eq) hoelzl@50134: hoelzl@50134: lemma surj_countable_vimage: "surj f \ countable (f -` B) \ countable B" hoelzl@50134: by (metis countable_vimage top_greatest) hoelzl@50134: hoelzl@50144: lemma countable_Collect[simp]: "countable A \ countable {a \ A. \ a}" hoelzl@50144: by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1) hoelzl@50144: hoelzl@50134: lemma countable_lists[intro, simp]: hoelzl@50134: assumes A: "countable A" shows "countable (lists A)" hoelzl@50134: proof - hoelzl@50134: have "countable (lists (range (from_nat_into A)))" hoelzl@50134: by (auto simp: lists_image) hoelzl@50134: with A show ?thesis hoelzl@50134: by (auto dest: subset_range_from_nat_into countable_subset lists_mono) hoelzl@50134: qed hoelzl@50134: immler@50245: lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV" immler@50245: using finite_list by auto immler@50245: immler@50245: lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\bool))" immler@50245: by (simp add: Collect_finite_eq_lists) immler@50245: hoelzl@50134: subsection {* Misc lemmas *} hoelzl@50134: hoelzl@50134: lemma countable_all: hoelzl@50134: assumes S: "countable S" hoelzl@50134: shows "(\s\S. P s) \ (\n::nat. from_nat_into S n \ S \ P (from_nat_into S n))" hoelzl@50134: using S[THEN subset_range_from_nat_into] by auto hoelzl@50134: hoelzl@50134: end