# HG changeset patch # User huffman # Date 1312847857 25200 # Node ID bcc60791b7b92db201217f029265cd4f0474b5be # Parent 8eac3858229c671112f4d3becf02774b2ed262ba remove duplicate lemmas diff -r 8eac3858229c -r bcc60791b7b9 src/HOL/Deriv.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 (\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: "\DERIV f x :> D; DERIV g x :> E\ \ DERIV (\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: - "\(a::'a::division_ring) \ 0; b \ 0\ - \ inverse a - inverse b = - (inverse a * (a - b) * inverse b)" -by (simp add: algebra_simps) - lemma DERIV_inverse_lemma: "\a \ 0; b \ (0::'a::real_normed_field)\ \ (inverse a - inverse b) / h diff -r 8eac3858229c -r bcc60791b7b9 src/HOL/Limits.thy --- 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 @@ "((\x. norm (f x)) ---> 0) net \ (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 "\(f ---> a) net; (g ---> b) net\ \ ((\x. f x + g x) ---> a + b) net" @@ -748,11 +738,6 @@ shows "Zfun (\x. f x ** g x) net" using flip g f by (rule bounded_bilinear.Zfun_prod_Bfun) -lemma inverse_diff_inverse: - "\(a::'a::division_ring) \ 0; b \ 0\ - \ 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 "\r \ norm x; 0 < r\ \ norm (inverse x) \ inverse r"