# HG changeset patch
# User hoelzl
# Date 1413822794 -7200
# Node ID e8ecc79aee432d084a1539f69bb95a656f4140fd
# Parent  42398b610f865c1699949e756defd44caefb70d5
add tendsto_const and tendsto_ident_at as simp and intro rules

diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Deriv.thy
--- 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)"
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Library/Indicator_Function.thy
--- 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"
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Limits.thy
--- 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}"
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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)
 
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Probability/Bochner_Integration.thy
--- 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
 
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Series.thy
--- 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
 
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Topological_Spaces.thy
--- 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)"
diff -r 42398b610f86 -r e8ecc79aee43 src/HOL/Transcendental.thy
--- 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