src/HOL/Limits.thy

   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::real_normed_vector"
   assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> a i) F"
   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"
   shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Sum>i\<in>S. f i x)"
   unfolding continuous_def by (rule tendsto_setsum)

   bounded_bilinear.tendsto_right_zero [OF bounded_bilinear_mult]
 
 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}"
   shows "continuous F f \<Longrightarrow> continuous F (\<lambda>x. (f x)^n)"
   unfolding continuous_def by (rule tendsto_power)

   fixes f :: "'a \<Rightarrow> 'b \<Rightarrow> 'c::{real_normed_algebra,comm_ring_1}"
   assumes "\<And>i. i \<in> S \<Longrightarrow> (f i ---> L i) F"
   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}"
   shows "(\<And>i. i \<in> S \<Longrightarrow> continuous F (f i)) \<Longrightarrow> continuous F (\<lambda>x. \<Prod>i\<in>S. f i x)"
   unfolding continuous_def by (rule tendsto_setprod)

   from x0 x1 have "1 < inverse x"
     by (rule one_less_inverse)
   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}"
   shows "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) ----> 0"
 apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])