author  wenzelm 
Wed, 28 Dec 2016 23:42:35 +0100  
changeset 64697  47c1e6b0886f 
parent 63993  9c0ff0c12116 
child 64967  1ab49aa7f3c0 
permissions  rwrr 
27407
68e111812b83
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
huffman
parents:
27368
diff
changeset

1 
(* Title: HOL/Library/Infinite_Set.thy 
20809  2 
Author: Stephan Merz 
3 
*) 

4 

60500  5 
section \<open>Infinite Sets and Related Concepts\<close> 
20809  6 

7 
theory Infinite_Set 

54612
7e291ae244ea
Backed out changeset: a8ad7f6dd217bypassing Main breaks theories that use \<inf> or \<sup>
traytel
parents:
54607
diff
changeset

8 
imports Main 
20809  9 
begin 
10 

61810  11 
text \<open>The set of natural numbers is infinite.\<close> 
20809  12 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

13 
lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

14 
using frequently_cofinite[of "\<lambda>x. x \<in> S"] 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

15 
by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

16 

1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

17 
lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

18 
using frequently_cofinite[of "\<lambda>x. x \<in> S"] 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

19 
by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense) 
20809  20 

59000  21 
lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})" 
60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

22 
using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) 
20809  23 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

24 
lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

25 
using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) 
20809  26 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

27 
lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

28 
by (simp add: finite_nat_iff_bounded) 
20809  29 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

30 

60500  31 
text \<open> 
20809  32 
For a set of natural numbers to be infinite, it is enough to know 
61585  33 
that for any number larger than some \<open>k\<close>, there is some larger 
20809  34 
number that is an element of the set. 
60500  35 
\<close> 
20809  36 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

37 
lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)" 
61810  38 
apply (clarsimp simp add: finite_nat_set_iff_bounded) 
39 
apply (drule_tac x="Suc (max m k)" in spec) 

40 
using less_Suc_eq by fastforce 

20809  41 

35056  42 
lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R" 
20809  43 
by simp 
44 

45 
lemma range_inj_infinite: 

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

47 
proof 

27407
68e111812b83
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
huffman
parents:
27368
diff
changeset

48 
assume "finite (range f)" and "inj f" 
20809  49 
then have "finite (UNIV::nat set)" 
27407
68e111812b83
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
huffman
parents:
27368
diff
changeset

50 
by (rule finite_imageD) 
20809  51 
then show False by simp 
52 
qed 

53 

61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

54 
text \<open>The set of integers is also infinite.\<close> 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

55 

d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

56 
lemma infinite_int_iff_infinite_nat_abs: "infinite (S::int set) \<longleftrightarrow> infinite ((nat o abs) ` S)" 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

57 
by (auto simp: transfer_nat_int_set_relations o_def image_comp dest: finite_image_absD) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

58 

61945  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)" 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

60 
apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded_le o_def image_def) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

61 
apply (metis abs_ge_zero nat_le_eq_zle le_nat_iff) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

62 
done 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

63 

61945  64 
proposition infinite_int_iff_unbounded: "infinite (S::int set) \<longleftrightarrow> (\<forall>m. \<exists>n. \<bar>n\<bar> > m \<and> n \<in> S)" 
61762
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

65 
apply (simp add: infinite_int_iff_infinite_nat_abs infinite_nat_iff_unbounded o_def image_def) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

66 
apply (metis (full_types) nat_le_iff nat_mono not_le) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

67 
done 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

68 

d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

69 
proposition finite_int_iff_bounded: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {..<k})" 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

70 
using infinite_int_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

71 

d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

72 
proposition finite_int_iff_bounded_le: "finite (S::int set) \<longleftrightarrow> (\<exists>k. abs ` S \<subseteq> {.. k})" 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

73 
using infinite_int_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le) 
d50b993b4fb9
Removal of redundant lemmas (diff_less_iff, diff_le_iff) and of the abbreviation Exp. Addition of some new material.
paulson <lp15@cam.ac.uk>
parents:
61585
diff
changeset

74 

