add tendsto_const and tendsto_ident_at as simp and intro rules
authorhoelzl
Mon Oct 20 18:33:14 2014 +0200 (2014-10-20)
changeset 58729e8ecc79aee43
parent 58728 42398b610f86
child 58730 b3fd0628f849
add tendsto_const and tendsto_ident_at as simp and intro rules
src/HOL/Deriv.thy
src/HOL/Library/Indicator_Function.thy
src/HOL/Limits.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Bochner_Integration.thy
src/HOL/Series.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Deriv.thy	Mon Oct 20 23:17:28 2014 +0200
     1.2 +++ b/src/HOL/Deriv.thy	Mon Oct 20 18:33:14 2014 +0200
     1.3 @@ -80,10 +80,10 @@
     1.4    using bounded_linear.linear[OF has_derivative_bounded_linear] .
     1.5  
     1.6  lemma has_derivative_ident[derivative_intros, simp]: "((\<lambda>x. x) has_derivative (\<lambda>x. x)) F"
     1.7 -  by (simp add: has_derivative_def tendsto_const)
     1.8 +  by (simp add: has_derivative_def)
     1.9  
    1.10  lemma has_derivative_const[derivative_intros, simp]: "((\<lambda>x. c) has_derivative (\<lambda>x. 0)) F"
    1.11 -  by (simp add: has_derivative_def tendsto_const)
    1.12 +  by (simp add: has_derivative_def)
    1.13  
    1.14  lemma (in bounded_linear) bounded_linear: "bounded_linear f" ..
    1.15  
    1.16 @@ -180,7 +180,7 @@
    1.17      show "(H ---> 0) (at x within s)" by fact
    1.18      show "eventually (\<lambda>n. norm (f n - f x - f' (n - x)) / norm (n - x) \<le> H n) (at x within s)"
    1.19        unfolding eventually_at using e sandwich by auto
    1.20 -  qed (auto simp: le_divide_eq tendsto_const)
    1.21 +  qed (auto simp: le_divide_eq)
    1.22  qed fact
    1.23  
    1.24  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)"
    1.25 @@ -1583,8 +1583,7 @@
    1.26    from \<zeta> have "eventually (\<lambda>x. norm (\<zeta> x) \<le> x) (at_right 0)"
    1.27      by eventually_elim auto
    1.28    then have "((\<lambda>x. norm (\<zeta> x)) ---> 0) (at_right 0)"
    1.29 -    by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"])
    1.30 -       (auto intro: tendsto_const tendsto_ident_at)
    1.31 +    by (rule_tac real_tendsto_sandwich[where f="\<lambda>x. 0" and h="\<lambda>x. x"]) auto
    1.32    then have "(\<zeta> ---> 0) (at_right 0)"
    1.33      by (rule tendsto_norm_zero_cancel)
    1.34    with \<zeta> have "filterlim \<zeta> (at_right 0) (at_right 0)"
     2.1 --- a/src/HOL/Library/Indicator_Function.thy	Mon Oct 20 23:17:28 2014 +0200
     2.2 +++ b/src/HOL/Library/Indicator_Function.thy	Mon Oct 20 18:33:14 2014 +0200
     2.3 @@ -87,8 +87,8 @@
     2.4      "(indicator (\<Union> i. A i) x :: 'a) = 1"
     2.5      using incseqD[OF `incseq A`, of i "n + i" for n] `x \<in> A i` by (auto simp: indicator_def)
     2.6    then show ?thesis
     2.7 -    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
     2.8 -qed (auto simp: indicator_def tendsto_const)
     2.9 +    by (rule_tac LIMSEQ_offset[of _ i]) simp
    2.10 +qed (auto simp: indicator_def)
    2.11  
    2.12  lemma LIMSEQ_indicator_UN:
    2.13    "(\<lambda>k. indicator (\<Union> i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Union>i. A i) x"
    2.14 @@ -112,8 +112,8 @@
    2.15      "(indicator (\<Inter>i. A i) x :: 'a) = 0"
    2.16      using decseqD[OF `decseq A`, of i "n + i" for n] `x \<notin> A i` by (auto simp: indicator_def)
    2.17    then show ?thesis
    2.18 -    by (rule_tac LIMSEQ_offset[of _ i]) (simp add: tendsto_const)
    2.19 -qed (auto simp: indicator_def tendsto_const)
    2.20 +    by (rule_tac LIMSEQ_offset[of _ i]) simp
    2.21 +qed (auto simp: indicator_def)
    2.22  
    2.23  lemma LIMSEQ_indicator_INT:
    2.24    "(\<lambda>k. indicator (\<Inter>i<k. A i) x :: 'a :: {topological_space, one, zero}) ----> indicator (\<Inter>i. A i) x"
     3.1 --- a/src/HOL/Limits.thy	Mon Oct 20 23:17:28 2014 +0200
     3.2 +++ b/src/HOL/Limits.thy	Mon Oct 20 18:33:14 2014 +0200
     3.3 @@ -544,11 +544,8 @@
     3.4    shows "((\<lambda>x. \<Sum>i\<in>S. f i x) ---> (\<Sum>i\<in>S. a i)) F"
     3.5  proof (cases "finite S")
     3.6    assume "finite S" thus ?thesis using assms
     3.7 -    by (induct, simp add: tendsto_const, simp add: tendsto_add)
     3.8 -next
     3.9 -  assume "\<not> finite S" thus ?thesis
    3.10 -    by (simp add: tendsto_const)
    3.11 -qed
    3.12 +    by (induct, simp, simp add: tendsto_add)
    3.13 +qed simp
    3.14  
    3.15  lemma continuous_setsum [continuous_intros]:
    3.16    fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::real_normed_vector"
    3.17 @@ -646,7 +643,7 @@
    3.18  lemma tendsto_power [tendsto_intros]:
    3.19    fixes f :: "'a \<Rightarrow> 'b::{power,real_normed_algebra}"
    3.20    shows "(f ---> a) F \<Longrightarrow> ((\<lambda>x. f x ^ n) ---> a ^ n) F"
    3.21 -  by (induct n) (simp_all add: tendsto_const tendsto_mult)
    3.22 +  by (induct n) (simp_all add: tendsto_mult)
    3.23  
    3.24  lemma continuous_power [continuous_intros]:
    3.25    fixes f :: "'a::t2_space \<Rightarrow> 'b::{power,real_normed_algebra}"
    3.26 @@ -664,11 +661,8 @@
    3.27    shows "((\<lambda>x. \<Prod>i\<in>S. f i x) ---> (\<Prod>i\<in>S. L i)) F"
    3.28  proof (cases "finite S")
    3.29    assume "finite S" thus ?thesis using assms
    3.30 -    by (induct, simp add: tendsto_const, simp add: tendsto_mult)
    3.31 -next
    3.32 -  assume "\<not> finite S" thus ?thesis
    3.33 -    by (simp add: tendsto_const)
    3.34 -qed
    3.35 +    by (induct, simp, simp add: tendsto_mult)
    3.36 +qed simp
    3.37  
    3.38  lemma continuous_setprod [continuous_intros]:
    3.39    fixes f :: "'a \<Rightarrow> 'b::t2_space \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
    3.40 @@ -1480,7 +1474,7 @@
    3.41    hence "(\<lambda>n. inverse (inverse x ^ n)) ----> 0"
    3.42      by (rule LIMSEQ_inverse_realpow_zero)
    3.43    thus ?thesis by (simp add: power_inverse)
    3.44 -qed (rule LIMSEQ_imp_Suc, simp add: tendsto_const)
    3.45 +qed (rule LIMSEQ_imp_Suc, simp)
    3.46  
    3.47  lemma LIMSEQ_power_zero:
    3.48    fixes x :: "'a::{real_normed_algebra_1}"
     4.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Oct 20 23:17:28 2014 +0200
     4.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Oct 20 18:33:14 2014 +0200
     4.3 @@ -3688,7 +3688,7 @@
     4.4        then obtain r where "subseq r" and fr: "\<forall>n. f (r n) = f l"
     4.5          using infinite_enumerate by blast
     4.6        then have "subseq r \<and> (f \<circ> r) ----> f l"
     4.7 -        by (simp add: fr tendsto_const o_def)
     4.8 +        by (simp add: fr o_def)
     4.9        with f show "\<exists>l\<in>s. \<exists>r. subseq r \<and> (f \<circ> r) ----> l"
    4.10          by auto
    4.11      next
    4.12 @@ -7526,8 +7526,6 @@
    4.13    ultimately show "\<exists>!x\<in>s. g x = x" using `a \<in> s` by blast
    4.14  qed
    4.15  
    4.16 -declare tendsto_const [intro] (* FIXME: move *)
    4.17 -
    4.18  no_notation
    4.19    eucl_less (infix "<e" 50)
    4.20  
     5.1 --- a/src/HOL/Probability/Bochner_Integration.thy	Mon Oct 20 23:17:28 2014 +0200
     5.2 +++ b/src/HOL/Probability/Bochner_Integration.thy	Mon Oct 20 18:33:14 2014 +0200
     5.3 @@ -2335,7 +2335,7 @@
     5.4           (auto split: split_indicator simp: natceiling_le_eq) }
     5.5    from filterlim_cong[OF refl refl this]
     5.6    have "AE x in M. (\<lambda>i. f x * indicator {..real i} x) ----> f x"
     5.7 -    by (simp add: tendsto_const)
     5.8 +    by simp
     5.9    have "(\<lambda>i. \<integral> x. f x * indicator {..real i} x \<partial>M) ----> x"
    5.10      using conv filterlim_real_sequentially by (rule filterlim_compose)
    5.11    have M_measure[simp]: "borel_measurable M = borel_measurable borel"
    5.12 @@ -2439,7 +2439,7 @@
    5.13      then 
    5.14      show "(\<lambda>i. f' i x) ----> integral\<^sup>L M (f x)"
    5.15        unfolding f'_def
    5.16 -      by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq tendsto_const)
    5.17 +      by (cases "integrable M (f x)") (simp_all add: not_integrable_integral_eq)
    5.18    qed
    5.19  qed
    5.20  
     6.1 --- a/src/HOL/Series.thy	Mon Oct 20 23:17:28 2014 +0200
     6.2 +++ b/src/HOL/Series.thy	Mon Oct 20 18:33:14 2014 +0200
     6.3 @@ -45,7 +45,7 @@
     6.4    by (simp add: suminf_def sums_def lim_def)
     6.5  
     6.6  lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
     6.7 -  unfolding sums_def by (simp add: tendsto_const)
     6.8 +  unfolding sums_def by simp
     6.9  
    6.10  lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
    6.11    by (rule sums_zero [THEN sums_summable])
    6.12 @@ -84,7 +84,7 @@
    6.13    note eq = this
    6.14    show ?thesis unfolding sums_def
    6.15      by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
    6.16 -       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
    6.17 +       (simp add: eq atLeast0LessThan del: add_Suc_right)
    6.18  qed
    6.19  
    6.20  lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
    6.21 @@ -232,7 +232,7 @@
    6.22      with tendsto_add[OF this tendsto_const, of "- f 0"]
    6.23      show "(\<lambda>i. f (Suc i)) sums s"
    6.24        by (simp add: sums_def)
    6.25 -  qed (auto intro: tendsto_add tendsto_const simp: sums_def)
    6.26 +  qed (auto intro: tendsto_add simp: sums_def)
    6.27    finally show ?thesis ..
    6.28  qed
    6.29  
     7.1 --- a/src/HOL/Topological_Spaces.thy	Mon Oct 20 23:17:28 2014 +0200
     7.2 +++ b/src/HOL/Topological_Spaces.thy	Mon Oct 20 18:33:14 2014 +0200
     7.3 @@ -1171,10 +1171,10 @@
     7.4      by (auto simp: min_less_iff_disj elim: eventually_elim1)
     7.5  qed
     7.6  
     7.7 -lemma tendsto_ident_at [tendsto_intros]: "((\<lambda>x. x) ---> a) (at a within s)"
     7.8 +lemma tendsto_ident_at [tendsto_intros, simp, intro]: "((\<lambda>x. x) ---> a) (at a within s)"
     7.9    unfolding tendsto_def eventually_at_topological by auto
    7.10  
    7.11 -lemma (in topological_space) tendsto_const [tendsto_intros]: "((\<lambda>x. k) ---> k) F"
    7.12 +lemma (in topological_space) tendsto_const [tendsto_intros, simp, intro]: "((\<lambda>x. k) ---> k) F"
    7.13    by (simp add: tendsto_def)
    7.14  
    7.15  lemma (in t2_space) tendsto_unique:
    7.16 @@ -1202,7 +1202,7 @@
    7.17  
    7.18  lemma (in t2_space) tendsto_const_iff:
    7.19    assumes "\<not> trivial_limit F" shows "((\<lambda>x. a :: 'a) ---> b) F \<longleftrightarrow> a = b"
    7.20 -  by (safe intro!: tendsto_const tendsto_unique [OF assms tendsto_const])
    7.21 +  by (auto intro!: tendsto_unique [OF assms tendsto_const])
    7.22  
    7.23  lemma increasing_tendsto:
    7.24    fixes f :: "_ \<Rightarrow> 'a::order_topology"
    7.25 @@ -1689,7 +1689,7 @@
    7.26  
    7.27  lemma LIMSEQ_le_const2:
    7.28    "\<lbrakk>X ----> (x::'a::linorder_topology); \<exists>N. \<forall>n\<ge>N. X n \<le> a\<rbrakk> \<Longrightarrow> x \<le> a"
    7.29 -  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) (auto simp: tendsto_const)
    7.30 +  by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
    7.31  
    7.32  lemma convergentD: "convergent X ==> \<exists>L. (X ----> L)"
    7.33  by (simp add: convergent_def)
    7.34 @@ -2117,10 +2117,10 @@
    7.35  qed
    7.36  
    7.37  lemma continuous_on_id[continuous_intros]: "continuous_on s (\<lambda>x. x)"
    7.38 -  unfolding continuous_on_def by (fast intro: tendsto_ident_at)
    7.39 +  unfolding continuous_on_def by fast
    7.40  
    7.41  lemma continuous_on_const[continuous_intros]: "continuous_on s (\<lambda>x. c)"
    7.42 -  unfolding continuous_on_def by (auto intro: tendsto_const)
    7.43 +  unfolding continuous_on_def by auto
    7.44  
    7.45  lemma continuous_on_compose[continuous_intros]:
    7.46    "continuous_on s f \<Longrightarrow> continuous_on (f ` s) g \<Longrightarrow> continuous_on s (g o f)"
     8.1 --- a/src/HOL/Transcendental.thy	Mon Oct 20 23:17:28 2014 +0200
     8.2 +++ b/src/HOL/Transcendental.thy	Mon Oct 20 18:33:14 2014 +0200
     8.3 @@ -1347,7 +1347,7 @@
     8.4      unfolding isCont_def
     8.5      by (subst filterlim_cong[OF _ refl, of _ "nhds (ln 0)" _ "\<lambda>_. ln 0"])
     8.6         (auto simp: ln_neg_is_const not_less eventually_at dist_real_def
     8.7 -                intro!: tendsto_const exI[of _ "\<bar>x\<bar>"])
     8.8 +                intro!: exI[of _ "\<bar>x\<bar>"])
     8.9  qed
    8.10  
    8.11  lemma tendsto_ln [tendsto_intros]:
    8.12 @@ -2214,7 +2214,7 @@
    8.13        unfolding eventually_at_right[OF zero_less_one]
    8.14        using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
    8.15    qed (simp_all add: at_eq_sup_left_right)
    8.16 -qed (simp add: tendsto_const)
    8.17 +qed simp
    8.18  
    8.19  lemma tendsto_exp_limit_at_top:
    8.20    fixes x :: real
    8.21 @@ -3733,7 +3733,7 @@
    8.22  proof (cases "x = 0")
    8.23    case True
    8.24    thus ?thesis
    8.25 -    unfolding One_nat_def by (auto simp add: tendsto_const)
    8.26 +    unfolding One_nat_def by auto
    8.27  next
    8.28    case False
    8.29    have "norm x \<le> 1" and "x \<le> 1" and "-1 \<le> x" using assms by auto