move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
authorhoelzl
Sun Apr 12 11:34:09 2015 +0200 (2015-04-12)
changeset 600401fa1023b13b9
parent 60039 d55937a8f97e
child 60041 6c86d58ab0ca
move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
src/HOL/Filter.thy
src/HOL/HOLCF/Library/Defl_Bifinite.thy
src/HOL/HOLCF/Plain_HOLCF.thy
src/HOL/Library/Infinite_Set.thy
src/HOL/Library/Polynomial.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Topological_Spaces.thy
     1.1 --- a/src/HOL/Filter.thy	Sun Apr 12 11:33:50 2015 +0200
     1.2 +++ b/src/HOL/Filter.thy	Sun Apr 12 11:34:09 2015 +0200
     1.3 @@ -63,6 +63,9 @@
     1.4    thus "eventually P F" by simp
     1.5  qed
     1.6  
     1.7 +lemma eventuallyI: "(\<And>x. P x) \<Longrightarrow> eventually P F"
     1.8 +  by (auto intro: always_eventually)
     1.9 +
    1.10  lemma eventually_mono:
    1.11    "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> eventually P F \<Longrightarrow> eventually Q F"
    1.12    unfolding eventually_def
    1.13 @@ -75,17 +78,6 @@
    1.14    using assms unfolding eventually_def
    1.15    by (rule is_filter.conj [OF is_filter_Rep_filter])
    1.16  
    1.17 -lemma eventually_Ball_finite:
    1.18 -  assumes "finite A" and "\<forall>y\<in>A. eventually (\<lambda>x. P x y) net"
    1.19 -  shows "eventually (\<lambda>x. \<forall>y\<in>A. P x y) net"
    1.20 -using assms by (induct set: finite, simp, simp add: eventually_conj)
    1.21 -
    1.22 -lemma eventually_all_finite:
    1.23 -  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    1.24 -  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    1.25 -  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    1.26 -using eventually_Ball_finite [of UNIV P] assms by simp
    1.27 -
    1.28  lemma eventually_mp:
    1.29    assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.30    assumes "eventually (\<lambda>x. P x) F"
    1.31 @@ -119,6 +111,29 @@
    1.32    shows "eventually (\<lambda>i. R i) F"
    1.33    using assms by (auto elim!: eventually_rev_mp)
    1.34  
    1.35 +lemma eventually_ball_finite_distrib:
    1.36 +  "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)"
    1.37 +  by (induction A rule: finite_induct) (auto simp: eventually_conj_iff)
    1.38 +
    1.39 +lemma eventually_ball_finite:
    1.40 +  "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"
    1.41 +  by (auto simp: eventually_ball_finite_distrib)
    1.42 +
    1.43 +lemma eventually_all_finite:
    1.44 +  fixes P :: "'a \<Rightarrow> 'b::finite \<Rightarrow> bool"
    1.45 +  assumes "\<And>y. eventually (\<lambda>x. P x y) net"
    1.46 +  shows "eventually (\<lambda>x. \<forall>y. P x y) net"
    1.47 +using eventually_ball_finite [of UNIV P] assms by simp
    1.48 +
    1.49 +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))"
    1.50 +proof
    1.51 +  assume "\<forall>\<^sub>Fx in F. \<exists>y. P x y"
    1.52 +  then have "\<forall>\<^sub>Fx in F. P x (SOME y. P x y)"
    1.53 +    by (auto intro: someI_ex eventually_elim1)
    1.54 +  then show "\<exists>Y. \<forall>\<^sub>Fx in F. P x (Y x)"
    1.55 +    by auto
    1.56 +qed (auto intro: eventually_elim1)
    1.57 +
    1.58  lemma not_eventually_impI: "eventually P F \<Longrightarrow> \<not> eventually Q F \<Longrightarrow> \<not> eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
    1.59    by (auto intro: eventually_mp)
    1.60  
    1.61 @@ -135,6 +150,93 @@
    1.62    then show ?thesis by (auto elim: eventually_elim2)
    1.63  qed
    1.64  
    1.65 +subsection \<open> Frequently as dual to eventually \<close>
    1.66 +
    1.67 +definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
    1.68 +  where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
    1.69 +
    1.70 +syntax (xsymbols)
    1.71 +  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
    1.72 +
    1.73 +translations
    1.74 +  "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
    1.75 +
    1.76 +lemma not_frequently_False [simp]: "\<not> (\<exists>\<^sub>Fx in F. False)"
    1.77 +  by (simp add: frequently_def)
    1.78 +
    1.79 +lemma frequently_ex: "\<exists>\<^sub>Fx in F. P x \<Longrightarrow> \<exists>x. P x"
    1.80 +  by (auto simp: frequently_def dest: not_eventuallyD)
    1.81 +
    1.82 +lemma frequentlyE: assumes "frequently P F" obtains x where "P x"
    1.83 +  using frequently_ex[OF assms] by auto
    1.84 +
    1.85 +lemma frequently_mp:
    1.86 +  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"
    1.87 +proof - 
    1.88 +  from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
    1.89 +    by (rule eventually_rev_mp) (auto intro!: always_eventually)
    1.90 +  from eventually_mp[OF this] P show ?thesis
    1.91 +    by (auto simp: frequently_def)
    1.92 +qed
    1.93 +
    1.94 +lemma frequently_rev_mp:
    1.95 +  assumes "\<exists>\<^sub>Fx in F. P x"
    1.96 +  assumes "\<forall>\<^sub>Fx in F. P x \<longrightarrow> Q x"
    1.97 +  shows "\<exists>\<^sub>Fx in F. Q x"
    1.98 +using assms(2) assms(1) by (rule frequently_mp)
    1.99 +
   1.100 +lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
   1.101 +  using frequently_mp[of P Q] by (simp add: always_eventually)
   1.102 +
   1.103 +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"
   1.104 +  by (metis frequently_mono)
   1.105 +
   1.106 +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)"
   1.107 +  by (simp add: frequently_def eventually_conj_iff)
   1.108 +
   1.109 +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"
   1.110 +  by (simp add: frequently_disj_iff)
   1.111 +
   1.112 +lemma frequently_bex_finite_distrib:
   1.113 +  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)"
   1.114 +  using assms by induction (auto simp: frequently_disj_iff)
   1.115 +
   1.116 +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"
   1.117 +  by (simp add: frequently_bex_finite_distrib)
   1.118 +
   1.119 +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))"
   1.120 +  using eventually_ex[of "\<lambda>x y. \<not> P x y" F] by (simp add: frequently_def)
   1.121 +
   1.122 +lemma
   1.123 +  shows not_eventually: "\<not> eventually P F \<longleftrightarrow> (\<exists>\<^sub>Fx in F. \<not> P x)"
   1.124 +    and not_frequently: "\<not> frequently P F \<longleftrightarrow> (\<forall>\<^sub>Fx in F. \<not> P x)"
   1.125 +  by (auto simp: frequently_def)
   1.126 +
   1.127 +lemma frequently_imp_iff:
   1.128 +  "(\<exists>\<^sub>Fx in F. P x \<longrightarrow> Q x) \<longleftrightarrow> (eventually P F \<longrightarrow> frequently Q F)"
   1.129 +  unfolding imp_conv_disj frequently_disj_iff not_eventually[symmetric] ..
   1.130 +
   1.131 +lemma eventually_frequently_const_simps:
   1.132 +  "(\<exists>\<^sub>Fx in F. P x \<and> C) \<longleftrightarrow> (\<exists>\<^sub>Fx in F. P x) \<and> C"
   1.133 +  "(\<exists>\<^sub>Fx in F. C \<and> P x) \<longleftrightarrow> C \<and> (\<exists>\<^sub>Fx in F. P x)"
   1.134 +  "(\<forall>\<^sub>Fx in F. P x \<or> C) \<longleftrightarrow> (\<forall>\<^sub>Fx in F. P x) \<or> C"
   1.135 +  "(\<forall>\<^sub>Fx in F. C \<or> P x) \<longleftrightarrow> C \<or> (\<forall>\<^sub>Fx in F. P x)"
   1.136 +  "(\<forall>\<^sub>Fx in F. P x \<longrightarrow> C) \<longleftrightarrow> ((\<exists>\<^sub>Fx in F. P x) \<longrightarrow> C)"
   1.137 +  "(\<forall>\<^sub>Fx in F. C \<longrightarrow> P x) \<longleftrightarrow> (C \<longrightarrow> (\<forall>\<^sub>Fx in F. P x))"
   1.138 +  by (cases C; simp add: not_frequently)+
   1.139 +
   1.140 +lemmas eventually_frequently_simps = 
   1.141 +  eventually_frequently_const_simps
   1.142 +  not_eventually
   1.143 +  eventually_conj_iff
   1.144 +  eventually_ball_finite_distrib
   1.145 +  eventually_ex
   1.146 +  not_frequently
   1.147 +  frequently_disj_iff
   1.148 +  frequently_bex_finite_distrib
   1.149 +  frequently_all
   1.150 +  frequently_imp_iff
   1.151 +
   1.152  ML {*
   1.153    fun eventually_elim_tac ctxt facts = SUBGOAL_CASES (fn (goal, i) =>
   1.154      let
   1.155 @@ -154,54 +256,6 @@
   1.156    Scan.succeed (fn ctxt => METHOD_CASES (HEADGOAL o eventually_elim_tac ctxt))
   1.157  *} "elimination of eventually quantifiers"
   1.158  
   1.159 -subsection \<open> Frequently as dual to eventually \<close>
   1.160 -
   1.161 -definition frequently :: "('a \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> bool"
   1.162 -  where "frequently P F \<longleftrightarrow> \<not> eventually (\<lambda>x. \<not> P x) F"
   1.163 -
   1.164 -syntax (xsymbols)
   1.165 -  "_frequently"  :: "pttrn \<Rightarrow> 'a filter \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>\<^sub>F _ in _./ _)" [0, 0, 10] 10)
   1.166 -
   1.167 -translations
   1.168 -  "\<exists>\<^sub>Fx in F. P" == "CONST frequently (\<lambda>x. P) F"
   1.169 -
   1.170 -lemma not_frequently_False [simp]: "\<not> frequently (\<lambda>x. False) F"
   1.171 -  by (simp add: frequently_def)
   1.172 -
   1.173 -lemma frequently_ex: "frequently P F \<Longrightarrow> \<exists>x. P x"
   1.174 -  by (auto simp: frequently_def dest: not_eventuallyD)
   1.175 -
   1.176 -lemma frequently_mp:
   1.177 -  assumes ev: "eventually (\<lambda>x. P x \<longrightarrow> Q x) F" and P: "frequently (\<lambda>x. P x) F"
   1.178 -  shows "frequently (\<lambda>x. Q x) F"
   1.179 -proof - 
   1.180 -  from ev have "eventually (\<lambda>x. \<not> Q x \<longrightarrow> \<not> P x) F"
   1.181 -    by (rule eventually_rev_mp) (auto intro!: always_eventually)
   1.182 -  from eventually_mp[OF this] P show ?thesis
   1.183 -    by (auto simp: frequently_def)
   1.184 -qed
   1.185 -
   1.186 -lemma frequently_rev_mp:
   1.187 -  assumes "frequently (\<lambda>x. P x) F"
   1.188 -  assumes "eventually (\<lambda>x. P x \<longrightarrow> Q x) F"
   1.189 -  shows "frequently (\<lambda>x. Q x) F"
   1.190 -using assms(2) assms(1) by (rule frequently_mp)
   1.191 -
   1.192 -lemma frequently_mono: "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> frequently P F \<Longrightarrow> frequently Q F"
   1.193 -  using frequently_mp[of P Q] by (simp add: always_eventually)
   1.194 -
   1.195 -lemma frequently_disj_iff:
   1.196 -  "frequently (\<lambda>x. P x \<or> Q x) F \<longleftrightarrow> frequently (\<lambda>x. P x) F \<or> frequently (\<lambda>x. Q x) F"
   1.197 -  by (simp add: frequently_def eventually_conj_iff)
   1.198 -
   1.199 -lemma frequently_disj:
   1.200 -  "frequently (\<lambda>x. P x) F \<Longrightarrow> frequently (\<lambda>x. Q x) F \<Longrightarrow> frequently (\<lambda>x. P x \<or> Q x) F"
   1.201 -  by (simp add: frequently_disj_iff)
   1.202 -
   1.203 -lemma frequently_Bex_finite:
   1.204 -  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)"
   1.205 -  using assms by induction (auto simp: frequently_disj_iff)
   1.206 -
   1.207  subsubsection {* Finer-than relation *}
   1.208  
   1.209  text {* @{term "F \<le> F'"} means that filter @{term F} is finer than
   1.210 @@ -318,15 +372,28 @@
   1.211    "eventually (\<lambda>x. False) F \<longleftrightarrow> F = bot"
   1.212    unfolding filter_eq_iff by (auto elim: eventually_rev_mp)
   1.213  
   1.214 +lemma eventually_frequently: "F \<noteq> bot \<Longrightarrow> eventually P F \<Longrightarrow> frequently P F"
   1.215 +  using eventually_conj[of P F "\<lambda>x. \<not> P x"]
   1.216 +  by (auto simp add: frequently_def eventually_False)
   1.217 +
   1.218 +lemma eventually_const_iff: "eventually (\<lambda>x. P) F \<longleftrightarrow> P \<or> F = bot"
   1.219 +  by (cases P) (auto simp: eventually_False)
   1.220 +
   1.221 +lemma eventually_const[simp]: "F \<noteq> bot \<Longrightarrow> eventually (\<lambda>x. P) F \<longleftrightarrow> P"
   1.222 +  by (simp add: eventually_const_iff)
   1.223 +
   1.224 +lemma frequently_const_iff: "frequently (\<lambda>x. P) F \<longleftrightarrow> P \<and> F \<noteq> bot"
   1.225 +  by (simp add: frequently_def eventually_const_iff)
   1.226 +
   1.227 +lemma frequently_const[simp]: "F \<noteq> bot \<Longrightarrow> frequently (\<lambda>x. P) F \<longleftrightarrow> P"
   1.228 +  by (simp add: frequently_const_iff)
   1.229 +
   1.230  abbreviation (input) trivial_limit :: "'a filter \<Rightarrow> bool"
   1.231    where "trivial_limit F \<equiv> F = bot"
   1.232  
   1.233  lemma trivial_limit_def: "trivial_limit F \<longleftrightarrow> eventually (\<lambda>x. False) F"
   1.234    by (rule eventually_False [symmetric])
   1.235  
   1.236 -lemma eventually_const: "\<not> trivial_limit net \<Longrightarrow> eventually (\<lambda>x. P) net \<longleftrightarrow> P"
   1.237 -  by (cases P) (simp_all add: eventually_False)
   1.238 -
   1.239  lemma eventually_Inf: "eventually P (Inf B) \<longleftrightarrow> (\<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X))"
   1.240  proof -
   1.241    let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
   1.242 @@ -601,22 +668,30 @@
   1.243    shows "eventually P sequentially"
   1.244  using assms by (auto simp: eventually_sequentially)
   1.245  
   1.246 -lemma eventually_sequentially_seg:
   1.247 -  "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.248 -  unfolding eventually_sequentially
   1.249 -  apply safe
   1.250 -   apply (rule_tac x="N + k" in exI)
   1.251 -   apply rule
   1.252 -   apply (erule_tac x="n - k" in allE)
   1.253 -   apply auto []
   1.254 -  apply (rule_tac x=N in exI)
   1.255 -  apply auto []
   1.256 -  done
   1.257 +lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.258 +  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
   1.259 +
   1.260 +lemma eventually_sequentially_seg: "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.261 +  using eventually_sequentially_Suc[of "\<lambda>n. P (n + k)" for k] by (induction k) auto
   1.262  
   1.263  subsection \<open> The cofinite filter \<close>
   1.264  
   1.265  definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
   1.266  
   1.267 +abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
   1.268 +  "Inf_many P \<equiv> frequently P cofinite"
   1.269 +
   1.270 +abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
   1.271 +  "Alm_all P \<equiv> eventually P cofinite"
   1.272 +
   1.273 +notation (xsymbols)
   1.274 +  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   1.275 +  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   1.276 +
   1.277 +notation (HTML output)
   1.278 +  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
   1.279 +  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
   1.280 +
   1.281  lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
   1.282    unfolding cofinite_def
   1.283  proof (rule eventually_Abs_filter, rule is_filter.intro)
   1.284 @@ -629,6 +704,9 @@
   1.285      by (intro finite_subset[OF _ P]) auto
   1.286  qed simp
   1.287  
   1.288 +lemma frequently_cofinite: "frequently P cofinite \<longleftrightarrow> \<not> finite {x. P x}"
   1.289 +  by (simp add: frequently_def eventually_cofinite)
   1.290 +
   1.291  lemma cofinite_bot[simp]: "cofinite = (bot::'a filter) \<longleftrightarrow> finite (UNIV :: 'a set)"
   1.292    unfolding trivial_limit_def eventually_cofinite by simp
   1.293  
   1.294 @@ -737,9 +815,6 @@
   1.295    "filterlim f F F1 \<Longrightarrow> filterlim f F F2 \<Longrightarrow> filterlim f F (sup F1 F2)"
   1.296    unfolding filterlim_def filtermap_sup by auto
   1.297  
   1.298 -lemma eventually_sequentially_Suc: "eventually (\<lambda>i. P (Suc i)) sequentially \<longleftrightarrow> eventually P sequentially"
   1.299 -  unfolding eventually_sequentially by (metis Suc_le_D Suc_le_mono le_Suc_eq)
   1.300 -
   1.301  lemma filterlim_sequentially_Suc:
   1.302    "(LIM x sequentially. f (Suc x) :> F) \<longleftrightarrow> (LIM x sequentially. f x :> F)"
   1.303    unfolding filterlim_iff by (subst eventually_sequentially_Suc) simp
     2.1 --- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Apr 12 11:33:50 2015 +0200
     2.2 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy	Sun Apr 12 11:34:09 2015 +0200
     2.3 @@ -12,38 +12,6 @@
     2.4  
     2.5  default_sort type
     2.6  
     2.7 -lemma MOST_INFM:
     2.8 -  assumes inf: "infinite (UNIV::'a set)"
     2.9 -  shows "MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
    2.10 -  unfolding Alm_all_def Inf_many_def
    2.11 -  apply (auto simp add: Collect_neg_eq)
    2.12 -  apply (drule (1) finite_UnI)
    2.13 -  apply (simp add: Compl_partition2 inf)
    2.14 -  done
    2.15 -
    2.16 -lemma MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
    2.17 -by (rule MOST_inj [OF _ inj_Suc])
    2.18 -
    2.19 -lemma MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
    2.20 -unfolding MOST_nat
    2.21 -apply (clarify, rule_tac x="Suc m" in exI, clarify)
    2.22 -apply (erule Suc_lessE, simp)
    2.23 -done
    2.24 -
    2.25 -lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
    2.26 -by (rule iffI [OF MOST_SucD MOST_SucI])
    2.27 -
    2.28 -lemma INFM_finite_Bex_distrib:
    2.29 -  "finite A \<Longrightarrow> (INFM y. \<exists>x\<in>A. P x y) \<longleftrightarrow> (\<exists>x\<in>A. INFM y. P x y)"
    2.30 -by (induct set: finite, simp, simp add: INFM_disj_distrib)
    2.31 -
    2.32 -lemma MOST_finite_Ball_distrib:
    2.33 -  "finite A \<Longrightarrow> (MOST y. \<forall>x\<in>A. P x y) \<longleftrightarrow> (\<forall>x\<in>A. MOST y. P x y)"
    2.34 -by (induct set: finite, simp, simp add: MOST_conj_distrib)
    2.35 -
    2.36 -lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
    2.37 -unfolding MOST_nat_le by fast
    2.38 -
    2.39  subsection {* Eventually constant sequences *}
    2.40  
    2.41  definition
     3.1 --- a/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Apr 12 11:33:50 2015 +0200
     3.2 +++ b/src/HOL/HOLCF/Plain_HOLCF.thy	Sun Apr 12 11:34:09 2015 +0200
     3.3 @@ -12,4 +12,6 @@
     3.4    Basic HOLCF concepts and types; does not include definition packages.
     3.5  *}
     3.6  
     3.7 +hide_const (open) Filter.principal
     3.8 +
     3.9  end
     4.1 --- a/src/HOL/Library/Infinite_Set.thy	Sun Apr 12 11:33:50 2015 +0200
     4.2 +++ b/src/HOL/Library/Infinite_Set.thy	Sun Apr 12 11:34:09 2015 +0200
     4.3 @@ -67,36 +67,22 @@
     4.4    infinite.
     4.5  *}
     4.6  
     4.7 -lemma finite_nat_bounded: assumes S: "finite (S::nat set)" shows "\<exists>k. S \<subseteq> {..<k}"
     4.8 -proof cases
     4.9 -  assume "S \<noteq> {}" with Max_less_iff[OF S this] show ?thesis
    4.10 -    by auto
    4.11 -qed simp
    4.12 +lemma infinite_nat_iff_unbounded_le: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. n \<in> S)"
    4.13 +  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    4.14 +  by (simp add: cofinite_eq_sequentially frequently_def eventually_sequentially)
    4.15 +
    4.16 +lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n>m. n \<in> S)"
    4.17 +  using frequently_cofinite[of "\<lambda>x. x \<in> S"]
    4.18 +  by (simp add: cofinite_eq_sequentially frequently_def eventually_at_top_dense)
    4.19  
    4.20  lemma finite_nat_iff_bounded: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..<k})"
    4.21 -  by (auto intro: finite_nat_bounded dest: finite_subset)
    4.22 +  using infinite_nat_iff_unbounded_le[of S] by (simp add: subset_eq) (metis not_le)
    4.23  
    4.24 -lemma finite_nat_iff_bounded_le:
    4.25 -  "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {..k})"  (is "?lhs \<longleftrightarrow> ?rhs")
    4.26 -proof
    4.27 -  assume ?lhs
    4.28 -  then obtain k where "S \<subseteq> {..<k}"
    4.29 -    by (blast dest: finite_nat_bounded)
    4.30 -  then have "S \<subseteq> {..k}" by auto
    4.31 -  then show ?rhs ..
    4.32 -next
    4.33 -  assume ?rhs
    4.34 -  then obtain k where "S \<subseteq> {..k}" ..
    4.35 -  then show "finite S"
    4.36 -    by (rule finite_subset) simp
    4.37 -qed
    4.38 +lemma finite_nat_iff_bounded_le: "finite (S::nat set) \<longleftrightarrow> (\<exists>k. S \<subseteq> {.. k})"
    4.39 +  using infinite_nat_iff_unbounded[of S] by (simp add: subset_eq) (metis not_le)
    4.40  
    4.41 -lemma infinite_nat_iff_unbounded: "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> n \<in> S)"
    4.42 -  unfolding finite_nat_iff_bounded_le by (auto simp: subset_eq not_le)
    4.43 -
    4.44 -lemma infinite_nat_iff_unbounded_le:
    4.45 -  "infinite (S::nat set) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> n \<in> S)"
    4.46 -  unfolding finite_nat_iff_bounded by (auto simp: subset_eq not_less)
    4.47 +lemma finite_nat_bounded: "finite (S::nat set) \<Longrightarrow> \<exists>k. S \<subseteq> {..<k}"
    4.48 +  by (simp add: finite_nat_iff_bounded)
    4.49  
    4.50  text {*
    4.51    For a set of natural numbers to be infinite, it is enough to know
    4.52 @@ -104,25 +90,9 @@
    4.53    number that is an element of the set.
    4.54  *}
    4.55  
    4.56 -lemma unbounded_k_infinite:
    4.57 -  assumes k: "\<forall>m. k < m \<longrightarrow> (\<exists>n. m < n \<and> n \<in> S)"
    4.58 -  shows "infinite (S::nat set)"
    4.59 -proof -
    4.60 -  {
    4.61 -    fix m have "\<exists>n. m < n \<and> n \<in> S"
    4.62 -    proof (cases "k < m")
    4.63 -      case True
    4.64 -      with k show ?thesis by blast
    4.65 -    next
    4.66 -      case False
    4.67 -      from k obtain n where "Suc k < n \<and> n \<in> S" by auto
    4.68 -      with False have "m < n \<and> n \<in> S" by auto
    4.69 -      then show ?thesis ..
    4.70 -    qed
    4.71 -  }
    4.72 -  then show ?thesis
    4.73 -    by (auto simp add: infinite_nat_iff_unbounded)
    4.74 -qed
    4.75 +lemma unbounded_k_infinite: "\<forall>m>k. \<exists>n>m. n \<in> S \<Longrightarrow> infinite (S::nat set)"
    4.76 +  by (metis (full_types) infinite_nat_iff_unbounded_le le_imp_less_Suc not_less
    4.77 +            not_less_iff_gr_or_eq sup.bounded_iff)
    4.78  
    4.79  lemma nat_not_finite: "finite (UNIV::nat set) \<Longrightarrow> R"
    4.80    by simp
    4.81 @@ -178,181 +148,106 @@
    4.82    we introduce corresponding binders and their proof rules.
    4.83  *}
    4.84  
    4.85 -definition Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10)
    4.86 -  where "Inf_many P \<longleftrightarrow> infinite {x. P x}"
    4.87 -
    4.88 -definition Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10)
    4.89 -  where "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)"
    4.90 -
    4.91 -notation (xsymbols)
    4.92 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
    4.93 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    4.94 -
    4.95 -notation (HTML output)
    4.96 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
    4.97 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    4.98 -
    4.99 -lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}"
   4.100 -  unfolding Inf_many_def ..
   4.101 -
   4.102 -lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}"
   4.103 -  unfolding Alm_all_def Inf_many_def by simp
   4.104 -
   4.105 -(* legacy name *)
   4.106 -lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   4.107 -
   4.108 -lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)"
   4.109 -  unfolding Alm_all_def not_not ..
   4.110 -
   4.111 -lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)"
   4.112 -  unfolding Alm_all_def not_not ..
   4.113 +(* The following two lemmas are available as filter-rules, but not in the simp-set *)
   4.114 +lemma not_INFM [simp]: "\<not> (INFM x. P x) \<longleftrightarrow> (MOST x. \<not> P x)" by (fact not_frequently)
   4.115 +lemma not_MOST [simp]: "\<not> (MOST x. P x) \<longleftrightarrow> (INFM x. \<not> P x)" by (fact not_eventually)
   4.116  
   4.117  lemma INFM_const [simp]: "(INFM x::'a. P) \<longleftrightarrow> P \<and> infinite (UNIV::'a set)"
   4.118 -  unfolding Inf_many_def by simp
   4.119 +  by (simp add: frequently_const_iff)
   4.120  
   4.121  lemma MOST_const [simp]: "(MOST x::'a. P) \<longleftrightarrow> P \<or> finite (UNIV::'a set)"
   4.122 -  unfolding Alm_all_def by simp
   4.123 -
   4.124 -lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)"
   4.125 -  apply (erule contrapos_pp)
   4.126 -  apply simp
   4.127 -  done
   4.128 -
   4.129 -lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x"
   4.130 -  by simp
   4.131 -
   4.132 -lemma INFM_E:
   4.133 -  assumes "INFM x. P x"
   4.134 -  obtains x where "P x"
   4.135 -  using INFM_EX [OF assms] by (rule exE)
   4.136 -
   4.137 -lemma MOST_I:
   4.138 -  assumes "\<And>x. P x"
   4.139 -  shows "MOST x. P x"
   4.140 -  using assms by simp
   4.141 +  by (simp add: eventually_const_iff)
   4.142  
   4.143 -lemma INFM_mono:
   4.144 -  assumes inf: "\<exists>\<^sub>\<infinity>x. P x" and q: "\<And>x. P x \<Longrightarrow> Q x"
   4.145 -  shows "\<exists>\<^sub>\<infinity>x. Q x"
   4.146 -proof -
   4.147 -  from inf have "infinite {x. P x}" unfolding Inf_many_def .
   4.148 -  moreover from q have "{x. P x} \<subseteq> {x. Q x}" by auto
   4.149 -  ultimately show ?thesis
   4.150 -    using Inf_many_def infinite_super by blast
   4.151 -qed
   4.152 -
   4.153 -lemma MOST_mono: "\<forall>\<^sub>\<infinity>x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> \<forall>\<^sub>\<infinity>x. Q x"
   4.154 -  unfolding Alm_all_def by (blast intro: INFM_mono)
   4.155 -
   4.156 -lemma INFM_disj_distrib:
   4.157 -  "(\<exists>\<^sub>\<infinity>x. P x \<or> Q x) \<longleftrightarrow> (\<exists>\<^sub>\<infinity>x. P x) \<or> (\<exists>\<^sub>\<infinity>x. Q x)"
   4.158 -  unfolding Inf_many_def by (simp add: Collect_disj_eq)
   4.159 -
   4.160 -lemma INFM_imp_distrib:
   4.161 -  "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   4.162 -  by (simp only: imp_conv_disj INFM_disj_distrib not_MOST)
   4.163 +lemma INFM_imp_distrib: "(INFM x. P x \<longrightarrow> Q x) \<longleftrightarrow> ((MOST x. P x) \<longrightarrow> (INFM x. Q x))"
   4.164 +  by (simp only: imp_conv_disj frequently_disj_iff not_eventually)
   4.165  
   4.166 -lemma MOST_conj_distrib:
   4.167 -  "(\<forall>\<^sub>\<infinity>x. P x \<and> Q x) \<longleftrightarrow> (\<forall>\<^sub>\<infinity>x. P x) \<and> (\<forall>\<^sub>\<infinity>x. Q x)"
   4.168 -  unfolding Alm_all_def by (simp add: INFM_disj_distrib del: disj_not1)
   4.169 -
   4.170 -lemma MOST_conjI:
   4.171 -  "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x"
   4.172 -  by (simp add: MOST_conj_distrib)
   4.173 -
   4.174 -lemma INFM_conjI:
   4.175 -  "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   4.176 -  unfolding MOST_iff_cofinite INFM_iff_infinite
   4.177 -  apply (drule (1) Diff_infinite_finite)
   4.178 -  apply (simp add: Collect_conj_eq Collect_neg_eq)
   4.179 -  done
   4.180 +lemma MOST_imp_iff: "MOST x. P x \<Longrightarrow> (MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   4.181 +  by (auto intro: eventually_rev_mp eventually_elim1)
   4.182  
   4.183 -lemma MOST_rev_mp:
   4.184 -  assumes "\<forall>\<^sub>\<infinity>x. P x" and "\<forall>\<^sub>\<infinity>x. P x \<longrightarrow> Q x"
   4.185 -  shows "\<forall>\<^sub>\<infinity>x. Q x"
   4.186 -proof -
   4.187 -  have "\<forall>\<^sub>\<infinity>x. P x \<and> (P x \<longrightarrow> Q x)"
   4.188 -    using assms by (rule MOST_conjI)
   4.189 -  thus ?thesis by (rule MOST_mono) simp
   4.190 -qed
   4.191 -
   4.192 -lemma MOST_imp_iff:
   4.193 -  assumes "MOST x. P x"
   4.194 -  shows "(MOST x. P x \<longrightarrow> Q x) \<longleftrightarrow> (MOST x. Q x)"
   4.195 -proof
   4.196 -  assume "MOST x. P x \<longrightarrow> Q x"
   4.197 -  with assms show "MOST x. Q x" by (rule MOST_rev_mp)
   4.198 -next
   4.199 -  assume "MOST x. Q x"
   4.200 -  then show "MOST x. P x \<longrightarrow> Q x" by (rule MOST_mono) simp
   4.201 -qed
   4.202 -
   4.203 -lemma INFM_MOST_simps [simp]:
   4.204 -  "\<And>P Q. (INFM x. P x \<and> Q) \<longleftrightarrow> (INFM x. P x) \<and> Q"
   4.205 -  "\<And>P Q. (INFM x. P \<and> Q x) \<longleftrightarrow> P \<and> (INFM x. Q x)"
   4.206 -  "\<And>P Q. (MOST x. P x \<or> Q) \<longleftrightarrow> (MOST x. P x) \<or> Q"
   4.207 -  "\<And>P Q. (MOST x. P \<or> Q x) \<longleftrightarrow> P \<or> (MOST x. Q x)"
   4.208 -  "\<And>P Q. (MOST x. P x \<longrightarrow> Q) \<longleftrightarrow> ((INFM x. P x) \<longrightarrow> Q)"
   4.209 -  "\<And>P Q. (MOST x. P \<longrightarrow> Q x) \<longleftrightarrow> (P \<longrightarrow> (MOST x. Q x))"
   4.210 -  unfolding Alm_all_def Inf_many_def
   4.211 -  by (simp_all add: Collect_conj_eq)
   4.212 +lemma INFM_conjI: "INFM x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> INFM x. P x \<and> Q x"
   4.213 +  by (rule frequently_rev_mp[of P]) (auto elim: eventually_elim1)
   4.214  
   4.215  text {* Properties of quantifiers with injective functions. *}
   4.216  
   4.217  lemma INFM_inj: "INFM x. P (f x) \<Longrightarrow> inj f \<Longrightarrow> INFM x. P x"
   4.218 -  unfolding INFM_iff_infinite
   4.219 -  apply clarify
   4.220 -  apply (drule (1) finite_vimageI)
   4.221 -  apply simp
   4.222 -  done
   4.223 +  using finite_vimageI[of "{x. P x}" f] by (auto simp: frequently_cofinite)
   4.224  
   4.225  lemma MOST_inj: "MOST x. P x \<Longrightarrow> inj f \<Longrightarrow> MOST x. P (f x)"
   4.226 -  unfolding MOST_iff_cofinite
   4.227 -  apply (drule (1) finite_vimageI)
   4.228 -  apply simp
   4.229 -  done
   4.230 +  using finite_vimageI[of "{x. \<not> P x}" f] by (auto simp: eventually_cofinite)
   4.231  
   4.232  text {* Properties of quantifiers with singletons. *}
   4.233  
   4.234  lemma not_INFM_eq [simp]:
   4.235    "\<not> (INFM x. x = a)"
   4.236    "\<not> (INFM x. a = x)"
   4.237 -  unfolding INFM_iff_infinite by simp_all
   4.238 +  unfolding frequently_cofinite by simp_all
   4.239  
   4.240  lemma MOST_neq [simp]:
   4.241    "MOST x. x \<noteq> a"
   4.242    "MOST x. a \<noteq> x"
   4.243 -  unfolding MOST_iff_cofinite by simp_all
   4.244 +  unfolding eventually_cofinite by simp_all
   4.245  
   4.246  lemma INFM_neq [simp]:
   4.247    "(INFM x::'a. x \<noteq> a) \<longleftrightarrow> infinite (UNIV::'a set)"
   4.248    "(INFM x::'a. a \<noteq> x) \<longleftrightarrow> infinite (UNIV::'a set)"
   4.249 -  unfolding INFM_iff_infinite by simp_all
   4.250 +  unfolding frequently_cofinite by simp_all
   4.251  
   4.252  lemma MOST_eq [simp]:
   4.253    "(MOST x::'a. x = a) \<longleftrightarrow> finite (UNIV::'a set)"
   4.254    "(MOST x::'a. a = x) \<longleftrightarrow> finite (UNIV::'a set)"
   4.255 -  unfolding MOST_iff_cofinite by simp_all
   4.256 +  unfolding eventually_cofinite by simp_all
   4.257  
   4.258  lemma MOST_eq_imp:
   4.259    "MOST x. x = a \<longrightarrow> P x"
   4.260    "MOST x. a = x \<longrightarrow> P x"
   4.261 -  unfolding MOST_iff_cofinite by simp_all
   4.262 +  unfolding eventually_cofinite by simp_all
   4.263  
   4.264  text {* Properties of quantifiers over the naturals. *}
   4.265  
   4.266 -lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m < n \<and> P n)"
   4.267 -  by (simp add: Inf_many_def infinite_nat_iff_unbounded)
   4.268 +lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n>m. P n)"
   4.269 +  by (auto simp add: eventually_cofinite finite_nat_iff_bounded_le subset_eq not_le[symmetric])
   4.270 +
   4.271 +lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n\<ge>m. P n)"
   4.272 +  by (auto simp add: eventually_cofinite finite_nat_iff_bounded subset_eq not_le[symmetric])
   4.273 +
   4.274 +lemma INFM_nat: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n>m. P n)"
   4.275 +  by (simp add: frequently_cofinite infinite_nat_iff_unbounded)
   4.276  
   4.277 -lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n. m \<le> n \<and> P n)"
   4.278 -  by (simp add: Inf_many_def infinite_nat_iff_unbounded_le)
   4.279 +lemma INFM_nat_le: "(\<exists>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<forall>m. \<exists>n\<ge>m. P n)"
   4.280 +  by (simp add: frequently_cofinite infinite_nat_iff_unbounded_le)
   4.281 +
   4.282 +lemma MOST_INFM: "infinite (UNIV::'a set) \<Longrightarrow> MOST x::'a. P x \<Longrightarrow> INFM x::'a. P x"
   4.283 +  by (simp add: eventually_frequently)
   4.284 +
   4.285 +lemma MOST_Suc_iff: "(MOST n. P (Suc n)) \<longleftrightarrow> (MOST n. P n)"
   4.286 +  by (simp add: cofinite_eq_sequentially eventually_sequentially_Suc)
   4.287  
   4.288 -lemma MOST_nat: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m < n \<longrightarrow> P n)"
   4.289 -  by (simp add: Alm_all_def INFM_nat)
   4.290 +lemma
   4.291 +  shows MOST_SucI: "MOST n. P n \<Longrightarrow> MOST n. P (Suc n)"
   4.292 +    and MOST_SucD: "MOST n. P (Suc n) \<Longrightarrow> MOST n. P n"
   4.293 +  by (simp_all add: MOST_Suc_iff)
   4.294 +
   4.295 +lemma MOST_ge_nat: "MOST n::nat. m \<le> n"
   4.296 +  by (simp add: cofinite_eq_sequentially eventually_ge_at_top)
   4.297  
   4.298 -lemma MOST_nat_le: "(\<forall>\<^sub>\<infinity>n. P (n::nat)) \<longleftrightarrow> (\<exists>m. \<forall>n. m \<le> n \<longrightarrow> P n)"
   4.299 -  by (simp add: Alm_all_def INFM_nat_le)
   4.300 -
   4.301 +(* legacy names *)
   4.302 +lemma Inf_many_def: "Inf_many P \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   4.303 +lemma Alm_all_def: "Alm_all P \<longleftrightarrow> \<not> (INFM x. \<not> P x)" by simp
   4.304 +lemma INFM_iff_infinite: "(INFM x. P x) \<longleftrightarrow> infinite {x. P x}" by (fact frequently_cofinite)
   4.305 +lemma MOST_iff_cofinite: "(MOST x. P x) \<longleftrightarrow> finite {x. \<not> P x}" by (fact eventually_cofinite)
   4.306 +lemma INFM_EX: "(\<exists>\<^sub>\<infinity>x. P x) \<Longrightarrow> (\<exists>x. P x)" by (fact frequently_ex)
   4.307 +lemma ALL_MOST: "\<forall>x. P x \<Longrightarrow> \<forall>\<^sub>\<infinity>x. P x" by (fact always_eventually)
   4.308 +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)
   4.309 +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)
   4.310 +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)
   4.311 +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)
   4.312 +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)
   4.313 +lemma MOST_conjI: "MOST x. P x \<Longrightarrow> MOST x. Q x \<Longrightarrow> MOST x. P x \<and> Q x" by (fact eventually_conj)
   4.314 +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)
   4.315 +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)
   4.316 +lemma INFM_E: "INFM x. P x \<Longrightarrow> (\<And>x. P x \<Longrightarrow> thesis) \<Longrightarrow> thesis" by (fact frequentlyE)
   4.317 +lemma MOST_I: "(\<And>x. P x) \<Longrightarrow> MOST x. P x" by (rule eventuallyI)
   4.318 +lemmas MOST_iff_finiteNeg = MOST_iff_cofinite
   4.319  
   4.320  subsection "Enumeration of an Infinite Set"
   4.321  
   4.322 @@ -360,6 +255,11 @@
   4.323    The set's element type must be wellordered (e.g. the natural numbers).
   4.324  *}
   4.325  
   4.326 +text \<open>
   4.327 +  Could be generalized to
   4.328 +    @{term "enumerate' S n = (SOME t. t \<in> s \<and> finite {s\<in>S. s < t} \<and> card {s\<in>S. s < t} = n)"}.
   4.329 +\<close>
   4.330 +
   4.331  primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a"
   4.332  where
   4.333    enumerate_0: "enumerate S 0 = (LEAST n. n \<in> S)"
   4.334 @@ -368,7 +268,7 @@
   4.335  lemma enumerate_Suc': "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   4.336    by simp
   4.337  
   4.338 -lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
   4.339 +lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n \<in> S"
   4.340    apply (induct n arbitrary: S)
   4.341     apply (fastforce intro: LeastI dest!: infinite_imp_nonempty)
   4.342    apply simp
   4.343 @@ -382,13 +282,13 @@
   4.344     apply (rule order_le_neq_trans)
   4.345      apply (simp add: enumerate_0 Least_le enumerate_in_set)
   4.346     apply (simp only: enumerate_Suc')
   4.347 -   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 : S - {enumerate S 0}")
   4.348 +   apply (subgoal_tac "enumerate (S - {enumerate S 0}) 0 \<in> S - {enumerate S 0}")
   4.349      apply (blast intro: sym)
   4.350     apply (simp add: enumerate_in_set del: Diff_iff)
   4.351    apply (simp add: enumerate_Suc')
   4.352    done
   4.353  
   4.354 -lemma enumerate_mono: "m<n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   4.355 +lemma enumerate_mono: "m < n \<Longrightarrow> infinite S \<Longrightarrow> enumerate S m < enumerate S n"
   4.356    apply (erule less_Suc_induct)
   4.357    apply (auto intro: enumerate_step)
   4.358    done
     5.1 --- a/src/HOL/Library/Polynomial.thy	Sun Apr 12 11:33:50 2015 +0200
     5.2 +++ b/src/HOL/Library/Polynomial.thy	Sun Apr 12 11:34:09 2015 +0200
     5.3 @@ -50,9 +50,6 @@
     5.4    "tl (x ## xs) = xs"
     5.5    by (simp add: cCons_def)
     5.6  
     5.7 -lemma MOST_SucD: "(\<forall>\<^sub>\<infinity> n. P (Suc n)) \<Longrightarrow> (\<forall>\<^sub>\<infinity> n. P n)"
     5.8 -  by (auto simp: MOST_nat) (metis Suc_lessE)
     5.9 -
    5.10  subsection {* Definition of type @{text poly} *}
    5.11  
    5.12  typedef 'a poly = "{f :: nat \<Rightarrow> 'a::zero. \<forall>\<^sub>\<infinity> n. f n = 0}"
    5.13 @@ -501,9 +498,9 @@
    5.14  
    5.15  lift_definition plus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    5.16    is "\<lambda>p q n. coeff p n + coeff q n"
    5.17 -proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
    5.18 -  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"
    5.19 -    by simp
    5.20 +proof -
    5.21 +  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n + coeff q n = 0"
    5.22 +    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
    5.23  qed
    5.24  
    5.25  lemma coeff_add [simp]:
    5.26 @@ -527,9 +524,9 @@
    5.27  
    5.28  lift_definition minus_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    5.29    is "\<lambda>p q n. coeff p n - coeff q n"
    5.30 -proof (rule MOST_rev_mp[OF MOST_coeff_eq_0 MOST_rev_mp[OF MOST_coeff_eq_0]])
    5.31 -  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"
    5.32 -    by simp
    5.33 +proof -
    5.34 +  fix q p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n - coeff q n = 0"
    5.35 +    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
    5.36  qed
    5.37  
    5.38  lemma coeff_diff [simp]:
    5.39 @@ -551,9 +548,9 @@
    5.40  
    5.41  lift_definition uminus_poly :: "'a poly \<Rightarrow> 'a poly"
    5.42    is "\<lambda>p n. - coeff p n"
    5.43 -proof (rule MOST_rev_mp[OF MOST_coeff_eq_0])
    5.44 -  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. coeff p n = 0 \<longrightarrow> - coeff p n = 0"
    5.45 -    by simp
    5.46 +proof -
    5.47 +  fix p :: "'a poly" show "\<forall>\<^sub>\<infinity>n. - coeff p n = 0"
    5.48 +    using MOST_coeff_eq_0 by simp
    5.49  qed
    5.50  
    5.51  lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
    5.52 @@ -707,11 +704,9 @@
    5.53  
    5.54  lift_definition smult :: "'a::comm_semiring_0 \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
    5.55    is "\<lambda>a p n. a * coeff p n"
    5.56 -proof (intro MOST_nat[THEN iffD2] exI allI impI) 
    5.57 -  fix a :: 'a and p :: "'a poly" and i
    5.58 -  assume "degree p < i"
    5.59 -  then show "a * coeff p i = 0"
    5.60 -    by (simp add: coeff_eq_0)
    5.61 +proof -
    5.62 +  fix a :: 'a and p :: "'a poly" show "\<forall>\<^sub>\<infinity> i. a * coeff p i = 0"
    5.63 +    using MOST_coeff_eq_0[of p] by eventually_elim simp
    5.64  qed
    5.65  
    5.66  lemma coeff_smult [simp]:
     6.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 12 11:33:50 2015 +0200
     6.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Apr 12 11:34:09 2015 +0200
     6.3 @@ -3331,10 +3331,8 @@
     6.4    have "(\<forall>B \<subseteq> Z. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {})"
     6.5    proof (intro allI impI)
     6.6      fix B assume "finite B" "B \<subseteq> Z"
     6.7 -    with `finite B` ev_Z have "eventually (\<lambda>x. \<forall>b\<in>B. x \<in> b) F"
     6.8 -      by (auto intro!: eventually_Ball_finite)
     6.9 -    with F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
    6.10 -      by eventually_elim auto
    6.11 +    with `finite B` ev_Z F(2) have "eventually (\<lambda>x. x \<in> U \<inter> (\<Inter>B)) F"
    6.12 +      by (auto simp: eventually_ball_finite_distrib eventually_conj_iff)
    6.13      with F show "U \<inter> \<Inter>B \<noteq> {}"
    6.14        by (intro notI) (simp add: eventually_False)
    6.15    qed
    6.16 @@ -7506,7 +7504,7 @@
    6.17    then have cont: "continuous_on ?D (\<lambda>x. dist ((g \<circ> fst) x) (snd x))"
    6.18      unfolding continuous_on_eq_continuous_within
    6.19      by (intro continuous_dist ballI continuous_within_compose)
    6.20 -       (auto intro!:  continuous_fst continuous_snd continuous_within_id simp: image_image)
    6.21 +       (auto intro!: continuous_fst continuous_snd continuous_within_id simp: image_image)
    6.22  
    6.23    obtain a where "a \<in> s" and le: "\<And>x. x \<in> s \<Longrightarrow> dist (g a) a \<le> dist (g x) x"
    6.24      using continuous_attains_inf[OF D cont] by auto
     7.1 --- a/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:33:50 2015 +0200
     7.2 +++ b/src/HOL/Topological_Spaces.thy	Sun Apr 12 11:34:09 2015 +0200
     7.3 @@ -1636,7 +1636,7 @@
     7.4      by (rule compactE)
     7.5    from `D \<subseteq> ?C` have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)" by auto
     7.6    with `finite D` have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
     7.7 -    by (simp add: eventually_Ball_finite)
     7.8 +    by (simp add: eventually_ball_finite)
     7.9    with `s \<subseteq> \<Union>D` have "eventually (\<lambda>y. y \<notin> s) (nhds y)"
    7.10      by (auto elim!: eventually_mono [rotated])
    7.11    thus "\<exists>t. open t \<and> y \<in> t \<and> t \<subseteq> - s"