20809  75 
subsection "Infinitely Many and Almost All" 
76 

60500  77 
text \<open> 
20809  78 
We often need to reason about the existence of infinitely many 
79 
(resp., all but finitely many) objects satisfying some predicate, so 

80 
we introduce corresponding binders and their proof rules. 

60500  81 
\<close> 
20809  82 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

83 
(* The following two lemmas are available as filterrules, but not in the simpset *) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

84 
lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

85 
lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually) 
34112  86 

87 
lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

88 
by (simp add: frequently_const_iff) 
34112  89 

90 
lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

91 
by (simp add: eventually_const_iff) 
20809  92 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

93 
lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

94 
by (simp only: imp_conv_disj frequently_disj_iff not_eventually) 
34112  95 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

96 
lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)" 
61810  97 
by (auto intro: eventually_rev_mp eventually_mono) 
34113  98 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

99 
lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x" 
61810  100 
by (rule frequently_rev_mp[of P]) (auto elim: eventually_mono) 
34112  101 

60500  102 
text \<open>Properties of quantifiers with injective functions.\<close> 
34112  103 

53239  104 
lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x" 
60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

105 
using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite) 
27407
68e111812b83
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
huffman
parents:
27368
diff
changeset

106 

53239  107 
lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)" 
60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

108 
using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite) 
34112  109 

60500  110 
text \<open>Properties of quantifiers with singletons.\<close> 
34112  111 

112 
lemma not_INFM_eq [simp]: 

113 
"\<not> (INFM x. x = a)" 

114 
"\<not> (INFM x. a = x)" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

115 
unfolding frequently_cofinite by simp_all 
34112  116 

117 
lemma MOST_neq [simp]: 

118 
"MOST x. x \<noteq> a" 

119 
"MOST x. a \<noteq> x" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

120 
unfolding eventually_cofinite by simp_all 
27407
68e111812b83
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
huffman
parents:
27368
diff
changeset

121 

34112  122 
lemma INFM_neq [simp]: 
123 
"(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)" 

124 
"(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

125 
unfolding frequently_cofinite by simp_all 
34112  126 

127 
lemma MOST_eq [simp]: 

128 
"(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)" 

129 
"(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

130 
unfolding eventually_cofinite by simp_all 
34112  131 

132 
lemma MOST_eq_imp: 

133 
"MOST x. x = a \<longrightarrow> P x" 

134 
"MOST x. a = x \<longrightarrow> P x" 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

135 
unfolding eventually_cofinite by simp_all 
34112  136 

60500  137 
text \<open>Properties of quantifiers over the naturals.\<close> 
27407
68e111812b83
rename lemmas INF_foo to INFM_foo; add new lemmas about MOST and INFM
huffman
parents:
27368
diff
changeset

138 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

139 
lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

140 
by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric]) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

141 

1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

142 
lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

143 
by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric]) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

144 

1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

145 
lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

146 
by (simp add: frequently_cofinite infinite_nat_iff_unbounded) 
20809  147 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

148 
lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

149 
by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

150 

1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

151 
lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

152 
by (simp add: eventually_frequently) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

153 

1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

154 
lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)" 
64697  155 
by (simp add: cofinite_eq_sequentially) 
20809  156 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

157 
lemma 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

158 
shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

159 
and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

160 
by (simp_all add: MOST_Suc_iff) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

161 

1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

162 
lemma MOST_ge_nat: "MOST n::nat. m \<le> n" 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

163 
by (simp add: cofinite_eq_sequentially eventually_ge_at_top) 
20809  164 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

165 
(* legacy names *) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

166 
lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

167 
lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

168 
lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

169 
lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

170 
lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

171 
lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

172 
lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1) 
61810  173 
lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_mono) 
60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

174 
lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

175 
lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

176 
lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

177 
lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

178 
lemma INFM_finite_Bex_distrib: "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" by (fact frequently_bex_finite_distrib) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

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) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

180 
lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

181 
lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI) 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

182 
lemmas MOST_iff_finiteNeg = MOST_iff_cofinite 
20809  183 

