author  hoelzl 
Thu, 17 Mar 2016 14:48:14 +0100  
changeset 62648  ee48e0b4f669 
parent 62390  842917225d56 
child 63092  a949b2a5f51d 
permissions  rwrr 
50134  1 
(* Title: HOL/Library/Countable_Set.thy 
2 
Author: Johannes Hölzl 

3 
Author: Andrei Popescu 

4 
*) 

5 

60500  6 
section \<open>Countable sets\<close> 
50134  7 

8 
theory Countable_Set 

51542  9 
imports Countable Infinite_Set 
50134  10 
begin 
11 

60500  12 
subsection \<open>Predicate for countable sets\<close> 
50134  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 

60500  52 
subsection \<open>Enumerate a countable set\<close> 
50134  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  

53381  58 
obtain f :: "'a \<Rightarrow> nat" where "inj_on f S" 
60500  59 
using \<open>countable S\<close> by (rule countableE) 
50134  60 
then have "bij_betw f S (f`S)" 
61 
unfolding bij_betw_def by simp 

62 
moreover 

60500  63 
from \<open>inj_on f S\<close> \<open>infinite S\<close> have inf_fS: "infinite (f`S)" 
50134  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_enum_cases: 

73 
assumes "countable S" 

74 
obtains (finite) f :: "'a \<Rightarrow> nat" where "finite S" "bij_betw f S {..<card S}" 

75 
 (infinite) f :: "'a \<Rightarrow> nat" where "infinite S" "bij_betw f S UNIV" 

60500  76 
using ex_bij_betw_finite_nat[of S] countableE_infinite \<open>countable S\<close> 
50134  77 
by (cases "finite S") (auto simp add: atLeast0LessThan) 
78 

79 
definition to_nat_on :: "'a set \<Rightarrow> 'a \<Rightarrow> nat" where 

80 
"to_nat_on S = (SOME f. if finite S then bij_betw f S {..< card S} else bij_betw f S UNIV)" 

81 

82 
definition from_nat_into :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where 

50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

83 
"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)" 
50134  84 

85 
lemma to_nat_on_finite: "finite S \<Longrightarrow> bij_betw (to_nat_on S) S {..< card S}" 

86 
using ex_bij_betw_finite_nat unfolding to_nat_on_def 

87 
by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S {..<card S}"]) (auto simp add: atLeast0LessThan) 

88 

89 
lemma to_nat_on_infinite: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (to_nat_on S) S UNIV" 

90 
using countableE_infinite unfolding to_nat_on_def 

91 
by (intro someI2_ex[where Q="\<lambda>f. bij_betw f S UNIV"]) auto 

92 

50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

93 
lemma bij_betw_from_nat_into_finite: "finite S \<Longrightarrow> bij_betw (from_nat_into S) {..< card S} S" 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

94 
unfolding from_nat_into_def[abs_def] 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

95 
using to_nat_on_finite[of S] 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

96 
apply (subst bij_betw_cong) 
62390  97 
apply (split if_split) 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

98 
apply (simp add: bij_betw_def) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

99 
apply (auto cong: bij_betw_cong 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

100 
intro: bij_betw_inv_into to_nat_on_finite) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

101 
done 
50134  102 

50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

103 
lemma bij_betw_from_nat_into: "countable S \<Longrightarrow> infinite S \<Longrightarrow> bij_betw (from_nat_into S) UNIV S" 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

104 
unfolding from_nat_into_def[abs_def] 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

105 
using to_nat_on_infinite[of S, unfolded bij_betw_def] 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

106 
by (auto cong: bij_betw_cong intro: bij_betw_inv_into to_nat_on_infinite) 
50134  107 

108 
lemma inj_on_to_nat_on[intro]: "countable A \<Longrightarrow> inj_on (to_nat_on A) A" 

109 
using to_nat_on_infinite[of A] to_nat_on_finite[of A] 

110 
by (cases "finite A") (auto simp: bij_betw_def) 

111 

112 
lemma to_nat_on_inj[simp]: 

113 
"countable A \<Longrightarrow> a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> to_nat_on A a = to_nat_on A b \<longleftrightarrow> a = b" 

114 
using inj_on_to_nat_on[of A] by (auto dest: inj_onD) 

115 

50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

116 
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" 
50134  117 
by (auto simp: from_nat_into_def intro!: inv_into_f_f) 
118 

119 
lemma subset_range_from_nat_into: "countable A \<Longrightarrow> A \<subseteq> range (from_nat_into A)" 

120 
by (auto intro: from_nat_into_to_nat_on[symmetric]) 

121 

50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

122 
lemma from_nat_into: "A \<noteq> {} \<Longrightarrow> from_nat_into A n \<in> A" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

