1 (* Title: HOL/BNF/Countable_Type.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_Type |
|
11 imports |
|
12 "~~/src/HOL/Cardinals/Cardinals" |
|
13 "~~/src/HOL/Library/Countable_Set" |
|
14 begin |
|
15 |
|
16 subsection{* Cardinal stuff *} |
|
17 |
|
18 lemma countable_card_of_nat: "countable A \<longleftrightarrow> |A| \<le>o |UNIV::nat set|" |
|
19 unfolding countable_def card_of_ordLeq[symmetric] by auto |
|
20 |
|
21 lemma countable_card_le_natLeq: "countable A \<longleftrightarrow> |A| \<le>o natLeq" |
|
22 unfolding countable_card_of_nat using card_of_nat ordLeq_ordIso_trans ordIso_symmetric by blast |
|
23 |
|
24 lemma countable_or_card_of: |
|
25 assumes "countable A" |
|
26 shows "(finite A \<and> |A| <o |UNIV::nat set| ) \<or> |
|
27 (infinite A \<and> |A| =o |UNIV::nat set| )" |
|
28 proof (cases "finite A") |
|
29 case True thus ?thesis by (metis finite_iff_cardOf_nat) |
|
30 next |
|
31 case False with assms show ?thesis |
|
32 by (metis countable_card_of_nat infinite_iff_card_of_nat ordIso_iff_ordLeq) |
|
33 qed |
|
34 |
|
35 lemma countable_cases_card_of[elim]: |
|
36 assumes "countable A" |
|
37 obtains (Fin) "finite A" "|A| <o |UNIV::nat set|" |
|
38 | (Inf) "infinite A" "|A| =o |UNIV::nat set|" |
|
39 using assms countable_or_card_of by blast |
|
40 |
|
41 lemma countable_or: |
|
42 "countable A \<Longrightarrow> (\<exists> f::'a\<Rightarrow>nat. finite A \<and> inj_on f A) \<or> (\<exists> f::'a\<Rightarrow>nat. infinite A \<and> bij_betw f A UNIV)" |
|
43 by (elim countable_enum_cases) fastforce+ |
|
44 |
|
45 lemma countable_cases[elim]: |
|
46 assumes "countable A" |
|
47 obtains (Fin) f :: "'a\<Rightarrow>nat" where "finite A" "inj_on f A" |
|
48 | (Inf) f :: "'a\<Rightarrow>nat" where "infinite A" "bij_betw f A UNIV" |
|
49 using assms countable_or by metis |
|
50 |
|
51 lemma countable_ordLeq: |
|
52 assumes "|A| \<le>o |B|" and "countable B" |
|
53 shows "countable A" |
|
54 using assms unfolding countable_card_of_nat by(rule ordLeq_transitive) |
|
55 |
|
56 lemma countable_ordLess: |
|
57 assumes AB: "|A| <o |B|" and B: "countable B" |
|
58 shows "countable A" |
|
59 using countable_ordLeq[OF ordLess_imp_ordLeq[OF AB] B] . |
|
60 |
|
61 subsection{* The type of countable sets *} |
|
62 |
|
63 typedef 'a cset = "{A :: 'a set. countable A}" morphisms rcset acset |
|
64 by (rule exI[of _ "{}"]) simp |
|
65 |
|
66 setup_lifting type_definition_cset |
|
67 |
|
68 declare |
|
69 rcset_inverse[simp] |
|
70 acset_inverse[Transfer.transferred, unfolded mem_Collect_eq, simp] |
|
71 acset_inject[Transfer.transferred, unfolded mem_Collect_eq, simp] |
|
72 rcset[Transfer.transferred, unfolded mem_Collect_eq, simp] |
|
73 |
|
74 lift_definition cin :: "'a \<Rightarrow> 'a cset \<Rightarrow> bool" is "op \<in>" parametric member_transfer |
|
75 .. |
|
76 lift_definition cempty :: "'a cset" is "{}" parametric empty_transfer |
|
77 by (rule countable_empty) |
|
78 lift_definition cinsert :: "'a \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is insert parametric Lifting_Set.insert_transfer |
|
79 by (rule countable_insert) |
|
80 lift_definition csingle :: "'a \<Rightarrow> 'a cset" is "\<lambda>x. {x}" |
|
81 by (rule countable_insert[OF countable_empty]) |
|
82 lift_definition cUn :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<union>" parametric union_transfer |
|
83 by (rule countable_Un) |
|
84 lift_definition cInt :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op \<inter>" parametric inter_transfer |
|
85 by (rule countable_Int1) |
|
86 lift_definition cDiff :: "'a cset \<Rightarrow> 'a cset \<Rightarrow> 'a cset" is "op -" parametric Diff_transfer |
|
87 by (rule countable_Diff) |
|
88 lift_definition cimage :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a cset \<Rightarrow> 'b cset" is "op `" parametric image_transfer |
|
89 by (rule countable_image) |
|
90 |
|
91 end |
|