--- a/src/HOL/Deriv.thy Mon Aug 08 16:19:57 2011 -0700
+++ b/src/HOL/Deriv.thy Mon Aug 08 16:57:37 2011 -0700
@@ -42,11 +42,6 @@
lemma DERIV_ident [simp]: "DERIV (\<lambda>x. x) x :> 1"
by (simp add: deriv_def cong: LIM_cong)
-lemma add_diff_add:
- fixes a b c d :: "'a::ab_group_add"
- shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
-
lemma DERIV_add:
"\<lbrakk>DERIV f x :> D; DERIV g x :> E\<rbrakk> \<Longrightarrow> DERIV (\<lambda>x. f x + g x) x :> D + E"
by (simp only: deriv_def add_diff_add add_divide_distrib LIM_add)
@@ -141,11 +136,6 @@
lemma DERIV_iff2: "(DERIV f x :> D) = ((%z. (f(z) - f(x)) / (z-x)) -- x --> D)"
by (simp add: deriv_def diff_minus [symmetric] DERIV_LIM_iff)
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: algebra_simps)
-
lemma DERIV_inverse_lemma:
"\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
\<Longrightarrow> (inverse a - inverse b) / h
--- a/src/HOL/Limits.thy Mon Aug 08 16:19:57 2011 -0700
+++ b/src/HOL/Limits.thy Mon Aug 08 16:57:37 2011 -0700
@@ -644,16 +644,6 @@
"((\<lambda>x. norm (f x)) ---> 0) net \<longleftrightarrow> (f ---> 0) net"
unfolding tendsto_iff dist_norm by simp
-lemma add_diff_add:
- fixes a b c d :: "'a::ab_group_add"
- shows "(a + c) - (b + d) = (a - b) + (c - d)"
-by simp
-
-lemma minus_diff_minus:
- fixes a b :: "'a::ab_group_add"
- shows "(- a) - (- b) = - (a - b)"
-by simp
-
lemma tendsto_add [tendsto_intros]:
fixes a b :: "'a::real_normed_vector"
shows "\<lbrakk>(f ---> a) net; (g ---> b) net\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x + g x) ---> a + b) net"
@@ -748,11 +738,6 @@
shows "Zfun (\<lambda>x. f x ** g x) net"
using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun)
-lemma inverse_diff_inverse:
- "\<lbrakk>(a::'a::division_ring) \<noteq> 0; b \<noteq> 0\<rbrakk>
- \<Longrightarrow> inverse a - inverse b = - (inverse a * (a - b) * inverse b)"
-by (simp add: algebra_simps)
-
lemma Bfun_inverse_lemma:
fixes x :: "'a::real_normed_div_algebra"
shows "\<lbrakk>r \<le> norm x; 0 < r\<rbrakk> \<Longrightarrow> norm (inverse x) \<le> inverse r"