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