remove duplicate lemmas
authorhuffman
Mon, 08 Aug 2011 16:57:37 -0700
changeset 44079 bcc60791b7b9
parent 44078 8eac3858229c
child 44080 53d95b52954c
remove duplicate lemmas
src/HOL/Deriv.thy
src/HOL/Limits.thy
--- 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"