de-applying, etc.
authorpaulson <lp15@cam.ac.uk>
Tue Jul 10 23:18:08 2018 +0100 (13 months ago)
changeset 686114bc4b5c0ccfc
parent 68609 9963bb965a0e
child 68612 ffc3fd6c7498
de-applying, etc.
src/HOL/Analysis/Inner_Product.thy
src/HOL/Analysis/Product_Vector.thy
src/HOL/Deriv.thy
src/HOL/Limits.thy
src/HOL/Nonstandard_Analysis/HLim.thy
src/HOL/Nonstandard_Analysis/HTranscendental.thy
src/HOL/NthRoot.thy
src/HOL/Power.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Inner_Product.thy	Tue Jul 10 09:52:22 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Inner_Product.thy	Tue Jul 10 23:18:08 2018 +0100
     1.3 @@ -153,7 +153,7 @@
     1.4          unfolding norm_eq_sqrt_inner by simp
     1.5      qed
     1.6    have "sqrt (a\<^sup>2 * inner x x) = \<bar>a\<bar> * sqrt (inner x x)"
     1.7 -    by (simp add: real_sqrt_mult_distrib)
     1.8 +    by (simp add: real_sqrt_mult)
     1.9    then show "norm (a *\<^sub>R x) = \<bar>a\<bar> * norm x"
    1.10      unfolding norm_eq_sqrt_inner
    1.11      by (simp add: power2_eq_square mult.assoc)
     2.1 --- a/src/HOL/Analysis/Product_Vector.thy	Tue Jul 10 09:52:22 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Product_Vector.thy	Tue Jul 10 23:18:08 2018 +0100
     2.3 @@ -297,7 +297,7 @@
     2.4      unfolding norm_prod_def
     2.5      apply (simp add: power_mult_distrib)
     2.6      apply (simp add: distrib_left [symmetric])
     2.7 -    apply (simp add: real_sqrt_mult_distrib)
     2.8 +    apply (simp add: real_sqrt_mult)
     2.9      done
    2.10    show "sgn x = scaleR (inverse (norm x)) x"
    2.11      by (rule sgn_prod_def)
     3.1 --- a/src/HOL/Deriv.thy	Tue Jul 10 09:52:22 2018 +0100
     3.2 +++ b/src/HOL/Deriv.thy	Tue Jul 10 23:18:08 2018 +0100
     3.3 @@ -1695,7 +1695,7 @@
     3.4    assumes der: "DERIV f (g x) :> D"
     3.5      and neq: "D \<noteq> 0"
     3.6      and x: "a < x" "x < b"
     3.7 -    and inj: "\<forall>y. a < y \<and> y < b \<longrightarrow> f (g y) = y"
     3.8 +    and inj: "\<And>y. \<lbrakk>a < y; y < b\<rbrakk> \<Longrightarrow> f (g y) = y"
     3.9      and cont: "isCont g x"
    3.10    shows "DERIV g x :> inverse D"
    3.11  unfolding DERIV_iff2
     4.1 --- a/src/HOL/Limits.thy	Tue Jul 10 09:52:22 2018 +0100
     4.2 +++ b/src/HOL/Limits.thy	Tue Jul 10 23:18:08 2018 +0100
     4.3 @@ -1030,13 +1030,6 @@
     4.4    shows "continuous (at a within s) (\<lambda>x. inverse (f x))"
     4.5    using assms unfolding continuous_within by (rule tendsto_inverse)
     4.6  
     4.7 -lemma continuous_at_inverse[continuous_intros, simp]:
     4.8 -  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
     4.9 -  assumes "isCont f a"
    4.10 -    and "f a \<noteq> 0"
    4.11 -  shows "isCont (\<lambda>x. inverse (f x)) a"
    4.12 -  using assms unfolding continuous_at by (rule tendsto_inverse)
    4.13 -
    4.14  lemma continuous_on_inverse[continuous_intros]:
    4.15    fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
    4.16    assumes "continuous_on s f"
    4.17 @@ -1135,14 +1128,14 @@
    4.18    shows   "filterlim (\<lambda>x. norm (f x)) at_top F"
    4.19  proof -
    4.20    {
    4.21 -    fix r :: real 
    4.22 -    have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms 
    4.23 -      by (cases "r > 0") 
    4.24 +    fix r :: real
    4.25 +    have "\<forall>\<^sub>F x in F. r \<le> norm (f x)" using filterlim_at_infinity[of 0 f F] assms
    4.26 +      by (cases "r > 0")
    4.27           (auto simp: not_less intro: always_eventually order.trans[OF _ norm_ge_zero])
    4.28    }
    4.29    thus ?thesis by (auto simp: filterlim_at_top)
    4.30  qed
    4.31 -  
    4.32 +
    4.33  lemma filterlim_norm_at_top_imp_at_infinity:
    4.34    fixes F
    4.35    assumes "filterlim (\<lambda>x. norm (f x)) at_top F"
    4.36 @@ -1203,7 +1196,7 @@
    4.37  lemma filterlim_of_real_at_infinity [tendsto_intros]:
    4.38    "filterlim (of_real :: real \<Rightarrow> 'a :: real_normed_algebra_1) at_infinity at_top"
    4.39    by (intro filterlim_norm_at_top_imp_at_infinity) (auto simp: filterlim_abs_real)
    4.40 -    
    4.41 +
    4.42  lemma not_tendsto_and_filterlim_at_infinity:
    4.43    fixes c :: "'a::real_normed_vector"
    4.44    assumes "F \<noteq> bot"
    4.45 @@ -1347,15 +1340,15 @@
    4.46    unfolding filterlim_at_bot eventually_at_top_dense
    4.47    by (metis leI less_minus_iff order_less_asym)
    4.48  
    4.49 -lemma at_bot_mirror : 
    4.50 -  shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top" 
    4.51 +lemma at_bot_mirror :
    4.52 +  shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
    4.53    apply (rule filtermap_fun_inverse[of uminus, symmetric])
    4.54    subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
    4.55    subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
    4.56    by auto
    4.57  
    4.58 -lemma at_top_mirror : 
    4.59 -  shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"  
    4.60 +lemma at_top_mirror :
    4.61 +  shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
    4.62    apply (subst at_bot_mirror)
    4.63    by (auto simp add: filtermap_filtermap)
    4.64  
    4.65 @@ -1553,7 +1546,7 @@
    4.66      by (auto intro: filterlim_at_infinity_imp_eventually_ne tendsto_imp_eventually_ne eventually_conj)
    4.67    then show ?thesis
    4.68      by (subst filterlim_inverse_at_iff[symmetric]) simp_all
    4.69 -qed  
    4.70 +qed
    4.71  
    4.72  lemma tendsto_inverse_0_at_top: "LIM x F. f x :> at_top \<Longrightarrow> ((\<lambda>x. inverse (f x) :: real) \<longlongrightarrow> 0) F"
    4.73   by (metis filterlim_at filterlim_mono[OF _ at_top_le_at_infinity order_refl] filterlim_inverse_at_iff)
    4.74 @@ -1734,7 +1727,7 @@
    4.75    assumes "filterlim f at_infinity F" "n > 0"
    4.76    shows   "filterlim (\<lambda>x. f x ^ n) at_infinity F"
    4.77    by (rule filterlim_norm_at_top_imp_at_infinity)
    4.78 -     (auto simp: norm_power intro!: filterlim_pow_at_top assms 
    4.79 +     (auto simp: norm_power intro!: filterlim_pow_at_top assms
    4.80             intro: filterlim_at_infinity_imp_norm_at_top)
    4.81  
    4.82  lemma filterlim_tendsto_add_at_top:
    4.83 @@ -2560,7 +2553,7 @@
    4.84  
    4.85  lemma isUCont_Cauchy: "isUCont f \<Longrightarrow> Cauchy X \<Longrightarrow> Cauchy (\<lambda>n. f (X n))"
    4.86    by (rule uniformly_continuous_on_Cauchy[where S=UNIV and f=f]) simp_all
    4.87 -  
    4.88 +
    4.89  lemma uniformly_continuous_imp_Cauchy_continuous:
    4.90    fixes f :: "'a::metric_space \<Rightarrow> 'b::metric_space"
    4.91    shows "\<lbrakk>uniformly_continuous_on S f; Cauchy \<sigma>; \<And>n. (\<sigma> n) \<in> S\<rbrakk> \<Longrightarrow> Cauchy(f \<circ> \<sigma>)"
    4.92 @@ -2824,8 +2817,8 @@
    4.93  lemma isCont_inverse_function:
    4.94    fixes f g :: "real \<Rightarrow> real"
    4.95    assumes d: "0 < d"
    4.96 -    and inj: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> g (f z) = z"
    4.97 -    and cont: "\<forall>z. \<bar>z-x\<bar> \<le> d \<longrightarrow> isCont f z"
    4.98 +    and inj: "\<And>z. \<bar>z-x\<bar> \<le> d \<Longrightarrow> g (f z) = z"
    4.99 +    and cont: "\<And>z. \<bar>z-x\<bar> \<le> d \<Longrightarrow> isCont f z"
   4.100    shows "isCont g (f x)"
   4.101  proof -
   4.102    let ?A = "f (x - d)"
   4.103 @@ -2854,20 +2847,13 @@
   4.104  lemma isCont_inverse_function2:
   4.105    fixes f g :: "real \<Rightarrow> real"
   4.106    shows
   4.107 -    "a < x \<Longrightarrow> x < b \<Longrightarrow>
   4.108 -      \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> g (f z) = z \<Longrightarrow>
   4.109 -      \<forall>z. a \<le> z \<and> z \<le> b \<longrightarrow> isCont f z \<Longrightarrow> isCont g (f x)"
   4.110 +    "\<lbrakk>a < x; x < b;
   4.111 +      \<And>z. \<lbrakk>a \<le> z; z \<le> b\<rbrakk> \<Longrightarrow> g (f z) = z;
   4.112 +      \<And>z. \<lbrakk>a \<le> z; z \<le> b\<rbrakk> \<Longrightarrow> isCont f z\<rbrakk> \<Longrightarrow> isCont g (f x)"
   4.113    apply (rule isCont_inverse_function [where f=f and d="min (x - a) (b - x)"])
   4.114    apply (simp_all add: abs_le_iff)
   4.115    done
   4.116  
   4.117 -(* need to rename second continuous_at_inverse *)
   4.118 -lemma isCont_inv_fun:
   4.119 -  fixes f g :: "real \<Rightarrow> real"
   4.120 -  shows "0 < d \<Longrightarrow> (\<forall>z. \<bar>z - x\<bar> \<le> d \<longrightarrow> g (f z) = z) \<Longrightarrow>
   4.121 -    \<forall>z. \<bar>z - x\<bar> \<le> d \<longrightarrow> isCont f z \<Longrightarrow> isCont g (f x)"
   4.122 -  by (rule isCont_inverse_function)
   4.123 -
   4.124  text \<open>Bartle/Sherbert: Introduction to Real Analysis, Theorem 4.2.9, p. 110.\<close>
   4.125  lemma LIM_fun_gt_zero: "f \<midarrow>c\<rightarrow> l \<Longrightarrow> 0 < l \<Longrightarrow> \<exists>r. 0 < r \<and> (\<forall>x. x \<noteq> c \<and> \<bar>c - x\<bar> < r \<longrightarrow> 0 < f x)"
   4.126    for f :: "real \<Rightarrow> real"
     5.1 --- a/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Jul 10 09:52:22 2018 +0100
     5.2 +++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Jul 10 23:18:08 2018 +0100
     5.3 @@ -234,7 +234,7 @@
     5.4  
     5.5  lemma isNSCont_inverse: "isNSCont f x \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> isNSCont (\<lambda>x. inverse (f x)) x"
     5.6    for f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_div_algebra"
     5.7 -  by (auto intro: continuous_at_inverse simp add: isNSCont_isCont_iff)
     5.8 +  using NSLIM_inverse NSLIM_isNSCont isNSCont_NSLIM by blast
     5.9  
    5.10  lemma isNSCont_const [simp]: "isNSCont (\<lambda>x. k) a"
    5.11    by (simp add: isNSCont_def)
     6.1 --- a/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Tue Jul 10 09:52:22 2018 +0100
     6.2 +++ b/src/HOL/Nonstandard_Analysis/HTranscendental.thy	Tue Jul 10 23:18:08 2018 +0100
     6.3 @@ -60,7 +60,7 @@
     6.4      "!!x y. [|0 < x; 0 <y |] ==>
     6.5        ( *f* sqrt)(x*y) = ( *f* sqrt)(x) * ( *f* sqrt)(y)"
     6.6  apply transfer
     6.7 -apply (auto intro: real_sqrt_mult_distrib) 
     6.8 +apply (auto intro: real_sqrt_mult) 
     6.9  done
    6.10  
    6.11  lemma hypreal_sqrt_mult_distrib2:
     7.1 --- a/src/HOL/NthRoot.thy	Tue Jul 10 09:52:22 2018 +0100
     7.2 +++ b/src/HOL/NthRoot.thy	Tue Jul 10 23:18:08 2018 +0100
     7.3 @@ -314,34 +314,28 @@
     7.4      using x .
     7.5    show "x < x + 1"
     7.6      by simp
     7.7 -  show "\<forall>y. 0 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
     7.8 -    using n by simp
     7.9    show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
    7.10      by (rule DERIV_pow)
    7.11    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
    7.12      using n x by simp
    7.13    show "isCont (root n) x"
    7.14      by (rule isCont_real_root)
    7.15 -qed
    7.16 +qed (use n in auto)
    7.17  
    7.18  lemma DERIV_odd_real_root:
    7.19    assumes n: "odd n"
    7.20      and x: "x \<noteq> 0"
    7.21    shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))"
    7.22  proof (rule DERIV_inverse_function)
    7.23 -  show "x - 1 < x"
    7.24 -    by simp
    7.25 -  show "x < x + 1"
    7.26 -    by simp
    7.27 -  show "\<forall>y. x - 1 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
    7.28 -    using n by (simp add: odd_real_root_pow)
    7.29 +  show "x - 1 < x" "x < x + 1"
    7.30 +    by auto
    7.31    show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
    7.32      by (rule DERIV_pow)
    7.33    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
    7.34      using odd_pos [OF n] x by simp
    7.35    show "isCont (root n) x"
    7.36      by (rule isCont_real_root)
    7.37 -qed
    7.38 +qed (use n odd_real_root_pow in auto)
    7.39  
    7.40  lemma DERIV_even_real_root:
    7.41    assumes n: "0 < n"
    7.42 @@ -353,10 +347,10 @@
    7.43      by simp
    7.44    show "x < 0"
    7.45      using x .
    7.46 -  show "\<forall>y. x - 1 < y \<and> y < 0 \<longrightarrow> - (root n y ^ n) = y"
    7.47 -  proof (rule allI, rule impI, erule conjE)
    7.48 -    fix y assume "x - 1 < y" and "y < 0"
    7.49 -    then have "root n (-y) ^ n = -y" using \<open>0 < n\<close> by simp
    7.50 +  show "- (root n y ^ n) = y" if "x - 1 < y" and "y < 0" for y
    7.51 +  proof -
    7.52 +    have "root n (-y) ^ n = -y" 
    7.53 +      using that \<open>0 < n\<close> by simp
    7.54      with real_root_minus and \<open>even n\<close>
    7.55      show "- (root n y ^ n) = y" by simp
    7.56    qed
    7.57 @@ -816,8 +810,6 @@
    7.58  lemmas real_root_pos2 = real_root_power_cancel
    7.59  lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
    7.60  lemmas real_root_pos_pos_le = real_root_ge_zero
    7.61 -lemmas real_sqrt_mult_distrib = real_sqrt_mult
    7.62 -lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
    7.63  lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
    7.64  
    7.65  end
     8.1 --- a/src/HOL/Power.thy	Tue Jul 10 09:52:22 2018 +0100
     8.2 +++ b/src/HOL/Power.thy	Tue Jul 10 23:18:08 2018 +0100
     8.3 @@ -745,6 +745,12 @@
     8.4  lemma abs_square_less_1: "x\<^sup>2 < 1 \<longleftrightarrow> \<bar>x\<bar> < 1"
     8.5    using  abs_square_eq_1 [of x] abs_square_le_1 [of x] by (auto simp add: le_less)
     8.6  
     8.7 +lemma square_le_1:
     8.8 +  assumes "- 1 \<le> x" "x \<le> 1"
     8.9 +  shows "x\<^sup>2 \<le> 1"
    8.10 +    using assms
    8.11 +    by (metis add.inverse_inverse linear mult_le_one neg_equal_0_iff_equal neg_le_iff_le power2_eq_square power_minus_Bit0)
    8.12 +
    8.13  end
    8.14  
    8.15  
     9.1 --- a/src/HOL/Transcendental.thy	Tue Jul 10 09:52:22 2018 +0100
     9.2 +++ b/src/HOL/Transcendental.thy	Tue Jul 10 23:18:08 2018 +0100
     9.3 @@ -10,7 +10,7 @@
     9.4  imports Series Deriv NthRoot
     9.5  begin
     9.6  
     9.7 -text \<open>A fact theorem on reals.\<close>
     9.8 +text \<open>A theorem about the factcorial function on the reals.\<close>
     9.9  
    9.10  lemma square_fact_le_2_fact: "fact n * fact n \<le> (fact (2 * n) :: real)"
    9.11  proof (induct n)
    9.12 @@ -1822,7 +1822,7 @@
    9.13  proof (cases "0 < x")
    9.14    case True
    9.15    then have "isCont ln (exp (ln x))"
    9.16 -    by (intro isCont_inv_fun[where d = "\<bar>x\<bar>" and f = exp]) auto
    9.17 +    by (intro isCont_inverse_function[where d = "\<bar>x\<bar>" and f = exp]) auto
    9.18    with True show ?thesis
    9.19      by simp
    9.20  next
    9.21 @@ -4540,6 +4540,9 @@
    9.22    unfolding tan_def
    9.23    by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
    9.24  
    9.25 +declare DERIV_tan[THEN DERIV_chain2, derivative_intros]
    9.26 +  and DERIV_tan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
    9.27 +
    9.28  lemmas has_derivative_tan[derivative_intros] = DERIV_tan[THEN DERIV_compose_FDERIV]
    9.29  
    9.30  lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
    9.31 @@ -4633,20 +4636,42 @@
    9.32      by (rule_tac x="-x" in exI) auto
    9.33  qed
    9.34  
    9.35 -lemma tan_total: "\<exists>! x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
    9.36 -  apply (insert lemma_tan_total1 [where y = y], auto)
    9.37 -  apply hypsubst_thin
    9.38 -  apply (cut_tac x = xa and y = y in linorder_less_linear, auto)
    9.39 -   apply (subgoal_tac [2] "\<exists>z. y < z \<and> z < xa \<and> DERIV tan z :> 0")
    9.40 -    apply (subgoal_tac "\<exists>z. xa < z \<and> z < y \<and> DERIV tan z :> 0")
    9.41 -     apply (rule_tac [4] Rolle)
    9.42 -        apply (rule_tac [2] Rolle)
    9.43 -           apply (auto del: exI intro!: DERIV_tan DERIV_isCont exI
    9.44 -            simp add: real_differentiable_def)
    9.45 -       apply (rule_tac [!] DERIV_tan asm_rl)
    9.46 -       apply (auto dest!: DERIV_unique [OF _ DERIV_tan]
    9.47 -        simp add: cos_gt_zero_pi [THEN less_imp_neq, THEN not_sym])
    9.48 -  done
    9.49 +proposition tan_total: "\<exists>! x. -(pi/2) < x \<and> x < (pi/2) \<and> tan x = y"
    9.50 +proof -
    9.51 +  have "u = v" if u: "- (pi / 2) < u" "u < pi / 2" and v: "- (pi / 2) < v" "v < pi / 2"
    9.52 +    and eq: "tan u = tan v" for u v
    9.53 +  proof (cases u v rule: linorder_cases)
    9.54 +    case less
    9.55 +    have "\<And>x. u \<le> x \<and> x \<le> v \<longrightarrow> isCont tan x"
    9.56 +      by (metis cos_gt_zero_pi isCont_tan less_numeral_extra(3) less_trans order.not_eq_order_implies_strict u v)
    9.57 +    moreover have "\<And>x. u < x \<and> x < v \<Longrightarrow> tan differentiable (at x)"
    9.58 +      by (metis DERIV_tan cos_gt_zero_pi differentiableI less_numeral_extra(3) order.strict_trans u(1) v(2))
    9.59 +    ultimately obtain z where "u < z" "z < v" "DERIV tan z :> 0"
    9.60 +      by (metis less Rolle eq)
    9.61 +    moreover have "cos z \<noteq> 0"
    9.62 +      by (metis (no_types) \<open>u < z\<close> \<open>z < v\<close> cos_gt_zero_pi less_le_trans linorder_not_less not_less_iff_gr_or_eq u(1) v(2))
    9.63 +    ultimately show ?thesis
    9.64 +      using DERIV_unique [OF _ DERIV_tan] by fastforce
    9.65 +  next
    9.66 +    case greater
    9.67 +    have "\<And>x. v \<le> x \<and> x \<le> u \<Longrightarrow> isCont tan x"
    9.68 +      by (metis cos_gt_zero_pi isCont_tan less_numeral_extra(3) less_trans order.not_eq_order_implies_strict u v)
    9.69 +    moreover have "\<And>x. v < x \<and> x < u \<Longrightarrow> tan differentiable (at x)"
    9.70 +      by (metis DERIV_tan cos_gt_zero_pi differentiableI less_numeral_extra(3) order.strict_trans u(2) v(1))
    9.71 +    ultimately obtain z where "v < z" "z < u" "DERIV tan z :> 0"
    9.72 +      by (metis greater Rolle eq)
    9.73 +    moreover have "cos z \<noteq> 0"
    9.74 +      by (metis  \<open>v < z\<close> \<open>z < u\<close> cos_gt_zero_pi less_le_trans linorder_not_less not_less_iff_gr_or_eq u(2) v(1))
    9.75 +    ultimately show ?thesis
    9.76 +      using DERIV_unique [OF _ DERIV_tan] by fastforce
    9.77 +  qed auto
    9.78 +  then have "\<exists>!x. - (pi / 2) < x \<and> x < pi / 2 \<and> tan x = y" 
    9.79 +    if x: "- (pi / 2) < x" "x < pi / 2" "tan x = y" for x
    9.80 +    using that by auto
    9.81 +  then show ?thesis
    9.82 +    using lemma_tan_total1 [where y = y]
    9.83 +    by auto
    9.84 +qed
    9.85  
    9.86  lemma tan_monotone:
    9.87    assumes "- (pi/2) < y" and "y < x" and "x < pi/2"
    9.88 @@ -4898,21 +4923,21 @@
    9.89  lemma arcsin_ubound: "- 1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arcsin y \<le> pi/2"
    9.90    by (blast dest: arcsin)
    9.91  
    9.92 -lemma arcsin_lt_bounded: "- 1 < y \<Longrightarrow> y < 1 \<Longrightarrow> - (pi/2) < arcsin y \<and> arcsin y < pi/2"
    9.93 -  apply (frule order_less_imp_le)
    9.94 -  apply (frule_tac y = y in order_less_imp_le)
    9.95 -  apply (frule arcsin_bounded, safe)
    9.96 -    apply simp
    9.97 -   apply (drule_tac y = "arcsin y" in order_le_imp_less_or_eq)
    9.98 -   apply (drule_tac [2] y = "pi/2" in order_le_imp_less_or_eq, safe)
    9.99 -   apply (drule_tac [!] f = sin in arg_cong, auto)
   9.100 -  done
   9.101 +lemma arcsin_lt_bounded:
   9.102 +  assumes "- 1 < y" "y < 1"
   9.103 +  shows  "- (pi/2) < arcsin y \<and> arcsin y < pi/2"
   9.104 +proof -
   9.105 +  have "arcsin y \<noteq> pi/2"
   9.106 +    by (metis arcsin assms not_less not_less_iff_gr_or_eq sin_pi_half)
   9.107 +  moreover have "arcsin y \<noteq> - pi/2"
   9.108 +    by (metis arcsin assms minus_divide_left not_less not_less_iff_gr_or_eq sin_minus sin_pi_half)
   9.109 +  ultimately show ?thesis
   9.110 +    using arcsin_bounded [of y] assms by auto
   9.111 +qed
   9.112  
   9.113  lemma arcsin_sin: "- (pi/2) \<le> x \<Longrightarrow> x \<le> pi/2 \<Longrightarrow> arcsin (sin x) = x"
   9.114 -  apply (unfold arcsin_def)
   9.115 -  apply (rule the1_equality)
   9.116 -   apply (rule sin_total, auto)
   9.117 -  done
   9.118 +  unfolding arcsin_def
   9.119 +  using the1_equality [OF sin_total]  by simp
   9.120  
   9.121  lemma arcsin_0 [simp]: "arcsin 0 = 0"
   9.122    using arcsin_sin [of 0] by simp
   9.123 @@ -4947,14 +4972,18 @@
   9.124  lemma arccos_ubound: "- 1 \<le> y \<Longrightarrow> y \<le> 1 \<Longrightarrow> arccos y \<le> pi"
   9.125    by (blast dest: arccos)
   9.126  
   9.127 -lemma arccos_lt_bounded: "- 1 < y \<Longrightarrow> y < 1 \<Longrightarrow> 0 < arccos y \<and> arccos y < pi"
   9.128 -  apply (frule order_less_imp_le)
   9.129 -  apply (frule_tac y = y in order_less_imp_le)
   9.130 -  apply (frule arccos_bounded, auto)
   9.131 -   apply (drule_tac y = "arccos y" in order_le_imp_less_or_eq)
   9.132 -   apply (drule_tac [2] y = pi in order_le_imp_less_or_eq, auto)
   9.133 -   apply (drule_tac [!] f = cos in arg_cong, auto)
   9.134 -  done
   9.135 +lemma arccos_lt_bounded: 
   9.136 +  assumes "- 1 < y" "y < 1"
   9.137 +  shows  "0 < arccos y \<and> arccos y < pi"
   9.138 +proof -
   9.139 +  have "arccos y \<noteq> 0"
   9.140 +    by (metis (no_types) arccos assms(1) assms(2) cos_zero less_eq_real_def less_irrefl)
   9.141 +  moreover have "arccos y \<noteq> -pi"
   9.142 +    by (metis arccos assms(1) assms(2) cos_minus cos_pi not_less not_less_iff_gr_or_eq)
   9.143 +  ultimately show ?thesis
   9.144 +    using arccos_bounded [of y] assms
   9.145 +    by (metis arccos cos_pi not_less not_less_iff_gr_or_eq)
   9.146 +qed
   9.147  
   9.148  lemma arccos_cos: "0 \<le> x \<Longrightarrow> x \<le> pi \<Longrightarrow> arccos (cos x) = x"
   9.149    by (auto simp: arccos_def intro!: the1_equality cos_total)
   9.150 @@ -4962,31 +4991,29 @@
   9.151  lemma arccos_cos2: "x \<le> 0 \<Longrightarrow> - pi \<le> x \<Longrightarrow> arccos (cos x) = -x"
   9.152    by (auto simp: arccos_def intro!: the1_equality cos_total)
   9.153  
   9.154 -lemma cos_arcsin: "- 1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> cos (arcsin x) = sqrt (1 - x\<^sup>2)"
   9.155 -  apply (subgoal_tac "x\<^sup>2 \<le> 1")
   9.156 -   apply (rule power2_eq_imp_eq)
   9.157 -     apply (simp add: cos_squared_eq)
   9.158 -    apply (rule cos_ge_zero)
   9.159 -     apply (erule (1) arcsin_lbound)
   9.160 -    apply (erule (1) arcsin_ubound)
   9.161 -   apply simp
   9.162 -  apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
   9.163 -  apply (rule power_mono, simp)
   9.164 -  apply simp
   9.165 -  done
   9.166 -
   9.167 -lemma sin_arccos: "- 1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> sin (arccos x) = sqrt (1 - x\<^sup>2)"
   9.168 -  apply (subgoal_tac "x\<^sup>2 \<le> 1")
   9.169 -   apply (rule power2_eq_imp_eq)
   9.170 -     apply (simp add: sin_squared_eq)
   9.171 -    apply (rule sin_ge_zero)
   9.172 -     apply (erule (1) arccos_lbound)
   9.173 -    apply (erule (1) arccos_ubound)
   9.174 -   apply simp
   9.175 -  apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 \<le> 1\<^sup>2", simp)
   9.176 -  apply (rule power_mono, simp)
   9.177 -  apply simp
   9.178 -  done
   9.179 +lemma cos_arcsin:
   9.180 +  assumes "- 1 \<le> x" "x \<le> 1"
   9.181 +  shows "cos (arcsin x) = sqrt (1 - x\<^sup>2)"
   9.182 +proof (rule power2_eq_imp_eq)
   9.183 +  show "(cos (arcsin x))\<^sup>2 = (sqrt (1 - x\<^sup>2))\<^sup>2"
   9.184 +    by (simp add: square_le_1 assms cos_squared_eq)
   9.185 +  show "0 \<le> cos (arcsin x)"
   9.186 +    using arcsin assms cos_ge_zero by blast
   9.187 +  show "0 \<le> sqrt (1 - x\<^sup>2)"
   9.188 +    by (simp add: square_le_1 assms)
   9.189 +qed
   9.190 +
   9.191 +lemma sin_arccos:
   9.192 +  assumes "- 1 \<le> x" "x \<le> 1"
   9.193 +  shows "sin (arccos x) = sqrt (1 - x\<^sup>2)"
   9.194 +proof (rule power2_eq_imp_eq)
   9.195 +  show "(sin (arccos x))\<^sup>2 = (sqrt (1 - x\<^sup>2))\<^sup>2"
   9.196 +    by (simp add: square_le_1 assms sin_squared_eq)
   9.197 +  show "0 \<le> sin (arccos x)"
   9.198 +    by (simp add: arccos_bounded assms sin_ge_zero)
   9.199 +  show "0 \<le> sqrt (1 - x\<^sup>2)"
   9.200 +    by (simp add: square_le_1 assms)
   9.201 +qed
   9.202  
   9.203  lemma arccos_0 [simp]: "arccos 0 = pi/2"
   9.204    by (metis arccos_cos cos_gt_zero cos_pi cos_pi_half pi_gt_zero
   9.205 @@ -5063,10 +5090,7 @@
   9.206  
   9.207  lemma tan_sec: "cos x \<noteq> 0 \<Longrightarrow> 1 + (tan x)\<^sup>2 = (inverse (cos x))\<^sup>2"
   9.208    for x :: "'a::{real_normed_field,banach,field}"
   9.209 -  apply (rule power_inverse [THEN subst])
   9.210 -  apply (rule_tac c1 = "(cos x)\<^sup>2" in mult_right_cancel [THEN iffD1])
   9.211 -   apply (auto simp: tan_def field_simps)
   9.212 -  done
   9.213 +  by (simp add: add_divide_eq_iff inverse_eq_divide power2_eq_square tan_def)
   9.214  
   9.215  lemma arctan_less_iff: "arctan x < arctan y \<longleftrightarrow> x < y"
   9.216    by (metis tan_monotone' arctan_lbound arctan_ubound tan_arctan)
   9.217 @@ -5141,14 +5165,21 @@
   9.218    by (auto simp: continuous_on_eq_continuous_at subset_eq)
   9.219  
   9.220  lemma isCont_arctan: "isCont arctan x"
   9.221 -  apply (rule arctan_lbound [of x, THEN dense, THEN exE], clarify)
   9.222 -  apply (rule arctan_ubound [of x, THEN dense, THEN exE], clarify)
   9.223 -  apply (subgoal_tac "isCont arctan (tan (arctan x))")
   9.224 -   apply (simp add: arctan)
   9.225 -  apply (erule (1) isCont_inverse_function2 [where f=tan])
   9.226 -   apply (metis arctan_tan order_le_less_trans order_less_le_trans)
   9.227 -  apply (metis cos_gt_zero_pi isCont_tan order_less_le_trans less_le)
   9.228 -  done
   9.229 +proof -
   9.230 +  obtain u where u: "- (pi / 2) < u" "u < arctan x"
   9.231 +    by (meson arctan arctan_less_iff linordered_field_no_lb)
   9.232 +  obtain v where v: "arctan x < v" "v < pi / 2"
   9.233 +    by (meson arctan_less_iff arctan_ubound linordered_field_no_ub)
   9.234 +  have "isCont arctan (tan (arctan x))"
   9.235 +  proof (rule isCont_inverse_function2 [of u "arctan x" v])
   9.236 +    show "\<And>z. \<lbrakk>u \<le> z; z \<le> v\<rbrakk> \<Longrightarrow> arctan (tan z) = z"
   9.237 +      using arctan_unique u(1) v(2) by auto
   9.238 +    then show "\<And>z. \<lbrakk>u \<le> z; z \<le> v\<rbrakk> \<Longrightarrow> isCont tan z"
   9.239 +      by (metis arctan cos_gt_zero_pi isCont_tan less_irrefl)
   9.240 +  qed (use u v in auto)
   9.241 +  then show ?thesis
   9.242 +    by (simp add: arctan)
   9.243 +qed
   9.244  
   9.245  lemma tendsto_arctan [tendsto_intros]: "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. arctan (f x)) \<longlongrightarrow> arctan x) F"
   9.246    by (rule isCont_tendsto_compose [OF isCont_arctan])
   9.247 @@ -5160,43 +5191,36 @@
   9.248    "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. arctan (f x))"
   9.249    unfolding continuous_on_def by (auto intro: tendsto_arctan)
   9.250  
   9.251 -lemma DERIV_arcsin: "- 1 < x \<Longrightarrow> x < 1 \<Longrightarrow> DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
   9.252 -  apply (rule DERIV_inverse_function [where f=sin and a="-1" and b=1])
   9.253 -       apply (rule DERIV_cong [OF DERIV_sin])
   9.254 -       apply (simp add: cos_arcsin)
   9.255 -      apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
   9.256 -      apply (rule power_strict_mono, simp)
   9.257 -       apply simp
   9.258 -      apply simp
   9.259 -     apply assumption
   9.260 -    apply assumption
   9.261 -   apply simp
   9.262 -  apply (erule (1) isCont_arcsin)
   9.263 -  done
   9.264 -
   9.265 -lemma DERIV_arccos: "- 1 < x \<Longrightarrow> x < 1 \<Longrightarrow> DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
   9.266 -  apply (rule DERIV_inverse_function [where f=cos and a="-1" and b=1])
   9.267 -       apply (rule DERIV_cong [OF DERIV_cos])
   9.268 -       apply (simp add: sin_arccos)
   9.269 -      apply (subgoal_tac "\<bar>x\<bar>\<^sup>2 < 1\<^sup>2", simp)
   9.270 -      apply (rule power_strict_mono, simp)
   9.271 -       apply simp
   9.272 -      apply simp
   9.273 -     apply assumption
   9.274 -    apply assumption
   9.275 -   apply simp
   9.276 -  apply (erule (1) isCont_arccos)
   9.277 -  done
   9.278 +lemma DERIV_arcsin:
   9.279 +  assumes "- 1 < x" "x < 1"
   9.280 +  shows "DERIV arcsin x :> inverse (sqrt (1 - x\<^sup>2))"
   9.281 +proof (rule DERIV_inverse_function)
   9.282 +  show "(sin has_real_derivative sqrt (1 - x\<^sup>2)) (at (arcsin x))"
   9.283 +    by (rule derivative_eq_intros | use assms cos_arcsin in force)+
   9.284 +  show "sqrt (1 - x\<^sup>2) \<noteq> 0"
   9.285 +    using abs_square_eq_1 assms by force
   9.286 +qed (use assms isCont_arcsin in auto)
   9.287 +
   9.288 +lemma DERIV_arccos:
   9.289 +  assumes "- 1 < x" "x < 1"
   9.290 +  shows "DERIV arccos x :> inverse (- sqrt (1 - x\<^sup>2))"
   9.291 +proof (rule DERIV_inverse_function)
   9.292 +  show "(cos has_real_derivative - sqrt (1 - x\<^sup>2)) (at (arccos x))"
   9.293 +    by (rule derivative_eq_intros | use assms sin_arccos in force)+
   9.294 +  show "- sqrt (1 - x\<^sup>2) \<noteq> 0"
   9.295 +    using abs_square_eq_1 assms by force
   9.296 +qed (use assms isCont_arccos in auto)
   9.297  
   9.298  lemma DERIV_arctan: "DERIV arctan x :> inverse (1 + x\<^sup>2)"
   9.299 -  apply (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
   9.300 -       apply (rule DERIV_cong [OF DERIV_tan])
   9.301 -        apply (rule cos_arctan_not_zero)
   9.302 -       apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
   9.303 -   apply (simp add: arctan power_inverse [symmetric] tan_sec [symmetric])
   9.304 -  apply (subgoal_tac "0 < 1 + x\<^sup>2", simp)
   9.305 -  apply (simp_all add: add_pos_nonneg arctan isCont_arctan)
   9.306 -  done
   9.307 +proof (rule DERIV_inverse_function [where f=tan and a="x - 1" and b="x + 1"])
   9.308 +  show "(tan has_real_derivative 1 + x\<^sup>2) (at (arctan x))"
   9.309 +    apply (rule derivative_eq_intros | simp)+
   9.310 +    by (metis arctan cos_arctan_not_zero power_inverse tan_sec)
   9.311 +  show "\<And>y. \<lbrakk>x - 1 < y; y < x + 1\<rbrakk> \<Longrightarrow> tan (arctan y) = y"
   9.312 +    using tan_arctan by blast
   9.313 +  show "1 + x\<^sup>2 \<noteq> 0"
   9.314 +    by (metis power_one sum_power2_eq_zero_iff zero_neq_one)
   9.315 +qed (use isCont_arctan in auto)
   9.316  
   9.317  declare
   9.318    DERIV_arcsin[THEN DERIV_chain2, derivative_intros]
   9.319 @@ -5830,7 +5854,7 @@
   9.320        moreover have "isCont (\<lambda> x. ?a x n - ?diff x n) x" for x
   9.321          unfolding diff_conv_add_uminus divide_inverse
   9.322          by (auto intro!: isCont_add isCont_rabs continuous_ident isCont_minus isCont_arctan
   9.323 -          continuous_at_inverse isCont_mult isCont_power continuous_const isCont_sum
   9.324 +          continuous_at_within_inverse isCont_mult isCont_power continuous_const isCont_sum
   9.325            simp del: add_uminus_conv_diff)
   9.326        ultimately have "0 \<le> ?a 1 n - ?diff 1 n"
   9.327          by (rule LIM_less_bound)