14442

1 
(* Title: HOL/Infnite_Set.thy


2 
ID: $Id$


3 
Author: Stefan Merz


4 
*)


5 


6 
header {* Infnite Sets and Related Concepts*}


7 


8 
theory Infinite_Set = Hilbert_Choice + Finite_Set:


9 


10 
subsection "Infinite Sets"


11 


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


13 


14 
syntax


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


16 
translations


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


18 


19 
text {*


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


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


22 
*}


23 


24 
lemma infinite_nonempty:


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


26 
by simp


27 


28 
lemma infinite_remove:


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


30 
by simp


31 


32 
lemma Diff_infinite_finite:


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


34 
shows "infinite (ST)"


35 
using T


36 
proof (induct)


37 
from S


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


39 
next


40 
fix T x


41 
assume ih: "infinite (ST)"


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


43 
by (rule Diff_insert)


44 
with ih


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


46 
by (simp add: infinite_remove)


47 
qed


48 


49 
lemma Un_infinite:


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


51 
by simp


52 


53 
lemma infinite_super:


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


55 
shows "infinite T"


56 
proof (rule ccontr)


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


58 
with T


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


60 
with S


61 
show False by simp


62 
qed


63 


64 
text {*


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


66 
numbers is infinite.


67 
*}


68 


69 
lemma finite_nat_bounded:


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


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


72 
using S


73 
proof (induct)


74 
have "?bounded {} 0" by simp


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


76 
next


77 
fix S x


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


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


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


81 
proof (cases "x<k")


82 
case True


83 
with k show ?thesis by auto


84 
next


85 
case False


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


87 
thus ?thesis by auto


88 
qed


89 
qed


90 


91 
lemma finite_nat_iff_bounded:


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


93 
proof


94 
assume ?lhs


95 
thus ?rhs by (rule finite_nat_bounded)


96 
next


97 
assume ?rhs


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


99 
thus "finite S"


100 
by (rule finite_subset, simp)


101 
qed


102 


103 
lemma finite_nat_iff_bounded_le:


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


105 
proof


106 
assume ?lhs


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


108 
by (blast dest: finite_nat_bounded)


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


110 
thus ?rhs ..


111 
next


112 
assume ?rhs


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


114 
thus "finite S"


115 
by (rule finite_subset, simp)


116 
qed


117 


118 
lemma infinite_nat_iff_unbounded:


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


120 
(is "?lhs = ?rhs")


121 
proof


122 
assume inf: ?lhs


123 
show ?rhs


124 
proof (rule ccontr)


125 
assume "\<not> ?rhs"


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


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


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


129 
with inf show "False"


130 
by (simp add: finite_nat_iff_bounded_le)


131 
qed


132 
next


133 
assume unbounded: ?rhs


134 
show ?lhs


135 
proof


136 
assume "finite S"


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


138 
by (auto simp add: finite_nat_iff_bounded_le)


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


140 
with unbounded show "False" by blast


141 
qed


142 
qed


143 


144 
lemma infinite_nat_iff_unbounded_le:


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


146 
(is "?lhs = ?rhs")


147 
proof


148 
assume inf: ?lhs


149 
show ?rhs


150 
proof


151 
fix m


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


153 
by (auto simp add: infinite_nat_iff_unbounded)


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


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


156 
qed


157 
next


158 
assume unbounded: ?rhs


159 
show ?lhs


160 
proof (auto simp add: infinite_nat_iff_unbounded)


161 
fix m


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


163 
by blast


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


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


166 
qed


167 
qed


168 


169 
text {*


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


171 
to know that for any number larger than some $k$, there


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


173 
*}


174 


175 
lemma unbounded_k_infinite:


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


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


178 
proof (auto simp add: infinite_nat_iff_unbounded)


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


180 
proof (cases "k<m")


181 
case True


182 
with k show ?thesis by blast


183 
next


184 
case False


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


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


187 
thus ?thesis ..


188 
qed


189 
qed


190 


191 
theorem nat_infinite [simp]:


192 
"infinite (UNIV :: nat set)"


193 
by (auto simp add: infinite_nat_iff_unbounded)


194 


195 
theorem nat_not_finite [elim]:


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


197 
by simp


198 


199 
text {*


200 
Every infinite set contains a countable subset. More precisely


201 
we show that a set $S$ is infinite if and only if there exists


202 
an injective function from the naturals into $S$.


203 
*}


204 


205 
lemma range_inj_infinite:


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


207 
proof


208 
assume "inj f"


209 
and "finite (range f)"


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


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


212 
thus "False" by simp


213 
qed


214 


