src/HOL/Deriv.thy
 changeset 29667 53103fc8ffa3 parent 29472 a63a2e46cec9 child 29803 c56a5571f60a
```--- a/src/HOL/Deriv.thy	Sun Jan 18 13:58:17 2009 +0100
+++ b/src/HOL/Deriv.thy	Wed Jan 28 16:29:16 2009 +0100
@@ -141,7 +141,7 @@
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)"

lemma DERIV_inverse_lemma:
"\<lbrakk>a \<noteq> 0; b \<noteq> (0::'a::real_normed_field)\<rbrakk>
@@ -206,7 +206,7 @@
case (Suc k)
from DERIV_mult' [OF f Suc] show ?case
apply (simp only: of_nat_Suc ring_distribs mult_1_left)
-    apply (simp only: power_Suc right_distrib mult_ac add_ac)
+    apply (simp only: power_Suc algebra_simps)
done
qed

@@ -724,7 +724,7 @@
from isCont_bounded [OF le this]
obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
-        by (simp add: M3 compare_rls)
+        by (simp add: M3 algebra_simps)
have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k
by (auto intro: order_le_less_trans [of _ k])
with Minv
@@ -1398,7 +1398,7 @@
have "?h b - ?h a =
((f b)*(g b) - (f a)*(g b) - (g b)*(f b) + (g a)*(f b)) -
((f b)*(g a) - (f a)*(g a) - (g b)*(f a) + (g a)*(f a))"
hence "?h b - ?h a = 0" by auto
}
ultimately have "(b - a) * (g'c * (f b - f a) - f'c * (g b - g a)) = 0" by auto
@@ -1427,7 +1427,7 @@

lemma coeff_pderiv: "coeff (pderiv p) n = of_nat (Suc n) * coeff p (Suc n)"
apply (induct p arbitrary: n, simp)
-  apply (simp add: pderiv_pCons coeff_pCons ring_simps split: nat.split)
+  apply (simp add: pderiv_pCons coeff_pCons algebra_simps split: nat.split)
done

lemma pderiv_eq_0_iff: "pderiv p = 0 \<longleftrightarrow> degree p = 0"
@@ -1451,21 +1451,21 @@

lemma pderiv_add: "pderiv (p + q) = pderiv p + pderiv q"
-by (rule poly_ext, simp add: coeff_pderiv ring_simps)
+by (rule poly_ext, simp add: coeff_pderiv algebra_simps)

lemma pderiv_minus: "pderiv (- p) = - pderiv p"
by (rule poly_ext, simp add: coeff_pderiv)

lemma pderiv_diff: "pderiv (p - q) = pderiv p - pderiv q"
-by (rule poly_ext, simp add: coeff_pderiv ring_simps)
+by (rule poly_ext, simp add: coeff_pderiv algebra_simps)

lemma pderiv_smult: "pderiv (smult a p) = smult a (pderiv p)"
-by (rule poly_ext, simp add: coeff_pderiv ring_simps)
+by (rule poly_ext, simp add: coeff_pderiv algebra_simps)

lemma pderiv_mult: "pderiv (p * q) = p * pderiv q + q * pderiv p"
apply (induct p)
apply simp