author hoelzl Sun Apr 12 11:33:50 2015 +0200 (2015-04-12) changeset 60039 d55937a8f97e parent 60038 ca431cbce2a3 child 60040 1fa1023b13b9
 src/HOL/Filter.thy file | annotate | diff | revisions
```     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
```