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