author | wenzelm |
Wed, 17 May 2017 13:47:19 +0200 | |
changeset 65851 | c103358a5559 |
parent 64435 | c93b0e6131c3 |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
62479 | 1 |
(* Title: HOL/Nonstandard_Analysis/Free_Ultrafilter.thy |
41589 | 2 |
Author: Jacques D. Fleuriot, University of Cambridge |
3 |
Author: Lawrence C Paulson |
|
4 |
Author: Brian Huffman |
|
64435 | 5 |
*) |
27468 | 6 |
|
61975 | 7 |
section \<open>Filters and Ultrafilters\<close> |
27468 | 8 |
|
60036 | 9 |
theory Free_Ultrafilter |
64435 | 10 |
imports "~~/src/HOL/Library/Infinite_Set" |
27468 | 11 |
begin |
12 |
||
64435 | 13 |
|
61975 | 14 |
subsection \<open>Definitions and basic properties\<close> |
27468 | 15 |
|
61975 | 16 |
subsubsection \<open>Ultrafilters\<close> |
27468 | 17 |
|
60041 | 18 |
locale ultrafilter = |
19 |
fixes F :: "'a filter" |
|
20 |
assumes proper: "F \<noteq> bot" |
|
21 |
assumes ultra: "eventually P F \<or> eventually (\<lambda>x. \<not> P x) F" |
|
47486
4d49f3ffe97e
replace locale 'UFT' with new un-named context block feature;
huffman
parents:
46008
diff
changeset
|
22 |
begin |
27468 | 23 |
|
60041 | 24 |
lemma eventually_imp_frequently: "frequently P F \<Longrightarrow> eventually P F" |
25 |
using ultra[of P] by (simp add: frequently_def) |
|
27468 | 26 |
|
60041 | 27 |
lemma frequently_eq_eventually: "frequently P F = eventually P F" |
28 |
using eventually_imp_frequently eventually_frequently[OF proper] .. |
|
27468 | 29 |
|
60041 | 30 |
lemma eventually_disj_iff: "eventually (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> eventually P F \<or> eventually Q F" |
31 |
unfolding frequently_eq_eventually[symmetric] frequently_disj_iff .. |
|
27468 | 32 |
|
60041 | 33 |
lemma eventually_all_iff: "eventually (\<lambda>x. \<forall>y. P x y) F = (\<forall>Y. eventually (\<lambda>x. P x (Y x)) F)" |
34 |
using frequently_all[of P F] by (simp add: frequently_eq_eventually) |
|
27468 | 35 |
|
60041 | 36 |
lemma eventually_imp_iff: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longrightarrow> eventually Q F)" |
37 |
using frequently_imp_iff[of P Q F] by (simp add: frequently_eq_eventually) |
|
27468 | 38 |
|
60041 | 39 |
lemma eventually_iff_iff: "eventually (\<lambda>x. P x \<longleftrightarrow> Q x) F \<longleftrightarrow> (eventually P F \<longleftrightarrow> eventually Q F)" |
40 |
unfolding iff_conv_conj_imp eventually_conj_iff eventually_imp_iff by simp |
|
27468 | 41 |
|
60041 | 42 |
lemma eventually_not_iff: "eventually (\<lambda>x. \<not> P x) F \<longleftrightarrow> \<not> eventually P F" |
43 |
unfolding not_eventually frequently_eq_eventually .. |
|
27468 | 44 |
|
47486
4d49f3ffe97e
replace locale 'UFT' with new un-named context block feature;
huffman
parents:
46008
diff
changeset
|
45 |
end |
4d49f3ffe97e
replace locale 'UFT' with new un-named context block feature;
huffman
parents:
46008
diff
changeset
|
46 |
|
64435 | 47 |
|
61975 | 48 |
subsection \<open>Maximal filter = Ultrafilter\<close> |
27468 | 49 |
|
61975 | 50 |
text \<open> |
64435 | 51 |
A filter \<open>F\<close> is an ultrafilter iff it is a maximal filter, |
52 |
i.e. whenever \<open>G\<close> is a filter and @{prop "F \<subseteq> G"} then @{prop "F = G"} |
|
61975 | 53 |
\<close> |
64435 | 54 |
|
61975 | 55 |
text \<open> |
64435 | 56 |
Lemma that shows existence of an extension to what was assumed to |
27468 | 57 |
be a maximal filter. Will be used to derive contradiction in proof of |
58 |
property of ultrafilter. |
|
61975 | 59 |
\<close> |
27468 | 60 |
|
64435 | 61 |
lemma extend_filter: "frequently P F \<Longrightarrow> inf F (principal {x. P x}) \<noteq> bot" |
62 |
by (simp add: trivial_limit_def eventually_inf_principal not_eventually) |
|
27468 | 63 |
|
60041 | 64 |
lemma max_filter_ultrafilter: |
64435 | 65 |
assumes "F \<noteq> bot" |
60041 | 66 |
assumes max: "\<And>G. G \<noteq> bot \<Longrightarrow> G \<le> F \<Longrightarrow> F = G" |
67 |
shows "ultrafilter F" |
|
68 |
proof |
|
64435 | 69 |
show "eventually P F \<or> (\<forall>\<^sub>Fx in F. \<not> P x)" for P |
60041 | 70 |
proof (rule disjCI) |
71 |
assume "\<not> (\<forall>\<^sub>Fx in F. \<not> P x)" |
|
72 |
then have "inf F (principal {x. P x}) \<noteq> bot" |
|
73 |
by (simp add: not_eventually extend_filter) |
|
74 |
then have F: "F = inf F (principal {x. P x})" |
|
75 |
by (rule max) simp |
|
76 |
show "eventually P F" |
|
77 |
by (subst F) (simp add: eventually_inf_principal) |
|
27468 | 78 |
qed |
60041 | 79 |
qed fact |
27468 | 80 |
|
60041 | 81 |
lemma le_filter_frequently: "F \<le> G \<longleftrightarrow> (\<forall>P. frequently P F \<longrightarrow> frequently P G)" |
82 |
unfolding frequently_def le_filter_def |
|
83 |
apply auto |
|
84 |
apply (erule_tac x="\<lambda>x. \<not> P x" in allE) |
|
85 |
apply auto |
|
86 |
done |
|
27468 | 87 |
|
88 |
lemma (in ultrafilter) max_filter: |
|
64435 | 89 |
assumes G: "G \<noteq> bot" |
90 |
and sub: "G \<le> F" |
|
91 |
shows "F = G" |
|
60041 | 92 |
proof (rule antisym) |
93 |
show "F \<le> G" |
|
94 |
using sub |
|
95 |
by (auto simp: le_filter_frequently[of F] frequently_eq_eventually le_filter_def[of G] |
|
96 |
intro!: eventually_frequently G proper) |
|
97 |
qed fact |
|
27468 | 98 |
|
64435 | 99 |
|
61975 | 100 |
subsection \<open>Ultrafilter Theorem\<close> |
27468 | 101 |
|
60041 | 102 |
lemma ex_max_ultrafilter: |
103 |
fixes F :: "'a filter" |
|
104 |
assumes F: "F \<noteq> bot" |
|
105 |
shows "\<exists>U\<le>F. ultrafilter U" |
|
106 |
proof - |
|
107 |
let ?X = "{G. G \<noteq> bot \<and> G \<le> F}" |
|
108 |
let ?R = "{(b, a). a \<noteq> bot \<and> a \<le> b \<and> b \<le> F}" |
|
27468 | 109 |
|
64435 | 110 |
have bot_notin_R: "c \<in> Chains ?R \<Longrightarrow> bot \<notin> c" for c |
60041 | 111 |
by (auto simp: Chains_def) |
27468 | 112 |
|
60041 | 113 |
have [simp]: "Field ?R = ?X" |
114 |
by (auto simp: Field_def bot_unique) |
|
27468 | 115 |
|
64435 | 116 |
have "\<exists>m\<in>Field ?R. \<forall>a\<in>Field ?R. (m, a) \<in> ?R \<longrightarrow> a = m" (is "\<exists>m\<in>?A. ?B m") |
60041 | 117 |
proof (rule Zorns_po_lemma) |
118 |
show "Partial_order ?R" |
|
64435 | 119 |
by (auto simp: partial_order_on_def preorder_on_def |
120 |
antisym_def refl_on_def trans_def Field_def bot_unique) |
|
60041 | 121 |
show "\<forall>C\<in>Chains ?R. \<exists>u\<in>Field ?R. \<forall>a\<in>C. (a, u) \<in> ?R" |
122 |
proof (safe intro!: bexI del: notI) |
|
64435 | 123 |
fix c x |
124 |
assume c: "c \<in> Chains ?R" |
|
27468 | 125 |
|
64435 | 126 |
have Inf_c: "Inf c \<noteq> bot" "Inf c \<le> F" if "c \<noteq> {}" |
127 |
proof - |
|
128 |
from c that have "Inf c = bot \<longleftrightarrow> (\<exists>x\<in>c. x = bot)" |
|
60041 | 129 |
unfolding trivial_limit_def by (intro eventually_Inf_base) (auto simp: Chains_def) |
64435 | 130 |
with c show "Inf c \<noteq> bot" |
60041 | 131 |
by (simp add: bot_notin_R) |
64435 | 132 |
from that obtain x where "x \<in> c" by auto |
133 |
with c show "Inf c \<le> F" |
|
60041 | 134 |
by (auto intro!: Inf_lower2[of x] simp: Chains_def) |
64435 | 135 |
qed |
60041 | 136 |
then have [simp]: "inf F (Inf c) = (if c = {} then F else Inf c)" |
137 |
using c by (auto simp add: inf_absorb2) |
|
27468 | 138 |
|
64435 | 139 |
from c show "inf F (Inf c) \<noteq> bot" |
140 |
by (simp add: F Inf_c) |
|
141 |
from c show "inf F (Inf c) \<in> Field ?R" |
|
142 |
by (simp add: Chains_def Inf_c F) |
|
27468 | 143 |
|
64435 | 144 |
assume "x \<in> c" |
60041 | 145 |
with c show "inf F (Inf c) \<le> x" "x \<le> F" |
146 |
by (auto intro: Inf_lower simp: Chains_def) |
|
147 |
qed |
|
148 |
qed |
|
64435 | 149 |
then obtain U where U: "U \<in> ?A" "?B U" .. |
150 |
show ?thesis |
|
151 |
proof |
|
152 |
from U show "U \<le> F \<and> ultrafilter U" |
|
153 |
by (auto intro!: max_filter_ultrafilter) |
|
154 |
qed |
|
27468 | 155 |
qed |
156 |
||
64435 | 157 |
|
61975 | 158 |
subsubsection \<open>Free Ultrafilters\<close> |
27468 | 159 |
|
64435 | 160 |
text \<open>There exists a free ultrafilter on any infinite set.\<close> |
27468 | 161 |
|
60041 | 162 |
locale freeultrafilter = ultrafilter + |
163 |
assumes infinite: "eventually P F \<Longrightarrow> infinite {x. P x}" |
|
164 |
begin |
|
165 |
||
166 |
lemma finite: "finite {x. P x} \<Longrightarrow> \<not> eventually P F" |
|
64435 | 167 |
by (erule contrapos_pn) (erule infinite) |
60041 | 168 |
|
169 |
lemma finite': "finite {x. \<not> P x} \<Longrightarrow> eventually P F" |
|
170 |
by (drule finite) (simp add: not_eventually frequently_eq_eventually) |
|
171 |
||
172 |
lemma le_cofinite: "F \<le> cofinite" |
|
173 |
by (intro filter_leI) |
|
64435 | 174 |
(auto simp add: eventually_cofinite not_eventually frequently_eq_eventually dest!: finite) |
60041 | 175 |
|
176 |
lemma singleton: "\<not> eventually (\<lambda>x. x = a) F" |
|
64435 | 177 |
by (rule finite) simp |
60041 | 178 |
|
179 |
lemma singleton': "\<not> eventually (op = a) F" |
|
64435 | 180 |
by (rule finite) simp |
60041 | 181 |
|
182 |
lemma ultrafilter: "ultrafilter F" .. |
|
183 |
||
184 |
end |
|
185 |
||
47486
4d49f3ffe97e
replace locale 'UFT' with new un-named context block feature;
huffman
parents:
46008
diff
changeset
|
186 |
lemma freeultrafilter_Ex: |
60041 | 187 |
assumes [simp]: "infinite (UNIV :: 'a set)" |
188 |
shows "\<exists>U::'a filter. freeultrafilter U" |
|
27468 | 189 |
proof - |
60041 | 190 |
from ex_max_ultrafilter[of "cofinite :: 'a filter"] |
191 |
obtain U :: "'a filter" where "U \<le> cofinite" "ultrafilter U" |
|
192 |
by auto |
|
193 |
interpret ultrafilter U by fact |
|
194 |
have "freeultrafilter U" |
|
195 |
proof |
|
64435 | 196 |
fix P |
197 |
assume "eventually P U" |
|
60041 | 198 |
with proper have "frequently P U" |
199 |
by (rule eventually_frequently) |
|
200 |
then have "frequently P cofinite" |
|
61975 | 201 |
using \<open>U \<le> cofinite\<close> by (simp add: le_filter_frequently) |
60041 | 202 |
then show "infinite {x. P x}" |
203 |
by (simp add: frequently_cofinite) |
|
27468 | 204 |
qed |
46008
c296c75f4cf4
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
wenzelm
parents:
41959
diff
changeset
|
205 |
then show ?thesis .. |
27468 | 206 |
qed |
207 |
||
47486
4d49f3ffe97e
replace locale 'UFT' with new un-named context block feature;
huffman
parents:
46008
diff
changeset
|
208 |
end |