src/HOL/Codatatype/Countable_Set.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 49314 f252c7c2ac7b
child 49440 4ff2976f4056
permissions -rw-r--r--
tuned simpset
     1 (*  Title:      HOL/Codatatype/Countable_Set.thy
     2     Author:     Andrei Popescu, TU Muenchen
     3     Copyright   2012
     4 
     5 (At most) countable sets.
     6 *)
     7 
     8 header {* (At Most) Countable Sets *}
     9 
    10 theory Countable_Set
    11 imports "../Cardinals/Cardinal_Arithmetic" "~~/src/HOL/Library/Countable"
    12 begin
    13 
    14 
    15 subsection{* Basics  *}
    16 
    17 definition "countable A \<equiv> |A| \<le>o natLeq"
    18 
    19 lemma countable_card_of_nat:
    20 "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|"
    21 unfolding countable_def using card_of_nat
    22 using ordLeq_ordIso_trans ordIso_symmetric by blast
    23 
    24 lemma countable_ex_to_nat:
    25 fixes A :: "'a set"
    26 shows "countable A \<longleftrightarrow> (\<exists> f::'a\<Rightarrow>nat. inj_on f A)"
    27 unfolding countable_card_of_nat card_of_ordLeq[symmetric] by auto
    28 
    29 lemma countable_or_card_of:
    30 assumes "countable A"
    31 shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or>
    32        (infinite A  \<and> |A| =o |UNIV::nat set| )"
    33 apply (cases "finite A")
    34   apply(metis finite_iff_cardOf_nat)
    35   by (metis assms countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq)
    36 
    37 lemma countable_or:
    38 assumes "countable A"
    39 shows "(\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or>
    40        (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)"
    41 using countable_or_card_of[OF assms]
    42 by (metis assms card_of_ordIso countable_ex_to_nat)
    43 
    44 lemma countable_cases_card_of[elim, consumes 1, case_names Fin Inf]:
    45 assumes "countable A"
    46 and "\<lbrakk>finite A; |A| <o |UNIV::nat set|\<rbrakk> \<Longrightarrow> phi"
    47 and "\<lbrakk>infinite A; |A| =o |UNIV::nat set|\<rbrakk> \<Longrightarrow> phi"
    48 shows phi
    49 using assms countable_or_card_of by blast
    50 
    51 lemma countable_cases[elim, consumes 1, case_names Fin Inf]:
    52 assumes "countable A"
    53 and "\<And> f::'a\<Rightarrow>nat. \<lbrakk>finite A; inj_on f A\<rbrakk> \<Longrightarrow> phi"
    54 and "\<And> f::'a\<Rightarrow>nat. \<lbrakk>infinite A; bij_betw f A UNIV\<rbrakk> \<Longrightarrow> phi"
    55 shows phi
    56 using assms countable_or by metis
    57 
    58 definition toNat_pred :: "'a set \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> bool"
    59 where
    60 "toNat_pred (A::'a set) f \<equiv>
    61  (finite A \<and> inj_on f A) \<or> (infinite A \<and> bij_betw f A UNIV)"
    62 definition toNat where "toNat A \<equiv> SOME f. toNat_pred A f"
    63 
    64 lemma toNat_pred:
    65 assumes "countable A"
    66 shows "\<exists> f. toNat_pred A f"
    67 using assms countable_ex_to_nat toNat_pred_def by (cases rule: countable_cases) auto
    68 
    69 lemma toNat_pred_toNat:
    70 assumes "countable A"
    71 shows "toNat_pred A (toNat A)"
    72 unfolding toNat_def apply(rule someI_ex[of "toNat_pred A"])
    73 using toNat_pred[OF assms] .
    74 
    75 lemma bij_betw_toNat:
    76 assumes c: "countable A" and i: "infinite A"
    77 shows "bij_betw (toNat A) A (UNIV::nat set)"
    78 using toNat_pred_toNat[OF c] unfolding toNat_pred_def using i by auto
    79 
    80 lemma inj_on_toNat:
    81 assumes c: "countable A"
    82 shows "inj_on (toNat A) A"
    83 using c apply(cases rule: countable_cases)
    84 using bij_betw_toNat[OF c] toNat_pred_toNat[OF c]
    85 unfolding toNat_pred_def unfolding bij_betw_def by auto
    86 
    87 lemma toNat_inj[simp]:
    88 assumes c: "countable A" and a: "a \<in> A" and b: "b \<in> A"
    89 shows "toNat A a = toNat A b \<longleftrightarrow> a = b"
    90 using inj_on_toNat[OF c] using a b unfolding inj_on_def by auto
    91 
    92 lemma image_toNat:
    93 assumes c: "countable A" and i: "infinite A"
    94 shows "toNat A ` A = UNIV"
    95 using bij_betw_toNat[OF assms] unfolding bij_betw_def by simp
    96 
    97 lemma toNat_surj:
    98 assumes "countable A" and i: "infinite A"
    99 shows "\<exists> a. a \<in> A \<and> toNat A a = n"
   100 using image_toNat[OF assms]
   101 by (metis (no_types) image_iff iso_tuple_UNIV_I)
   102 
   103 definition
   104 "fromNat A n \<equiv>
   105  if n \<in> toNat A ` A then inv_into A (toNat A) n
   106  else (SOME a. a \<in> A)"
   107 
   108 lemma fromNat:
   109 assumes "A \<noteq> {}"
   110 shows "fromNat A n \<in> A"
   111 unfolding fromNat_def by (metis assms equals0I inv_into_into someI_ex)
   112 
   113 lemma toNat_fromNat[simp]:
   114 assumes "n \<in> toNat A ` A"
   115 shows "toNat A (fromNat A n) = n"
   116 by (metis assms f_inv_into_f fromNat_def)
   117 
   118 lemma infinite_toNat_fromNat[simp]:
   119 assumes c: "countable A" and i: "infinite A"
   120 shows "toNat A (fromNat A n) = n"
   121 apply(rule toNat_fromNat) using toNat_surj[OF assms]
   122 by (metis image_iff)
   123 
   124 lemma fromNat_toNat[simp]:
   125 assumes c: "countable A" and a: "a \<in> A"
   126 shows "fromNat A (toNat A a) = a"
   127 by (metis a c equals0D fromNat imageI toNat_fromNat toNat_inj)
   128 
   129 lemma fromNat_inj:
   130 assumes c: "countable A" and i: "infinite A"
   131 shows "fromNat A m = fromNat A n \<longleftrightarrow> m = n" (is "?L = ?R \<longleftrightarrow> ?K")
   132 proof-
   133   have "?L = ?R \<longleftrightarrow> toNat A ?L = toNat A ?R"
   134   unfolding toNat_inj[OF c fromNat[OF infinite_imp_nonempty[OF i]]
   135                            fromNat[OF infinite_imp_nonempty[OF i]]] ..
   136   also have "... \<longleftrightarrow> ?K" using c i by simp
   137   finally show ?thesis .
   138 qed
   139 
   140 lemma fromNat_surj:
   141 assumes c: "countable A" and a: "a \<in> A"
   142 shows "\<exists> n. fromNat A n = a"
   143 apply(rule exI[of _ "toNat A a"]) using assms by simp
   144 
   145 lemma fromNat_image_incl:
   146 assumes "A \<noteq> {}"
   147 shows "fromNat A ` UNIV \<subseteq> A"
   148 using fromNat[OF assms] by auto
   149 
   150 lemma incl_fromNat_image:
   151 assumes "countable A"
   152 shows "A \<subseteq> fromNat A ` UNIV"
   153 unfolding image_def using fromNat_surj[OF assms] by auto
   154 
   155 lemma fromNat_image[simp]:
   156 assumes "A \<noteq> {}" and "countable A"
   157 shows "fromNat A ` UNIV = A"
   158 by (metis assms equalityI fromNat_image_incl incl_fromNat_image)
   159 
   160 lemma fromNat_inject[simp]:
   161 assumes A: "A \<noteq> {}" "countable A" and B: "B \<noteq> {}" "countable B"
   162 shows "fromNat A = fromNat B \<longleftrightarrow> A = B"
   163 by (metis assms fromNat_image)
   164 
   165 lemma inj_on_fromNat:
   166 "inj_on fromNat ({A. A \<noteq> {} \<and> countable A})"
   167 unfolding inj_on_def by auto
   168 
   169 
   170 subsection {* Preservation under the set theoretic operations *}
   171 
   172 lemma contable_empty[simp,intro]:
   173 "countable {}"
   174 by (metis countable_ex_to_nat inj_on_empty)
   175 
   176 lemma incl_countable:
   177 assumes "A \<subseteq> B" and "countable B"
   178 shows "countable A"
   179 by (metis assms countable_ex_to_nat subset_inj_on)
   180 
   181 lemma countable_diff:
   182 assumes "countable A"
   183 shows "countable (A - B)"
   184 by (metis Diff_subset assms incl_countable)
   185 
   186 lemma finite_countable[simp]:
   187 assumes "finite A"
   188 shows "countable A"
   189 by (metis assms countable_ex_to_nat finite_imp_inj_to_nat_seg)
   190 
   191 lemma countable_singl[simp]:
   192 "countable {a}"
   193 by simp
   194 
   195 lemma countable_insert[simp]:
   196 "countable (insert a A) \<longleftrightarrow> countable A"
   197 proof
   198   assume c: "countable A"
   199   thus "countable (insert a A)"
   200   apply (cases rule: countable_cases_card_of)
   201     apply (metis finite_countable finite_insert)
   202     unfolding countable_card_of_nat
   203     by (metis infinite_card_of_insert ordIso_imp_ordLeq ordIso_transitive)
   204 qed(insert incl_countable, metis incl_countable subset_insertI)
   205 
   206 lemma contable_IntL[simp]:
   207 assumes "countable A"
   208 shows "countable (A \<inter> B)"
   209 by (metis Int_lower1 assms incl_countable)
   210 
   211 lemma contable_IntR[simp]:
   212 assumes "countable B"
   213 shows "countable (A \<inter> B)"
   214 by (metis assms contable_IntL inf.commute)
   215 
   216 lemma countable_UN[simp]:
   217 assumes cI: "countable I" and cA: "\<And> i. i \<in> I \<Longrightarrow> countable (A i)"
   218 shows "countable (\<Union> i \<in> I. A i)"
   219 using assms unfolding countable_card_of_nat
   220 apply(intro card_of_UNION_ordLeq_infinite) by auto
   221 
   222 lemma contable_Un[simp]:
   223 "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B"
   224 proof safe
   225   assume cA: "countable A" and cB: "countable B"
   226   let ?I = "{0,Suc 0}"  let ?As = "\<lambda> i. case i of 0 \<Rightarrow> A|Suc 0 \<Rightarrow> B"
   227   have AB: "A \<union> B = (\<Union> i \<in> ?I. ?As i)" by simp
   228   show "countable (A \<union> B)" unfolding AB apply(rule countable_UN)
   229   using cA cB by auto
   230 qed (metis Un_upper1 incl_countable, metis Un_upper2 incl_countable)
   231 
   232 lemma countable_INT[simp]:
   233 assumes "i \<in> I" and "countable (A i)"
   234 shows "countable (\<Inter> i \<in> I. A i)"
   235 by (metis INF_insert assms contable_IntL insert_absorb)
   236 
   237 lemma countable_class[simp]:
   238 fixes A :: "('a::countable) set"
   239 shows "countable A"
   240 proof-
   241   have "inj_on to_nat A" by (metis inj_on_to_nat)
   242   thus ?thesis by (metis countable_ex_to_nat)
   243 qed
   244 
   245 lemma countable_image[simp]:
   246 assumes "countable A"
   247 shows "countable (f ` A)"
   248 using assms unfolding countable_card_of_nat
   249 by (metis card_of_image ordLeq_transitive)
   250 
   251 lemma countable_ordLeq:
   252 assumes "|A| \<le>o |B|" and "countable B"
   253 shows "countable A"
   254 using assms unfolding countable_card_of_nat by(rule ordLeq_transitive)
   255 
   256 lemma countable_ordLess:
   257 assumes AB: "|A| <o |B|" and B: "countable B"
   258 shows "countable A"
   259 using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] .
   260 
   261 lemma countable_vimage:
   262 assumes "B \<subseteq> range f" and "countable (f -` B)"
   263 shows "countable B"
   264 by (metis Int_absorb2 assms countable_image image_vimage_eq)
   265 
   266 lemma surj_countable_vimage:
   267 assumes s: "surj f" and c: "countable (f -` B)"
   268 shows "countable B"
   269 apply(rule countable_vimage[OF _ c]) using s by auto
   270 
   271 lemma countable_Collect[simp]:
   272 assumes "countable A"
   273 shows "countable {a \<in> A. \<phi> a}"
   274 by (metis Collect_conj_eq Int_absorb Int_commute Int_def assms contable_IntR)
   275 
   276 
   277 subsection{*  The type of countable sets *}
   278 
   279 typedef (open) 'a cset = "{A :: 'a set. countable A}"
   280 apply(rule exI[of _ "{}"]) by simp
   281 
   282 abbreviation rcset where "rcset \<equiv> Rep_cset"
   283 abbreviation acset where "acset \<equiv> Abs_cset"
   284 
   285 lemmas acset_rcset = Rep_cset_inverse
   286 declare acset_rcset[simp]
   287 
   288 lemma acset_surj:
   289 "\<exists> A. countable A \<and> acset A = C"
   290 apply(cases rule: Abs_cset_cases[of C]) by auto
   291 
   292 lemma rcset_acset[simp]:
   293 assumes "countable A"
   294 shows "rcset (acset A) = A"
   295 using Abs_cset_inverse assms by auto
   296 
   297 lemma acset_inj[simp]:
   298 assumes "countable A" and "countable B"
   299 shows "acset A = acset B \<longleftrightarrow> A = B"
   300 using assms Abs_cset_inject by auto
   301 
   302 lemma rcset[simp]:
   303 "countable (rcset C)"
   304 using Rep_cset by simp
   305 
   306 lemma rcset_inj[simp]:
   307 "rcset C = rcset D \<longleftrightarrow> C = D"
   308 by (metis acset_rcset)
   309 
   310 lemma rcset_surj:
   311 assumes "countable A"
   312 shows "\<exists> C. rcset C = A"
   313 apply(cases rule: Rep_cset_cases[of A])
   314 using assms by auto
   315 
   316 definition "cIn a C \<equiv> (a \<in> rcset C)"
   317 definition "cEmp \<equiv> acset {}"
   318 definition "cIns a C \<equiv> acset (insert a (rcset C))"
   319 abbreviation cSingl where "cSingl a \<equiv> cIns a cEmp"
   320 definition "cUn C D \<equiv> acset (rcset C \<union> rcset D)"
   321 definition "cInt C D \<equiv> acset (rcset C \<inter> rcset D)"
   322 definition "cDif C D \<equiv> acset (rcset C - rcset D)"
   323 definition "cIm f C \<equiv> acset (f ` rcset C)"
   324 definition "cVim f D \<equiv> acset (f -` rcset D)"
   325 (* TODO eventually: nice setup for these operations, copied from the set setup *)
   326 
   327 end