author  haftmann 
Mon, 24 Apr 2006 16:37:07 +0200  
changeset 19457  b6eb4b4546fa 
parent 19363  667b5ea637dd 
child 19537  213ff8b0c60c 
permissions  rwrr 
14442  1 
(* Title: HOL/Infnite_Set.thy 
2 
ID: $Id$ 

14896  3 
Author: Stephan Merz 
14442  4 
*) 
5 

19457  6 
header {* Infinite Sets and Related Concepts*} 
14442  7 

15131  8 
theory Infinite_Set 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
15140
diff
changeset

9 
imports Hilbert_Choice Binomial 
15131  10 
begin 
14442  11 

12 
subsection "Infinite Sets" 

13 

14 
text {* Some elementary facts about infinite sets, by Stefan Merz. *} 

15 

19363  16 
abbreviation 
17 
infinite :: "'a set \<Rightarrow> bool" 

18 
"infinite S == \<not> finite S" 

14442  19 

20 
text {* 

21 
Infinite sets are nonempty, and if we remove some elements 

22 
from an infinite set, the result is still infinite. 

23 
*} 

24 

25 
lemma infinite_nonempty: 

26 
"\<not> (infinite {})" 

27 
by simp 

28 

29 
lemma infinite_remove: 

30 
"infinite S \<Longrightarrow> infinite (S  {a})" 

31 
by simp 

32 

33 
lemma Diff_infinite_finite: 

34 
assumes T: "finite T" and S: "infinite S" 

35 
shows "infinite (ST)" 

36 
using T 

37 
proof (induct) 

38 
from S 

39 
show "infinite (S  {})" by auto 

40 
next 

41 
fix T x 

42 
assume ih: "infinite (ST)" 

43 
have "S  (insert x T) = (ST)  {x}" 

44 
by (rule Diff_insert) 

45 
with ih 

46 
show "infinite (S  (insert x T))" 

47 
by (simp add: infinite_remove) 

48 
qed 

49 

50 
lemma Un_infinite: 

51 
"infinite S \<Longrightarrow> infinite (S \<union> T)" 

52 
by simp 

53 

54 
lemma infinite_super: 

55 
assumes T: "S \<subseteq> T" and S: "infinite S" 

56 
shows "infinite T" 

57 
proof (rule ccontr) 

58 
assume "\<not>(infinite T)" 

59 
with T 

60 
have "finite S" by (simp add: finite_subset) 

61 
with S 

62 
show False by simp 

63 
qed 

64 

65 
text {* 

66 
As a concrete example, we prove that the set of natural 

67 
numbers is infinite. 

68 
*} 

69 

70 
lemma finite_nat_bounded: 

71 
assumes S: "finite (S::nat set)" 

15045  72 
shows "\<exists>k. S \<subseteq> {..<k}" (is "\<exists>k. ?bounded S k") 
14442  73 
using S 
74 
proof (induct) 

75 
have "?bounded {} 0" by simp 

76 
thus "\<exists>k. ?bounded {} k" .. 

77 
next 

78 
fix S x 

79 
assume "\<exists>k. ?bounded S k" 

80 
then obtain k where k: "?bounded S k" .. 

81 
show "\<exists>k. ?bounded (insert x S) k" 

82 
proof (cases "x<k") 

83 
case True 

84 
with k show ?thesis by auto 

85 
next 

86 
case False 

87 
with k have "?bounded S (Suc x)" by auto 

88 
thus ?thesis by auto 

89 
qed 

90 
qed 

91 

92 
lemma finite_nat_iff_bounded: 

15045  93 
"finite (S::nat set) = (\<exists>k. S \<subseteq> {..<k})" (is "?lhs = ?rhs") 
14442  94 
proof 
95 
assume ?lhs 

96 
thus ?rhs by (rule finite_nat_bounded) 

97 
next 

98 
assume ?rhs 

15045  99 
then obtain k where "S \<subseteq> {..<k}" .. 
14442  100 
thus "finite S" 
101 
by (rule finite_subset, simp) 

102 
qed 

103 

104 
lemma finite_nat_iff_bounded_le: 

105 
"finite (S::nat set) = (\<exists>k. S \<subseteq> {..k})" (is "?lhs = ?rhs") 

106 
proof 

107 
assume ?lhs 

15045  108 
then obtain k where "S \<subseteq> {..<k}" 
14442  109 
by (blast dest: finite_nat_bounded) 
110 
hence "S \<subseteq> {..k}" by auto 

111 
thus ?rhs .. 

112 
next 

