move MOST and INFM in Infinite_Set to Filter; change them to abbreviations over the cofinite filter
--- 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
--- 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
--- 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
--- 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
--- 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]:
--- 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
--- 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"