14442

1 
(* Title: HOL/Infnite_Set.thy


2 
ID: $Id$

14896

3 
Author: Stephan Merz

14442

4 
*)


5 


6 
header {* Infnite Sets and Related Concepts*}


7 

15131

8 
theory Infinite_Set

15140

9 
imports Hilbert_Choice Finite_Set SetInterval

15131

10 
begin

14442

11 


12 
subsection "Infinite Sets"


13 


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


15 


16 
syntax


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


18 
translations


19 
"infinite S" == "S \<notin> Finites"


20 


21 
text {*


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


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


24 
*}


25 


26 
lemma infinite_nonempty:


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


28 
by simp


29 


30 
lemma infinite_remove:


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


32 
by simp


33 


34 
lemma Diff_infinite_finite:


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


36 
shows "infinite (ST)"


37 
using T


38 
proof (induct)


39 
from S


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


41 
next


42 
fix T x


43 
assume ih: "infinite (ST)"


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


45 
by (rule Diff_insert)


46 
with ih


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


48 
by (simp add: infinite_remove)


49 
qed


50 


51 
lemma Un_infinite:


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


53 
by simp


54 


55 
lemma infinite_super:


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


57 
shows "infinite T"


58 
proof (rule ccontr)


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


60 
with T


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


62 
with S


63 
show False by simp


64 
qed


65 


66 
text {*


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


68 
numbers is infinite.


69 
*}


70 


71 
lemma finite_nat_bounded:


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

15045

73 
shows "\<exists>k. S \<subseteq> {..<k}" (is "\<exists>k. ?bounded S k")

14442

74 
using S


75 
proof (induct)


76 
have "?bounded {} 0" by simp


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


78 
next


79 
fix S x


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


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


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


83 
proof (cases "x<k")


84 
case True


85 
with k show ?thesis by auto


86 
next


87 
case False


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


89 
thus ?thesis by auto


90 
qed


91 
qed


92 


93 
lemma finite_nat_iff_bounded:

15045

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

14442

95 
proof


96 
assume ?lhs


97 
thus ?rhs by (rule finite_nat_bounded)


98 
next


99 
assume ?rhs

15045

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

14442

101 
thus "finite S"


102 
by (rule finite_subset, simp)


103 
qed


104 


105 
lemma finite_nat_iff_bounded_le:


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


107 
proof


108 
assume ?lhs

15045

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

14442

110 
by (blast dest: finite_nat_bounded)


111 
hence "S \<subseteq> {..k}" by auto


112 
thus ?rhs ..


113 
next


114 
assume ?rhs


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


116 
thus "finite S"


117 
by (rule finite_subset, simp)


118 
qed


119 


120 
lemma infinite_nat_iff_unbounded:


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


122 
(is "?lhs = ?rhs")


123 
proof


124 
assume inf: ?lhs


125 
show ?rhs


126 
proof (rule ccontr)


127 
assume "\<not> ?rhs"


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


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


130 
by (auto simp add: sym[OF not_less_iff_le])


131 
with inf show "False"


132 
by (simp add: finite_nat_iff_bounded_le)


133 
qed


134 
next


135 
assume unbounded: ?rhs


136 
show ?lhs


137 
proof


138 
assume "finite S"


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


140 
by (auto simp add: finite_nat_iff_bounded_le)


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


142 
with unbounded show "False" by blast


143 
qed


144 
qed


145 


146 
lemma infinite_nat_iff_unbounded_le:


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


148 
(is "?lhs = ?rhs")


149 
proof


150 
assume inf: ?lhs


151 
show ?rhs


152 
proof


153 
fix m


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


155 
by (auto simp add: infinite_nat_iff_unbounded)


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


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


158 
qed


159 
next


160 
assume unbounded: ?rhs


161 
show ?lhs


162 
proof (auto simp add: infinite_nat_iff_unbounded)


163 
fix m


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


165 
by blast


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


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


168 
qed


169 
qed


170 


171 
text {*


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

14957

173 
to know that for any number larger than some @{text k}, there

14442

174 
is some larger number that is an element of the set.


175 
*}


176 


177 
lemma unbounded_k_infinite:


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


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


180 
proof (auto simp add: infinite_nat_iff_unbounded)


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


182 
proof (cases "k<m")


183 
case True


184 
with k show ?thesis by blast


185 
next


186 
case False


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


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


189 
thus ?thesis ..


190 
qed


191 
qed


192 


193 
theorem nat_infinite [simp]:


194 
"infinite (UNIV :: nat set)"


195 
by (auto simp add: infinite_nat_iff_unbounded)


196 


197 
theorem nat_not_finite [elim]:


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


199 
by simp


200 


201 
text {*


202 
Every infinite set contains a countable subset. More precisely

14957

203 
we show that a set @{text S} is infinite if and only if there exists


204 
an injective function from the naturals into @{text S}.

14442

205 
*}