113 
assume ?rhs 

114 
then obtain k where "S \<subseteq> {..k}" .. 

115 
thus "finite S" 

116 
by (rule finite_subset, simp) 

117 
qed 

118 

119 
lemma infinite_nat_iff_unbounded: 

120 
"infinite (S::nat set) = (\<forall>m. \<exists>n. m<n \<and> n\<in>S)" 

121 
(is "?lhs = ?rhs") 

122 
proof 

123 
assume inf: ?lhs 

124 
show ?rhs 

125 
proof (rule ccontr) 

126 
assume "\<not> ?rhs" 

127 
then obtain m where m: "\<forall>n. m<n \<longrightarrow> n\<notin>S" by blast 

128 
hence "S \<subseteq> {..m}" 

16796  129 
by (auto simp add: sym[OF linorder_not_less]) 
14442  130 
with inf show "False" 
131 
by (simp add: finite_nat_iff_bounded_le) 

132 
qed 

133 
next 

134 
assume unbounded: ?rhs 

135 
show ?lhs 

136 
proof 

137 
assume "finite S" 

138 
then obtain m where "S \<subseteq> {..m}" 

139 
by (auto simp add: finite_nat_iff_bounded_le) 

140 
hence "\<forall>n. m<n \<longrightarrow> n\<notin>S" by auto 

141 
with unbounded show "False" by blast 

142 
qed 

143 
qed 

144 

145 
lemma infinite_nat_iff_unbounded_le: 

146 
"infinite (S::nat set) = (\<forall>m. \<exists>n. m\<le>n \<and> n\<in>S)" 

147 
(is "?lhs = ?rhs") 

148 
proof 

149 
assume inf: ?lhs 

150 
show ?rhs 

151 
proof 

152 
fix m 

153 
from inf obtain n where "m<n \<and> n\<in>S" 

154 
by (auto simp add: infinite_nat_iff_unbounded) 

155 
hence "m\<le>n \<and> n\<in>S" by auto 

156 
thus "\<exists>n. m \<le> n \<and> n \<in> S" .. 

157 
qed 

158 
next 

159 
assume unbounded: ?rhs 

160 
show ?lhs 

161 
proof (auto simp add: infinite_nat_iff_unbounded) 

162 
fix m 

163 
from unbounded obtain n where "(Suc m)\<le>n \<and> n\<in>S" 

164 
by blast 

165 
hence "m<n \<and> n\<in>S" by auto 

166 
thus "\<exists>n. m < n \<and> n \<in> S" .. 

167 
qed 

168 
qed 

169 

170 
text {* 

171 
For a set of natural numbers to be infinite, it is enough 

14957  172 
to know that for any number larger than some @{text k}, there 
14442  173 
is some larger number that is an element of the set. 
174 
*} 

175 

176 
lemma unbounded_k_infinite: 

177 
assumes k: "\<forall>m. k<m \<longrightarrow> (\<exists>n. m<n \<and> n\<in>S)" 

178 
shows "infinite (S::nat set)" 

179 
proof (auto simp add: infinite_nat_iff_unbounded) 

180 
fix m show "\<exists>n. m<n \<and> n\<in>S" 

181 
proof (cases "k<m") 

182 
case True 

183 
with k show ?thesis by blast 

184 
next 

185 
case False 

186 
from k obtain n where "Suc k < n \<and> n\<in>S" by auto 

187 
with False have "m<n \<and> n\<in>S" by auto 

188 
thus ?thesis .. 

189 
qed 

190 
qed 

191 

192 
theorem nat_infinite [simp]: 

193 
"infinite (UNIV :: nat set)" 

194 
by (auto simp add: infinite_nat_iff_unbounded) 

195 

196 
theorem nat_not_finite [elim]: 

197 
"finite (UNIV::nat set) \<Longrightarrow> R" 

198 
by simp 

199 

200 
text {* 

201 
Every infinite set contains a countable subset. More precisely 

14957  202 
we show that a set @{text S} is infinite if and only if there exists 
203 
an injective function from the naturals into @{text S}. 

14442  204 
*} 
205 

206 
lemma range_inj_infinite: 

207 
"inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)" 

208 
proof 

209 
assume "inj f" 

210 
and "finite (range f)" 

211 
hence "finite (UNIV::nat set)" 

212 
by (auto intro: finite_imageD simp del: nat_infinite) 

213 
thus "False" by simp 

214 
qed 

215 

