src/HOL/Filter.thy
changeset 61531 ab2e862263e7
parent 61378 3e04c9ca001a
child 61806 d2e62ae01cd8
     1.1 --- a/src/HOL/Filter.thy	Thu Oct 29 15:40:52 2015 +0100
     1.2 +++ b/src/HOL/Filter.thy	Mon Nov 02 11:56:28 2015 +0100
     1.3 @@ -393,6 +393,11 @@
     1.4  lemma eventually_happens: "eventually P net \<Longrightarrow> net = bot \<or> (\<exists>x. P x)"
     1.5    by (metis frequentlyE eventually_frequently)
     1.6  
     1.7 +lemma eventually_happens':
     1.8 +  assumes "F \<noteq> bot" "eventually P F"
     1.9 +  shows   "\<exists>x. P x"
    1.10 +  using assms eventually_frequently frequentlyE by blast
    1.11 +
    1.12  abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
    1.13    where "trivial_limit F \<equiv> F = bot"
    1.14  
    1.15 @@ -611,6 +616,15 @@
    1.16  lemma eventually_gt_at_top: "eventually (\<lambda>x. (c::_::{no_top, linorder}) < x) at_top"
    1.17    unfolding eventually_at_top_dense by auto
    1.18  
    1.19 +lemma eventually_all_ge_at_top:
    1.20 +  assumes "eventually P (at_top :: ('a :: linorder) filter)"
    1.21 +  shows   "eventually (\<lambda>x. \<forall>y\<ge>x. P y) at_top"
    1.22 +proof -
    1.23 +  from assms obtain x where "\<And>y. y \<ge> x \<Longrightarrow> P y" by (auto simp: eventually_at_top_linorder)
    1.24 +  hence "\<forall>z\<ge>y. P z" if "y \<ge> x" for y using that by simp
    1.25 +  thus ?thesis by (auto simp: eventually_at_top_linorder)
    1.26 +qed
    1.27 +
    1.28  definition at_bot :: "('a::order) filter"
    1.29    where "at_bot = (INF k. principal {.. k})"
    1.30