65 text {* |
65 text {* |
66 As a concrete example, we prove that the set of natural numbers is |
66 As a concrete example, we prove that the set of natural numbers is |
67 infinite. |
67 infinite. |
68 *} |
68 *} |
69 |
69 |
70 lemma finite_nat_bounded: |
70 lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\<exists>k. S \<subseteq> {..<k}" |
71 assumes S: "finite (S::nat set)" |
71 proof cases |
72 shows "\<exists>k. S \<subseteq> {..<k}" (is "\<exists>k. ?bounded S k") |
72 assume "S \<noteq> {}" with Max_less_iff[OF S this] show ?thesis |
73 using S |
73 by auto |
74 proof induct |
74 qed simp |
75 have "?bounded {} 0" by simp |
75 |
76 then show "\<exists>k. ?bounded {} k" .. |
76 lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})" |
77 next |
77 by (auto intro: finite_nat_bounded dest: finite_subset) |
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 then show ?thesis by auto |
|
89 qed |
|
90 qed |
|
91 |
|
92 lemma finite_nat_iff_bounded: |
|
93 "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})" (is "?lhs \<longleftrightarrow> ?rhs") |
|
94 proof |
|
95 assume ?lhs |
|
96 then show ?rhs by (rule finite_nat_bounded) |
|
97 next |
|
98 assume ?rhs |
|
99 then obtain k where "S \<subseteq> {..<k}" .. |
|
100 then show "finite S" |
|
101 by (rule finite_subset) simp |
|
102 qed |
|
103 |
78 |
104 lemma finite_nat_iff_bounded_le: |
79 lemma finite_nat_iff_bounded_le: |
105 "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})" (is "?lhs \<longleftrightarrow> ?rhs") |
80 "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})" (is "?lhs \<longleftrightarrow> ?rhs") |
106 proof |
81 proof |
107 assume ?lhs |
82 assume ?lhs |
114 then obtain k where "S \<subseteq> {..k}" .. |
89 then obtain k where "S \<subseteq> {..k}" .. |
115 then show "finite S" |
90 then show "finite S" |
116 by (rule finite_subset) simp |
91 by (rule finite_subset) simp |
117 qed |
92 qed |
118 |
93 |
119 lemma infinite_nat_iff_unbounded: |
94 lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)" |
120 "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)" |
95 unfolding finite_nat_iff_bounded_le by (auto simp: subset_eq not_le) |
121 (is "?lhs \<longleftrightarrow> ?rhs") |
|
122 proof |
|
123 assume ?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 then have "S \<subseteq> {..m}" |
|
129 by (auto simp add: sym [OF linorder_not_less]) |
|
130 with `?lhs` show False |
|
131 by (simp add: finite_nat_iff_bounded_le) |
|
132 qed |
|
133 next |
|
134 assume ?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 then have "\<forall>n. m < n \<longrightarrow> n \<notin> S" by auto |
|
141 with `?rhs` show False by blast |
|
142 qed |
|
143 qed |
|
144 |
96 |
145 lemma infinite_nat_iff_unbounded_le: |
97 lemma infinite_nat_iff_unbounded_le: |
146 "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)" |
98 "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)" |
147 (is "?lhs \<longleftrightarrow> ?rhs") |
99 unfolding finite_nat_iff_bounded by (auto simp: subset_eq not_less) |
148 proof |
|
149 assume ?lhs |
|
150 show ?rhs |
|
151 proof |
|
152 fix m |
|
153 from `?lhs` obtain n where "m < n \<and> n \<in> S" |
|
154 by (auto simp add: infinite_nat_iff_unbounded) |
|
155 then have "m \<le> n \<and> n \<in> S" by simp |
|
156 then show "\<exists>n. m \<le> n \<and> n \<in> S" .. |
|
157 qed |
|
158 next |
|
159 assume ?rhs |
|
160 show ?lhs |
|
161 proof (auto simp add: infinite_nat_iff_unbounded) |
|
162 fix m |
|
163 from `?rhs` obtain n where "Suc m \<le> n \<and> n \<in> S" |
|
164 by blast |
|
165 then have "m < n \<and> n \<in> S" by simp |
|
166 then show "\<exists>n. m < n \<and> n \<in> S" .. |
|
167 qed |
|
168 qed |
|
169 |
100 |
170 text {* |
101 text {* |
171 For a set of natural numbers to be infinite, it is enough to know |
102 For a set of natural numbers to be infinite, it is enough to know |
172 that for any number larger than some @{text k}, there is some larger |
103 that for any number larger than some @{text k}, there is some larger |
173 number that is an element of the set. |
104 number that is an element of the set. |