src/HOL/Deriv.thy
 changeset 37891 c26f9d06e82c parent 37888 d78a3cdbd615 child 41368 8afa26855137
equal inserted replaced
37890:aae46a9ef66c 37891:c26f9d06e82c
`  1253   shows "f a \<le> f b"`
`  1253   shows "f a \<le> f b"`
`  1254 proof (rule ccontr, cases "a = b")`
`  1254 proof (rule ccontr, cases "a = b")`
`  1255   assume "~ f a \<le> f b"`
`  1255   assume "~ f a \<le> f b"`
`  1256   assume "a = b"`
`  1256   assume "a = b"`
`  1257   with prems show False by auto`
`  1257   with prems show False by auto`
`  1258   next assume "~ f a \<le> f b"`
`  1258 next`
`  1259   assume "a ~= b"`
`  1259   assume A: "~ f a \<le> f b"`
`       `
`  1260   assume B: "a ~= b"`
`  1260   with assms have "EX l z. a < z & z < b & DERIV f z :> l`
`  1261   with assms have "EX l z. a < z & z < b & DERIV f z :> l`
`  1261       & f b - f a = (b - a) * l"`
`  1262       & f b - f a = (b - a) * l"`
`  1262     apply -`
`  1263     apply -`
`  1263     apply (rule MVT)`
`  1264     apply (rule MVT)`
`  1264       apply auto`
`  1265       apply auto`
`  1265       apply (metis DERIV_isCont)`
`  1266       apply (metis DERIV_isCont)`
`  1266      apply (metis differentiableI less_le)`
`  1267      apply (metis differentiableI less_le)`
`  1267     done`
`  1268     done`
`  1268   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"`
`  1269   then obtain l z where "a < z" and "z < b" and "DERIV f z :> l"`
`  1269       and "f b - f a = (b - a) * l"`
`  1270       and C: "f b - f a = (b - a) * l"`
`  1270     by auto`
`  1271     by auto`
`  1271   from prems have "~(l >= 0)"`
`  1272   with A have "a < b" "f b < f a" by auto`
`  1272     by (metis diff_self diff_eq_diff_less_eq le_iff_diff_le_0 order_antisym linear`
`  1273   with C have "\<not> l \<ge> 0" by (auto simp add: not_le algebra_simps)`
`  1273               split_mult_pos_le)`
`  1274     (metis A add_le_cancel_right assms(1) less_eq_real_def mult_right_mono real_add_left_mono real_le_linear real_le_refl)`
`  1274   with prems show False`
`  1275   with prems show False`
`  1275     by (metis DERIV_unique order_less_imp_le)`
`  1276     by (metis DERIV_unique order_less_imp_le)`
`  1276 qed`
`  1277 qed`
`  1277 `
`  1278 `
`  1278 lemma DERIV_neg_imp_decreasing:`
`  1279 lemma DERIV_neg_imp_decreasing:`