111 subsection{*Existence of Free Ultrafilter over the Naturals*} |
111 subsection{*Existence of Free Ultrafilter over the Naturals*} |
112 |
112 |
113 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
113 text{*Also, proof of various properties of @{term FreeUltrafilterNat}: |
114 an arbitrary free ultrafilter*} |
114 an arbitrary free ultrafilter*} |
115 |
115 |
116 lemma FreeUltrafilterNat_Ex: "\<exists>U. U \<in> FreeUltrafilter (UNIV::nat set)" |
116 lemma FreeUltrafilterNat_Ex: "\<exists>U::nat set set. freeultrafilter U" |
117 by (rule not_finite_nat [THEN FreeUltrafilter_Ex]) |
117 by (rule not_finite_nat [THEN freeultrafilter_Ex]) |
118 |
118 |
119 lemma FreeUltrafilterNat_mem [simp]: |
119 lemma FreeUltrafilterNat_mem [simp]: "freeultrafilter FreeUltrafilterNat" |
120 "FreeUltrafilterNat \<in> FreeUltrafilter(UNIV:: nat set)" |
|
121 apply (unfold FreeUltrafilterNat_def) |
120 apply (unfold FreeUltrafilterNat_def) |
122 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
121 apply (rule someI_ex) |
123 apply (rule someI2, assumption+) |
122 apply (rule FreeUltrafilterNat_Ex) |
124 done |
123 done |
|
124 |
|
125 lemma UltrafilterNat_mem: "ultrafilter FreeUltrafilterNat" |
|
126 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.ultrafilter]) |
|
127 |
|
128 lemma FilterNat_mem: "filter FreeUltrafilterNat" |
|
129 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.filter]) |
125 |
130 |
126 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat" |
131 lemma FreeUltrafilterNat_finite: "finite x ==> x \<notin> FreeUltrafilterNat" |
127 apply (unfold FreeUltrafilterNat_def) |
132 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.finite]) |
128 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
|
129 apply (rule someI2, assumption) |
|
130 apply (blast dest: mem_FreeUltrafiltersetD1) |
|
131 done |
|
132 |
133 |
133 lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x" |
134 lemma FreeUltrafilterNat_not_finite: "x \<in> FreeUltrafilterNat ==> ~ finite x" |
134 by (blast dest: FreeUltrafilterNat_finite) |
135 by (rule FreeUltrafilterNat_mem [THEN freeultrafilter.infinite]) |
135 |
136 |
136 lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat" |
137 lemma FreeUltrafilterNat_empty [simp]: "{} \<notin> FreeUltrafilterNat" |
137 apply (unfold FreeUltrafilterNat_def) |
138 by (rule FilterNat_mem [THEN filter.empty]) |
138 apply (rule FreeUltrafilterNat_Ex [THEN exE]) |
|
139 apply (rule someI2, assumption) |
|
140 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter |
|
141 Filter_empty_not_mem) |
|
142 done |
|
143 |
139 |
144 lemma FreeUltrafilterNat_Int: |
140 lemma FreeUltrafilterNat_Int: |
145 "[| X \<in> FreeUltrafilterNat; Y \<in> FreeUltrafilterNat |] |
141 "[| X \<in> FreeUltrafilterNat; Y \<in> FreeUltrafilterNat |] |
146 ==> X Int Y \<in> FreeUltrafilterNat" |
142 ==> X Int Y \<in> FreeUltrafilterNat" |
147 apply (insert FreeUltrafilterNat_mem) |
143 by (rule FilterNat_mem [THEN filter.Int]) |
148 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD1) |
|
149 done |
|
150 |
144 |
151 lemma FreeUltrafilterNat_subset: |
145 lemma FreeUltrafilterNat_subset: |
152 "[| X \<in> FreeUltrafilterNat; X \<subseteq> Y |] |
146 "[| X \<in> FreeUltrafilterNat; X \<subseteq> Y |] |
153 ==> Y \<in> FreeUltrafilterNat" |
147 ==> Y \<in> FreeUltrafilterNat" |
154 apply (insert FreeUltrafilterNat_mem) |
148 by (rule FilterNat_mem [THEN filter.subset]) |
155 apply (blast dest: FreeUltrafilter_Ultrafilter Ultrafilter_Filter mem_FiltersetD2) |
|
156 done |
|
157 |
149 |
158 lemma FreeUltrafilterNat_Compl: |
150 lemma FreeUltrafilterNat_Compl: |
159 "X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
151 "X \<in> FreeUltrafilterNat ==> -X \<notin> FreeUltrafilterNat" |
160 proof |
152 apply (erule contrapos_pn) |
161 assume "X \<in> \<U>" and "- X \<in> \<U>" |
153 apply (erule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD2]) |
162 hence "X Int - X \<in> \<U>" by (rule FreeUltrafilterNat_Int) |
154 done |
163 thus False by force |
|
164 qed |
|
165 |
155 |
166 lemma FreeUltrafilterNat_Compl_mem: |
156 lemma FreeUltrafilterNat_Compl_mem: |
167 "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
157 "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat" |
168 apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]]) |
158 by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff, THEN iffD1]) |
169 apply (safe, drule_tac x = X in bspec) |
|
170 apply (auto) |
|
171 done |
|
172 |
159 |
173 lemma FreeUltrafilterNat_Compl_iff1: |
160 lemma FreeUltrafilterNat_Compl_iff1: |
174 "(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)" |
161 "(X \<notin> FreeUltrafilterNat) = (-X \<in> FreeUltrafilterNat)" |
175 by (blast dest: FreeUltrafilterNat_Compl FreeUltrafilterNat_Compl_mem) |
162 by (rule UltrafilterNat_mem [THEN ultrafilter.not_mem_iff]) |
176 |
163 |
177 lemma FreeUltrafilterNat_Compl_iff2: |
164 lemma FreeUltrafilterNat_Compl_iff2: |
178 "(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
165 "(X \<in> FreeUltrafilterNat) = (-X \<notin> FreeUltrafilterNat)" |
179 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
166 by (auto simp add: FreeUltrafilterNat_Compl_iff1 [symmetric]) |
180 |
167 |