206 


207 
lemma range_inj_infinite:


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


209 
proof


210 
assume "inj f"


211 
and "finite (range f)"


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


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


214 
thus "False" by simp


215 
qed


216 


217 
text {*


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


219 
construction of a sequence of pairwise different elements of

14957

220 
an infinite set @{text S}. The idea is to construct a sequence of


221 
nonempty and infinite subsets of @{text S} obtained by successively


222 
removing elements of @{text S}.

14442

223 
*}


224 


225 
lemma linorder_injI:


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


227 
shows "inj f"


228 
proof (rule inj_onI)


229 
fix x y


230 
assume f_eq: "f x = f y"


231 
show "x = y"


232 
proof (rule linorder_cases)


233 
assume "x < y"


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


235 
with f_eq show ?thesis by simp


236 
next


237 
assume "x = y"


238 
thus ?thesis .


239 
next


240 
assume "y < x"


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


242 
with f_eq show ?thesis by simp


243 
qed


244 
qed


245 


246 
lemma infinite_countable_subset:


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


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


249 
proof 

14766

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


251 
def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"

14442

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


253 
proof 


254 
fix n


255 
show "infinite (Sseq n)"


256 
proof (induct n)


257 
from inf show "infinite (Sseq 0)"


258 
by (simp add: Sseq_def)


259 
next


260 
fix n


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


262 
by (simp add: Sseq_def infinite_remove)


263 
qed


264 
qed


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


266 
proof 


267 
fix n


268 
show "Sseq n \<subseteq> S"


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


270 
qed


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


272 
proof 


273 
fix n


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


275 
proof (unfold pick_def, rule someI_ex)


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


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


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


279 
qed


280 
qed


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


282 
by auto


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


284 
proof 


285 
fix n m


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


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


288 
qed


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


290 
proof 


291 
fix n m


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


293 
moreover from pick_Sseq_gt


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


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


296 
by auto


297 
qed


298 
have inj: "inj pick"


299 
proof (rule linorder_injI)


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


301 
proof (clarify)


302 
fix i j


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


304 
and eq: "pick i = pick j"


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


306 
by (auto simp add: less_iff_Suc_add)


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


308 
with eq show "False" by simp


309 
qed


310 
qed


311 
from rng inj show ?thesis by auto


312 
qed


313 


314 
theorem infinite_iff_countable_subset:


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


316 
(is "?lhs = ?rhs")


317 
by (auto simp add: infinite_countable_subset


318 
range_inj_infinite infinite_super)


319 


320 
text {*


321 
For any function with infinite domain and finite range


322 
there is some element that is the image of infinitely


323 
many domain elements. In particular, any infinite sequence


324 
of elements from a finite set contains some element that


325 
occurs infinitely often.


326 
*}


327 


328 
theorem inf_img_fin_dom:


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


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


331 
proof (rule ccontr)


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


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


334 
by (blast intro: finite_UN_I)


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


336 
moreover note dom


337 
ultimately show "False"


338 
by (simp add: infinite_super)


339 
qed


340 


341 
theorems inf_img_fin_domE = inf_img_fin_dom[THEN bexE]


342 


343 


344 
subsection "Infinitely Many and Almost All"


345 


346 
text {*


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


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


349 
so we introduce corresponding binders and their proof rules.


350 
*}


351 


352 
consts


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


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


355 


356 
defs


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


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


359 


360 
syntax (xsymbols)


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


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


363 

14565

364 
syntax (HTML output)


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


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


367 

14442

368 
lemma INF_EX:


369 
"(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"


370 
proof (unfold INF_def, rule ccontr)


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


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


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


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


375 
with inf show "False" by simp


376 
qed


377 


378 
lemma MOST_iff_finiteNeg:


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


380 
by (simp add: MOST_def INF_def)


381 


382 
lemma ALL_MOST:


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


384 
by (simp add: MOST_iff_finiteNeg)


385 


386 
lemma INF_mono:


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


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


389 
proof 


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


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


392 
ultimately show ?thesis


393 
by (simp add: INF_def infinite_super)


394 
qed


395 


396 
lemma MOST_mono:


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


398 
by (unfold MOST_def, blast intro: INF_mono)


399 


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


401 
by (simp add: INF_def infinite_nat_iff_unbounded)


402 


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


404 
by (simp add: INF_def infinite_nat_iff_unbounded_le)


405 


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


407 
by (simp add: MOST_def INF_nat)


408 


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


410 
by (simp add: MOST_def INF_nat_le)


411 


412 


413 
subsection "Miscellaneous"


414 


415 
text {*


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


417 
These simplify the reasoning about deterministic automata.


418 
*}


419 


420 
constdefs


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


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


423 


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


425 
by (simp add: atmost_one_def)


426 


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


428 
by (simp add: atmost_one_def)


429 


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


431 
by (simp add: atmost_one_def)


432 


433 
end
