# HG changeset patch
# User wenzelm
# Date 1258241661 -3600
# Node ID 889d06128608945fc225c5b48902c7d611f669c6
# Parent  d0a9ce721e0c49ffcb056bc1dd5759ea68a3718c
simplified bulky metis proofs;

diff -r d0a9ce721e0c -r 889d06128608 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Sun Nov 15 00:23:26 2009 +0100
+++ b/src/HOL/Deriv.thy	Sun Nov 15 00:34:21 2009 +0100
@@ -1224,27 +1224,30 @@
 (* A function with positive derivative is increasing. 
    A simple proof using the MVT, by Jeremy Avigad. And variants.
 *)
-
 lemma DERIV_pos_imp_increasing:
   fixes a::real and b::real and f::"real => real"
   assumes "a < b" and "\<forall>x. a \<le> x & x \<le> b --> (EX y. DERIV f x :> y & y > 0)"
   shows "f a < f b"
 proof (rule ccontr)
   assume "~ f a < f b"
-  from assms have "EX l z. a < z & z < b & DERIV f z :> l
+  have "EX l z. a < z & z < b & DERIV f z :> l
       & f b - f a = (b - a) * l"
-    by (metis MVT DERIV_isCont differentiableI real_less_def)
+    apply (rule MVT)
+      using assms
+      apply auto
+      apply (metis DERIV_isCont)
+     apply (metis differentiableI real_less_def)
+    done
   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
       and "f b - f a = (b - a) * l"
     by auto
   
   from prems have "~(l > 0)"
-    by (metis assms(1) linorder_not_le mult_le_0_iff real_le_eq_diff)
+    by (metis linorder_not_le mult_le_0_iff real_le_eq_diff)
   with prems show False
     by (metis DERIV_unique real_less_def)
 qed
 
-
 lemma DERIV_nonneg_imp_nonincreasing:
   fixes a::real and b::real and f::"real => real"
   assumes "a \<le> b" and
@@ -1258,10 +1261,11 @@
   assume "a ~= b"
   with assms have "EX l z. a < z & z < b & DERIV f z :> l
       & f b - f a = (b - a) * l"
-    apply (intro MVT)
-    apply auto
-    apply (metis DERIV_isCont)
-    apply (metis differentiableI real_less_def)
+    apply -
+    apply (rule MVT)
+      apply auto
+      apply (metis DERIV_isCont)
+     apply (metis differentiableI real_less_def)
     done
   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"
       and "f b - f a = (b - a) * l"
@@ -1281,7 +1285,8 @@
 proof -
   have "(%x. -f x) a < (%x. -f x) b"
     apply (rule DERIV_pos_imp_increasing [of a b "%x. -f x"])
-    apply (insert prems, auto)
+    using assms
+    apply auto
     apply (metis DERIV_minus neg_0_less_iff_less)
     done
   thus ?thesis
@@ -1296,7 +1301,8 @@
 proof -
   have "(%x. -f x) a \<le> (%x. -f x) b"
     apply (rule DERIV_nonneg_imp_nonincreasing [of a b "%x. -f x"])
-    apply (insert prems, auto)
+    using assms
+    apply auto
     apply (metis DERIV_minus neg_0_le_iff_le)
     done
   thus ?thesis