src/HOL/Library/Countable_Set.thy
 author haftmann Fri Mar 22 19:18:08 2019 +0000 (3 months ago) changeset 69946 494934c30f38 parent 69661 a03a63b81f44 child 70178 4900351361b0 permissions -rw-r--r--
improved code equations taken over from AFP
```     1 (*  Title:      HOL/Library/Countable_Set.thy
```
```     2     Author:     Johannes Hölzl
```
```     3     Author:     Andrei Popescu
```
```     4 *)
```
```     5
```
```     6 section \<open>Countable sets\<close>
```
```     7
```
```     8 theory Countable_Set
```
```     9 imports Countable Infinite_Set
```
```    10 begin
```
```    11
```
```    12 subsection \<open>Predicate for countable sets\<close>
```
```    13
```
```    14 definition countable :: "'a set \<Rightarrow> bool" where
```
```    15   "countable S \<longleftrightarrow> (\<exists>f::'a \<Rightarrow> nat. inj_on f S)"
```
```    16
```
```    17 lemma countableE:
```
```    18   assumes S: "countable S" obtains f :: "'a \<Rightarrow> nat" where "inj_on f S"
```
```    19   using S by (auto simp: countable_def)
```
```    20
```
```    21 lemma countableI: "inj_on (f::'a \<Rightarrow> nat) S \<Longrightarrow> countable S"
```
```    22   by (auto simp: countable_def)
```
```    23
```
```    24 lemma countableI': "inj_on (f::'a \<Rightarrow> 'b::countable) S \<Longrightarrow> countable S"
```
```    25   using comp_inj_on[of f S to_nat] by (auto intro: countableI)
```
```    26
```
```    27 lemma countableE_bij:
```
```    28   assumes S: "countable S" obtains f :: "nat \<Rightarrow> 'a" and C :: "nat set" where "bij_betw f C S"
```
```    29   using S by (blast elim: countableE dest: inj_on_imp_bij_betw bij_betw_inv)
```
```    30
```
```    31 lemma countableI_bij: "bij_betw f (C::nat set) S \<Longrightarrow> countable S"
```
```    32   by (blast intro: countableI bij_betw_inv_into bij_betw_imp_inj_on)
```
```    33
```
```    34 lemma countable_finite: "finite S \<Longrightarrow> countable S"
```
```    35   by (blast dest: finite_imp_inj_to_nat_seg countableI)
```
```    36
```
```    37 lemma countableI_bij1: "bij_betw f A B \<Longrightarrow> countable A \<Longrightarrow> countable B"
```
```    38   by (blast elim: countableE_bij intro: bij_betw_trans countableI_bij)
```
```    39
```
```    40 lemma countableI_bij2: "bij_betw f B A \<Longrightarrow> countable A \<Longrightarrow> countable B"
```
```    41   by (blast elim: countableE_bij intro: bij_betw_trans bij_betw_inv_into countableI_bij)
```
```    42
```
```    43 lemma countable_iff_bij[simp]: "bij_betw f A B \<Longrightarrow> countable A \<longleftrightarrow> countable B"
```
```    44   by (blast intro: countableI_bij1 countableI_bij2)
```
```    45
```
```    46 lemma countable_subset: "A \<subseteq> B \<Longrightarrow> countable B \<Longrightarrow> countable A"
```
```    47   by (auto simp: countable_def intro: subset_inj_on)
```
```    48
```
```    49 lemma countableI_type[intro, simp]: "countable (A:: 'a :: countable set)"
```
```    50   using countableI[of to_nat A] by auto
```
```    51
```
```    52 subsection \<open>Enumerate a countable set\<close>
```
```    53
```
```    54 lemma countableE_infinite:
```
```    55   assumes "countable S" "infinite S"
```
```    56   obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
```
```    57 proof -
```
```    58   obtain f :: "'a \<Rightarrow> nat" where "inj_on f S"
```
```    59     using \<open>countable S\<close> by (rule countableE)
```
```    60   then have "bij_betw f S (f`S)"
```
```    61     unfolding bij_betw_def by simp
```
```    62   moreover
```
```    63   from \<open>inj_on f S\<close> \<open>infinite S\<close> have inf_fS: "infinite (f`S)"
```
```    64     by (auto dest: finite_imageD)
```
```    65   then have "bij_betw (the_inv_into UNIV (enumerate (f`S))) (f`S) UNIV"
```
```    66     by (intro bij_betw_the_inv_into bij_enumerate)
```
```    67   ultimately have "bij_betw (the_inv_into UNIV (enumerate (f`S)) \<circ> f) S UNIV"
```
```    68     by (rule bij_betw_trans)
```
```    69   then show thesis ..
```
```    70 qed
```
```    71
```
```    72 lemma countable_infiniteE':
```
```    73   assumes "countable A" "infinite A"
```
```    74   obtains g where "bij_betw g (UNIV :: nat set) A"
```
```    75   using bij_betw_inv[OF countableE_infinite[OF assms]] that by blast
```
```    76
```
```    77 lemma countable_enum_cases:
```
```    78   assumes "countable S"
```
```    79   obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}"
```
```    80         | (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV"
```
```    81   using ex_bij_betw_finite_nat[of S] countableE_infinite \<open>countable S\<close>
```
```    82   by (cases "finite S") (auto simp add: atLeast0LessThan)
```
```    83
```
```    84 definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where
```
```    85   "to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)"
```
```    86
```
```    87 definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
```
```    88   "from_nat_into S n = (if n \<in> to_nat_on S ` S then inv_into S (to_nat_on S) n else SOME s. s\<in>S)"
```
```    89
```
```    90 lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}"
```
```    91   using ex_bij_betw_finite_nat unfolding to_nat_on_def
```
```    92   by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan)
```
```    93
```
```    94 lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV"
```
```    95   using countableE_infinite unfolding to_nat_on_def
```
```    96   by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto
```
```    97
```
```    98 lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S"
```
```    99   unfolding from_nat_into_def[abs_def]
```
```   100   using to_nat_on_finite[of S]
```
```   101   apply (subst bij_betw_cong)
```
```   102   apply (split if_split)
```
```   103   apply (simp add: bij_betw_def)
```
```   104   apply (auto cong: bij_betw_cong
```
```   105               intro: bij_betw_inv_into to_nat_on_finite)
```
```   106   done
```
```   107
```
```   108 lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S"
```
```   109   unfolding from_nat_into_def[abs_def]
```
```   110   using to_nat_on_infinite[of S, unfolded bij_betw_def]
```
```   111   by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite)
```
```   112
```
```   113 lemma countable_as_injective_image:
```
```   114   assumes "countable A" "infinite A"
```
```   115   obtains f :: "nat \<Rightarrow> 'a" where "A = range f" "inj f"
```
```   116 by (metis bij_betw_def bij_betw_from_nat_into [OF assms])
```
```   117
```
```   118 lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A"
```
```   119   using to_nat_on_infinite[of A] to_nat_on_finite[of A]
```
```   120   by (cases "finite A") (auto simp: bij_betw_def)
```
```   121
```
```   122 lemma to_nat_on_inj[simp]:
```
```   123   "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b"
```
```   124   using inj_on_to_nat_on[of A] by (auto dest: inj_onD)
```
```   125
```
```   126 lemma from_nat_into_to_nat_on[simp]: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> from_nat_into A (to_nat_on A a) = a"
```
```   127   by (auto simp: from_nat_into_def intro!: inv_into_f_f)
```
```   128
```
```   129 lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)"
```
```   130   by (auto intro: from_nat_into_to_nat_on[symmetric])
```
```   131
```
```   132 lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A"
```
```   133   unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex)
```
```   134
```
```   135 lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A"
```
```   136   using from_nat_into[of A] by auto
```
```   137
```
```   138 lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A"
```
```   139   by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into)
```
```   140
```
```   141 lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV"
```
```   142   using to_nat_on_infinite[of A] by (simp add: bij_betw_def)
```
```   143
```
```   144 lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n"
```
```   145   by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on)
```
```   146
```
```   147 lemma to_nat_on_from_nat_into[simp]: "n \<in> to_nat_on A ` A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
```
```   148   by (simp add: f_inv_into_f from_nat_into_def)
```
```   149
```
```   150 lemma to_nat_on_from_nat_into_infinite[simp]:
```
```   151   "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n"
```
```   152   by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into)
```
```   153
```
```   154 lemma from_nat_into_inj:
```
```   155   "countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow>
```
```   156     from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
```
```   157   by (subst to_nat_on_inj[symmetric, of A]) auto
```
```   158
```
```   159 lemma from_nat_into_inj_infinite[simp]:
```
```   160   "countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n"
```
```   161   using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp
```
```   162
```
```   163 lemma eq_from_nat_into_iff:
```
```   164   "countable A \<Longrightarrow> x \<in> A \<Longrightarrow> i \<in> to_nat_on A ` A \<Longrightarrow> x = from_nat_into A i \<longleftrightarrow> i = to_nat_on A x"
```
```   165   by auto
```
```   166
```
```   167 lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a"
```
```   168   by (rule exI[of _ "to_nat_on A a"]) simp
```
```   169
```
```   170 lemma from_nat_into_inject[simp]:
```
```   171   "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B"
```
```   172   by (metis range_from_nat_into)
```
```   173
```
```   174 lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})"
```
```   175   unfolding inj_on_def by auto
```
```   176
```
```   177 subsection \<open>Closure properties of countability\<close>
```
```   178
```
```   179 lemma countable_SIGMA[intro, simp]:
```
```   180   "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
```
```   181   by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
```
```   182
```
```   183 lemma countable_image[intro, simp]:
```
```   184   assumes "countable A"
```
```   185   shows "countable (f`A)"
```
```   186 proof -
```
```   187   obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
```
```   188     using assms by (rule countableE)
```
```   189   moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
```
```   190     by (auto intro: inj_on_inv_into inv_into_into)
```
```   191   ultimately show ?thesis
```
```   192     by (blast dest: comp_inj_on subset_inj_on intro: countableI)
```
```   193 qed
```
```   194
```
```   195 lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A"
```
```   196   by (metis countable_image the_inv_into_onto)
```
```   197
```
```   198 lemma countable_UN[intro, simp]:
```
```   199   fixes I :: "'i set" and A :: "'i => 'a set"
```
```   200   assumes I: "countable I"
```
```   201   assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)"
```
```   202   shows "countable (\<Union>i\<in>I. A i)"
```
```   203 proof -
```
```   204   have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff)
```
```   205   then show ?thesis by (simp add: assms)
```
```   206 qed
```
```   207
```
```   208 lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)"
```
```   209   by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A | False \<Rightarrow> B", simplified])
```
```   210      (simp split: bool.split)
```
```   211
```
```   212 lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
```
```   213   by (metis countable_Un countable_subset inf_sup_ord(3,4))
```
```   214
```
```   215 lemma countable_Plus[intro, simp]:
```
```   216   "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)"
```
```   217   by (simp add: Plus_def)
```
```   218
```
```   219 lemma countable_empty[intro, simp]: "countable {}"
```
```   220   by (blast intro: countable_finite)
```
```   221
```
```   222 lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)"
```
```   223   using countable_Un[of "{a}" A] by (auto simp: countable_finite)
```
```   224
```
```   225 lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)"
```
```   226   by (force intro: countable_subset)
```
```   227
```
```   228 lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)"
```
```   229   by (blast intro: countable_subset)
```
```   230
```
```   231 lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)"
```
```   232   by (blast intro: countable_subset)
```
```   233
```
```   234 lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A - B)"
```
```   235   by (blast intro: countable_subset)
```
```   236
```
```   237 lemma countable_insert_eq [simp]: "countable (insert x A) = countable A"
```
```   238     by auto (metis Diff_insert_absorb countable_Diff insert_absorb)
```
```   239
```
```   240 lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
```
```   241   by (metis Int_absorb2 countable_image image_vimage_eq)
```
```   242
```
```   243 lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f -` B) \<Longrightarrow> countable B"
```
```   244   by (metis countable_vimage top_greatest)
```
```   245
```
```   246 lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}"
```
```   247   by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1)
```
```   248
```
```   249 lemma countable_Image:
```
```   250   assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})"
```
```   251   assumes "countable Y"
```
```   252   shows "countable (X `` Y)"
```
```   253 proof -
```
```   254   have "countable (X `` (\<Union>y\<in>Y. {y}))"
```
```   255     unfolding Image_UN by (intro countable_UN assms)
```
```   256   then show ?thesis by simp
```
```   257 qed
```
```   258
```
```   259 lemma countable_relpow:
```
```   260   fixes X :: "'a rel"
```
```   261   assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)"
```
```   262   assumes Y: "countable Y"
```
```   263   shows "countable ((X ^^ i) `` Y)"
```
```   264   using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X)
```
```   265
```
```   266 lemma countable_funpow:
```
```   267   fixes f :: "'a set \<Rightarrow> 'a set"
```
```   268   assumes "\<And>A. countable A \<Longrightarrow> countable (f A)"
```
```   269   and "countable A"
```
```   270   shows "countable ((f ^^ n) A)"
```
```   271 by(induction n)(simp_all add: assms)
```
```   272
```
```   273 lemma countable_rtrancl:
```
```   274   "(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X\<^sup>* `` Y)"
```
```   275   unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow)
```
```   276
```
```   277 lemma countable_lists[intro, simp]:
```
```   278   assumes A: "countable A" shows "countable (lists A)"
```
```   279 proof -
```
```   280   have "countable (lists (range (from_nat_into A)))"
```
```   281     by (auto simp: lists_image)
```
```   282   with A show ?thesis
```
```   283     by (auto dest: subset_range_from_nat_into countable_subset lists_mono)
```
```   284 qed
```
```   285
```
```   286 lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV"
```
```   287   using finite_list by auto
```
```   288
```
```   289 lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))"
```
```   290   by (simp add: Collect_finite_eq_lists)
```
```   291
```
```   292 lemma countable_int: "countable \<int>"
```
```   293   unfolding Ints_def by auto
```
```   294
```
```   295 lemma countable_rat: "countable \<rat>"
```
```   296   unfolding Rats_def by auto
```
```   297
```
```   298 lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T"
```
```   299   using finite_list by (auto simp: lists_eq_set)
```
```   300
```
```   301 lemma countable_Collect_finite_subset:
```
```   302   "countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}"
```
```   303   unfolding Collect_finite_subset_eq_lists by auto
```
```   304
```
```   305 lemma countable_set_option [simp]: "countable (set_option x)"
```
```   306 by(cases x) auto
```
```   307
```
```   308 subsection \<open>Misc lemmas\<close>
```
```   309
```
```   310 lemma countable_subset_image:
```
```   311    "countable B \<and> B \<subseteq> (f ` A) \<longleftrightarrow> (\<exists>A'. countable A' \<and> A' \<subseteq> A \<and> (B = f ` A'))"
```
```   312    (is "?lhs = ?rhs")
```
```   313 proof
```
```   314   assume ?lhs
```
```   315   show ?rhs
```
```   316     by (rule exI [where x="inv_into A f ` B"])
```
```   317       (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>)
```
```   318 next
```
```   319   assume ?rhs
```
```   320   then show ?lhs by force
```
```   321 qed
```
```   322
```
```   323 lemma infinite_countable_subset':
```
```   324   assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
```
```   325 proof -
```
```   326   from infinite_countable_subset[OF X] guess f ..
```
```   327   then show ?thesis
```
```   328     by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite)
```
```   329 qed
```
```   330
```
```   331 lemma countable_all:
```
```   332   assumes S: "countable S"
```
```   333   shows "(\<forall>s\<in>S. P s) \<longleftrightarrow> (\<forall>n::nat. from_nat_into S n \<in> S \<longrightarrow> P (from_nat_into S n))"
```
```   334   using S[THEN subset_range_from_nat_into] by auto
```
```   335
```
```   336 lemma finite_sequence_to_countable_set:
```
```   337   assumes "countable X"
```
```   338   obtains F where "\<And>i. F i \<subseteq> X" "\<And>i. F i \<subseteq> F (Suc i)" "\<And>i. finite (F i)" "(\<Union>i. F i) = X"
```
```   339 proof -
```
```   340   show thesis
```
```   341     apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"])
```
```   342        apply (auto simp add: image_iff intro: from_nat_into split: if_splits)
```
```   343     using assms from_nat_into_surj by (fastforce cong: image_cong)
```
```   344 qed
```
```   345
```
```   346 lemma transfer_countable[transfer_rule]:
```
```   347   "bi_unique R \<Longrightarrow> rel_fun (rel_set R) (=) countable countable"
```
```   348   by (rule rel_funI, erule (1) bi_unique_rel_set_lemma)
```
```   349      (auto dest: countable_image_inj_on)
```
```   350
```
```   351 subsection \<open>Uncountable\<close>
```
```   352
```
```   353 abbreviation uncountable where
```
```   354   "uncountable A \<equiv> \<not> countable A"
```
```   355
```
```   356 lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)"
```
```   357   by (auto intro: inj_on_inv_into simp: countable_def)
```
```   358      (metis all_not_in_conv inj_on_iff_surj subset_UNIV)
```
```   359
```
```   360 lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A"
```
```   361   unfolding bij_betw_def by (metis countable_image)
```
```   362
```
```   363 lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A"
```
```   364   by (metis countable_finite)
```
```   365
```
```   366 lemma uncountable_minus_countable:
```
```   367   "uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A - B)"
```
```   368   using countable_Un[of B "A - B"] by auto
```
```   369
```
```   370 lemma countable_Diff_eq [simp]: "countable (A - {x}) = countable A"
```
```   371   by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable)
```
```   372
```
```   373 end
```