--- a/src/HOL/Deriv.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Deriv.thy Mon Oct 20 18:33:14 2014 +0200
@@ -80,10 +80,10 @@
using bounded_linear.linear[OF has_derivative_bounded_linear] .
lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
- by (simp add: has_derivative_def tendsto_const)
+ by (simp add: has_derivative_def)
lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
- by (simp add: has_derivative_def tendsto_const)
+ by (simp add: has_derivative_def)
lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
@@ -180,7 +180,7 @@
show "(H ---> 0) (at x within s)" by fact
show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)"
unfolding eventually_at using e sandwich by auto
- qed (auto simp: le_divide_eq tendsto_const)
+ qed (auto simp: le_divide_eq)
qed fact
lemma has_derivative_subset: "(f has_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_derivative f') (at x within t)"
@@ -1583,8 +1583,7 @@
from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
by eventually_elim auto
then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
- by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
- (auto intro: tendsto_const tendsto_ident_at)
+ by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto
then have "(\<zeta> ---> 0) (at_right 0)"
by (rule tendsto_norm_zero_cancel)
with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
--- a/src/HOL/Library/Indicator_Function.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Library/Indicator_Function.thy Mon Oct 20 18:33:14 2014 +0200
@@ -87,8 +87,8 @@
"(indicator (\<Union> i. A i) x :: 'a) = 1"
using incseqD[OF `incseq A`, of i "n + i" for n] `x \<in> A i` by (auto simp: indicator_def)
then show ?thesis
- by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
-qed (auto simp: indicator_def tendsto_const)
+ by (rule_tac LIMSEQ_offset[of _ i]) simp
+qed (auto simp: indicator_def)
lemma LIMSEQ_indicator_UN:
"(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
@@ -112,8 +112,8 @@
"(indicator (\<Inter>i. A i) x :: 'a) = 0"
using decseqD[OF `decseq A`, of i "n + i" for n] `x \<notin> A i` by (auto simp: indicator_def)
then show ?thesis
- by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
-qed (auto simp: indicator_def tendsto_const)
+ by (rule_tac LIMSEQ_offset[of _ i]) simp
+qed (auto simp: indicator_def)
lemma LIMSEQ_indicator_INT:
"(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
--- a/src/HOL/Limits.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Limits.thy Mon Oct 20 18:33:14 2014 +0200
@@ -544,11 +544,8 @@
shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) F"
proof (cases "finite S")
assume "finite S" thus ?thesis using assms
- by (induct, simp add: tendsto_const, simp add: tendsto_add)
-next
- assume "\<not> finite S" thus ?thesis
- by (simp add: tendsto_const)
-qed
+ by (induct, simp, simp add: tendsto_add)
+qed simp
lemma continuous_setsum [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
@@ -646,7 +643,7 @@
lemma tendsto_power [tendsto_intros]:
fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
- by (induct n) (simp_all add: tendsto_const tendsto_mult)
+ by (induct n) (simp_all add: tendsto_mult)
lemma continuous_power [continuous_intros]:
fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
@@ -664,11 +661,8 @@
shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) F"
proof (cases "finite S")
assume "finite S" thus ?thesis using assms
- by (induct, simp add: tendsto_const, simp add: tendsto_mult)
-next
- assume "\<not> finite S" thus ?thesis
- by (simp add: tendsto_const)
-qed
+ by (induct, simp, simp add: tendsto_mult)
+qed simp
lemma continuous_setprod [continuous_intros]:
fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
@@ -1480,7 +1474,7 @@
hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
by (rule LIMSEQ_inverse_realpow_zero)
thus ?thesis by (simp add: power_inverse)
-qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
+qed (rule LIMSEQ_imp_Suc, simp)
lemma LIMSEQ_power_zero:
fixes x :: "'a::{real_normed_algebra_1}"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Mon Oct 20 18:33:14 2014 +0200
@@ -3688,7 +3688,7 @@
then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
using infinite_enumerate by blast
then have "subseq r \<and> (f \<circ> r) ----> f l"
- by (simp add: fr tendsto_const o_def)
+ by (simp add: fr o_def)
with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
by auto
next
@@ -7526,8 +7526,6 @@
ultimately show "\<exists>!x\<in>s. g x = x" using `a \<in> s` by blast
qed
-declare tendsto_const [intro] (* FIXME: move *)
-
no_notation
eucl_less (infix "<e" 50)
--- a/src/HOL/Probability/Bochner_Integration.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Probability/Bochner_Integration.thy Mon Oct 20 18:33:14 2014 +0200
@@ -2335,7 +2335,7 @@
(auto split: split_indicator simp: natceiling_le_eq) }
from filterlim_cong[OF refl refl this]
have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
- by (simp add: tendsto_const)
+ by simp
have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
using conv filterlim_real_sequentially by (rule filterlim_compose)
have M_measure[simp]: "borel_measurable M = borel_measurable borel"
@@ -2439,7 +2439,7 @@
then
show "(\<lambda>i. f' i x) ----> integral\<^sup>L M (f x)"
unfolding f'_def
- by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq tendsto_const)
+ by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
qed
qed
--- a/src/HOL/Series.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Series.thy Mon Oct 20 18:33:14 2014 +0200
@@ -45,7 +45,7 @@
by (simp add: suminf_def sums_def lim_def)
lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
- unfolding sums_def by (simp add: tendsto_const)
+ unfolding sums_def by simp
lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
by (rule sums_zero [THEN sums_summable])
@@ -84,7 +84,7 @@
note eq = this
show ?thesis unfolding sums_def
by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
- (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
+ (simp add: eq atLeast0LessThan del: add_Suc_right)
qed
lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
@@ -232,7 +232,7 @@
with tendsto_add[OF this tendsto_const, of "- f 0"]
show "(\<lambda>i. f (Suc i)) sums s"
by (simp add: sums_def)
- qed (auto intro: tendsto_add tendsto_const simp: sums_def)
+ qed (auto intro: tendsto_add simp: sums_def)
finally show ?thesis ..
qed
--- a/src/HOL/Topological_Spaces.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Topological_Spaces.thy Mon Oct 20 18:33:14 2014 +0200
@@ -1171,10 +1171,10 @@
by (auto simp: min_less_iff_disj elim: eventually_elim1)
qed
-lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
+lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
unfolding tendsto_def eventually_at_topological by auto
-lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
+lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F"
by (simp add: tendsto_def)
lemma (in t2_space) tendsto_unique:
@@ -1202,7 +1202,7 @@
lemma (in t2_space) tendsto_const_iff:
assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
- by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
+ by (auto intro!: tendsto_unique [OF assms tendsto_const])
lemma increasing_tendsto:
fixes f :: "_ \<Rightarrow> 'a::order_topology"
@@ -1689,7 +1689,7 @@
lemma LIMSEQ_le_const2:
"\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
- by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
+ by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
by (simp add: convergent_def)
@@ -2117,10 +2117,10 @@
qed
lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
- unfolding continuous_on_def by (fast intro: tendsto_ident_at)
+ unfolding continuous_on_def by fast
lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
- unfolding continuous_on_def by (auto intro: tendsto_const)
+ unfolding continuous_on_def by auto
lemma continuous_on_compose[continuous_intros]:
"continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
--- a/src/HOL/Transcendental.thy Mon Oct 20 23:17:28 2014 +0200
+++ b/src/HOL/Transcendental.thy Mon Oct 20 18:33:14 2014 +0200
@@ -1347,7 +1347,7 @@
unfolding isCont_def
by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
(auto simp: ln_neg_is_const not_less eventually_at dist_real_def
- intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
+ intro!: exI[of _ "\<bar>x\<bar>"])
qed
lemma tendsto_ln [tendsto_intros]:
@@ -2214,7 +2214,7 @@
unfolding eventually_at_right[OF zero_less_one]
using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
qed (simp_all add: at_eq_sup_left_right)
-qed (simp add: tendsto_const)
+qed simp
lemma tendsto_exp_limit_at_top:
fixes x :: real
@@ -3733,7 +3733,7 @@
proof (cases "x = 0")
case True
thus ?thesis
- unfolding One_nat_def by (auto simp add: tendsto_const)
+ unfolding One_nat_def by auto
next
case False
have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto