# HG changeset patch
# User hoelzl
# Date 1246378915 -7200
# Node ID eba74a5790d227c7d8e5159a0f73a04c5b934cf7
# Parent  6fb86c61747c6944728903979dba09a0c53d38dc
use DERIV_intros

diff -r 6fb86c61747c -r eba74a5790d2 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 30 18:16:22 2009 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 30 18:21:55 2009 +0200
@@ -2670,11 +2670,6 @@
 "DERIV_floatarith x (Num f)           = Num 0" |
 "DERIV_floatarith x (Atom n)          = (if x = n then Num 1 else Num 0)"
 
-lemma DERIV_chain'': "\<lbrakk>DERIV g (f x) :> E ; DERIV f x :> D; x' = E * D \<rbrakk> \<Longrightarrow>
-  DERIV (\<lambda>x. g (f x)) x :> x'" using DERIV_chain' by auto
-
-lemma DERIV_cong: "\<lbrakk> DERIV f x :> X ; X = X' \<rbrakk> \<Longrightarrow> DERIV f x :> X'" by simp
-
 lemma DERIV_floatarith:
   assumes "n < length vs"
   assumes isDERIV: "isDERIV n f (vs[n := x])"
@@ -2682,31 +2677,20 @@
                interpret_floatarith (DERIV_floatarith n f) (vs[n := x])"
    (is "DERIV (?i f) x :> _")
 using isDERIV proof (induct f arbitrary: x)
