src/HOL/Deriv.thy
changeset 29803 c56a5571f60a
parent 29667 53103fc8ffa3
child 29975 28c5322f0df3
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/Deriv.thy	Wed Feb 04 18:10:07 2009 +0100
     1.2 +++ b/src/HOL/Deriv.thy	Thu Feb 05 11:34:42 2009 +0100
     1.3 @@ -1038,6 +1038,15 @@
     1.4    qed
     1.5  qed
     1.6  
     1.7 +lemma MVT2:
     1.8 +     "[| a < b; \<forall>x. a \<le> x & x \<le> b --> DERIV f x :> f'(x) |]
     1.9 +      ==> \<exists>z::real. a < z & z < b & (f b - f a = (b - a) * f'(z))"
    1.10 +apply (drule MVT)
    1.11 +apply (blast intro: DERIV_isCont)
    1.12 +apply (force dest: order_less_imp_le simp add: differentiable_def)
    1.13 +apply (blast dest: DERIV_unique order_less_imp_le)
    1.14 +done
    1.15 +
    1.16  
    1.17  text{*A function is constant if its derivative is 0 over an interval.*}
    1.18  
    1.19 @@ -1073,6 +1082,30 @@
    1.20  apply (blast dest: DERIV_isconst1)
    1.21  done
    1.22  
    1.23 +lemma DERIV_isconst3: fixes a b x y :: real
    1.24 +  assumes "a < b" and "x \<in> {a <..< b}" and "y \<in> {a <..< b}"
    1.25 +  assumes derivable: "\<And>x. x \<in> {a <..< b} \<Longrightarrow> DERIV f x :> 0"
    1.26 +  shows "f x = f y"
    1.27 +proof (cases "x = y")
    1.28 +  case False
    1.29 +  let ?a = "min x y"
    1.30 +  let ?b = "max x y"
    1.31 +  
    1.32 +  have "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> DERIV f z :> 0"
    1.33 +  proof (rule allI, rule impI)
    1.34 +    fix z :: real assume "?a \<le> z \<and> z \<le> ?b"
    1.35 +    hence "a < z" and "z < b" using `x \<in> {a <..< b}` and `y \<in> {a <..< b}` by auto
    1.36 +    hence "z \<in> {a<..<b}" by auto
    1.37 +    thus "DERIV f z :> 0" by (rule derivable)
    1.38 +  qed
    1.39 +  hence isCont: "\<forall>z. ?a \<le> z \<and> z \<le> ?b \<longrightarrow> isCont f z"
    1.40 +    and DERIV: "\<forall>z. ?a < z \<and> z < ?b \<longrightarrow> DERIV f z :> 0" using DERIV_isCont by auto
    1.41 +
    1.42 +  have "?a < ?b" using `x \<noteq> y` by auto
    1.43 +  from DERIV_isconst2[OF this isCont DERIV, of x] and DERIV_isconst2[OF this isCont DERIV, of y]
    1.44 +  show ?thesis by auto
    1.45 +qed auto
    1.46 +
    1.47  lemma DERIV_isconst_all:
    1.48    fixes f :: "real => real"
    1.49    shows "\<forall>x. DERIV f x :> 0 ==> f(x) = f(y)"