src/HOL/Filter.thy
changeset 60039 d55937a8f97e
parent 60038 ca431cbce2a3
child 60040 1fa1023b13b9
     1.1 --- a/src/HOL/Filter.thy	Sun Apr 12 11:33:44 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Sun Apr 12 11:33:50 2015 +0200
     1.3 @@ -613,6 +613,41 @@
     1.4    apply auto []
     1.5    done
     1.6  
     1.7 +subsection \<open> The cofinite filter \<close>
     1.8 +
     1.9 +definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
    1.10 +
    1.11 +lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
    1.12 +  unfolding cofinite_def
    1.13 +proof (rule eventually_Abs_filter, rule is_filter.intro)
    1.14 +  fix P Q :: "'a \<Rightarrow> bool" assume "finite {x. \<not> P x}" "finite {x. \<not> Q x}"
    1.15 +  from finite_UnI[OF this] show "finite {x. \<not> (P x \<and> Q x)}"
    1.16 +    by (rule rev_finite_subset) auto
    1.17 +next
    1.18 +  fix P Q :: "'a \<Rightarrow> bool" assume P: "finite {x. \<not> P x}" and *: "\<forall>x. P x \<longrightarrow> Q x"
    1.19 +  from * show "finite {x. \<not> Q x}"
    1.20 +    by (intro finite_subset[OF _ P]) auto
    1.21 +qed simp
    1.22 +
    1.23 +lemma cofinite_bot[simp]: "cofinite = (bot::'a filter) \<longleftrightarrow> finite (UNIV :: 'a set)"
    1.24 +  unfolding trivial_limit_def eventually_cofinite by simp
    1.25 +
    1.26 +lemma cofinite_eq_sequentially: "cofinite = sequentially"
    1.27 +  unfolding filter_eq_iff eventually_sequentially eventually_cofinite
    1.28 +proof safe
    1.29 +  fix P :: "nat \<Rightarrow> bool" assume [simp]: "finite {x. \<not> P x}"
    1.30 +  show "\<exists>N. \<forall>n\<ge>N. P n"
    1.31 +  proof cases
    1.32 +    assume "{x. \<not> P x} \<noteq> {}" then show ?thesis
    1.33 +      by (intro exI[of _ "Suc (Max {x. \<not> P x})"]) (auto simp: Suc_le_eq)
    1.34 +  qed auto
    1.35 +next
    1.36 +  fix P :: "nat \<Rightarrow> bool" and N :: nat assume "\<forall>n\<ge>N. P n"
    1.37 +  then have "{x. \<not> P x} \<subseteq> {..< N}"
    1.38 +    by (auto simp: not_le)
    1.39 +  then show "finite {x. \<not> P x}"
    1.40 +    by (blast intro: finite_subset)
    1.41 +qed
    1.42  
    1.43  subsection {* Limits *}
    1.44