-  case (Add a b) thus ?case by (auto intro: DERIV_add)
-next case (Mult a b) thus ?case by (auto intro!: DERIV_mult[THEN DERIV_cong])
-next case (Minus a) thus ?case by (auto intro!: DERIV_minus[THEN DERIV_cong])
-next case (Inverse a) thus ?case
-    by (auto intro!: DERIV_inverse_fun[THEN DERIV_cong] DERIV_inverse[THEN DERIV_cong]
+     case (Inverse a) thus ?case
+    by (auto intro!: DERIV_intros
              simp add: algebra_simps power2_eq_square)
 next case (Cos a) thus ?case
-  by (auto intro!: DERIV_chain''[of cos "?i a"]
-                   DERIV_cos[THEN DERIV_cong]
+  by (auto intro!: DERIV_intros
            simp del: interpret_floatarith.simps(5)
            simp add: interpret_floatarith_sin interpret_floatarith.simps(5)[of a])
-next case (Arctan a) thus ?case
-  by (auto intro!: DERIV_chain''[of arctan "?i a"] DERIV_arctan[THEN DERIV_cong])
-next case (Exp a) thus ?case
-  by (auto intro!: DERIV_chain''[of exp "?i a"] DERIV_exp[THEN DERIV_cong])
 next case (Power a n) thus ?case
-  by (cases n, auto intro!: DERIV_power_Suc[THEN DERIV_cong]
+  by (cases n, auto intro!: DERIV_intros
                     simp del: power_Suc simp add: real_eq_of_nat)
-next case (Sqrt a) thus ?case
-    by (auto intro!: DERIV_chain''[of sqrt "?i a"] DERIV_real_sqrt[THEN DERIV_cong])
 next case (Ln a) thus ?case
-    by (auto intro!: DERIV_chain''[of ln "?i a"] DERIV_ln[THEN DERIV_cong]
-                     simp add: divide_inverse)
+    by (auto intro!: DERIV_intros simp add: divide_inverse)
 next case (Atom i) thus ?case using `n < length vs` by auto
-qed auto
+qed (auto intro!: DERIV_intros)
 
 declare approx.simps[simp del]
 
diff -r 6fb86c61747c -r eba74a5790d2 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 18:16:22 2009 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jun 30 18:21:55 2009 +0200
@@ -85,13 +85,7 @@
 by (rule lemma_DERIV_subst, rule DERIV_add, auto)
 
 lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
-apply (induct p)
-apply simp
-apply (simp add: pderiv_pCons)
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_add DERIV_mult DERIV_const DERIV_ident | assumption)+
-apply simp
-done
+  by (induct p, auto intro!: DERIV_intros simp add: pderiv_pCons)
 
 text{* Consequences of the derivative theorem above*}
 
diff -r 6fb86c61747c -r eba74a5790d2 src/HOL/MacLaurin.thy
--- a/src/HOL/MacLaurin.thy	Tue Jun 30 18:16:22 2009 +0200
+++ b/src/HOL/MacLaurin.thy	Tue Jun 30 18:21:55 2009 +0200
@@ -91,7 +91,7 @@
  apply (simp (no_asm) add: divide_inverse mult_assoc del: fact_Suc power_Suc)
  apply (rule DERIV_cmult)
  apply (rule lemma_DERIV_subst)
-  apply (best intro: DERIV_chain2 intro!: DERIV_intros)
+  apply (best intro!: DERIV_intros)
  apply (subst fact_Suc)
  apply (subst real_of_nat_mult)
  apply (simp add: mult_ac)
@@ -565,9 +565,7 @@
     apply (clarify)
     apply (subst (1 2 3) mod_Suc_eq_Suc_mod)
     apply (cut_tac m=m in mod_exhaust_less_4)
-    apply (safe, simp_all)
-    apply (rule DERIV_minus, simp)
-    apply (rule lemma_DERIV_subst, rule DERIV_minus, rule DERIV_cos, simp)
+    apply (safe, auto intro!: DERIV_intros)
     done
   from Maclaurin_all_le [OF diff_0 DERIV_diff]
   obtain t where t1: "\<bar>t\<bar> \<le> \<bar>x\<bar>" and
diff -r 6fb86c61747c -r eba74a5790d2 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Jun 30 18:16:22 2009 +0200
+++ b/src/HOL/Transcendental.thy	Tue Jun 30 18:21:55 2009 +0200
@@ -784,9 +784,8 @@
 	  also have "\<dots> = \<bar>f n * real (Suc n) * R' ^ n\<bar> * \<bar>x - y\<bar>" unfolding abs_mult real_mult_assoc[symmetric] by algebra
 	  finally show ?thesis .
 	qed }
-      { fix n
-	from DERIV_pow[of "Suc n" x0, THEN DERIV_cmult[where c="f n"]]
-	show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)" unfolding real_mult_assoc by auto }
+      { fix n show "DERIV (\<lambda> x. ?f x n) x0 :> (?f' x0 n)"
+	  by (auto intro!: DERIV_intros simp del: power_Suc) }
       { fix x assume "x \<in> {-R' <..< R'}" hence "R' \<in> {-R <..< R}" and "norm x < norm R'" using assms `R' < R` by auto
 	have "summable (\<lambda> n. f n * x^n)"
 	proof (rule summable_le2[THEN conjunct1, OF _ powser_insidea[OF converges[OF `R' \<in> {-R <..< R}`] `norm x < norm R'`]], rule allI)
@@ -1416,24 +1415,17 @@
 by auto
 
 lemma DERIV_cos_realpow2b: "DERIV (%x. (cos x)\<twosuperior>) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_realpow2a, auto)
-done
+  by (auto intro!: DERIV_intros)
 
 (* most useful *)
 lemma DERIV_cos_cos_mult3 [simp]:
      "DERIV (%x. cos(x)*cos(x)) x :> -(2 * cos(x) * sin(x))"
-apply (rule lemma_DERIV_subst)
-apply (rule DERIV_cos_cos_mult2, auto)
-done
+  by (auto intro!: DERIV_intros)
 
 lemma DERIV_sin_circle_all: 
      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :>  
              (2*cos(x)*sin(x) - 2*cos(x)*sin(x))"
-apply (simp only: diff_minus, safe)
-apply (rule DERIV_add) 
-apply (auto simp add: numeral_2_eq_2)
-done
+  by (auto intro!: DERIV_intros)
 
 lemma DERIV_sin_circle_all_zero [simp]:
      "\<forall>x. DERIV (%x. (sin x)\<twosuperior> + (cos x)\<twosuperior>) x :> 0"
@@ -1524,11 +1516,7 @@
      "\<forall>x.  
          DERIV (%x. (sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
                (cos (x + y) - (cos x * cos y - sin x * sin y)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2) 
-  --{*replaces the old @{text DERIV_tac}*}
-apply (auto simp add: algebra_simps)
-done
+  by (auto intro!: DERIV_intros simp add: algebra_simps)
 
 lemma sin_cos_add [simp]:
      "(sin (x + y) - (sin x * cos y + cos x * sin y)) ^ 2 +  
@@ -1550,10 +1538,8 @@
 
 lemma lemma_DERIV_sin_cos_minus:
     "\<forall>x. DERIV (%x. (sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2) x :> 0"
-apply (safe, rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)
-apply (simp add: algebra_simps)
-done
+  by (auto intro!: DERIV_intros simp add: algebra_simps)
+
 
 lemma sin_cos_minus: 
     "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0"
@@ -2121,10 +2107,7 @@
 
 lemma lemma_DERIV_tan:
      "cos x \<noteq> 0 ==> DERIV (%x. sin(x)/cos(x)) x :> inverse((cos x)\<twosuperior>)"
-apply (rule lemma_DERIV_subst)
-apply (best intro!: DERIV_intros intro: DERIV_chain2) 
-apply (auto simp add: divide_inverse numeral_2_eq_2)
-done
+  by (auto intro!: DERIV_intros simp add: field_simps numeral_2_eq_2)
 
 lemma DERIV_tan [simp]: "cos x \<noteq> 0 ==> DERIV tan x :> inverse((cos x)\<twosuperior>)"
 by (auto dest: lemma_DERIV_tan simp add: tan_def [symmetric])
@@ -2594,11 +2577,7 @@
 by (simp only: cos_add sin_add real_of_nat_Suc add_divide_distrib left_distrib, auto)
 
 lemma DERIV_sin_add [simp]: "DERIV (%x. sin (x + k)) xa :> cos (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = sin and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+  by (auto intro!: DERIV_intros)
 
 lemma sin_cos_npi [simp]: "sin (real (Suc (2 * n)) * pi / 2) = (-1) ^ n"
 proof -
@@ -2639,11 +2618,7 @@
 by (simp only: cos_add sin_add real_of_nat_Suc left_distrib right_distrib add_divide_distrib, auto)
 
 lemma DERIV_cos_add [simp]: "DERIV (%x. cos (x + k)) xa :> - sin (xa + k)"
-apply (rule lemma_DERIV_subst)
-apply (rule_tac f = cos and g = "%x. x + k" in DERIV_chain2)
-apply (best intro!: DERIV_intros intro: DERIV_chain2)+
-apply (simp (no_asm))
-done
+  by (auto intro!: DERIV_intros)
 
 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
 by (auto simp add: sin_zero_iff even_mult_two_ex)