216 
text {* 

217 
The ``only if'' direction is harder because it requires the 

218 
construction of a sequence of pairwise different elements of 

14957  219 
an infinite set @{text S}. The idea is to construct a sequence of 
220 
nonempty and infinite subsets of @{text S} obtained by successively 

221 
removing elements of @{text S}. 

14442  222 
*} 
223 

224 
lemma linorder_injI: 

225 
assumes hyp: "\<forall>x y. x < (y::'a::linorder) \<longrightarrow> f x \<noteq> f y" 

226 
shows "inj f" 

227 
proof (rule inj_onI) 

228 
fix x y 

229 
assume f_eq: "f x = f y" 

230 
show "x = y" 

231 
proof (rule linorder_cases) 

232 
assume "x < y" 

233 
with hyp have "f x \<noteq> f y" by blast 

234 
with f_eq show ?thesis by simp 

235 
next 

236 
assume "x = y" 

237 
thus ?thesis . 

238 
next 

239 
assume "y < x" 

240 
with hyp have "f y \<noteq> f x" by blast 

241 
with f_eq show ?thesis by simp 

242 
qed 

243 
qed 

244 

245 
lemma infinite_countable_subset: 

246 
assumes inf: "infinite (S::'a set)" 

247 
shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S" 

248 
proof  

14766  249 
def Sseq \<equiv> "nat_rec S (\<lambda>n T. T  {SOME e. e \<in> T})" 
250 
def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)" 

14442  251 
have Sseq_inf: "\<And>n. infinite (Sseq n)" 
252 
proof  

253 
fix n 

254 
show "infinite (Sseq n)" 

255 
proof (induct n) 

256 
from inf show "infinite (Sseq 0)" 

257 
by (simp add: Sseq_def) 

258 
next 

259 
fix n 

260 
assume "infinite (Sseq n)" thus "infinite (Sseq (Suc n))" 

261 
by (simp add: Sseq_def infinite_remove) 

262 
qed 

263 
qed 

264 
have Sseq_S: "\<And>n. Sseq n \<subseteq> S" 

265 
proof  

266 
fix n 

267 
show "Sseq n \<subseteq> S" 

268 
by (induct n, auto simp add: Sseq_def) 

269 
qed 

270 
have Sseq_pick: "\<And>n. pick n \<in> Sseq n" 

271 
proof  

272 
fix n 

273 
show "pick n \<in> Sseq n" 

274 
proof (unfold pick_def, rule someI_ex) 

275 
from Sseq_inf have "infinite (Sseq n)" . 

276 
hence "Sseq n \<noteq> {}" by auto 

277 
thus "\<exists>x. x \<in> Sseq n" by auto 

278 
qed 

279 
qed 

280 
with Sseq_S have rng: "range pick \<subseteq> S" 

281 
by auto 

282 
have pick_Sseq_gt: "\<And>n m. pick n \<notin> Sseq (n + Suc m)" 

283 
proof  

284 
fix n m 

285 
show "pick n \<notin> Sseq (n + Suc m)" 

286 
by (induct m, auto simp add: Sseq_def pick_def) 

287 
qed 

288 
have pick_pick: "\<And>n m. pick n \<noteq> pick (n + Suc m)" 

289 
proof  

290 
fix n m 

291 
from Sseq_pick have "pick (n + Suc m) \<in> Sseq (n + Suc m)" . 

292 
moreover from pick_Sseq_gt 

293 
have "pick n \<notin> Sseq (n + Suc m)" . 

294 
ultimately show "pick n \<noteq> pick (n + Suc m)" 

295 
by auto 

296 
qed 

297 
have inj: "inj pick" 

298 
proof (rule linorder_injI) 

299 
show "\<forall>i j. i<(j::nat) \<longrightarrow> pick i \<noteq> pick j" 

300 
proof (clarify) 

301 
fix i j 

302 
assume ij: "i<(j::nat)" 

303 
and eq: "pick i = pick j" 

304 
from ij obtain k where "j = i + (Suc k)" 

305 
by (auto simp add: less_iff_Suc_add) 

306 
with pick_pick have "pick i \<noteq> pick j" by simp 

307 
with eq show "False" by simp 

308 
qed 

309 
qed 

310 
from rng inj show ?thesis by auto 

311 
qed 

312 

313 
theorem infinite_iff_countable_subset: 

314 
"infinite S = (\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S)" 

315 
(is "?lhs = ?rhs") 

316 
by (auto simp add: infinite_countable_subset 

317 
range_inj_infinite infinite_super) 

318 