123 
unfolding from_nat_into_def by (metis equals0I inv_into_into someI_ex) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

124 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

125 
lemma range_from_nat_into_subset: "A \<noteq> {} \<Longrightarrow> range (from_nat_into A) \<subseteq> A" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

126 
using from_nat_into[of A] by auto 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

127 

50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

128 
lemma range_from_nat_into[simp]: "A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> range (from_nat_into A) = A" 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

129 
by (metis equalityI range_from_nat_into_subset subset_range_from_nat_into) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

130 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

131 
lemma image_to_nat_on: "countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A ` A = UNIV" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

132 
using to_nat_on_infinite[of A] by (simp add: bij_betw_def) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

133 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

134 
lemma to_nat_on_surj: "countable A \<Longrightarrow> infinite A \<Longrightarrow> \<exists>a\<in>A. to_nat_on A a = n" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

135 
by (metis (no_types) image_iff iso_tuple_UNIV_I image_to_nat_on) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

136 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

137 
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" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

138 
by (simp add: f_inv_into_f from_nat_into_def) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

139 

50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

140 
lemma to_nat_on_from_nat_into_infinite[simp]: 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

141 
"countable A \<Longrightarrow> infinite A \<Longrightarrow> to_nat_on A (from_nat_into A n) = n" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

142 
by (metis image_iff to_nat_on_surj to_nat_on_from_nat_into) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

143 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

144 
lemma from_nat_into_inj: 
50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

145 
"countable A \<Longrightarrow> m \<in> to_nat_on A ` A \<Longrightarrow> n \<in> to_nat_on A ` A \<Longrightarrow> 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

146 
from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

147 
by (subst to_nat_on_inj[symmetric, of A]) auto 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

148 

b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

149 
lemma from_nat_into_inj_infinite[simp]: 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

150 
"countable A \<Longrightarrow> infinite A \<Longrightarrow> from_nat_into A m = from_nat_into A n \<longleftrightarrow> m = n" 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

151 
using image_to_nat_on[of A] from_nat_into_inj[of A m n] by simp 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

152 

b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

153 
lemma eq_from_nat_into_iff: 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

154 
"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" 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

155 
by auto 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

156 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

157 
lemma from_nat_into_surj: "countable A \<Longrightarrow> a \<in> A \<Longrightarrow> \<exists>n. from_nat_into A n = a" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

158 
by (rule exI[of _ "to_nat_on A a"]) simp 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

159 

885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

160 
lemma from_nat_into_inject[simp]: 
50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

161 
"A \<noteq> {} \<Longrightarrow> countable A \<Longrightarrow> B \<noteq> {} \<Longrightarrow> countable B \<Longrightarrow> from_nat_into A = from_nat_into B \<longleftrightarrow> A = B" 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

162 
by (metis range_from_nat_into) 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

163 

50148
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

164 
lemma inj_on_from_nat_into: "inj_on from_nat_into ({A. A \<noteq> {} \<and> countable A})" 
b8cff6a8fda2
Countable_Set: tuned lemma names; more generic lemmas
hoelzl
parents:
50144
diff
changeset

165 
unfolding inj_on_def by auto 
50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

166 

60500  167 
subsection \<open>Closure properties of countability\<close> 
50134  168 

169 
lemma countable_SIGMA[intro, simp]: 

170 
"countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)" 

171 
by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def) 

172 

53381  173 
lemma countable_image[intro, simp]: 
174 
assumes "countable A" 

175 
shows "countable (f`A)" 

50134  176 
proof  
53381  177 
obtain g :: "'a \<Rightarrow> nat" where "inj_on g A" 
178 
using assms by (rule countableE) 

50134  179 
moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A" 
180 
by (auto intro: inj_on_inv_into inv_into_into) 

181 
ultimately show ?thesis 

182 
by (blast dest: comp_inj_on subset_inj_on intro: countableI) 

183 
qed 

184 

60303  185 
lemma countable_image_inj_on: "countable (f ` A) \<Longrightarrow> inj_on f A \<Longrightarrow> countable A" 
186 
by (metis countable_image the_inv_into_onto) 

187 

50134  188 
lemma countable_UN[intro, simp]: 
189 
fixes I :: "'i set" and A :: "'i => 'a set" 

190 
assumes I: "countable I" 

191 
assumes A: "\<And>i. i \<in> I \<Longrightarrow> countable (A i)" 

192 
shows "countable (\<Union>i\<in>I. A i)" 

193 
proof  

194 
have "(\<Union>i\<in>I. A i) = snd ` (SIGMA i : I. A i)" by (auto simp: image_iff) 

195 
then show ?thesis by (simp add: assms) 

196 
qed 

197 

198 
lemma countable_Un[intro]: "countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A \<union> B)" 

199 
by (rule countable_UN[of "{True, False}" "\<lambda>True \<Rightarrow> A  False \<Rightarrow> B", simplified]) 

200 
(simp split: bool.split) 

201 

202 
lemma countable_Un_iff[simp]: "countable (A \<union> B) \<longleftrightarrow> countable A \<and> countable B" 

203 
by (metis countable_Un countable_subset inf_sup_ord(3,4)) 

204 

205 
lemma countable_Plus[intro, simp]: 

206 
"countable A \<Longrightarrow> countable B \<Longrightarrow> countable (A <+> B)" 

207 
by (simp add: Plus_def) 

208 

209 
lemma countable_empty[intro, simp]: "countable {}" 

210 
by (blast intro: countable_finite) 

211 

212 
lemma countable_insert[intro, simp]: "countable A \<Longrightarrow> countable (insert a A)" 

213 
using countable_Un[of "{a}" A] by (auto simp: countable_finite) 

214 

215 
lemma countable_Int1[intro, simp]: "countable A \<Longrightarrow> countable (A \<inter> B)" 

216 
by (force intro: countable_subset) 

217 

218 
lemma countable_Int2[intro, simp]: "countable B \<Longrightarrow> countable (A \<inter> B)" 

219 
by (blast intro: countable_subset) 

220 

221 
lemma countable_INT[intro, simp]: "i \<in> I \<Longrightarrow> countable (A i) \<Longrightarrow> countable (\<Inter>i\<in>I. A i)" 

222 
by (blast intro: countable_subset) 

223 

224 
lemma countable_Diff[intro, simp]: "countable A \<Longrightarrow> countable (A  B)" 

225 
by (blast intro: countable_subset) 

226 

60303  227 
lemma countable_insert_eq [simp]: "countable (insert x A) = countable A" 
228 
by auto (metis Diff_insert_absorb countable_Diff insert_absorb) 

229 

50134  230 
lemma countable_vimage: "B \<subseteq> range f \<Longrightarrow> countable (f ` B) \<Longrightarrow> countable B" 
231 
by (metis Int_absorb2 assms countable_image image_vimage_eq) 

232 

233 
lemma surj_countable_vimage: "surj f \<Longrightarrow> countable (f ` B) \<Longrightarrow> countable B" 

234 
by (metis countable_vimage top_greatest) 

235 

50144
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

236 
lemma countable_Collect[simp]: "countable A \<Longrightarrow> countable {a \<in> A. \<phi> a}" 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

237 
by (metis Collect_conj_eq Int_absorb Int_commute Int_def countable_Int1) 
885deccc264e
renamed BNF/Countable_Set to Countable_Type and moved its generic stuff to Library/Countable_Set
hoelzl
parents:
50134
diff
changeset

238 

54410
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

239 
lemma countable_Image: 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

240 
assumes "\<And>y. y \<in> Y \<Longrightarrow> countable (X `` {y})" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

241 
assumes "countable Y" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

242 
shows "countable (X `` Y)" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

243 
proof  
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

244 
have "countable (X `` (\<Union>y\<in>Y. {y}))" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

245 
unfolding Image_UN by (intro countable_UN assms) 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

246 
then show ?thesis by simp 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

247 
qed 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

248 

0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

249 
lemma countable_relpow: 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

250 
fixes X :: "'a rel" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

251 
assumes Image_X: "\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

252 
assumes Y: "countable Y" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

253 
shows "countable ((X ^^ i) `` Y)" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

254 
using Y by (induct i arbitrary: Y) (auto simp: relcomp_Image Image_X) 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

255 

60058  256 
lemma countable_funpow: 
257 
fixes f :: "'a set \<Rightarrow> 'a set" 

258 
assumes "\<And>A. countable A \<Longrightarrow> countable (f A)" 

259 
and "countable A" 

260 
shows "countable ((f ^^ n) A)" 

261 
by(induction n)(simp_all add: assms) 

262 

54410
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

263 
lemma countable_rtrancl: 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

264 
"(\<And>Y. countable Y \<Longrightarrow> countable (X `` Y)) \<Longrightarrow> countable Y \<Longrightarrow> countable (X^* `` Y)" 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

265 
unfolding rtrancl_is_UN_relpow UN_Image by (intro countable_UN countableI_type countable_relpow) 
0a578fb7fb73
countability of the image of a reflexive transitive closure
hoelzl
parents:
53381
diff
changeset

266 

50134  267 
lemma countable_lists[intro, simp]: 
268 
assumes A: "countable A" shows "countable (lists A)" 

