3 *) |
3 *) |
4 |
4 |
5 section \<open>Infinite Sets and Related Concepts\<close> |
5 section \<open>Infinite Sets and Related Concepts\<close> |
6 |
6 |
7 theory Infinite_Set |
7 theory Infinite_Set |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text \<open>The set of natural numbers is infinite.\<close> |
11 subsection \<open>The set of natural numbers is infinite\<close> |
12 |
12 |
13 lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)" |
13 lemma infinite_nat_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)" |
|
14 for S :: "nat set" |
14 using frequently_cofinite[of "\<lambda>x. x \<in> S"] |
15 using frequently_cofinite[of "\<lambda>x. x \<in> S"] |
15 by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially) |
16 by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially) |
16 |
17 |
17 lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)" |
18 lemma infinite_nat_iff_unbounded: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)" |
|
19 for S :: "nat set" |
18 using frequently_cofinite[of "\<lambda>x. x \<in> S"] |
20 using frequently_cofinite[of "\<lambda>x. x \<in> S"] |
19 by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense) |
21 by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense) |
20 |
22 |
21 lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})" |
23 lemma finite_nat_iff_bounded: "finite S \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})" |
|
24 for S :: "nat set" |
22 using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) |
25 using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) |
23 |
26 |
24 lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})" |
27 lemma finite_nat_iff_bounded_le: "finite S \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})" |
|
28 for S :: "nat set" |
25 using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) |
29 using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) |
26 |
30 |
27 lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}" |
31 lemma finite_nat_bounded: "finite S \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}" |
|
32 for S :: "nat set" |
28 by (simp add: finite_nat_iff_bounded) |
33 by (simp add: finite_nat_iff_bounded) |
29 |
34 |
30 |
35 |
31 text \<open> |
36 text \<open> |
32 For a set of natural numbers to be infinite, it is enough to know |
37 For a set of natural numbers to be infinite, it is enough to know |
33 that for any number larger than some \<open>k\<close>, there is some larger |
38 that for any number larger than some \<open>k\<close>, there is some larger |
34 number that is an element of the set. |
39 number that is an element of the set. |
35 \<close> |
40 \<close> |
36 |
41 |
37 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)" |
42 lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)" |
38 apply (clarsimp simp add: finite_nat_set_iff_bounded) |
43 apply (clarsimp simp add: finite_nat_set_iff_bounded) |
39 apply (drule_tac x="Suc (max m k)" in spec) |
44 apply (drule_tac x="Suc (max m k)" in spec) |
40 using less_Suc_eq by fastforce |
45 using less_Suc_eq apply fastforce |
|
46 done |
41 |
47 |
42 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R" |
48 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R" |
43 by simp |
49 by simp |
44 |
50 |
45 lemma range_inj_infinite: |
51 lemma range_inj_infinite: |
46 "inj (f::nat \<Rightarrow> 'a) \<Longrightarrow> infinite (range f)" |
52 fixes f :: "nat \<Rightarrow> 'a" |
|
53 assumes "inj f" |
|
54 shows "infinite (range f)" |
47 proof |
55 proof |
48 assume "finite (range f)" and "inj f" |
56 assume "finite (range f)" |
49 then have "finite (UNIV::nat set)" |
57 from this assms have "finite (UNIV::nat set)" |
50 by (rule finite_imageD) |
58 by (rule finite_imageD) |
51 then show False by simp |
59 then show False by simp |
52 qed |
60 qed |
53 |
61 |
54 text \<open>The set of integers is also infinite.\<close> |
62 |
55 |
63 subsection \<open>The set of integers is also infinite\<close> |
56 lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)" |
64 |
|
65 lemma infinite_int_iff_infinite_nat_abs: "infinite S \<longleftrightarrow> infinite ((nat \<circ> abs) ` S)" |
|
66 for S :: "int set" |
57 by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD) |
67 by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD) |
58 |
68 |
59 proposition infinite_int_iff_unbounded_le: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)" |
69 proposition infinite_int_iff_unbounded_le: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> \<ge> m \<and> n \<in> S)" |
60 apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def) |
70 for S :: "int set" |
61 apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff) |
71 by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def) |
62 done |
72 (metis abs_ge_zero nat_le_eq_zle le_nat_iff) |
63 |
73 |
64 proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)" |
74 proposition infinite_int_iff_unbounded: "infinite S \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)" |
65 apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def) |
75 for S :: "int set" |
66 apply (metis (full_types) nat_le_iff nat_mono not_le) |
76 by (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def) |
67 done |
77 (metis (full_types) nat_le_iff nat_mono not_le) |
68 |
78 |
69 proposition finite_int_iff_bounded: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})" |
79 proposition finite_int_iff_bounded: "finite S \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})" |
|
80 for S :: "int set" |
70 using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) |
81 using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) |
71 |
82 |
72 proposition finite_int_iff_bounded_le: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})" |
83 proposition finite_int_iff_bounded_le: "finite S \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})" |
|
84 for S :: "int set" |
73 using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) |
85 using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) |
74 |
86 |
75 subsection "Infinitely Many and Almost All" |
87 |
|
88 subsection \<open>Infinitely Many and Almost All\<close> |
76 |
89 |
77 text \<open> |
90 text \<open> |
78 We often need to reason about the existence of infinitely many |
91 We often need to reason about the existence of infinitely many |
79 (resp., all but finitely many) objects satisfying some predicate, so |
92 (resp., all but finitely many) objects satisfying some predicate, so |
80 we introduce corresponding binders and their proof rules. |
93 we introduce corresponding binders and their proof rules. |
81 \<close> |
94 \<close> |
82 |
95 |
83 (* The following two lemmas are available as filter-rules, but not in the simp-set *) |
96 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" |
84 lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently) |
97 by (rule not_frequently) |
85 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually) |
98 |
|
99 lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" |
|
100 by (rule not_eventually) |
86 |
101 |
87 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)" |
102 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)" |
88 by (simp add: frequently_const_iff) |
103 by (simp add: frequently_const_iff) |
89 |
104 |
90 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)" |
105 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)" |
91 by (simp add: eventually_const_iff) |
106 by (simp add: eventually_const_iff) |
92 |
107 |
93 lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))" |
108 lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))" |
94 by (simp only: imp_conv_disj frequently_disj_iff not_eventually) |
109 by (rule frequently_imp_iff) |
95 |
110 |
96 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)" |
111 lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)" |
97 by (auto intro: eventually_rev_mp eventually_mono) |
112 by (auto intro: eventually_rev_mp eventually_mono) |
98 |
113 |
99 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x" |
114 lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x" |
100 by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono) |
115 by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono) |
101 |
116 |
|
117 |
102 text \<open>Properties of quantifiers with injective functions.\<close> |
118 text \<open>Properties of quantifiers with injective functions.\<close> |
103 |
119 |
104 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x" |
120 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x" |
105 using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite) |
121 using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite) |
106 |
122 |
107 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)" |
123 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)" |
108 using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite) |
124 using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite) |
|
125 |
109 |
126 |
110 text \<open>Properties of quantifiers with singletons.\<close> |
127 text \<open>Properties of quantifiers with singletons.\<close> |
111 |
128 |
112 lemma not_INFM_eq [simp]: |
129 lemma not_INFM_eq [simp]: |
113 "\<not> (INFM x. x = a)" |
130 "\<not> (INFM x. x = a)" |
132 lemma MOST_eq_imp: |
149 lemma MOST_eq_imp: |
133 "MOST x. x = a \<longrightarrow> P x" |
150 "MOST x. x = a \<longrightarrow> P x" |
134 "MOST x. a = x \<longrightarrow> P x" |
151 "MOST x. a = x \<longrightarrow> P x" |
135 unfolding eventually_cofinite by simp_all |
152 unfolding eventually_cofinite by simp_all |
136 |
153 |
|
154 |
137 text \<open>Properties of quantifiers over the naturals.\<close> |
155 text \<open>Properties of quantifiers over the naturals.\<close> |
138 |
156 |
139 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)" |
157 lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)" |
|
158 for P :: "nat \<Rightarrow> bool" |
140 by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric]) |
159 by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric]) |
141 |
160 |
142 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)" |
161 lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)" |
|
162 for P :: "nat \<Rightarrow> bool" |
143 by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric]) |
163 by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric]) |
144 |
164 |
145 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)" |
165 lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)" |
|
166 for P :: "nat \<Rightarrow> bool" |
146 by (simp add: frequently_cofinite infinite_nat_iff_unbounded) |
167 by (simp add: frequently_cofinite infinite_nat_iff_unbounded) |
147 |
168 |
148 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)" |
169 lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P n) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)" |
|
170 for P :: "nat \<Rightarrow> bool" |
149 by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le) |
171 by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le) |
150 |
172 |
151 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x" |
173 lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x" |
152 by (simp add: eventually_frequently) |
174 by (simp add: eventually_frequently) |
153 |
175 |
154 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)" |
176 lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)" |
155 by (simp add: cofinite_eq_sequentially) |
177 by (simp add: cofinite_eq_sequentially) |
156 |
178 |
157 lemma |
179 lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)" |
158 shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)" |
180 and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n" |
159 and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n" |
|
160 by (simp_all add: MOST_Suc_iff) |
181 by (simp_all add: MOST_Suc_iff) |
161 |
182 |
162 lemma MOST_ge_nat: "MOST n::nat. m \<le> n" |
183 lemma MOST_ge_nat: "MOST n::nat. m \<le> n" |
163 by (simp add: cofinite_eq_sequentially eventually_ge_at_top) |
184 by (simp add: cofinite_eq_sequentially eventually_ge_at_top) |
164 |
185 |
179 lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib) |
200 lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib) |
180 lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE) |
201 lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE) |
181 lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI) |
202 lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI) |
182 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite |
203 lemmas MOST_iff_finiteNeg = MOST_iff_cofinite |
183 |
204 |
184 subsection "Enumeration of an Infinite Set" |
205 |
185 |
206 subsection \<open>Enumeration of an Infinite Set\<close> |
186 text \<open> |
207 |
187 The set's element type must be wellordered (e.g. the natural numbers). |
208 text \<open>The set's element type must be wellordered (e.g. the natural numbers).\<close> |
188 \<close> |
|
189 |
209 |
190 text \<open> |
210 text \<open> |
191 Could be generalized to |
211 Could be generalized to |
192 @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}. |
212 @{prop "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}. |
193 \<close> |
213 \<close> |
194 |
214 |
195 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" |
215 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" |
196 where |
216 where |
197 enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)" |
217 enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)" |
198 | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n" |
218 | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n" |
199 |
219 |
200 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" |
220 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n" |
201 by simp |
221 by simp |
202 |
222 |
203 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S" |
223 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S" |
204 apply (induct n arbitrary: S) |
224 proof (induct n arbitrary: S) |
205 apply (fastforce intro: LeastI dest!: infinite_imp_nonempty) |
225 case 0 |
206 apply simp |
226 then show ?case |
207 apply (metis DiffE infinite_remove) |
227 by (fastforce intro: LeastI dest!: infinite_imp_nonempty) |
208 done |
228 next |
|
229 case (Suc n) |
|
230 then show ?case |
|
231 by simp (metis DiffE infinite_remove) |
|
232 qed |
209 |
233 |
210 declare enumerate_0 [simp del] enumerate_Suc [simp del] |
234 declare enumerate_0 [simp del] enumerate_Suc [simp del] |
211 |
235 |
212 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)" |
236 lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)" |
213 apply (induct n arbitrary: S) |
237 apply (induct n arbitrary: S) |
256 case (Suc n S) |
277 case (Suc n S) |
257 show ?case |
278 show ?case |
258 using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close> |
279 using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close> |
259 apply (subst (1 2) enumerate_Suc') |
280 apply (subst (1 2) enumerate_Suc') |
260 apply (subst Suc) |
281 apply (subst Suc) |
261 using \<open>infinite S\<close> |
282 apply (use \<open>infinite S\<close> in simp) |
262 apply simp |
|
263 apply (intro arg_cong[where f = Least] ext) |
283 apply (intro arg_cong[where f = Least] ext) |
264 apply (auto simp: enumerate_Suc'[symmetric]) |
284 apply (auto simp: enumerate_Suc'[symmetric]) |
265 done |
285 done |
266 qed |
286 qed |
267 |
287 |
268 lemma enumerate_Ex: |
288 lemma enumerate_Ex: |
269 assumes S: "infinite (S::nat set)" |
289 fixes S :: "nat set" |
270 shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s" |
290 assumes S: "infinite S" |
|
291 and s: "s \<in> S" |
|
292 shows "\<exists>n. enumerate S n = s" |
|
293 using s |
271 proof (induct s rule: less_induct) |
294 proof (induct s rule: less_induct) |
272 case (less s) |
295 case (less s) |
273 show ?case |
296 show ?case |
274 proof cases |
297 proof (cases "\<exists>y\<in>S. y < s") |
|
298 case True |
275 let ?y = "Max {s'\<in>S. s' < s}" |
299 let ?y = "Max {s'\<in>S. s' < s}" |
276 assume "\<exists>y\<in>S. y < s" |
300 from True have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)" |
277 then have y: "\<And>x. ?y < x \<longleftrightarrow> (\<forall>s'\<in>S. s' < s \<longrightarrow> s' < x)" |
|
278 by (subst Max_less_iff) auto |
301 by (subst Max_less_iff) auto |
279 then have y_in: "?y \<in> {s'\<in>S. s' < s}" |
302 then have y_in: "?y \<in> {s'\<in>S. s' < s}" |
280 by (intro Max_in) auto |
303 by (intro Max_in) auto |
281 with less.hyps[of ?y] obtain n where "enumerate S n = ?y" |
304 with less.hyps[of ?y] obtain n where "enumerate S n = ?y" |
282 by auto |
305 by auto |
283 with S have "enumerate S (Suc n) = s" |
306 with S have "enumerate S (Suc n) = s" |
284 by (auto simp: y less enumerate_Suc'' intro!: Least_equality) |
307 by (auto simp: y less enumerate_Suc'' intro!: Least_equality) |
285 then show ?case by auto |
308 then show ?thesis by auto |
286 next |
309 next |
287 assume *: "\<not> (\<exists>y\<in>S. y < s)" |
310 case False |
288 then have "\<forall>t\<in>S. s \<le> t" by auto |
311 then have "\<forall>t\<in>S. s \<le> t" by auto |
289 with \<open>s \<in> S\<close> show ?thesis |
312 with \<open>s \<in> S\<close> show ?thesis |
290 by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0) |
313 by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0) |
291 qed |
314 qed |
292 qed |
315 qed |
305 moreover note \<open>infinite S\<close> |
328 moreover note \<open>infinite S\<close> |
306 ultimately show ?thesis |
329 ultimately show ?thesis |
307 unfolding bij_betw_def by (auto intro: enumerate_in_set) |
330 unfolding bij_betw_def by (auto intro: enumerate_in_set) |
308 qed |
331 qed |
309 |
332 |
310 text\<open>A pair of weird and wonderful lemmas from HOL Light\<close> |
333 text \<open>A pair of weird and wonderful lemmas from HOL Light.\<close> |
311 lemma finite_transitivity_chain: |
334 lemma finite_transitivity_chain: |
312 assumes "finite A" |
335 assumes "finite A" |
313 and R: "\<And>x. ~ R x x" "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z" |
336 and R: "\<And>x. \<not> R x x" "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z" |
314 and A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> A \<and> R x y" |
337 and A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> A \<and> R x y" |
315 shows "A = {}" |
338 shows "A = {}" |
316 using \<open>finite A\<close> A |
339 using \<open>finite A\<close> A |
317 proof (induction A) |
340 proof (induct A) |
|
341 case empty |
|
342 then show ?case by simp |
|
343 next |
318 case (insert a A) |
344 case (insert a A) |
319 with R show ?case |
345 with R show ?case |
320 by (metis empty_iff insert_iff) |
346 by (metis empty_iff insert_iff) (* somewhat slow *) |
321 qed simp |
347 qed |
322 |
348 |
323 corollary Union_maximal_sets: |
349 corollary Union_maximal_sets: |
324 assumes "finite \<F>" |
350 assumes "finite \<F>" |
325 shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>" |
351 shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>" |
326 (is "?lhs = ?rhs") |
352 (is "?lhs = ?rhs") |
327 proof |
353 proof |
|
354 show "?lhs \<subseteq> ?rhs" by force |
328 show "?rhs \<subseteq> ?lhs" |
355 show "?rhs \<subseteq> ?lhs" |
329 proof (rule Union_subsetI) |
356 proof (rule Union_subsetI) |
330 fix S |
357 fix S |
331 assume "S \<in> \<F>" |
358 assume "S \<in> \<F>" |
332 have "{T \<in> \<F>. S \<subseteq> T} = {}" if "~ (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)" |
359 have "{T \<in> \<F>. S \<subseteq> T} = {}" |
|
360 if "\<not> (\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y)" |
333 apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"]) |
361 apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"]) |
334 using assms that apply auto |
362 apply (use assms that in auto) |
335 by (blast intro: dual_order.trans psubset_imp_subset) |
363 apply (blast intro: dual_order.trans psubset_imp_subset) |
336 then show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y" |
364 done |
337 using \<open>S \<in> \<F>\<close> by blast |
365 with \<open>S \<in> \<F>\<close> show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y" |
|
366 by blast |
338 qed |
367 qed |
339 qed force |
368 qed |
340 |
369 |
341 end |
370 end |
342 |
|