tuned proofs
authorhaftmann
Fri Jun 14 08:34:28 2019 +0000 (5 weeks ago)
changeset 70346408e15cbd2a6
parent 70345 80a1aa30e24d
child 70347 e5cd5471c18a
tuned proofs
src/HOL/Analysis/Conformal_Mappings.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Elementary_Normed_Spaces.thy
src/HOL/Deriv.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
     1.1 --- a/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Analysis/Conformal_Mappings.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -1878,9 +1878,9 @@
     1.4          apply (simp add: power2_eq_square divide_simps C_def norm_mult)
     1.5          proof -
     1.6            have "norm z * (norm (deriv f 0) * (r - norm z - norm z)) \<le> norm z * (norm (deriv f 0) * (r - norm z) - norm (deriv f 0) * norm z)"
     1.7 -            by (simp add: linordered_field_class.sign_simps(38))
     1.8 +            by (simp add: sign_simps)
     1.9            then show "(norm z * (r - norm z) - norm z * norm z) * norm (deriv f 0) \<le> norm (deriv f 0) * norm z * (r - norm z) - norm z * norm z * norm (deriv f 0)"
    1.10 -            by (simp add: linordered_field_class.sign_simps(38) mult.commute mult.left_commute)
    1.11 +            by (simp add: sign_simps)
    1.12          qed
    1.13      qed
    1.14      have sq201 [simp]: "0 < (1 - sqrt 2 / 2)" "(1 - sqrt 2 / 2)  < 1"
     2.1 --- a/src/HOL/Analysis/Derivative.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ b/src/HOL/Analysis/Derivative.thy	Fri Jun 14 08:34:28 2019 +0000
     2.3 @@ -862,7 +862,8 @@
     2.4      have "u *\<^sub>R y = u *\<^sub>R (y - x) + u *\<^sub>R x"
     2.5        by (simp add: scale_right_diff_distrib)
     2.6      then show "x + u *\<^sub>R (y - x) \<in> S"
     2.7 -      using that \<open>convex S\<close> unfolding convex_alt by (metis (no_types) atLeastAtMost_iff linordered_field_class.sign_simps(2) pth_c(3) scaleR_collapse x y)
     2.8 +      using that \<open>convex S\<close> x y by (simp add: convex_alt)
     2.9 +        (metis pth_b(2) pth_c(1) scaleR_collapse)
    2.10    qed
    2.11    have "\<And>z. z \<in> (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1} \<Longrightarrow>
    2.12            (f has_derivative f' z) (at z within (\<lambda>u. x + u *\<^sub>R (y - x)) ` {0..1})"
     3.1 --- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Jun 14 08:34:27 2019 +0000
     3.2 +++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Fri Jun 14 08:34:28 2019 +0000
     3.3 @@ -131,8 +131,10 @@
     3.4        show "\<lbrakk>\<not> 0 \<le> m; a \<le> b;  x \<in> {m *\<^sub>R b + c..m *\<^sub>R a + c}\<rbrakk>
     3.5              \<Longrightarrow> x \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}" for x
     3.6          apply (rule_tac x="inverse m *\<^sub>R (x-c)" in rev_image_eqI)
     3.7 -        apply (auto simp: diff_le_eq neg_le_divideR_eq)
     3.8 -        using diff_eq_diff_less_eq linordered_field_class.sign_simps(11) minus_diff_eq not_less scaleR_le_cancel_left_neg by fastforce
     3.9 +        apply (auto simp add: neg_le_divideR_eq not_le)
    3.10 +         apply (auto simp: field_simps)
    3.11 +        apply (metis (no_types, lifting) add_diff_cancel_left' add_le_imp_le_right diff_add_cancel inverse_eq_divide neg_le_divideR_eq neg_le_iff_le scale_minus_right)
    3.12 +        done
    3.13      qed
    3.14    qed
    3.15  qed
     4.1 --- a/src/HOL/Deriv.thy	Fri Jun 14 08:34:27 2019 +0000
     4.2 +++ b/src/HOL/Deriv.thy	Fri Jun 14 08:34:28 2019 +0000
     4.3 @@ -1409,12 +1409,14 @@
     4.4      and dif: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> f differentiable (at x)"
     4.5    shows "\<exists>l z. a < z \<and> z < b \<and> DERIV f z :> l \<and> f b - f a = (b - a) * l"
     4.6  proof -
     4.7 -  obtain f' where derf: "\<And>x. \<lbrakk>a < x; x < b\<rbrakk> \<Longrightarrow> (f has_derivative f' x) (at x)"
     4.8 +  obtain f' :: "real \<Rightarrow> real \<Rightarrow> real"
     4.9 +    where derf: "\<And>x. a < x \<Longrightarrow> x < b \<Longrightarrow> (f has_derivative f' x) (at x)"
    4.10      using dif unfolding differentiable_def by metis
    4.11    then obtain z where "a < z" "z < b" "f b - f a = (f' z) (b - a)"
    4.12      using mvt [OF lt contf] by blast
    4.13    then show ?thesis
    4.14 -    by (metis derf dif has_derivative_unique has_field_derivative_imp_has_derivative linordered_field_class.sign_simps(5) real_differentiable_def)
    4.15 +    by (simp add: ac_simps)
    4.16 +      (metis derf dif has_derivative_unique has_field_derivative_imp_has_derivative real_differentiable_def)
    4.17  qed
    4.18  
    4.19  corollary MVT2:
     5.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jun 14 08:34:27 2019 +0000
     5.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Fri Jun 14 08:34:28 2019 +0000
     5.3 @@ -1928,13 +1928,12 @@
     5.4  text \<open>The next lemma is wrong for $a = top$, for $b = c = 1$ for instance.\<close>
     5.5  
     5.6  lemma ennreal_right_diff_distrib:
     5.7 -  fixes a b c::ennreal
     5.8 +  fixes a b c :: ennreal
     5.9    assumes "a \<noteq> top"
    5.10    shows "a * (b - c) = a * b - a * c"
    5.11 -  apply (cases a, cases b, cases c, auto simp add: assms)
    5.12 -  apply (metis (mono_tags, lifting) ennreal_minus ennreal_mult' linordered_field_class.sign_simps(38) split_mult_pos_le)
    5.13 -  apply (metis ennreal_minus_zero ennreal_mult_cancel_left ennreal_top_eq_mult_iff minus_top_ennreal mult_eq_0_iff top_neq_ennreal)
    5.14 -  apply (metis ennreal_minus_eq_top ennreal_minus_zero ennreal_mult_eq_top_iff mult_eq_0_iff)
    5.15 +  apply (cases a; cases b; cases c)
    5.16 +         apply (use assms in \<open>auto simp add: ennreal_mult_top ennreal_minus ennreal_mult' [symmetric]\<close>)
    5.17 +  apply (simp add: algebra_simps)
    5.18    done
    5.19  
    5.20  lemma SUP_diff_ennreal: