# HG changeset patch
# User hoelzl
# Date 1428831249 -7200
# Node ID 1fa1023b13b9cb1fcf810859213afffd2a506162
# Parent  d55937a8f97e9a0158eabdf149a4e3eeaab6121b
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter

diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/Filter.thy
--- a/src/HOL/Filter.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/Filter.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -63,6 +63,9 @@
   thus "eventually P F" by simp
 qed
 
+lemma eventuallyI: "(\<And>x. P x) \<Longrightarrow> eventually P F"
+  by (auto intro: always_eventually)
+
 lemma eventually_mono:
   "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
   unfolding eventually_def
@@ -75,17 +78,6 @@
   using assms unfolding eventually_def
   by (rule is_filter.conj [OF is_filter_Rep_filter])
 
-lemma eventually_Ball_finite:
-  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
-using assms by (induct set: finite, simp, simp add: eventually_conj)
-
-lemma eventually_all_finite:
-  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
-  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
-  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
-using eventually_Ball_finite [of UNIV P] assms by simp
-
 lemma eventually_mp:
   assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   assumes "eventually (\<lambda>x. P x) F"
@@ -119,6 +111,29 @@
   shows "eventually (\<lambda>i. R i) F"
   using assms by (auto elim!: eventually_rev_mp)
 
+lemma eventually_ball_finite_distrib:
+  "finite A \<Longrightarrow> (eventually (\<lambda>x. \<forall>y\<in>A. P x y) net) \<longleftrightarrow> (\<forall>y\<in>A. eventually (\<lambda>x. P x y) net)"
+  by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)
+
+lemma eventually_ball_finite:
+  "finite A \<Longrightarrow> \<forall>y\<in>A. eventually (\<lambda>x. P x y) net \<Longrightarrow> eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
+  by (auto simp: eventually_ball_finite_distrib)
+
+lemma eventually_all_finite:
+  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
+  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
+  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
+using eventually_ball_finite [of UNIV P] assms by simp
+
+lemma eventually_ex: "(\<forall>\<^sub>Fx in F. \<exists>y. P x y) \<longleftrightarrow> (\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x))"
+proof
+  assume "\<forall>\<^sub>Fx in F. \<exists>y. P x y"
+  then have "\<forall>\<^sub>Fx in F. P x (SOME y. P x y)"
+    by (auto intro: someI_ex eventually_elim1)
+  then show "\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x)"
+    by auto
+qed (auto intro: eventually_elim1)
+
 lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   by (auto intro: eventually_mp)
 
@@ -135,6 +150,93 @@
   then show ?thesis by (auto elim: eventually_elim2)
 qed
 
+subsection \<open> Frequently as dual to eventually \<close>
+
+definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
+  where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
+
+syntax (xsymbols)
+  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
+
+translations
+  "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
+
+lemma not_frequently_False [simp]: "\<not> (\<exists>\<^sub>Fx in F. False)"
+  by (simp add: frequently_def)
+
+lemma frequently_ex: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>x. P x"
+  by (auto simp: frequently_def dest: not_eventuallyD)
+
+lemma frequentlyE: assumes "frequently P F" obtains x where "P x"
+  using frequently_ex[OF assms] by auto
+
+lemma frequently_mp:
+  assumes ev: "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x" and P: "\<exists>\<^sub>Fx in F. P x" shows "\<exists>\<^sub>Fx in F. Q x"
+proof - 
+  from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
+    by (rule eventually_rev_mp) (auto intro!: always_eventually)
+  from eventually_mp[OF this] P show ?thesis
+    by (auto simp: frequently_def)
+qed
+
+lemma frequently_rev_mp:
+  assumes "\<exists>\<^sub>Fx in F. P x"
+  assumes "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x"
+  shows "\<exists>\<^sub>Fx in F. Q x"
+using assms(2) assms(1) by (rule frequently_mp)
+
+lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
+  using frequently_mp[of P Q] by (simp add: always_eventually)
+
+lemma frequently_elim1: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> (\<And>i. P i \<Longrightarrow> Q i) \<Longrightarrow> \<exists>\<^sub>Fx in F. Q x"
+  by (metis frequently_mono)
+
+lemma frequently_disj_iff: "(\<exists>\<^sub>Fx in F. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<or> (\<exists>\<^sub>Fx in F. Q x)"
+  by (simp add: frequently_def eventually_conj_iff)
+
+lemma frequently_disj: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>\<^sub>Fx in F. Q x \<Longrightarrow> \<exists>\<^sub>Fx in F. P x \<or> Q x"
+  by (simp add: frequently_disj_iff)
+
+lemma frequently_bex_finite_distrib:
+  assumes "finite A" shows "(\<exists>\<^sub>Fx in F. \<exists>y\<in>A. P x y) \<longleftrightarrow> (\<exists>y\<in>A. \<exists>\<^sub>Fx in F. P x y)"
+  using assms by induction (auto simp: frequently_disj_iff)
+
+lemma frequently_bex_finite: "finite A \<Longrightarrow> \<exists>\<^sub>Fx in F. \<exists>y\<in>A. P x y \<Longrightarrow> \<exists>y\<in>A. \<exists>\<^sub>Fx in F. P x y"
+  by (simp add: frequently_bex_finite_distrib)
+
+lemma frequently_all: "(\<exists>\<^sub>Fx in F. \<forall>y. P x y) \<longleftrightarrow> (\<forall>Y. \<exists>\<^sub>Fx in F. P x (Y x))"
+  using eventually_ex[of "\<lambda>x y. \<not> P x y" F] by (simp add: frequently_def)
+
+lemma
+  shows not_eventually: "\<not> eventually P F \<longleftrightarrow> (\<exists>\<^sub>Fx in F. \<not> P x)"
+    and not_frequently: "\<not> frequently P F \<longleftrightarrow> (\<forall>\<^sub>Fx in F. \<not> P x)"
+  by (auto simp: frequently_def)
+
+lemma frequently_imp_iff:
+  "(\<exists>\<^sub>Fx in F. P x \<longrightarrow> Q x) \<longleftrightarrow> (eventually P F \<longrightarrow> frequently Q F)"
+  unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..
+
+lemma eventually_frequently_const_simps:
+  "(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
+  "(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
+  "(\<forall>\<^sub>Fx in F. P x \<or> C) \<longleftrightarrow> (\<forall>\<^sub>Fx in F. P x) \<or> C"
+  "(\<forall>\<^sub>Fx in F. C \<or> P x) \<longleftrightarrow> C \<or> (\<forall>\<^sub>Fx in F. P x)"
+  "(\<forall>\<^sub>Fx in F. P x \<longrightarrow> C) \<longleftrightarrow> ((\<exists>\<^sub>Fx in F. P x) \<longrightarrow> C)"
+  "(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
+  by (cases C; simp add: not_frequently)+
+
+lemmas eventually_frequently_simps = 
+  eventually_frequently_const_simps
+  not_eventually
+  eventually_conj_iff
+  eventually_ball_finite_distrib
+  eventually_ex
+  not_frequently
+  frequently_disj_iff
+  frequently_bex_finite_distrib
+  frequently_all
+  frequently_imp_iff
+
 ML {*
   fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
     let
@@ -154,54 +256,6 @@
   Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
 *} "elimination of eventually quantifiers"
 
-subsection \<open> Frequently as dual to eventually \<close>
-
-definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
-  where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
-
-syntax (xsymbols)
-  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
-
-translations
-  "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
-
-lemma not_frequently_False [simp]: "\<not> frequently (\<lambda>x. False) F"
-  by (simp add: frequently_def)
-
-lemma frequently_ex: "frequently P F \<Longrightarrow> \<exists>x. P x"
-  by (auto simp: frequently_def dest: not_eventuallyD)
-
-lemma frequently_mp:
-  assumes ev: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" and P: "frequently (\<lambda>x. P x) F"
-  shows "frequently (\<lambda>x. Q x) F"
-proof - 
-  from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
-    by (rule eventually_rev_mp) (auto intro!: always_eventually)
-  from eventually_mp[OF this] P show ?thesis
-    by (auto simp: frequently_def)
-qed
-
-lemma frequently_rev_mp:
-  assumes "frequently (\<lambda>x. P x) F"
-  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
-  shows "frequently (\<lambda>x. Q x) F"
-using assms(2) assms(1) by (rule frequently_mp)
-
-lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
-  using frequently_mp[of P Q] by (simp add: always_eventually)
-
-lemma frequently_disj_iff:
-  "frequently (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> frequently (\<lambda>x. P x) F \<or> frequently (\<lambda>x. Q x) F"
-  by (simp add: frequently_def eventually_conj_iff)
-
-lemma frequently_disj:
-  "frequently (\<lambda>x. P x) F \<Longrightarrow> frequently (\<lambda>x. Q x) F \<Longrightarrow> frequently (\<lambda>x. P x \<or> Q x) F"
-  by (simp add: frequently_disj_iff)
-
-lemma frequently_Bex_finite:
-  assumes "finite A" shows "frequently (\<lambda>x. \<exists>y\<in>A. P x y) net \<longleftrightarrow> (\<exists>y\<in>A. frequently (\<lambda>x. P x y) net)"
-  using assms by induction (auto simp: frequently_disj_iff)
-
 subsubsection {* Finer-than relation *}
 
 text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
@@ -318,15 +372,28 @@
   "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
 
+lemma eventually_frequently: "F \<noteq> bot \<Longrightarrow> eventually P F \<Longrightarrow> frequently P F"
+  using eventually_conj[of P F "\<lambda>x. \<not> P x"]
+  by (auto simp add: frequently_def eventually_False)
+
+lemma eventually_const_iff: "eventually (\<lambda>x. P) F \<longleftrightarrow> P \<or> F = bot"
+  by (cases P) (auto simp: eventually_False)
+
+lemma eventually_const[simp]: "F \<noteq> bot \<Longrightarrow> eventually (\<lambda>x. P) F \<longleftrightarrow> P"
+  by (simp add: eventually_const_iff)
+
+lemma frequently_const_iff: "frequently (\<lambda>x. P) F \<longleftrightarrow> P \<and> F \<noteq> bot"
+  by (simp add: frequently_def eventually_const_iff)
+
+lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
+  by (simp add: frequently_const_iff)
+
 abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   where "trivial_limit F \<equiv> F = bot"
 
 lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   by (rule eventually_False [symmetric])
 
-lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
-  by (cases P) (simp_all add: eventually_False)
-
 lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
 proof -
   let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
@@ -601,22 +668,30 @@
   shows "eventually P sequentially"
 using assms by (auto simp: eventually_sequentially)
 
-lemma eventually_sequentially_seg:
-  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
-  unfolding eventually_sequentially
-  apply safe
-   apply (rule_tac x="N + k" in exI)
-   apply rule
-   apply (erule_tac x="n - k" in allE)
-   apply auto []
-  apply (rule_tac x=N in exI)
-  apply auto []
-  done
+lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
+  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
+
+lemma eventually_sequentially_seg: "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
+  using eventually_sequentially_Suc[of "\<lambda>n. P (n + k)" for k] by (induction k) auto
 
 subsection \<open> The cofinite filter \<close>
 
 definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
 
+abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
+  "Inf_many P \<equiv> frequently P cofinite"
+
+abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
+  "Alm_all P \<equiv> eventually P cofinite"
+
+notation (xsymbols)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
+  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
+
+notation (HTML output)
+  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
+  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
+
 lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
   unfolding cofinite_def
 proof (rule eventually_Abs_filter, rule is_filter.intro)
@@ -629,6 +704,9 @@
     by (intro finite_subset[OF _ P]) auto
 qed simp
 
+lemma frequently_cofinite: "frequently P cofinite \<longleftrightarrow> \<not> finite {x. P x}"
+  by (simp add: frequently_def eventually_cofinite)
+
 lemma cofinite_bot[simp]: "cofinite = (bot::'a filter) \<longleftrightarrow> finite (UNIV :: 'a set)"
   unfolding trivial_limit_def eventually_cofinite by simp
 
@@ -737,9 +815,6 @@
   "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   unfolding filterlim_def filtermap_sup by auto
 
-lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
-  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
-
 lemma filterlim_sequentially_Suc:
   "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
   unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/HOLCF/Library/Defl_Bifinite.thy
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -12,38 +12,6 @@
 
 default_sort type
 
-lemma MOST_INFM:
-  assumes inf: "infinite (UNIV::'a set)"
-  shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
-  unfolding Alm_all_def Inf_many_def
-  apply (auto simp add: Collect_neg_eq)
-  apply (drule (1) finite_UnI)
-  apply (simp add: Compl_partition2 inf)
-  done
-
-lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
-by (rule MOST_inj [OF _ inj_Suc])
-
-lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
-unfolding MOST_nat
-apply (clarify, rule_tac x="Suc m" in exI, clarify)
-apply (erule Suc_lessE, simp)
-done
-
-lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
-by (rule iffI [OF MOST_SucD MOST_SucI])
-
-lemma INFM_finite_Bex_distrib:
-  "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
-by (induct set: finite, simp, simp add: INFM_disj_distrib)
-
-lemma MOST_finite_Ball_distrib:
-  "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
-by (induct set: finite, simp, simp add: MOST_conj_distrib)
-
-lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
-unfolding MOST_nat_le by fast
-
 subsection {* Eventually constant sequences *}
 
 definition
diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/HOLCF/Plain_HOLCF.thy
--- a/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -12,4 +12,6 @@
   Basic HOLCF concepts and types; does not include definition packages.
 *}
 
+hide_const (open) Filter.principal
+
 end
diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -67,36 +67,22 @@
   infinite.
 *}
 
-lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\<exists>k. S \<subseteq> {..<k}"
-proof cases
-  assume "S \<noteq> {}" with Max_less_iff[OF S this] show ?thesis
-    by auto
-qed simp
+lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
+  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
+  by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
+
+lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
+  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
+  by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
 
 lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
-  by (auto intro: finite_nat_bounded dest: finite_subset)
+  using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
 
-lemma finite_nat_iff_bounded_le:
-  "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})"  (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?lhs
-  then obtain k where "S \<subseteq> {..<k}"
-    by (blast dest: finite_nat_bounded)
-  then have "S \<subseteq> {..k}" by auto
-  then show ?rhs ..
-next
-  assume ?rhs
-  then obtain k where "S \<subseteq> {..k}" ..
-  then show "finite S"
-    by (rule finite_subset) simp
-qed
+lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
+  using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
 
-lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
-  unfolding finite_nat_iff_bounded_le by (auto simp: subset_eq not_le)
-
-lemma infinite_nat_iff_unbounded_le:
-  "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)"
-  unfolding finite_nat_iff_bounded by (auto simp: subset_eq not_less)
+lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
+  by (simp add: finite_nat_iff_bounded)
 
 text {*
   For a set of natural numbers to be infinite, it is enough to know
@@ -104,25 +90,9 @@
   number that is an element of the set.
 *}
 
-lemma unbounded_k_infinite:
-  assumes k: "\<forall>m. k < m \<longrightarrow> (\<exists>n. m < n \<and> n \<in> S)"
-  shows "infinite (S::nat set)"
-proof -
-  {
-    fix m have "\<exists>n. m < n \<and> n \<in> S"
-    proof (cases "k < m")
-      case True
-      with k show ?thesis by blast
-    next
-      case False
-      from k obtain n where "Suc k < n \<and> n \<in> S" by auto
-      with False have "m < n \<and> n \<in> S" by auto
-      then show ?thesis ..
-    qed
-  }
-  then show ?thesis
-    by (auto simp add: infinite_nat_iff_unbounded)
-qed
+lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
+  by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
+            not_less_iff_gr_or_eq sup.bounded_iff)
 
 lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
   by simp
@@ -178,181 +148,106 @@
   we introduce corresponding binders and their proof rules.
 *}
 
-definition Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10)
-  where "Inf_many P \<longleftrightarrow> infinite {x. P x}"
-
-definition Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10)
-  where "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)"
-
-notation (xsymbols)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
-  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
-
-notation (HTML output)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
-  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
-
-lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
-  unfolding Inf_many_def ..
-
-lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
-  unfolding Alm_all_def Inf_many_def by simp
-
-(* legacy name *)
-lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
-
-lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
-  unfolding Alm_all_def not_not ..
-
-lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
-  unfolding Alm_all_def not_not ..
+(* The following two lemmas are available as filter-rules, but not in the simp-set *)
+lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
+lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
 
 lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
-  unfolding Inf_many_def by simp
+  by (simp add: frequently_const_iff)
 
 lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
-  unfolding Alm_all_def by simp
-
-lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
-  apply (erule contrapos_pp)
-  apply simp
-  done
-
-lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
-  by simp
-
-lemma INFM_E:
-  assumes "INFM x. P x"
-  obtains x where "P x"
-  using INFM_EX [OF assms] by (rule exE)
-
-lemma MOST_I:
-  assumes "\<And>x. P x"
-  shows "MOST x. P x"
-  using assms by simp
+  by (simp add: eventually_const_iff)
 
-lemma INFM_mono:
-  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
-  shows "\<exists>\<^sub>\<infinity>x. Q x"
-proof -
-  from inf have "infinite {x. P x}" unfolding Inf_many_def .
-  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
-  ultimately show ?thesis
-    using Inf_many_def infinite_super by blast
-qed
-
-lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
-  unfolding Alm_all_def by (blast intro: INFM_mono)
-
-lemma INFM_disj_distrib:
-  "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
-  unfolding Inf_many_def by (simp add: Collect_disj_eq)
-
-lemma INFM_imp_distrib:
-  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
-  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
+lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
+  by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
 
-lemma MOST_conj_distrib:
-  "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
-  unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
-
-lemma MOST_conjI:
-  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
-  by (simp add: MOST_conj_distrib)
-
-lemma INFM_conjI:
-  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
-  unfolding MOST_iff_cofinite INFM_iff_infinite
-  apply (drule (1) Diff_infinite_finite)
-  apply (simp add: Collect_conj_eq Collect_neg_eq)
-  done
+lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
+  by (auto intro: eventually_rev_mp eventually_elim1)
 
-lemma MOST_rev_mp:
-  assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
-  shows "\<forall>\<^sub>\<infinity>x. Q x"
-proof -
-  have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
-    using assms by (rule MOST_conjI)
-  thus ?thesis by (rule MOST_mono) simp
-qed
-
-lemma MOST_imp_iff:
-  assumes "MOST x. P x"
-  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
-proof
-  assume "MOST x. P x \<longrightarrow> Q x"
-  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
-next
-  assume "MOST x. Q x"
-  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
-qed
-
-lemma INFM_MOST_simps [simp]:
-  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
-  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
-  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
-  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
-  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
-  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
-  unfolding Alm_all_def Inf_many_def
-  by (simp_all add: Collect_conj_eq)
+lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
+  by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
 
 text {* Properties of quantifiers with injective functions. *}
 
 lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
-  unfolding INFM_iff_infinite
-  apply clarify
-  apply (drule (1) finite_vimageI)
-  apply simp
-  done
+  using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
 
 lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
-  unfolding MOST_iff_cofinite
-  apply (drule (1) finite_vimageI)
-  apply simp
-  done
+  using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
 
 text {* Properties of quantifiers with singletons. *}
 
 lemma not_INFM_eq [simp]:
   "\<not> (INFM x. x = a)"
   "\<not> (INFM x. a = x)"
-  unfolding INFM_iff_infinite by simp_all
+  unfolding frequently_cofinite by simp_all
 
 lemma MOST_neq [simp]:
   "MOST x. x \<noteq> a"
   "MOST x. a \<noteq> x"
-  unfolding MOST_iff_cofinite by simp_all
+  unfolding eventually_cofinite by simp_all
 
 lemma INFM_neq [simp]:
   "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
-  unfolding INFM_iff_infinite by simp_all
+  unfolding frequently_cofinite by simp_all
 
 lemma MOST_eq [simp]:
   "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
-  unfolding MOST_iff_cofinite by simp_all
+  unfolding eventually_cofinite by simp_all
 
 lemma MOST_eq_imp:
   "MOST x. x = a \<longrightarrow> P x"
   "MOST x. a = x \<longrightarrow> P x"
-  unfolding MOST_iff_cofinite by simp_all
+  unfolding eventually_cofinite by simp_all
 
 text {* Properties of quantifiers over the naturals. *}
 
-lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> P n)"
-  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
+lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
+  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
+
+lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
+  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
+
+lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
+  by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
 
-lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> P n)"
-  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
+lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
+  by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
+
+lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
+  by (simp add: eventually_frequently)
+
+lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
+  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
 
-lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m < n \<longrightarrow> P n)"
-  by (simp add: Alm_all_def INFM_nat)
+lemma
+  shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
+    and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
+  by (simp_all add: MOST_Suc_iff)
+
+lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
+  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
 
-lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m \<le> n \<longrightarrow> P n)"
-  by (simp add: Alm_all_def INFM_nat_le)
-
+(* legacy names *)
+lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
+lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
+lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
+lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
+lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
+lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
+lemma INFM_mono: "\<exists>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<exists>\<^sub>\<infinity>x. Q x" by (fact frequently_elim1)
+lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_elim1)
+lemma INFM_disj_distrib: "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)" by (fact frequently_disj_iff)
+lemma MOST_rev_mp: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x" by (fact eventually_rev_mp)
+lemma MOST_conj_distrib: "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)" by (fact eventually_conj_iff)
+lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
+lemma INFM_finite_Bex_distrib: "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)" by (fact frequently_bex_finite_distrib)
+lemma MOST_finite_Ball_distrib: "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)" by (fact eventually_ball_finite_distrib)
+lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
+lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
+lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
 
 subsection "Enumeration of an Infinite Set"
 
@@ -360,6 +255,11 @@
   The set's element type must be wellordered (e.g. the natural numbers).
 *}
 
+text \<open>
+  Could be generalized to
+    @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
+\<close>
+
 primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
 where
   enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
@@ -368,7 +268,7 @@
 lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   by simp
 
-lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
+lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   apply (induct n arbitrary: S)
    apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   apply simp
@@ -382,13 +282,13 @@
    apply (rule order_le_neq_trans)
     apply (simp add: enumerate_0 Least_le enumerate_in_set)
    apply (simp only: enumerate_Suc')
-   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
+   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
     apply (blast intro: sym)
    apply (simp add: enumerate_in_set del: Diff_iff)
   apply (simp add: enumerate_Suc')
   done
 
-lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
+lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   apply (erule less_Suc_induct)
   apply (auto intro: enumerate_step)
   done
diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -50,9 +50,6 @@
   "tl (x ## xs) = xs"
   by (simp add: cCons_def)
 
-lemma MOST_SucD: "(\<forall>\<^sub>\<infinity> n. P (Suc n)) \<Longrightarrow> (\<forall>\<^sub>\<infinity> n. P n)"
-  by (auto simp: MOST_nat) (metis Suc_lessE)
-
 subsection {* Definition of type @{text poly} *}
 
 typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
@@ -501,9 +498,9 @@
 
 lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n + coeff q n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
-  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n + coeff q n = 0"
-    by simp
+proof -
+  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
+    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
 qed
 
 lemma coeff_add [simp]:
@@ -527,9 +524,9 @@
 
 lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p q n. coeff p n - coeff q n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
-  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> coeff q n = 0 \<longrightarrow> coeff p n - coeff q n = 0"
-    by simp
+proof -
+  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
+    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
 qed
 
 lemma coeff_diff [simp]:
@@ -551,9 +548,9 @@
 
 lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
   is "\<lambda>p n. - coeff p n"
-proof (rule MOST_rev_mp[OF MOST_coeff_eq_0])
-  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> - coeff p n = 0"
-    by simp
+proof -
+  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
+    using MOST_coeff_eq_0 by simp
 qed
 
 lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
@@ -707,11 +704,9 @@
 
 lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
   is "\<lambda>a p n. a * coeff p n"
-proof (intro MOST_nat[THEN iffD2] exI allI impI) 
-  fix a :: 'a and p :: "'a poly" and i
-  assume "degree p < i"
-  then show "a * coeff p i = 0"
-    by (simp add: coeff_eq_0)
+proof -
+  fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
+    using MOST_coeff_eq_0[of p] by eventually_elim simp
 qed
 
 lemma coeff_smult [simp]:
diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -3331,10 +3331,8 @@
   have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
   proof (intro allI impI)
     fix B assume "finite B" "B \<subseteq> Z"
-    with `finite B` ev_Z have "eventually (\<lambda>x. \<forall>b\<in>B. x \<in> b) F"
-      by (auto intro!: eventually_Ball_finite)
-    with F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
-      by eventually_elim auto
+    with `finite B` ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
+      by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
     with F show "U \<inter> \<Inter>B \<noteq> {}"
       by (intro notI) (simp add: eventually_False)
   qed
@@ -7506,7 +7504,7 @@
   then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
     unfolding continuous_on_eq_continuous_within
     by (intro continuous_dist ballI continuous_within_compose)
-       (auto intro!:  continuous_fst continuous_snd continuous_within_id simp: image_image)
+       (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
 
   obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
     using continuous_attains_inf[OF D cont] by auto
diff -r d55937a8f97e -r 1fa1023b13b9 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:33:50 2015 +0200
+++ b/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:34:09 2015 +0200
@@ -1636,7 +1636,7 @@
     by (rule compactE)
   from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
   with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
-    by (simp add: eventually_Ball_finite)
+    by (simp add: eventually_ball_finite)
   with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
     by (auto elim!: eventually_mono [rotated])
   thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"