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)"
```