src/HOL/Infinite_Set.thy
 changeset 19537 213ff8b0c60c parent 19457 b6eb4b4546fa child 19656 09be06943252
equal inserted replaced
19536:1a3a3cf8b4fa 19537:213ff8b0c60c
22   from an infinite set, the result is still infinite.
22   from an infinite set, the result is still infinite.
23 *}
23 *}
24
24
25 lemma infinite_nonempty:
25 lemma infinite_nonempty:
26   "\<not> (infinite {})"
26   "\<not> (infinite {})"
27 by simp
27   by simp
28
28
29 lemma infinite_remove:
29 lemma infinite_remove:
30   "infinite S \<Longrightarrow> infinite (S - {a})"
30   "infinite S \<Longrightarrow> infinite (S - {a})"
31 by simp
31   by simp
32
32
33 lemma Diff_infinite_finite:
33 lemma Diff_infinite_finite:
34   assumes T: "finite T" and S: "infinite S"
34   assumes T: "finite T" and S: "infinite S"
35   shows "infinite (S-T)"
35   shows "infinite (S-T)"
36 using T
36   using T
37 proof (induct)
37 proof induct
38   from S
38   from S
39   show "infinite (S - {})" by auto
39   show "infinite (S - {})" by auto
40 next
40 next
41   fix T x
41   fix T x
42   assume ih: "infinite (S-T)"
42   assume ih: "infinite (S-T)"
48 qed
48 qed
49
49
50 lemma Un_infinite:
50 lemma Un_infinite:
51   "infinite S \<Longrightarrow> infinite (S \<union> T)"
51   "infinite S \<Longrightarrow> infinite (S \<union> T)"
52 by simp
52   by simp
53
53
54 lemma infinite_super:
54 lemma infinite_super:
55   assumes T: "S \<subseteq> T" and S: "infinite S"
55   assumes T: "S \<subseteq> T" and S: "infinite S"
56   shows "infinite T"
56   shows "infinite T"
57 proof (rule ccontr)
57 proof (rule ccontr)
58   assume "\<not>(infinite T)"
58   assume "\<not>(infinite T)"
59   with T
59   with T have "finite S" by (simp add: finite_subset)
60   have "finite S" by (simp add: finite_subset)
60   with S show False by simp
61   with S

62   show False by simp

63 qed
61 qed
64
62
65 text {*
63 text {*
66   As a concrete example, we prove that the set of natural
64   As a concrete example, we prove that the set of natural
67   numbers is infinite.
65   numbers is infinite.
354
352
355 defs
353 defs
356   INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
354   INF_def:  "Inf_many P \<equiv> infinite {x. P x}"
357   MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
355   MOST_def: "Alm_all P \<equiv> \<not>(INF x. \<not> P x)"
358
356
359 syntax (xsymbols)
357 abbreviation (xsymbols)
360   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
358   Inf_many1  (binder "\<exists>\<^sub>\<infinity>" 10)
361   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
359   "Inf_many1 == Inf_many"
362
360   Alm_all1  (binder "\<forall>\<^sub>\<infinity>" 10)
363 syntax (HTML output)
361   "Alm_all1 == Alm_all"
364   "MOST " :: "[idts, bool] \<Rightarrow> bool"       ("(3\<forall>\<^sub>\<infinity>_./ _)" [0,10] 10)
362
365   "INF "    :: "[idts, bool] \<Rightarrow> bool"     ("(3\<exists>\<^sub>\<infinity>_./ _)" [0,10] 10)
363 abbreviation (HTML output)

364   Inf_many2  (binder "\<exists>\<^sub>\<infinity>" 10)

365   "Inf_many2 == Inf_many"

366   Alm_all2  (binder "\<forall>\<^sub>\<infinity>" 10)

367   "Alm_all2 == Alm_all"
366
368
367 lemma INF_EX:
369 lemma INF_EX:
368   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
370   "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
369 proof (unfold INF_def, rule ccontr)
371 proof (unfold INF_def, rule ccontr)
370   assume inf: "infinite {x. P x}"
372   assume inf: "infinite {x. P x}"
419 constdefs
421 constdefs
420   atmost_one :: "'a set \<Rightarrow> bool"
422   atmost_one :: "'a set \<Rightarrow> bool"
421   "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
423   "atmost_one S \<equiv> \<forall>x y. x\<in>S \<and> y\<in>S \<longrightarrow> x=y"
422
424
423 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"
425 lemma atmost_one_empty: "S={} \<Longrightarrow> atmost_one S"
425
427
426 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"
428 lemma atmost_one_singleton: "S = {x} \<Longrightarrow> atmost_one S"