269 
proof  

270 
have "countable (lists (range (from_nat_into A)))" 

271 
by (auto simp: lists_image) 

272 
with A show ?thesis 

273 
by (auto dest: subset_range_from_nat_into countable_subset lists_mono) 

274 
qed 

275 

50245
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50148
diff
changeset

276 
lemma Collect_finite_eq_lists: "Collect finite = set ` lists UNIV" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50148
diff
changeset

277 
using finite_list by auto 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50148
diff
changeset

278 

dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50148
diff
changeset

279 
lemma countable_Collect_finite: "countable (Collect (finite::'a::countable set\<Rightarrow>bool))" 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50148
diff
changeset

280 
by (simp add: Collect_finite_eq_lists) 
dea9363887a6
based countable topological basis on Countable_Set
immler
parents:
50148
diff
changeset

281 

50936
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

282 
lemma countable_rat: "countable \<rat>" 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

283 
unfolding Rats_def by auto 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

284 

b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

285 
lemma Collect_finite_subset_eq_lists: "{A. finite A \<and> A \<subseteq> T} = set ` lists T" 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

286 
using finite_list by (auto simp: lists_eq_set) 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

287 

b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

288 
lemma countable_Collect_finite_subset: 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

289 
"countable T \<Longrightarrow> countable {A. finite A \<and> A \<subseteq> T}" 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

290 
unfolding Collect_finite_subset_eq_lists by auto 
b28f258ebc1a
countablility of finite subsets and rational numbers
hoelzl
parents:
50245
diff
changeset

291 

60058  292 
lemma countable_set_option [simp]: "countable (set_option x)" 
293 
by(cases x) auto 

294 

60500  295 
subsection \<open>Misc lemmas\<close> 
50134  296 

62648  297 
lemma infinite_countable_subset': 
298 
assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C" 

299 
proof  

300 
from infinite_countable_subset[OF X] guess f .. 

301 
then show ?thesis 

302 
by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite) 

303 
qed 

304 

50134  305 
lemma countable_all: 
306 
assumes S: "countable S" 

307 
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))" 

308 
using S[THEN subset_range_from_nat_into] by auto 

309 

57025  310 
lemma finite_sequence_to_countable_set: 
311 
assumes "countable X" 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" 

312 
proof  show thesis 

313 
apply (rule that[of "\<lambda>i. if X = {} then {} else from_nat_into X ` {..i}"]) 

62390  314 
apply (auto simp: image_iff Ball_def intro: from_nat_into split: if_split_asm) 
57025  315 
proof  
316 
fix x n assume "x \<in> X" "\<forall>i m. m \<le> i \<longrightarrow> x \<noteq> from_nat_into X m" 

60500  317 
with from_nat_into_surj[OF \<open>countable X\<close> \<open>x \<in> X\<close>] 
57025  318 
show False 
319 
by auto 

320 
qed 

321 
qed 

322 

62370  323 
lemma transfer_countable[transfer_rule]: 
324 
"bi_unique R \<Longrightarrow> rel_fun (rel_set R) op = countable countable" 

325 
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma) 

326 
(auto dest: countable_image_inj_on) 

327 

60500  328 
subsection \<open>Uncountable\<close> 
57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

329 

596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

330 
abbreviation uncountable where 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

331 
"uncountable A \<equiv> \<not> countable A" 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

332 

596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

333 
lemma uncountable_def: "uncountable A \<longleftrightarrow> A \<noteq> {} \<and> \<not> (\<exists>f::(nat \<Rightarrow> 'a). range f = A)" 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

334 
by (auto intro: inj_on_inv_into simp: countable_def) 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

335 
(metis all_not_in_conv inj_on_iff_surj subset_UNIV) 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

336 

596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

337 
lemma uncountable_bij_betw: "bij_betw f A B \<Longrightarrow> uncountable B \<Longrightarrow> uncountable A" 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

338 
unfolding bij_betw_def by (metis countable_image) 
62370  339 

57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

340 
lemma uncountable_infinite: "uncountable A \<Longrightarrow> infinite A" 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

341 
by (metis countable_finite) 
62370  342 

57234
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

343 
lemma uncountable_minus_countable: 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

344 
"uncountable A \<Longrightarrow> countable B \<Longrightarrow> uncountable (A  B)" 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

345 
using countable_Un[of B "A  B"] assms by auto 
596a499318ab
clean up ContNotDenum; add lemmas by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57025
diff
changeset

346 

60303  347 
lemma countable_Diff_eq [simp]: "countable (A  {x}) = countable A" 
348 
by (meson countable_Diff countable_empty countable_insert uncountable_minus_countable) 

349 

50134  350 
end 