215 
text {*


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


217 
construction of a sequence of pairwise different elements of


218 
an infinite set $S$. The idea is to construct a sequence of


219 
nonempty and infinite subsets of $S$ obtained by successively


220 
removing elements of $S$.


221 
*}


222 


223 
lemma linorder_injI:


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


225 
shows "inj f"


226 
proof (rule inj_onI)


227 
fix x y


228 
assume f_eq: "f x = f y"


229 
show "x = y"


230 
proof (rule linorder_cases)


231 
assume "x < y"


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


233 
with f_eq show ?thesis by simp


234 
next


235 
assume "x = y"


236 
thus ?thesis .


237 
next


238 
assume "y < x"


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


240 
with f_eq show ?thesis by simp


241 
qed


242 
qed


243 


244 
lemma infinite_countable_subset:


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


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


247 
proof 


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


249 
def pick \<equiv> "\<lambda>n. (\<epsilon> e. e \<in> Sseq n)"


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


251 
proof 


252 
fix n


253 
show "infinite (Sseq n)"


254 
proof (induct n)


255 
from inf show "infinite (Sseq 0)"


256 
by (simp add: Sseq_def)


257 
next


258 
fix n


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


260 
by (simp add: Sseq_def infinite_remove)


261 
qed


262 
qed


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


264 
proof 


265 
fix n


266 
show "Sseq n \<subseteq> S"


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


268 
qed


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


270 
proof 


271 
fix n


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


273 
proof (unfold pick_def, rule someI_ex)


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


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


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


277 
qed


278 
qed


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


280 
by auto


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


282 
proof 


283 
fix n m


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


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


286 
qed


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


288 
proof 


289 
fix n m


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


291 
moreover from pick_Sseq_gt


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


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


294 
by auto


295 
qed


296 
have inj: "inj pick"


297 
proof (rule linorder_injI)


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


299 
proof (clarify)


300 
fix i j


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


302 
and eq: "pick i = pick j"


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


304 
by (auto simp add: less_iff_Suc_add)


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


306 
with eq show "False" by simp


307 
qed


308 
qed


309 
from rng inj show ?thesis by auto


310 
qed


311 


312 
theorem infinite_iff_countable_subset:


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


314 
(is "?lhs = ?rhs")


315 
by (auto simp add: infinite_countable_subset


316 
range_inj_infinite infinite_super)


317 


318 
text {*


319 
For any function with infinite domain and finite range


320 
there is some element that is the image of infinitely


321 
many domain elements. In particular, any infinite sequence


322 
of elements from a finite set contains some element that


323 
occurs infinitely often.


324 
*}


325 


326 
theorem inf_img_fin_dom:


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


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


329 
proof (rule ccontr)


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


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


332 
by (blast intro: finite_UN_I)


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


334 
moreover note dom


335 
ultimately show "False"


336 
by (simp add: infinite_super)


337 
qed


338 


339 
theorems inf_img_fin_domE = inf_img_fin_dom[THEN bexE]


340 


341 


342 
subsection "Infinitely Many and Almost All"


343 


344 
text {*


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


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


347 
so we introduce corresponding binders and their proof rules.


348 
*}


349 


350 
consts


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


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


353 


354 
defs


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


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


357 


358 
syntax (xsymbols)


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


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


361 


362 
lemma INF_EX:


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


364 
proof (unfold INF_def, rule ccontr)


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


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


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


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


369 
with inf show "False" by simp


370 
qed


371 


372 
lemma MOST_iff_finiteNeg:


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


374 
by (simp add: MOST_def INF_def)


375 


376 
lemma ALL_MOST:


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


378 
by (simp add: MOST_iff_finiteNeg)


379 


380 
lemma INF_mono:


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


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


383 
proof 


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


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


386 
ultimately show ?thesis


387 
by (simp add: INF_def infinite_super)


388 
qed


389 


390 
lemma MOST_mono:


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


392 
by (unfold MOST_def, blast intro: INF_mono)


393 


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


395 
by (simp add: INF_def infinite_nat_iff_unbounded)


396 


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


398 
by (simp add: INF_def infinite_nat_iff_unbounded_le)


399 


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


401 
by (simp add: MOST_def INF_nat)


402 


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


404 
by (simp add: MOST_def INF_nat_le)


405 


406 


407 
subsection "Miscellaneous"


408 


409 
text {*


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


411 
These simplify the reasoning about deterministic automata.


412 
*}


413 


414 
constdefs


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


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


417 


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


419 
by (simp add: atmost_one_def)


420 


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


422 
by (simp add: atmost_one_def)


423 


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


425 
by (simp add: atmost_one_def)


426 


427 
end
