add type annotations for DERIV
authorhuffman
Sat Sep 30 17:10:55 2006 +0200 (2006-09-30)
changeset 20792add17d26151b
parent 20791 497e1c9d4a9f
child 20793 3b0489715b0e
add type annotations for DERIV
src/HOL/Hyperreal/Integration.thy
src/HOL/Hyperreal/MacLaurin.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/Series.thy
     1.1 --- a/src/HOL/Hyperreal/Integration.thy	Sat Sep 30 14:32:36 2006 +0200
     1.2 +++ b/src/HOL/Hyperreal/Integration.thy	Sat Sep 30 17:10:55 2006 +0200
     1.3 @@ -871,6 +871,7 @@
     1.4  by (blast dest: partition_exists) 
     1.5  
     1.6  lemma monotonic_anti_derivative:
     1.7 +  fixes f g :: "real => real" shows
     1.8       "[| a \<le> b; \<forall>c. a \<le> c & c \<le> b --> f' c \<le> g' c;
     1.9           \<forall>x. DERIV f x :> f' x; \<forall>x. DERIV g x :> g' x |]
    1.10        ==> f b - f a \<le> g b - g a"
     2.1 --- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Sep 30 14:32:36 2006 +0200
     2.2 +++ b/src/HOL/Hyperreal/MacLaurin.thy	Sat Sep 30 17:10:55 2006 +0200
     2.3 @@ -100,6 +100,7 @@
     2.4  
     2.5  
     2.6  lemma Maclaurin_lemma3:
     2.7 +  fixes difg :: "nat => real => real" shows
     2.8       "[|\<forall>k t. k < Suc m \<and> 0\<le>t & t\<le>h \<longrightarrow> DERIV (difg k) t :> difg (Suc k) t;
     2.9          \<forall>k<Suc m. difg k 0 = 0; DERIV (difg n) t :> 0;  n < m; 0 < t;
    2.10          t < h|]
     3.1 --- a/src/HOL/Hyperreal/Poly.thy	Sat Sep 30 14:32:36 2006 +0200
     3.2 +++ b/src/HOL/Hyperreal/Poly.thy	Sat Sep 30 17:10:55 2006 +0200
     3.3 @@ -224,7 +224,7 @@
     3.4  lemma pderiv_Cons: "pderiv (h#t) = pderiv_aux 1 t"
     3.5  by (simp add: pderiv_def)
     3.6  
     3.7 -lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c) x :> D * c"
     3.8 +lemma DERIV_cmult2: "DERIV f x :> D ==> DERIV (%x. (f x) * c :: real) x :> D * c"
     3.9  by (simp add: DERIV_cmult mult_commute [of _ c])
    3.10  
    3.11  lemma DERIV_pow2: "DERIV (%x. x ^ Suc n) x :> real (Suc n) * (x ^ n)"
    3.12 @@ -246,7 +246,7 @@
    3.13          x ^ n * poly (pderiv_aux (Suc n) p) x "
    3.14  by (simp add: lemma_DERIV_poly1 del: realpow_Suc)
    3.15  
    3.16 -lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x) x :> D"
    3.17 +lemma DERIV_add_const: "DERIV f x :> D ==>  DERIV (%x. a + f x :: real) x :> D"
    3.18  by (rule lemma_DERIV_subst, rule DERIV_add, auto)
    3.19  
    3.20  lemma poly_DERIV: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
     4.1 --- a/src/HOL/Hyperreal/Series.thy	Sat Sep 30 14:32:36 2006 +0200
     4.2 +++ b/src/HOL/Hyperreal/Series.thy	Sat Sep 30 17:10:55 2006 +0200
     4.3 @@ -539,7 +539,7 @@
     4.4  
     4.5  lemma DERIV_sumr [rule_format (no_asm)]:
     4.6       "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
     4.7 -      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
     4.8 +      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x :: real) x :> (\<Sum>r=m..<n. f' r x)"
     4.9  apply (induct "n")
    4.10  apply (auto intro: DERIV_add)
    4.11  done