319 
text {* 

320 
For any function with infinite domain and finite range 

321 
there is some element that is the image of infinitely 

322 
many domain elements. In particular, any infinite sequence 

323 
of elements from a finite set contains some element that 

324 
occurs infinitely often. 

325 
*} 

326 

327 
theorem inf_img_fin_dom: 

328 
assumes img: "finite (f`A)" and dom: "infinite A" 

329 
shows "\<exists>y \<in> f`A. infinite (f ` {y})" 

330 
proof (rule ccontr) 

331 
assume "\<not> (\<exists>y\<in>f ` A. infinite (f ` {y}))" 

332 
with img have "finite (UN y:f`A. f ` {y})" 

333 
by (blast intro: finite_UN_I) 

334 
moreover have "A \<subseteq> (UN y:f`A. f ` {y})" by auto 

335 
moreover note dom 

336 
ultimately show "False" 

337 
by (simp add: infinite_super) 

338 
qed 

339 

340 
theorems inf_img_fin_domE = inf_img_fin_dom[THEN bexE] 

341 

342 

343 
subsection "Infinitely Many and Almost All" 

344 

345 
text {* 

346 
We often need to reason about the existence of infinitely many 

347 
(resp., all but finitely many) objects satisfying some predicate, 

348 
so we introduce corresponding binders and their proof rules. 

349 
*} 

350 

351 
consts 

352 
Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "INF " 10) 

353 
Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "MOST " 10) 

354 

355 
defs 

356 
INF_def: "Inf_many P \<equiv> infinite {x. P x}" 

357 
MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)" 

358 

359 
syntax (xsymbols) 

360 
"MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) 

361 
"INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) 

362 

14565  363 
syntax (HTML output) 
364 
"MOST " :: "[idts, bool] \<Rightarrow> bool" ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10) 

365 
"INF " :: "[idts, bool] \<Rightarrow> bool" ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10) 

366 

14442  367 
lemma INF_EX: 
368 
"(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" 

369 
proof (unfold INF_def, rule ccontr) 

370 
assume inf: "infinite {x. P x}" 

371 
and notP: "\<not>(\<exists>x. P x)" 

372 
from notP have "{x. P x} = {}" by simp 

373 
hence "finite {x. P x}" by simp 

374 
with inf show "False" by simp 

375 
qed 

376 

377 
lemma MOST_iff_finiteNeg: 

378 
"(\<forall>\<^sub>\<infinity>x. P x) = finite {x. \<not> P x}" 

379 
by (simp add: MOST_def INF_def) 

380 

381 
lemma ALL_MOST: 

382 
"\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" 

383 
by (simp add: MOST_iff_finiteNeg) 

384 

385 
lemma INF_mono: 

386 
assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x" 

387 
shows "\<exists>\<^sub>\<infinity>x. Q x" 

388 
proof  

389 
from inf have "infinite {x. P x}" by (unfold INF_def) 

390 
moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto 

391 
ultimately show ?thesis 

392 
by (simp add: INF_def infinite_super) 

393 
qed 

394 

395 
lemma MOST_mono: 

396 
"\<lbrakk> \<forall>\<^sub>\<infinity>x. P x; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" 

397 
by (unfold MOST_def, blast intro: INF_mono) 

398 

399 
lemma INF_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m<n \<and> P n)" 

400 
by (simp add: INF_def infinite_nat_iff_unbounded) 

401 

402 
lemma INF_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) = (\<forall>m. \<exists>n. m\<le>n \<and> P n)" 

403 
by (simp add: INF_def infinite_nat_iff_unbounded_le) 

404 

405 
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m<n \<longrightarrow> P n)" 

406 
by (simp add: MOST_def INF_nat) 

407 

408 
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) = (\<exists>m. \<forall>n. m\<le>n \<longrightarrow> P n)" 

409 
by (simp add: MOST_def INF_nat_le) 

410 

411 

412 
subsection "Miscellaneous" 

413 

414 
text {* 

415 
A few trivial lemmas about sets that contain at most one element. 

416 
These simplify the reasoning about deterministic automata. 

417 
*} 

418 

419 
constdefs 

420 
atmost_one :: "'a set \<Rightarrow> bool" 

421 
"atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y" 

422 

423 
lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S" 

424 
by (simp add: atmost_one_def) 

425 

426 
lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S" 

427 
by (simp add: atmost_one_def) 

428 

429 
lemma atmost_one_unique [elim]: "\<lbrakk> atmost_one S; x \<in> S; y \<in> S \<rbrakk> \<Longrightarrow> y=x" 

430 
by (simp add: atmost_one_def) 

431 

432 
end 