184 
subsection "Enumeration of an Infinite Set" 

185 

60500  186 
text \<open> 
20809  187 
The set's element type must be wellordered (e.g. the natural numbers). 
60500  188 
\<close> 
20809  189 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

190 
text \<open> 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

191 
Could be generalized to 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

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)"}. 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

193 
\<close> 
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

194 

53239  195 
primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" 
196 
where 

197 
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" 

20809  199 

53239  200 
lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S  {enumerate S 0}) n" 
20809  201 
by simp 
202 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

203 
lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S" 
53239  204 
apply (induct n arbitrary: S) 
205 
apply (fastforce intro: LeastI dest!: infinite_imp_nonempty) 

206 
apply simp 

207 
apply (metis DiffE infinite_remove) 

208 
done 

20809  209 

210 
declare enumerate_0 [simp del] enumerate_Suc [simp del] 

211 

212 
lemma enumerate_step: "infinite S \<Longrightarrow> enumerate S n < enumerate S (Suc n)" 

213 
apply (induct n arbitrary: S) 

214 
apply (rule order_le_neq_trans) 

215 
apply (simp add: enumerate_0 Least_le enumerate_in_set) 

216 
apply (simp only: enumerate_Suc') 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

217 
apply (subgoal_tac "enumerate (S  {enumerate S 0}) 0 \<in> S  {enumerate S 0}") 
20809  218 
apply (blast intro: sym) 
219 
apply (simp add: enumerate_in_set del: Diff_iff) 

220 
apply (simp add: enumerate_Suc') 

221 
done 

222 

60040
1fa1023b13b9
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
hoelzl
parents:
59506
diff
changeset

223 
lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n" 
20809  224 
apply (erule less_Suc_induct) 
225 
apply (auto intro: enumerate_step) 

226 
done 

227 

228 

50134  229 
lemma le_enumerate: 
230 
assumes S: "infinite S" 

231 
shows "n \<le> enumerate S n" 

61810  232 
using S 
50134  233 
proof (induct n) 
53239  234 
case 0 
235 
then show ?case by simp 

236 
next 

50134  237 
case (Suc n) 
238 
then have "n \<le> enumerate S n" by simp 

60500  239 
also note enumerate_mono[of n "Suc n", OF _ \<open>infinite S\<close>] 
50134  240 
finally show ?case by simp 
53239  241 
qed 
50134  242 

243 
lemma enumerate_Suc'': 

244 
fixes S :: "'a::wellorder set" 

53239  245 
assumes "infinite S" 
246 
shows "enumerate S (Suc n) = (LEAST s. s \<in> S \<and> enumerate S n < s)" 

247 
using assms 

50134  248 
proof (induct n arbitrary: S) 
249 
case 0 

53239  250 
then have "\<forall>s \<in> S. enumerate S 0 \<le> s" 
50134  251 
by (auto simp: enumerate.simps intro: Least_le) 
252 
then show ?case 

253 
unfolding enumerate_Suc' enumerate_0[of "S  {enumerate S 0}"] 

53239  254 
by (intro arg_cong[where f = Least] ext) auto 
50134  255 
next 
256 
case (Suc n S) 

257 
show ?case 

60500  258 
using enumerate_mono[OF zero_less_Suc \<open>infinite S\<close>, of n] \<open>infinite S\<close> 
50134  259 
apply (subst (1 2) enumerate_Suc') 
260 
apply (subst Suc) 

60500  261 
using \<open>infinite S\<close> 
53239  262 
apply simp 
263 
apply (intro arg_cong[where f = Least] ext) 

264 
apply (auto simp: enumerate_Suc'[symmetric]) 

265 
done 

50134  266 
qed 
267 

268 
lemma enumerate_Ex: 

269 
assumes S: "infinite (S::nat set)" 

270 
shows "s \<in> S \<Longrightarrow> \<exists>n. enumerate S n = s" 

271 
proof (induct s rule: less_induct) 

272 
case (less s) 

273 
show ?case 

274 
proof cases 

275 
let ?y = "Max {s'\<in>S. s' < s}" 

276 
assume "\<exists>y\<in>S. y < s" 

53239  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 

279 
then have y_in: "?y \<in> {s'\<in>S. s' < s}" 

280 
by (intro Max_in) auto 

281 
with less.hyps[of ?y] obtain n where "enumerate S n = ?y" 

282 
by auto 

50134  283 
with S have "enumerate S (Suc n) = s" 
284 
by (auto simp: y less enumerate_Suc'' intro!: Least_equality) 

285 
then show ?case by auto 

286 
next 

287 
assume *: "\<not> (\<exists>y\<in>S. y < s)" 

288 
then have "\<forall>t\<in>S. s \<le> t" by auto 

60500  289 
with \<open>s \<in> S\<close> show ?thesis 
50134  290 
by (auto intro!: exI[of _ 0] Least_equality simp: enumerate_0) 
291 
qed 

292 
qed 

293 

294 
lemma bij_enumerate: 

295 
fixes S :: "nat set" 

296 
assumes S: "infinite S" 

297 
shows "bij_betw (enumerate S) UNIV S" 

298 
proof  

299 
have "\<And>n m. n \<noteq> m \<Longrightarrow> enumerate S n \<noteq> enumerate S m" 

60500  300 
using enumerate_mono[OF _ \<open>infinite S\<close>] by (auto simp: neq_iff) 
50134  301 
then have "inj (enumerate S)" 
302 
by (auto simp: inj_on_def) 

53239  303 
moreover have "\<forall>s \<in> S. \<exists>i. enumerate S i = s" 
50134  304 
using enumerate_Ex[OF S] by auto 
60500  305 
moreover note \<open>infinite S\<close> 
50134  306 
ultimately show ?thesis 
307 
unfolding bij_betw_def by (auto intro: enumerate_in_set) 

308 
qed 

309 

63492
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

310 
text\<open>A pair of weird and wonderful lemmas from HOL Light\<close> 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

311 
lemma finite_transitivity_chain: 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

312 
assumes "finite A" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

313 
and R: "\<And>x. ~ R x x" "\<And>x y z. \<lbrakk>R x y; R y z\<rbrakk> \<Longrightarrow> R x z" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

314 
and A: "\<And>x. x \<in> A \<Longrightarrow> \<exists>y. y \<in> A \<and> R x y" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

315 
shows "A = {}" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

316 
using \<open>finite A\<close> A 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

317 
proof (induction A) 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

318 
case (insert a A) 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

319 
with R show ?case 
64697  320 
by (metis empty_iff insert_iff) 
63492
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

321 
qed simp 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

322 

a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

323 
corollary Union_maximal_sets: 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

324 
assumes "finite \<F>" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

325 
shows "\<Union>{T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} = \<Union>\<F>" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

326 
(is "?lhs = ?rhs") 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

327 
proof 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

328 
show "?rhs \<subseteq> ?lhs" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

329 
proof (rule Union_subsetI) 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

330 
fix S 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

331 
assume "S \<in> \<F>" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

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)" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

333 
apply (rule finite_transitivity_chain [of _ "\<lambda>T U. S \<subseteq> T \<and> T \<subset> U"]) 
63993  334 
using assms that apply auto 
63492
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

335 
by (blast intro: dual_order.trans psubset_imp_subset) 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

336 
then show "\<exists>y. y \<in> {T \<in> \<F>. \<forall>U\<in>\<F>. \<not> T \<subset> U} \<and> S \<subseteq> y" 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

337 
using \<open>S \<in> \<F>\<close> by blast 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

338 
qed 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

339 
qed force 
a662e8139804
More advanced theorems about retracts, homotopies., etc
paulson <lp15@cam.ac.uk>
parents:
61945
diff
changeset

340 

20809  341 
end 
54612
7e291ae244ea
Backed out changeset: a8ad7f6dd217bypassing Main breaks theories that use \<inf> or \<sup>
traytel
parents:
54607
diff
changeset

342 