Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
authorpaulson <lp15@cam.ac.uk>
Sat Apr 11 11:56:40 2015 +0100 (2015-04-11)
changeset 60017b785d6d06430
parent 59991 09be0495dcc2
child 60018 05d4dce039c6
Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala.
src/HOL/Complex.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/ex/Approximation_Ex.thy
src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy
src/HOL/Library/Code_Real_Approx_By_Float.thy
src/HOL/Library/Float.thy
src/HOL/Library/Formal_Power_Series.thy
src/HOL/Limits.thy
src/HOL/MacLaurin.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy
src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy
src/HOL/Multivariate_Analysis/Complex_Transcendental.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/NSA/HLog.thy
src/HOL/NSA/HTranscendental.thy
src/HOL/NSA/NSComplex.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Information.thy
src/HOL/Probability/Regularity.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Set_Interval.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Complex.thy	Thu Apr 09 20:42:38 2015 +0200
     1.2 +++ b/src/HOL/Complex.thy	Sat Apr 11 11:56:40 2015 +0100
     1.3 @@ -167,6 +167,10 @@
     1.4  lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w"
     1.5    by (simp add: Im_divide sqr_conv_mult)
     1.6  
     1.7 +lemma of_real_Re [simp]:
     1.8 +    "z \<in> \<real> \<Longrightarrow> of_real (Re z) = z"
     1.9 +  by (auto simp: Reals_def)
    1.10 +
    1.11  subsection {* The Complex Number $i$ *}
    1.12  
    1.13  primcorec "ii" :: complex  ("\<i>") where
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Apr 09 20:42:38 2015 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Sat Apr 11 11:56:40 2015 +0100
     2.3 @@ -241,7 +241,9 @@
     2.4    show ?case
     2.5    proof (cases x)
     2.6      case (Float m e)
     2.7 -    hence "0 < m" using assms powr_gt_zero[of 2 e] by (auto simp: sign_simps)
     2.8 +    hence "0 < m" using assms 
     2.9 +      apply (auto simp: sign_simps)
    2.10 +      by (meson not_less powr_ge_pzero)
    2.11      hence "0 < sqrt m" by auto
    2.12  
    2.13      have int_nat_bl: "(nat (bitlen m)) = bitlen m" using bitlen_nonneg by auto
    2.14 @@ -1858,7 +1860,8 @@
    2.15    finally show "?ln \<le> ?ub" .
    2.16  qed
    2.17  
    2.18 -lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
    2.19 +lemma ln_add: 
    2.20 +  fixes x::real assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)"
    2.21  proof -
    2.22    have "x \<noteq> 0" using assms by auto
    2.23    have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \<noteq> 0`] by auto
    2.24 @@ -1885,7 +1888,7 @@
    2.25    let ?uthird = "rapprox_rat (max prec 1) 1 3"
    2.26    let ?lthird = "lapprox_rat prec 1 3"
    2.27  
    2.28 -  have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1)"
    2.29 +  have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1::real)"
    2.30      using ln_add[of "3 / 2" "1 / 2"] by auto
    2.31    have lb3: "?lthird \<le> 1 / 3" using lapprox_rat[of prec 1 3] by auto
    2.32    hence lb3_ub: "real ?lthird < 1" by auto
    2.33 @@ -1955,10 +1958,8 @@
    2.34  
    2.35  lemma float_pos_eq_mantissa_pos:  "x > 0 \<longleftrightarrow> mantissa x > 0"
    2.36    apply (subst Float_mantissa_exponent[of x, symmetric])
    2.37 -  apply (auto simp add: zero_less_mult_iff zero_float_def powr_gt_zero[of 2 "exponent x"] dest: less_zeroE)
    2.38 -  using powr_gt_zero[of 2 "exponent x"]
    2.39 -  apply simp
    2.40 -  done
    2.41 +  apply (auto simp add: zero_less_mult_iff zero_float_def  dest: less_zeroE)
    2.42 +  by (metis not_le powr_ge_pzero)
    2.43  
    2.44  lemma Float_pos_eq_mantissa_pos:  "Float m e > 0 \<longleftrightarrow> m > 0"
    2.45    using powr_gt_zero[of 2 "e"]
    2.46 @@ -2140,8 +2141,9 @@
    2.47      let ?s = "Float (e + (bitlen m - 1)) 0"
    2.48      let ?x = "Float m (- (bitlen m - 1))"
    2.49  
    2.50 -    have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e]
    2.51 -      by (auto simp: zero_less_mult_iff)
    2.52 +    have "0 < m" and "m \<noteq> 0" using `0 < x` Float powr_gt_zero[of 2 e] 
    2.53 +      apply (auto simp add: zero_less_mult_iff)
    2.54 +      using not_le powr_ge_pzero by blast
    2.55      def bl \<equiv> "bitlen m - 1" hence "bl \<ge> 0" using `m > 0` by (simp add: bitlen_def)
    2.56      have "1 \<le> Float m e" using `1 \<le> x` Float unfolding less_eq_float_def by auto
    2.57      from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \<le> Float m e`] `bl \<ge> 0`
    2.58 @@ -2180,7 +2182,7 @@
    2.59          from float_gt1_scale[OF `1 \<le> Float m e`]
    2.60          show "0 \<le> real (e + (bitlen m - 1))" by auto
    2.61        next
    2.62 -        have "0 \<le> ln 2" by simp
    2.63 +        have "0 \<le> ln (2 :: real)" by simp
    2.64          thus "0 \<le> real (ub_ln2 prec)" using ub_ln2[of prec] by arith
    2.65        qed auto
    2.66        ultimately have "ln x \<le> float_plus_up prec ?ub2 ?ub_horner"
    2.67 @@ -2333,10 +2335,9 @@
    2.68    unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse
    2.69    by auto
    2.70  
    2.71 -lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)"
    2.72 -  unfolding powr_def interpret_floatarith.simps ..
    2.73 -
    2.74 -lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)"
    2.75 +lemma interpret_floatarith_log: 
    2.76 +    "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = 
    2.77 +     log (interpret_floatarith b vs) (interpret_floatarith x vs)"
    2.78    unfolding log_def interpret_floatarith.simps divide_inverse ..
    2.79  
    2.80  lemma interpret_floatarith_num:
    2.81 @@ -3481,7 +3482,7 @@
    2.82  subsection {* Implement proof method \texttt{approximation} *}
    2.83  
    2.84  lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num
    2.85 -  interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log
    2.86 +  interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log
    2.87    interpret_floatarith_sin
    2.88  
    2.89  oracle approximation_oracle = {* fn (thy, t) =>
     3.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Thu Apr 09 20:42:38 2015 +0200
     3.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy	Sat Apr 11 11:56:40 2015 +0100
     3.3 @@ -35,7 +35,7 @@
     3.4  
     3.5  section "Compute some transcendental values"
     3.6  
     3.7 -lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < inverse (2^51) "
     3.8 +lemma "\<bar> ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \<bar> < (inverse (2^51) :: real)"
     3.9    by (approximation 60)
    3.10  
    3.11  lemma "\<bar> exp 1.626 - 5.083499996273 \<bar> < (inverse 10 ^ 10 :: real)"
     4.1 --- a/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy	Thu Apr 09 20:42:38 2015 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy	Sat Apr 11 11:56:40 2015 +0100
     4.3 @@ -28,7 +28,7 @@
     4.4  
     4.5  lemma
     4.6    fixes x::real
     4.7 -  shows "x > 1 \<Longrightarrow> x \<le> 2 powr 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
     4.8 +  shows "x > 1 \<Longrightarrow> x \<le> 2 ^ 20 * log 2 x + 1 \<and> (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1"
     4.9    using [[quickcheck_approximation_custom_seed = 1]]
    4.10    using [[quickcheck_approximation_epsilon = 0.00000001]]
    4.11      --\<open>avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"}
     5.1 --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy	Thu Apr 09 20:42:38 2015 +0200
     5.2 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy	Sat Apr 11 11:56:40 2015 +0100
     5.3 @@ -103,7 +103,7 @@
     5.4    constant ln \<rightharpoonup>
     5.5      (SML) "Math.ln"
     5.6      and (OCaml) "Pervasives.ln"
     5.7 -declare ln_def[code del]
     5.8 +declare ln_real_def[code del]
     5.9  
    5.10  code_printing
    5.11    constant cos \<rightharpoonup>
     6.1 --- a/src/HOL/Library/Float.thy	Thu Apr 09 20:42:38 2015 +0200
     6.2 +++ b/src/HOL/Library/Float.thy	Sat Apr 11 11:56:40 2015 +0100
     6.3 @@ -82,16 +82,18 @@
     6.4  lemma uminus_float[simp]: "x \<in> float \<Longrightarrow> -x \<in> float"
     6.5    apply (auto simp: float_def)
     6.6    apply hypsubst_thin
     6.7 -  apply (rule_tac x="-x" in exI)
     6.8 -  apply (rule_tac x="xa" in exI)
     6.9 +  apply (rename_tac m e)
    6.10 +  apply (rule_tac x="-m" in exI)
    6.11 +  apply (rule_tac x="e" in exI)
    6.12    apply (simp add: field_simps)
    6.13    done
    6.14  
    6.15  lemma times_float[simp]: "x \<in> float \<Longrightarrow> y \<in> float \<Longrightarrow> x * y \<in> float"
    6.16    apply (auto simp: float_def)
    6.17    apply hypsubst_thin
    6.18 -  apply (rule_tac x="x * xa" in exI)
    6.19 -  apply (rule_tac x="xb + xc" in exI)
    6.20 +  apply (rename_tac mx my ex ey)
    6.21 +  apply (rule_tac x="mx * my" in exI)
    6.22 +  apply (rule_tac x="ex + ey" in exI)
    6.23    apply (simp add: powr_add)
    6.24    done
    6.25  
    6.26 @@ -107,16 +109,18 @@
    6.27  lemma div_power_2_float[simp]: "x \<in> float \<Longrightarrow> x / 2^d \<in> float"
    6.28    apply (auto simp add: float_def)
    6.29    apply hypsubst_thin
    6.30 -  apply (rule_tac x="x" in exI)
    6.31 -  apply (rule_tac x="xa - d" in exI)
    6.32 +  apply (rename_tac m e)
    6.33 +  apply (rule_tac x="m" in exI)
    6.34 +  apply (rule_tac x="e - d" in exI)
    6.35    apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
    6.36    done
    6.37  
    6.38  lemma div_power_2_int_float[simp]: "x \<in> float \<Longrightarrow> x / (2::int)^d \<in> float"
    6.39    apply (auto simp add: float_def)
    6.40    apply hypsubst_thin
    6.41 -  apply (rule_tac x="x" in exI)
    6.42 -  apply (rule_tac x="xa - d" in exI)
    6.43 +  apply (rename_tac m e)
    6.44 +  apply (rule_tac x="m" in exI)
    6.45 +  apply (rule_tac x="e - d" in exI)
    6.46    apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric])
    6.47    done
    6.48  
    6.49 @@ -687,8 +691,9 @@
    6.50  
    6.51    from neg have "2 powr real p \<le> 2 powr 0"
    6.52      by (intro powr_mono) auto
    6.53 -  also have "\<dots> \<le> \<lfloor>2 powr 0\<rfloor>" by simp
    6.54 -  also have "\<dots> \<le> \<lfloor>x * 2 powr real p\<rfloor>" unfolding real_of_int_le_iff
    6.55 +  also have "\<dots> \<le> \<lfloor>2 powr 0::real\<rfloor>" by simp
    6.56 +  also have "... \<le> \<lfloor>x * 2 powr (real p)\<rfloor>" 
    6.57 +    unfolding real_of_int_le_iff
    6.58      using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps)
    6.59    finally show ?thesis
    6.60      using prec x
    6.61 @@ -723,7 +728,7 @@
    6.62  proof
    6.63    have "round_up e f - f \<le> round_up e f - round_down e f" using round_down by simp
    6.64    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
    6.65 -  finally show "round_up e f - f \<le> 2 powr real (- e)"
    6.66 +  finally show "round_up e f - f \<le> 2 powr - (real e)"
    6.67      by simp
    6.68  qed (simp add: algebra_simps round_up)
    6.69  
    6.70 @@ -740,7 +745,7 @@
    6.71  proof
    6.72    have "f - round_down e f \<le> round_up e f - round_down e f" using round_up by simp
    6.73    also have "\<dots> \<le> 2 powr -e" using round_up_diff_round_down by simp
    6.74 -  finally show "f - round_down e f \<le> 2 powr real (- e)"
    6.75 +  finally show "f - round_down e f \<le> 2 powr - (real e)"
    6.76      by simp
    6.77  qed (simp add: algebra_simps round_down)
    6.78  
    6.79 @@ -923,8 +928,9 @@
    6.80    shows "0 \<le> e + (bitlen m - 1)"
    6.81  proof -
    6.82    have "0 < Float m e" using assms by auto
    6.83 -  hence "0 < m" using powr_gt_zero[of 2 e]
    6.84 -    by (auto simp: zero_less_mult_iff)
    6.85 +  hence "0 < m" using powr_gt_zero[of 2 e]  
    6.86 +    apply (auto simp: zero_less_mult_iff)
    6.87 +    using not_le powr_ge_pzero by blast
    6.88    hence "m \<noteq> 0" by auto
    6.89    show ?thesis
    6.90    proof (cases "0 \<le> e")
    6.91 @@ -2017,8 +2023,7 @@
    6.92    by (simp add: truncate_up_eq_truncate_down truncate_down_mono)
    6.93  
    6.94  lemma Float_le_zero_iff: "Float a b \<le> 0 \<longleftrightarrow> a \<le> 0"
    6.95 - apply (auto simp: zero_float_def mult_le_0_iff)
    6.96 - using powr_gt_zero[of 2 b] by simp
    6.97 + by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric])
    6.98  
    6.99  lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)"
   6.100    unfolding pprt_def sup_float_def max_def sup_real_def by auto
     7.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Thu Apr 09 20:42:38 2015 +0200
     7.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Sat Apr 11 11:56:40 2015 +0100
     7.3 @@ -624,7 +624,7 @@
     7.4        by blast
     7.5    }
     7.6    then show ?thesis
     7.7 -    unfolding LIMSEQ_def by blast
     7.8 +    unfolding lim_sequentially by blast
     7.9  qed
    7.10  
    7.11  
     8.1 --- a/src/HOL/Limits.thy	Thu Apr 09 20:42:38 2015 +0200
     8.2 +++ b/src/HOL/Limits.thy	Sat Apr 11 11:56:40 2015 +0100
     8.3 @@ -1287,7 +1287,7 @@
     8.4  lemma LIMSEQ_iff:
     8.5    fixes L :: "'a::real_normed_vector"
     8.6    shows "(X ----> L) = (\<forall>r>0. \<exists>no. \<forall>n \<ge> no. norm (X n - L) < r)"
     8.7 -unfolding LIMSEQ_def dist_norm ..
     8.8 +unfolding lim_sequentially dist_norm ..
     8.9  
    8.10  lemma LIMSEQ_I:
    8.11    fixes L :: "'a::real_normed_vector"
     9.1 --- a/src/HOL/MacLaurin.thy	Thu Apr 09 20:42:38 2015 +0200
     9.2 +++ b/src/HOL/MacLaurin.thy	Sat Apr 11 11:56:40 2015 +0100
     9.3 @@ -389,6 +389,12 @@
     9.4                         (exp t / (fact n)) * x ^ n"
     9.5  by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
     9.6  
     9.7 +lemma exp_lower_taylor_quadratic:
     9.8 +  fixes x::real
     9.9 +  shows "0 \<le> x \<Longrightarrow> 1 + x + x\<^sup>2 / 2 \<le> exp x"
    9.10 +  using Maclaurin_exp_le [of x 3]
    9.11 +  by (auto simp: numeral_3_eq_3 power2_eq_square power_Suc)
    9.12 +
    9.13  
    9.14  subsection{*Version for Sine Function*}
    9.15  
    10.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Thu Apr 09 20:42:38 2015 +0200
    10.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Sat Apr 11 11:56:40 2015 +0100
    10.3 @@ -189,18 +189,15 @@
    10.4  
    10.5  lemma zero_le_float:
    10.6    "(0 <= float (a,b)) = (0 <= a)"
    10.7 -  using powr_gt_zero[of 2 "real b", arith]
    10.8 -  by (simp add: float_def zero_le_mult_iff)
    10.9 +  by (simp add: float_def zero_le_mult_iff) (simp add: not_less [symmetric])
   10.10  
   10.11  lemma float_le_zero:
   10.12    "(float (a,b) <= 0) = (a <= 0)"
   10.13 -  using powr_gt_zero[of 2 "real b", arith]
   10.14 -  by (simp add: float_def mult_le_0_iff)
   10.15 +  by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric])
   10.16  
   10.17  lemma float_abs:
   10.18    "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))"
   10.19 -  using powr_gt_zero[of 2 "real b", arith]
   10.20 -  by (simp add: float_def abs_if mult_less_0_iff)
   10.21 +  by (simp add: float_def abs_if mult_less_0_iff not_less)
   10.22  
   10.23  lemma float_zero:
   10.24    "float (0, b) = 0"
    11.1 --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Thu Apr 09 20:42:38 2015 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy	Sat Apr 11 11:56:40 2015 +0100
    11.3 @@ -188,7 +188,7 @@
    11.4        by simp
    11.5    qed
    11.6    show "convergent f"
    11.7 -  proof (rule convergentI, subst LIMSEQ_def, safe)
    11.8 +  proof (rule convergentI, subst lim_sequentially, safe)
    11.9      --{* The limit function converges according to its norm *}
   11.10      fix e::real
   11.11      assume "e > 0" hence "e/2 > 0" by simp
    12.1 --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Thu Apr 09 20:42:38 2015 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy	Sat Apr 11 11:56:40 2015 +0100
    12.3 @@ -250,6 +250,21 @@
    12.4      by (metis closed_halfspace_Im_eq)
    12.5  qed
    12.6  
    12.7 +lemma closed_Real_halfspace_Re_le: "closed (\<real> \<inter> {w. Re w \<le> x})"
    12.8 +  by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le)
    12.9 +
   12.10 +lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
   12.11 +  using closed_halfspace_Re_ge
   12.12 +  by (simp add: closed_Int closed_complex_Reals)
   12.13 +
   12.14 +lemma closed_real_abs_le: "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
   12.15 +proof -
   12.16 +  have "{w \<in> \<real>. \<bar>Re w\<bar> \<le> r} = (\<real> \<inter> {w. Re w \<le> r}) \<inter> (\<real> \<inter> {w. Re w \<ge> -r})"
   12.17 +    by auto
   12.18 +  then show "closed {w \<in> \<real>. \<bar>Re w\<bar> \<le> r}"
   12.19 +    by (simp add: closed_Int closed_Real_halfspace_Re_ge closed_Real_halfspace_Re_le)
   12.20 +qed
   12.21 +
   12.22  lemma real_lim:
   12.23    fixes l::complex
   12.24    assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\<And>a. P a \<Longrightarrow> f a \<in> \<real>"
   12.25 @@ -1151,4 +1166,93 @@
   12.26      done
   12.27  qed
   12.28  
   12.29 +
   12.30 +subsection {* Polynomal function extremal theorem, from HOL Light*}
   12.31 +
   12.32 +lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*)
   12.33 +    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   12.34 +  assumes "0 < e"
   12.35 +    shows "\<exists>M. \<forall>z. M \<le> norm(z) \<longrightarrow> norm (\<Sum>i\<le>n. c(i) * z^i) \<le> e * norm(z) ^ (Suc n)"
   12.36 +proof (induct n)
   12.37 +  case 0 with assms
   12.38 +  show ?case
   12.39 +    apply (rule_tac x="norm (c 0) / e" in exI)
   12.40 +    apply (auto simp: field_simps)
   12.41 +    done
   12.42 +next
   12.43 +  case (Suc n)
   12.44 +  obtain M where M: "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
   12.45 +    using Suc assms by blast
   12.46 +  show ?case
   12.47 +  proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc)
   12.48 +    fix z::'a
   12.49 +    assume z1: "M \<le> norm z" and "1 + norm (c (Suc n)) / e \<le> norm z"
   12.50 +    then have z2: "e + norm (c (Suc n)) \<le> e * norm z"
   12.51 +      using assms by (simp add: field_simps)
   12.52 +    have "norm (\<Sum>i\<le>n. c i * z^i) \<le> e * norm z ^ Suc n"
   12.53 +      using M [OF z1] by simp
   12.54 +    then have "norm (\<Sum>i\<le>n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
   12.55 +      by simp
   12.56 +    then have "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)"
   12.57 +      by (blast intro: norm_triangle_le elim: )
   12.58 +    also have "... \<le> (e + norm (c (Suc n))) * norm z ^ Suc n"
   12.59 +      by (simp add: norm_power norm_mult algebra_simps)
   12.60 +    also have "... \<le> (e * norm z) * norm z ^ Suc n"
   12.61 +      by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power)
   12.62 +    finally show "norm ((\<Sum>i\<le>n. c i * z^i) + c (Suc n) * z ^ Suc n) \<le> e * norm z ^ Suc (Suc n)"
   12.63 +      by (simp add: power_Suc)
   12.64 +  qed
   12.65 +qed
   12.66 +
   12.67 +lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*)
   12.68 +    fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
   12.69 +  assumes k: "c k \<noteq> 0" "1\<le>k" and kn: "k\<le>n"
   12.70 +    shows "eventually (\<lambda>z. norm (\<Sum>i\<le>n. c(i) * z^i) \<ge> B) at_infinity"
   12.71 +using kn
   12.72 +proof (induction n)
   12.73 +  case 0
   12.74 +  then show ?case
   12.75 +    using k  by simp
   12.76 +next
   12.77 +  case (Suc m)
   12.78 +  let ?even = ?case
   12.79 +  show ?even
   12.80 +  proof (cases "c (Suc m) = 0")
   12.81 +    case True
   12.82 +    then show ?even using Suc k
   12.83 +      by auto (metis antisym_conv less_eq_Suc_le not_le)
   12.84 +  next
   12.85 +    case False
   12.86 +    then obtain M where M:
   12.87 +          "\<And>z. M \<le> norm z \<Longrightarrow> norm (\<Sum>i\<le>m. c i * z^i) \<le> norm (c (Suc m)) / 2 * norm z ^ Suc m"
   12.88 +      using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc
   12.89 +      by auto
   12.90 +    have "\<exists>b. \<forall>z. b \<le> norm z \<longrightarrow> B \<le> norm (\<Sum>i\<le>Suc m. c i * z^i)"
   12.91 +    proof (rule exI [where x="max M (max 1 (\<bar>B\<bar> / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc)
   12.92 +      fix z::'a
   12.93 +      assume z1: "M \<le> norm z" "1 \<le> norm z"
   12.94 +         and "\<bar>B\<bar> * 2 / norm (c (Suc m)) \<le> norm z"
   12.95 +      then have z2: "\<bar>B\<bar> \<le> norm (c (Suc m)) * norm z / 2"
   12.96 +        using False by (simp add: field_simps)
   12.97 +      have nz: "norm z \<le> norm z ^ Suc m"
   12.98 +        by (metis `1 \<le> norm z` One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc)
   12.99 +      have *: "\<And>y x. norm (c (Suc m)) * norm z / 2 \<le> norm y - norm x \<Longrightarrow> B \<le> norm (x + y)"
  12.100 +        by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2)
  12.101 +      have "norm z * norm (c (Suc m)) + 2 * norm (\<Sum>i\<le>m. c i * z^i)
  12.102 +            \<le> norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m"
  12.103 +        using M [of z] Suc z1  by auto
  12.104 +      also have "... \<le> 2 * (norm (c (Suc m)) * norm z ^ Suc m)"
  12.105 +        using nz by (simp add: mult_mono del: power_Suc)
  12.106 +      finally show "B \<le> norm ((\<Sum>i\<le>m. c i * z^i) + c (Suc m) * z ^ Suc m)"
  12.107 +        using Suc.IH
  12.108 +        apply (auto simp: eventually_at_infinity)
  12.109 +        apply (rule *)
  12.110 +        apply (simp add: field_simps norm_mult norm_power)
  12.111 +        done
  12.112 +    qed
  12.113 +    then show ?even
  12.114 +      by (simp add: eventually_at_infinity)
  12.115 +  qed
  12.116 +qed
  12.117 +
  12.118  end
    13.1 --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Thu Apr 09 20:42:38 2015 +0200
    13.2 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy	Sat Apr 11 11:56:40 2015 +0100
    13.3 @@ -8,7 +8,6 @@
    13.4  imports  "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics"
    13.5  begin
    13.6  
    13.7 -
    13.8  lemma cmod_add_real_less:
    13.9    assumes "Im z \<noteq> 0" "r\<noteq>0"
   13.10      shows "cmod (z + r) < cmod z + abs r"
   13.11 @@ -613,6 +612,14 @@
   13.12    apply (simp only: pos_le_divide_eq [symmetric], linarith)
   13.13    done
   13.14  
   13.15 +lemma e_less_3: "exp 1 < (3::real)"
   13.16 +  using e_approx_32
   13.17 +  by (simp add: abs_if split: split_if_asm)
   13.18 +
   13.19 +lemma ln3_gt_1: "ln 3 > (1::real)"
   13.20 +  by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp)
   13.21 +
   13.22 +
   13.23  subsection{*The argument of a complex number*}
   13.24  
   13.25  definition Arg :: "complex \<Rightarrow> real" where
   13.26 @@ -892,8 +899,9 @@
   13.27  
   13.28  subsection{*Complex logarithms (the conventional principal value)*}
   13.29  
   13.30 -definition Ln where
   13.31 -   "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   13.32 +definition Ln :: "complex \<Rightarrow> complex"
   13.33 +  where "Ln \<equiv> \<lambda>z. THE w. exp w = z & -pi < Im(w) & Im(w) \<le> pi"
   13.34 +
   13.35  
   13.36  lemma
   13.37    assumes "z \<noteq> 0"
   13.38 @@ -941,6 +949,7 @@
   13.39    apply (auto simp: exp_of_nat_mult [symmetric])
   13.40    done
   13.41  
   13.42 +
   13.43  subsection{*The Unwinding Number and the Ln-product Formula*}
   13.44  
   13.45  text{*Note that in this special case the unwinding number is -1, 0 or 1.*}
   13.46 @@ -1128,8 +1137,8 @@
   13.47    apply (cases "z=0", auto)
   13.48    apply (rule exp_complex_eqI)
   13.49    apply (auto simp: abs_if split: split_if_asm)
   13.50 -  apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps(1) cnj.simps(2) mult_2 neg_equal_0_iff_equal)
   13.51 -  apply (metis add_mono_thms_linordered_field(5) complex_cnj_zero_iff diff_0_right diff_minus_eq_add minus_diff_eq mpi_less_Im_Ln mult.commute mult_2_right neg_less_iff_less)
   13.52 +  apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal)
   13.53 +  apply (metis complex_cnj_zero_iff diff_minus_eq_add diff_strict_mono minus_less_iff mpi_less_Im_Ln mult.commute mult_2_right)
   13.54    by (metis exp_Ln exp_cnj)
   13.55  
   13.56  lemma Ln_inverse: "(Im(z) = 0 \<Longrightarrow> 0 < Re z) \<Longrightarrow> Ln(inverse z) = -(Ln z)"
   13.57 @@ -1141,7 +1150,7 @@
   13.58                 inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right)
   13.59    done
   13.60  
   13.61 -lemma Ln_1 [simp]: "Ln(1) = 0"
   13.62 +lemma Ln_1 [simp]: "Ln 1 = 0"
   13.63  proof -
   13.64    have "Ln (exp 0) = 0"
   13.65      by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one)
   13.66 @@ -1149,6 +1158,18 @@
   13.67      by simp
   13.68  qed
   13.69  
   13.70 +instantiation complex :: ln
   13.71 +begin
   13.72 +
   13.73 +definition ln_complex :: "complex \<Rightarrow> complex"
   13.74 +  where "ln_complex \<equiv> Ln"
   13.75 +
   13.76 +instance 
   13.77 +  by intro_classes (simp add: ln_complex_def)
   13.78 +
   13.79 +end
   13.80 +
   13.81 +
   13.82  lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi"
   13.83    apply (rule exp_complex_eqI)
   13.84    using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi
   13.85 @@ -1242,6 +1263,93 @@
   13.86    by (auto simp: of_real_numeral Ln_times)
   13.87  
   13.88  
   13.89 +
   13.90 +subsection{*Complex Powers*}
   13.91 +
   13.92 +lemma powr_0 [simp]: "0 powr z = 0"
   13.93 +  by (simp add: powr_def)
   13.94 +
   13.95 +lemma powr_to_1 [simp]: "z powr 1 = (z::complex)"
   13.96 +  by (simp add: powr_def ln_complex_def)
   13.97 +
   13.98 +lemma powr_nat:
   13.99 +  fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
  13.100 +  by (simp add: exp_of_nat_mult powr_def ln_complex_def)
  13.101 +
  13.102 +lemma powr_add:
  13.103 +  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
  13.104 +  by (simp add: powr_def algebra_simps exp_add)
  13.105 +
  13.106 +lemma powr_minus:
  13.107 +  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
  13.108 +  by (simp add: powr_def exp_minus)
  13.109 +
  13.110 +lemma powr_diff:
  13.111 +  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
  13.112 +  by (simp add: powr_def algebra_simps exp_diff)
  13.113 +
  13.114 +lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
  13.115 +  apply (simp add: powr_def ln_complex_def)
  13.116 +  using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
  13.117 +  by auto
  13.118 +
  13.119 +lemma powr_real_real:
  13.120 +    "\<lbrakk>w \<in> \<real>; z \<in> \<real>; 0 < Re w\<rbrakk> \<Longrightarrow> w powr z = exp(Re z * ln(Re w))"
  13.121 +  apply (simp add: powr_def ln_complex_def)
  13.122 +  by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero
  13.123 +       exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult)
  13.124 +
  13.125 +lemma powr_of_real:
  13.126 +  fixes x::real
  13.127 +  shows "0 < x \<Longrightarrow> x powr y = x powr y"
  13.128 +  by (simp add: powr_def powr_real_real)
  13.129 +
  13.130 +lemma norm_powr_real_mono:
  13.131 +    "w \<in> \<real> \<Longrightarrow> 1 < Re w
  13.132 +             \<Longrightarrow> norm(w powr z1) \<le> norm(w powr z2) \<longleftrightarrow> Re z1 \<le> Re z2"
  13.133 +  by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real)
  13.134 +
  13.135 +lemma powr_times_real:
  13.136 +    "\<lbrakk>x \<in> \<real>; y \<in> \<real>; 0 \<le> Re x; 0 \<le> Re y\<rbrakk>
  13.137 +           \<Longrightarrow> (x * y) powr z = x powr z * y powr z"
  13.138 +  by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real)
  13.139 +
  13.140 +lemma has_field_derivative_powr:
  13.141 +    "(Im z = 0 \<Longrightarrow> 0 < Re z)
  13.142 +     \<Longrightarrow> ((\<lambda>z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)"
  13.143 +  apply (cases "z=0", auto)
  13.144 +  apply (simp add: powr_def ln_complex_def)
  13.145 +  apply (rule DERIV_transform_at [where d = "norm z" and f = "\<lambda>z. exp (s * Ln z)"])
  13.146 +  apply (auto simp: dist_complex_def ln_complex_def)
  13.147 +  apply (intro derivative_eq_intros | simp add: assms)+
  13.148 +  apply (simp add: field_simps exp_diff)
  13.149 +  done
  13.150 +
  13.151 +lemma has_field_derivative_powr_right:
  13.152 +    "w \<noteq> 0 \<Longrightarrow> ((\<lambda>z. w powr z) has_field_derivative Ln w * w powr z) (at z)"
  13.153 +  apply (simp add: powr_def ln_complex_def)
  13.154 +  apply (intro derivative_eq_intros | simp add: assms)+
  13.155 +  done
  13.156 +
  13.157 +lemma complex_differentiable_powr_right:
  13.158 +    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) complex_differentiable (at z)"
  13.159 +using complex_differentiable_def has_field_derivative_powr_right by blast
  13.160 +
  13.161 +
  13.162 +lemma holomorphic_on_powr_right:
  13.163 +    "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
  13.164 +    unfolding holomorphic_on_def
  13.165 +    using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce
  13.166 +
  13.167 +
  13.168 +lemma norm_powr_real_powr:
  13.169 +  "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = Re w powr Re z"
  13.170 +  by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def)
  13.171 +
  13.172 +lemma cmod_Ln_Reals [simp]:"z \<in> Reals \<Longrightarrow> 0 < Re z \<Longrightarrow> cmod (Ln z) = norm (ln (Re z))"
  13.173 +  using Ln_of_real by force
  13.174 +
  13.175 +
  13.176  subsection{*Relation between Square Root and exp/ln, hence its derivative*}
  13.177  
  13.178  lemma csqrt_exp_Ln:
  13.179 @@ -1336,10 +1444,6 @@
  13.180    using open_Compl
  13.181    by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg)
  13.182  
  13.183 -lemma closed_Real_halfspace_Re_ge: "closed (\<real> \<inter> {w. x \<le> Re(w)})"
  13.184 -  using closed_halfspace_Re_ge
  13.185 -  by (simp add: closed_Int closed_complex_Reals)
  13.186 -
  13.187  lemma continuous_within_csqrt_posreal:
  13.188      "continuous (at z within (\<real> \<inter> {w. 0 \<le> Re(w)})) csqrt"
  13.189  proof (cases "Im z = 0 --> 0 < Re(z)")
  13.190 @@ -1867,15 +1971,15 @@
  13.191               Re z = pi & Im z \<le> 0"
  13.192        shows "Arccos(cos z) = z"
  13.193  proof -
  13.194 -  have *: "((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z))) = sin z"
  13.195 +  have *: "((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z))) = sin z"
  13.196      by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square)
  13.197 -  have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2"
  13.198 +  have "1 - (exp (\<i> * z) + inverse (exp (\<i> * z)))\<^sup>2 / 4 = ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2"
  13.199      by (simp add: field_simps power2_eq_square)
  13.200    then have "Arccos(cos z) = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  13.201 -                           \<i> * csqrt (((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))\<^sup>2)))"
  13.202 +                           \<i> * csqrt (((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))\<^sup>2)))"
  13.203      by (simp add: cos_exp_eq Arccos_def exp_minus)
  13.204    also have "... = - (\<i> * Ln ((exp (\<i> * z) + inverse (exp (\<i> * z))) / 2 +
  13.205 -                              \<i> * ((\<i> - (Exp (\<i> * z))\<^sup>2 * \<i>) / (2 * Exp (\<i> * z)))))"
  13.206 +                              \<i> * ((\<i> - (exp (\<i> * z))\<^sup>2 * \<i>) / (2 * exp (\<i> * z)))))"
  13.207      apply (subst csqrt_square)
  13.208      using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z]
  13.209      apply (auto simp: * Re_sin Im_sin)
  13.210 @@ -2177,4 +2281,129 @@
  13.211  lemma of_real_arccos: "abs x \<le> 1 \<Longrightarrow> of_real(arccos x) = Arccos(of_real x)"
  13.212    by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0)
  13.213  
  13.214 +subsection{*Some interrelationships among the real inverse trig functions.*}
  13.215 +
  13.216 +lemma arccos_arctan:
  13.217 +  assumes "-1 < x" "x < 1"
  13.218 +    shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))"
  13.219 +proof -
  13.220 +  have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0"
  13.221 +  proof (rule sin_eq_0_pi)
  13.222 +    show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)"
  13.223 +      using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
  13.224 +      by (simp add: algebra_simps)
  13.225 +  next
  13.226 +    show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi"
  13.227 +      using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"]  arccos_bounded [of x] assms
  13.228 +      by (simp add: algebra_simps)
  13.229 +  next
  13.230 +    show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0"
  13.231 +      using assms
  13.232 +      by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan
  13.233 +                    power2_eq_square square_eq_1_iff)
  13.234 +  qed
  13.235 +  then show ?thesis
  13.236 +    by simp
  13.237 +qed
  13.238 +
  13.239 +lemma arcsin_plus_arccos:
  13.240 +  assumes "-1 \<le> x" "x \<le> 1"
  13.241 +    shows "arcsin x + arccos x = pi/2"
  13.242 +proof -
  13.243 +  have "arcsin x = pi/2 - arccos x"
  13.244 +    apply (rule sin_inj_pi)
  13.245 +    using assms arcsin [OF assms] arccos [OF assms]
  13.246 +    apply (auto simp: algebra_simps sin_diff)
  13.247 +    done
  13.248 +  then show ?thesis
  13.249 +    by (simp add: algebra_simps)
  13.250 +qed
  13.251 +
  13.252 +lemma arcsin_arccos_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = pi/2 - arccos x"
  13.253 +  using arcsin_plus_arccos by force
  13.254 +
  13.255 +lemma arccos_arcsin_eq: "-1 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = pi/2 - arcsin x"
  13.256 +  using arcsin_plus_arccos by force
  13.257 +
  13.258 +lemma arcsin_arctan: "-1 < x \<Longrightarrow> x < 1 \<Longrightarrow> arcsin x = arctan(x / sqrt(1 - x\<^sup>2))"
  13.259 +  by (simp add: arccos_arctan arcsin_arccos_eq)
  13.260 +
  13.261 +lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \<le> 1 then sqrt (1 - x^2) else \<i> * sqrt (x^2 - 1))"
  13.262 +  by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg)
  13.263 +
  13.264 +lemma arcsin_arccos_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arcsin x = arccos(sqrt(1 - x\<^sup>2))"
  13.265 +  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  13.266 +  apply (subst Arcsin_Arccos_csqrt_pos)
  13.267 +  apply (auto simp: power_le_one zz)
  13.268 +  done
  13.269 +
  13.270 +lemma arcsin_arccos_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arcsin x = -arccos(sqrt(1 - x\<^sup>2))"
  13.271 +  using arcsin_arccos_sqrt_pos [of "-x"]
  13.272 +  by (simp add: arcsin_minus)
  13.273 +
  13.274 +lemma arccos_arcsin_sqrt_pos: "0 \<le> x \<Longrightarrow> x \<le> 1 \<Longrightarrow> arccos x = arcsin(sqrt(1 - x\<^sup>2))"
  13.275 +  apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos)
  13.276 +  apply (subst Arccos_Arcsin_csqrt_pos)
  13.277 +  apply (auto simp: power_le_one zz)
  13.278 +  done
  13.279 +
  13.280 +lemma arccos_arcsin_sqrt_neg: "-1 \<le> x \<Longrightarrow> x \<le> 0 \<Longrightarrow> arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))"
  13.281 +  using arccos_arcsin_sqrt_pos [of "-x"]
  13.282 +  by (simp add: arccos_minus)
  13.283 +
  13.284 +subsection{*continuity results for arcsin and arccos.*}
  13.285 +
  13.286 +lemma continuous_on_Arcsin_real [continuous_intros]:
  13.287 +    "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arcsin"
  13.288 +proof -
  13.289 +  have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arcsin (Re x))) =
  13.290 +        continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arcsin (of_real (Re x)))))"
  13.291 +    by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin)
  13.292 +  also have "... = ?thesis"
  13.293 +    by (rule continuous_on_cong [OF refl]) simp
  13.294 +  finally show ?thesis
  13.295 +    using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
  13.296 +          continuous_on_of_real
  13.297 +    by fastforce
  13.298 +qed
  13.299 +
  13.300 +lemma continuous_within_Arcsin_real:
  13.301 +    "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arcsin"
  13.302 +proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
  13.303 +  case True then show ?thesis
  13.304 +    using continuous_on_Arcsin_real continuous_on_eq_continuous_within
  13.305 +    by blast
  13.306 +next
  13.307 +  case False
  13.308 +  with closed_real_abs_le [of 1] show ?thesis
  13.309 +    by (rule continuous_within_closed_nontrivial)
  13.310 +qed
  13.311 +
  13.312 +lemma continuous_on_Arccos_real:
  13.313 +    "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} Arccos"
  13.314 +proof -
  13.315 +  have "continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (arccos (Re x))) =
  13.316 +        continuous_on {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1} (\<lambda>x. complex_of_real (Re (Arccos (of_real (Re x)))))"
  13.317 +    by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos)
  13.318 +  also have "... = ?thesis"
  13.319 +    by (rule continuous_on_cong [OF refl]) simp
  13.320 +  finally show ?thesis
  13.321 +    using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}"]
  13.322 +          continuous_on_of_real
  13.323 +    by fastforce
  13.324 +qed
  13.325 +
  13.326 +lemma continuous_within_Arccos_real:
  13.327 +    "continuous (at z within {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}) Arccos"
  13.328 +proof (cases "z \<in> {w \<in> \<real>. \<bar>Re w\<bar> \<le> 1}")
  13.329 +  case True then show ?thesis
  13.330 +    using continuous_on_Arccos_real continuous_on_eq_continuous_within
  13.331 +    by blast
  13.332 +next
  13.333 +  case False
  13.334 +  with closed_real_abs_le [of 1] show ?thesis
  13.335 +    by (rule continuous_within_closed_nontrivial)
  13.336 +qed
  13.337 +
  13.338 +
  13.339  end
    14.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Apr 09 20:42:38 2015 +0200
    14.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sat Apr 11 11:56:40 2015 +0100
    14.3 @@ -4077,7 +4077,7 @@
    14.4          apply (erule_tac x="e/2" in allE)
    14.5          apply auto
    14.6          done
    14.7 -      from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]]
    14.8 +      from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]]
    14.9        obtain M where M:"\<forall>n\<ge>M. dist ((f \<circ> r) n) l < e/2"
   14.10          using `e > 0` by auto
   14.11        {
   14.12 @@ -4096,7 +4096,7 @@
   14.13        then have "\<exists>N. \<forall>n\<ge>N. dist (f n) l < e" by blast
   14.14      }
   14.15      then have "\<exists>l\<in>s. (f ---> l) sequentially" using `l\<in>s`
   14.16 -      unfolding LIMSEQ_def by auto
   14.17 +      unfolding lim_sequentially by auto
   14.18    }
   14.19    then show ?thesis unfolding complete_def by auto
   14.20  qed
   14.21 @@ -4442,7 +4442,7 @@
   14.22        fix e :: real
   14.23        assume "e > 0"
   14.24        then obtain N :: nat where N: "\<forall>n\<ge>N. dist (t n) l < e"
   14.25 -        using l[unfolded LIMSEQ_def] by auto
   14.26 +        using l[unfolded lim_sequentially] by auto
   14.27        have "t (max n N) \<in> s n"
   14.28          using assms(3)
   14.29          unfolding subset_eq
   14.30 @@ -4542,7 +4542,7 @@
   14.31        fix x
   14.32        assume "P x"
   14.33        then obtain M where M:"\<forall>n\<ge>M. dist (s n x) (l x) < e/2"
   14.34 -        using l[THEN spec[where x=x], unfolded LIMSEQ_def] and `e > 0`
   14.35 +        using l[THEN spec[where x=x], unfolded lim_sequentially] and `e > 0`
   14.36          by (auto elim!: allE[where x="e/2"])
   14.37        fix n :: nat
   14.38        assume "n \<ge> N"
   14.39 @@ -4571,7 +4571,7 @@
   14.40      assume "P x"
   14.41      then have "l x = l' x"
   14.42        using tendsto_unique[OF trivial_limit_sequentially, of "\<lambda>n. s n x" "l x" "l' x"]
   14.43 -      using l and assms(2) unfolding LIMSEQ_def by blast
   14.44 +      using l and assms(2) unfolding lim_sequentially by blast
   14.45    }
   14.46    ultimately show ?thesis by auto
   14.47  qed
   14.48 @@ -4809,7 +4809,7 @@
   14.49        then obtain d where "d > 0" and d: "\<forall>x\<in>s. \<forall>x'\<in>s. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
   14.50          using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto
   14.51        obtain N where N: "\<forall>n\<ge>N. dist (x n) (y n) < d"
   14.52 -        using xy[unfolded LIMSEQ_def dist_norm] and `d>0` by auto
   14.53 +        using xy[unfolded lim_sequentially dist_norm] and `d>0` by auto
   14.54        {
   14.55          fix n
   14.56          assume "n\<ge>N"
   14.57 @@ -4824,7 +4824,7 @@
   14.58          by auto
   14.59      }
   14.60      then have "((\<lambda>n. dist (f(x n)) (f(y n))) ---> 0) sequentially"
   14.61 -      unfolding LIMSEQ_def and dist_real_def by auto
   14.62 +      unfolding lim_sequentially and dist_real_def by auto
   14.63    }
   14.64    then show ?rhs by auto
   14.65  next
   14.66 @@ -4864,7 +4864,7 @@
   14.67      }
   14.68      then have "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. dist (f (x n)) (f (y n)) < e"
   14.69        using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn
   14.70 -      unfolding LIMSEQ_def dist_real_def by auto
   14.71 +      unfolding lim_sequentially dist_real_def by auto
   14.72      then have False using fxy and `e>0` by auto
   14.73    }
   14.74    then show ?lhs
   14.75 @@ -6615,7 +6615,7 @@
   14.76          then have "\<exists>N::nat. \<forall>n\<ge>N. inverse (real n + 1) < e" by auto
   14.77        }
   14.78        then have "((\<lambda>n. inverse (real n + 1)) ---> 0) sequentially"
   14.79 -        unfolding LIMSEQ_def by(auto simp add: dist_norm)
   14.80 +        unfolding lim_sequentially by(auto simp add: dist_norm)
   14.81        then have "(f ---> x) sequentially"
   14.82          unfolding f_def
   14.83          using tendsto_add[OF tendsto_const, of "\<lambda>n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x]
   14.84 @@ -7446,7 +7446,7 @@
   14.85        unfolding e_def using zero_le_dist[of "f x" x]
   14.86        by (metis dist_eq_0_iff dist_nz e_def)
   14.87      then obtain N where N:"\<forall>n\<ge>N. dist (z n) x < e / 2"
   14.88 -      using x[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto
   14.89 +      using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto
   14.90      then have N':"dist (z N) x < e / 2" by auto
   14.91  
   14.92      have *: "c * dist (z N) x \<le> dist (z N) x"
    15.1 --- a/src/HOL/NSA/HLog.thy	Thu Apr 09 20:42:38 2015 +0200
    15.2 +++ b/src/HOL/NSA/HLog.thy	Sat Apr 11 11:56:40 2015 +0100
    15.3 @@ -34,13 +34,13 @@
    15.4  
    15.5  lemma powhr_mult:
    15.6    "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)"
    15.7 -by (transfer, rule powr_mult)
    15.8 +by (transfer, simp add: powr_mult)
    15.9  
   15.10 -lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a"
   15.11 +lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \<longleftrightarrow> x \<noteq> 0"
   15.12  by (transfer, simp)
   15.13  
   15.14 -lemma powhr_not_zero [simp]: "x powhr a \<noteq> 0"
   15.15 -by (metis less_numeral_extra(3) powhr_gt_zero)
   15.16 +lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
   15.17 +by transfer simp
   15.18  
   15.19  lemma powhr_divide:
   15.20    "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)"
   15.21 @@ -105,8 +105,8 @@
   15.22        ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x"
   15.23  by (transfer, rule log_eq_div_ln_mult_log)
   15.24  
   15.25 -lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)"
   15.26 -by (transfer, simp add: powr_def)
   15.27 +lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))"
   15.28 +  by (transfer, simp add: powr_def)
   15.29  
   15.30  lemma HInfinite_powhr:
   15.31       "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal;  
    16.1 --- a/src/HOL/NSA/HTranscendental.thy	Thu Apr 09 20:42:38 2015 +0200
    16.2 +++ b/src/HOL/NSA/HTranscendental.thy	Sat Apr 11 11:56:40 2015 +0100
    16.3 @@ -306,34 +306,37 @@
    16.4  lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x"
    16.5  by transfer (rule exp_gt_one)
    16.6  
    16.7 -lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x"
    16.8 +abbreviation real_ln :: "real \<Rightarrow> real" where 
    16.9 +  "real_ln \<equiv> ln"
   16.10 +
   16.11 +lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x"
   16.12  by transfer (rule ln_exp)
   16.13  
   16.14 -lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)"
   16.15 +lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)"
   16.16  by transfer (rule exp_ln_iff)
   16.17  
   16.18 -lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u"
   16.19 +lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u"
   16.20  by transfer (rule ln_unique)
   16.21  
   16.22 -lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x"
   16.23 +lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x"
   16.24  by transfer (rule ln_less_self)
   16.25  
   16.26 -lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* ln) x"
   16.27 +lemma starfun_ln_ge_zero [simp]: "!!x. 1 \<le> x ==> 0 \<le> ( *f* real_ln) x"
   16.28  by transfer (rule ln_ge_zero)
   16.29  
   16.30 -lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x"
   16.31 +lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x"
   16.32  by transfer (rule ln_gt_zero)
   16.33  
   16.34 -lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* ln) x \<noteq> 0"
   16.35 +lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \<noteq> 1 |] ==> ( *f* real_ln) x \<noteq> 0"
   16.36  by transfer simp
   16.37  
   16.38 -lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* ln) x \<in> HFinite"
   16.39 +lemma starfun_ln_HFinite: "[| x \<in> HFinite; 1 \<le> x |] ==> ( *f* real_ln) x \<in> HFinite"
   16.40  apply (rule HFinite_bounded)
   16.41  apply assumption 
   16.42  apply (simp_all add: starfun_ln_less_self order_less_imp_le)
   16.43  done
   16.44  
   16.45 -lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x"
   16.46 +lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x"
   16.47  by transfer (rule ln_inverse)
   16.48  
   16.49  lemma starfun_abs_exp_cancel: "\<And>x. \<bar>( *f* exp) (x::hypreal)\<bar> = ( *f* exp) x"
   16.50 @@ -360,7 +363,7 @@
   16.51  
   16.52  (* using previous result to get to result *)
   16.53  lemma starfun_ln_HInfinite:
   16.54 -     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   16.55 +     "[| x \<in> HInfinite; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   16.56  apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2])
   16.57  apply (drule starfun_exp_HFinite)
   16.58  apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff)
   16.59 @@ -374,7 +377,7 @@
   16.60  
   16.61  (* check out this proof!!! *)
   16.62  lemma starfun_ln_HFinite_not_Infinitesimal:
   16.63 -     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HFinite"
   16.64 +     "[| x \<in> HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HFinite"
   16.65  apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2])
   16.66  apply (drule starfun_exp_HInfinite_Infinitesimal_disj)
   16.67  apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff
   16.68 @@ -383,22 +386,22 @@
   16.69  
   16.70  (* we do proof by considering ln of 1/x *)
   16.71  lemma starfun_ln_Infinitesimal_HInfinite:
   16.72 -     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x \<in> HInfinite"
   16.73 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \<in> HInfinite"
   16.74  apply (drule Infinitesimal_inverse_HInfinite)
   16.75  apply (frule positive_imp_inverse_positive)
   16.76  apply (drule_tac [2] starfun_ln_HInfinite)
   16.77  apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff)
   16.78  done
   16.79  
   16.80 -lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0"
   16.81 +lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0"
   16.82  by transfer (rule ln_less_zero)
   16.83  
   16.84  lemma starfun_ln_Infinitesimal_less_zero:
   16.85 -     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0"
   16.86 +     "[| x \<in> Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0"
   16.87  by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def)
   16.88  
   16.89  lemma starfun_ln_HInfinite_gt_zero:
   16.90 -     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* ln) x"
   16.91 +     "[| x \<in> HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x"
   16.92  by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def)
   16.93  
   16.94  
    17.1 --- a/src/HOL/NSA/NSComplex.thy	Thu Apr 09 20:42:38 2015 +0200
    17.2 +++ b/src/HOL/NSA/NSComplex.thy	Sat Apr 11 11:56:40 2015 +0100
    17.3 @@ -72,7 +72,7 @@
    17.4    (*------------ e ^ (x + iy) ------------*)
    17.5  definition
    17.6    hExp :: "hcomplex => hcomplex" where
    17.7 -  "hExp = *f* Exp"
    17.8 +  "hExp = *f* exp"
    17.9  
   17.10  definition
   17.11    HComplex :: "[hypreal,hypreal] => hcomplex" where
   17.12 @@ -485,7 +485,7 @@
   17.13  by transfer (rule rcis_Ex)
   17.14  
   17.15  lemma hRe_hcomplex_polar [simp]:
   17.16 -  "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   17.17 +  "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   17.18        r * ( *f* cos) a"
   17.19  by transfer simp
   17.20  
   17.21 @@ -493,7 +493,7 @@
   17.22  by transfer (rule Re_rcis)
   17.23  
   17.24  lemma hIm_hcomplex_polar [simp]:
   17.25 -  "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = 
   17.26 +  "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) =
   17.27        r * ( *f* sin) a"
   17.28  by transfer simp
   17.29  
   17.30 @@ -621,8 +621,8 @@
   17.31  
   17.32  subsection{*Numerals and Arithmetic*}
   17.33  
   17.34 -lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: 
   17.35 -     "hcomplex_of_hypreal (hypreal_of_real x) =  
   17.36 +lemma hcomplex_of_hypreal_eq_hcomplex_of_complex:
   17.37 +     "hcomplex_of_hypreal (hypreal_of_real x) =
   17.38        hcomplex_of_complex (complex_of_real x)"
   17.39  by transfer (rule refl)
   17.40  
   17.41 @@ -642,15 +642,15 @@
   17.42        "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)"
   17.43  by transfer (rule norm_numeral)
   17.44  
   17.45 -lemma hcomplex_neg_numeral_hcmod [simp]: 
   17.46 +lemma hcomplex_neg_numeral_hcmod [simp]:
   17.47        "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)"
   17.48  by transfer (rule norm_neg_numeral)
   17.49  
   17.50 -lemma hcomplex_numeral_hRe [simp]: 
   17.51 +lemma hcomplex_numeral_hRe [simp]:
   17.52        "hRe(numeral v :: hcomplex) = numeral v"
   17.53  by transfer (rule complex_Re_numeral)
   17.54  
   17.55 -lemma hcomplex_numeral_hIm [simp]: 
   17.56 +lemma hcomplex_numeral_hIm [simp]:
   17.57        "hIm(numeral v :: hcomplex) = 0"
   17.58  by transfer (rule complex_Im_numeral)
   17.59  
    18.1 --- a/src/HOL/Probability/Borel_Space.thy	Thu Apr 09 20:42:38 2015 +0200
    18.2 +++ b/src/HOL/Probability/Borel_Space.thy	Sat Apr 11 11:56:40 2015 +0100
    18.3 @@ -1038,7 +1038,7 @@
    18.4  
    18.5  lemma borel_measurable_ln[measurable (raw)]:
    18.6    assumes f: "f \<in> borel_measurable M"
    18.7 -  shows "(\<lambda>x. ln (f x)) \<in> borel_measurable M"
    18.8 +  shows "(\<lambda>x. ln (f x :: real)) \<in> borel_measurable M"
    18.9    apply (rule measurable_compose[OF f])
   18.10    apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"])
   18.11    apply (auto intro!: continuous_on_ln continuous_on_id)
    19.1 --- a/src/HOL/Probability/Information.thy	Thu Apr 09 20:42:38 2015 +0200
    19.2 +++ b/src/HOL/Probability/Information.thy	Sat Apr 11 11:56:40 2015 +0100
    19.3 @@ -46,7 +46,7 @@
    19.4      finally have "exp u \<noteq> x"
    19.5        by auto }
    19.6    then show "log b x = log b 0"
    19.7 -    by (simp add: log_def ln_def)
    19.8 +    by (simp add: log_def ln_real_def)
    19.9  qed
   19.10  
   19.11  lemma log_mult_eq:
    20.1 --- a/src/HOL/Probability/Regularity.thy	Thu Apr 09 20:42:38 2015 +0200
    20.2 +++ b/src/HOL/Probability/Regularity.thy	Sat Apr 11 11:56:40 2015 +0100
    20.3 @@ -363,7 +363,7 @@
    20.4        fix e::real assume "e > 0"
    20.5        with measure_LIMSEQ
    20.6        have "\<exists>no. \<forall>n\<ge>no. \<bar>(\<Sum>i<n. measure M (D i)) -measure M (\<Union>x. D x)\<bar> < e/2"
    20.7 -        by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1)
    20.8 +        by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1)
    20.9        hence "\<exists>n0. \<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>x. D x)\<bar> < e/2" by auto
   20.10        then obtain n0 where n0: "\<bar>(\<Sum>i<n0. measure M (D i)) - measure M (\<Union>i. D i)\<bar> < e/2"
   20.11          unfolding choice_iff by blast
    21.1 --- a/src/HOL/Real_Vector_Spaces.thy	Thu Apr 09 20:42:38 2015 +0200
    21.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Sat Apr 11 11:56:40 2015 +0100
    21.3 @@ -1544,19 +1544,19 @@
    21.4  
    21.5  subsubsection {* Limits of Sequences *}
    21.6  
    21.7 -lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    21.8 +lemma lim_sequentially: "X ----> (L::'a::metric_space) \<longleftrightarrow> (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. dist (X n) L < r)"
    21.9    unfolding tendsto_iff eventually_sequentially ..
   21.10  
   21.11  lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\<forall>r>0. \<exists>no>0. \<forall>n\<ge>no. dist (X n) L < r)"
   21.12 -  unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc)
   21.13 +  unfolding lim_sequentially by (metis Suc_leD zero_less_Suc)
   21.14  
   21.15  lemma metric_LIMSEQ_I:
   21.16    "(\<And>r. 0 < r \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r) \<Longrightarrow> X ----> (L::'a::metric_space)"
   21.17 -by (simp add: LIMSEQ_def)
   21.18 +by (simp add: lim_sequentially)
   21.19  
   21.20  lemma metric_LIMSEQ_D:
   21.21    "\<lbrakk>X ----> (L::'a::metric_space); 0 < r\<rbrakk> \<Longrightarrow> \<exists>no. \<forall>n\<ge>no. dist (X n) L < r"
   21.22 -by (simp add: LIMSEQ_def)
   21.23 +by (simp add: lim_sequentially)
   21.24  
   21.25  
   21.26  subsubsection {* Limits of Functions *}
   21.27 @@ -1823,7 +1823,7 @@
   21.28  proof (rule tendstoI)
   21.29    fix e :: real assume "0 < e"
   21.30    with limseq obtain N :: nat where N: "\<And>n. N \<le> n \<Longrightarrow> \<bar>f (real n) - y\<bar> < e"
   21.31 -    by (auto simp: LIMSEQ_def dist_real_def)
   21.32 +    by (auto simp: lim_sequentially dist_real_def)
   21.33    { fix x :: real
   21.34      obtain n where "x \<le> real_of_nat n"
   21.35        using ex_le_of_nat[of x] ..
    22.1 --- a/src/HOL/Set_Interval.thy	Thu Apr 09 20:42:38 2015 +0200
    22.2 +++ b/src/HOL/Set_Interval.thy	Sat Apr 11 11:56:40 2015 +0100
    22.3 @@ -1562,12 +1562,6 @@
    22.4       "(\<Sum>i\<le>n. (\<Sum>j<i. a i j)) = (\<Sum>j<n. \<Sum>i = Suc j..n. a i j)"
    22.5    by (induction n) (auto simp: setsum.distrib)
    22.6  
    22.7 -lemma setsum_zero_power [simp]:
    22.8 -  fixes c :: "nat \<Rightarrow> 'a::division_ring"
    22.9 -  shows "(\<Sum>i\<in>A. c i * 0^i) = (if finite A \<and> 0 \<in> A then c 0 else 0)"
   22.10 -apply (cases "finite A")
   22.11 -  by (induction A rule: finite_induct) auto
   22.12 -
   22.13  lemma setsum_zero_power' [simp]:
   22.14    fixes c :: "nat \<Rightarrow> 'a::field"
   22.15    shows "(\<Sum>i\<in>A. c i * 0^i / d i) = (if finite A \<and> 0 \<in> A then c 0 / d 0 else 0)"
    23.1 --- a/src/HOL/Transcendental.thy	Thu Apr 09 20:42:38 2015 +0200
    23.2 +++ b/src/HOL/Transcendental.thy	Sat Apr 11 11:56:40 2015 +0100
    23.3 @@ -1285,88 +1285,130 @@
    23.4  
    23.5  subsection {* Natural Logarithm *}
    23.6  
    23.7 -definition ln :: "real \<Rightarrow> real"
    23.8 -  where "ln x = (THE u. exp u = x)"
    23.9 -
   23.10 -lemma ln_exp [simp]: "ln (exp x) = x"
   23.11 -  by (simp add: ln_def)
   23.12 -
   23.13 -lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
   23.14 +class ln = real_normed_algebra_1 + banach +
   23.15 +  fixes ln :: "'a \<Rightarrow> 'a"
   23.16 +  assumes ln_one [simp]: "ln 1 = 0"
   23.17 +
   23.18 +definition powr :: "['a,'a] => 'a::ln"     (infixr "powr" 80)
   23.19 +  -- {*exponentation via ln and exp*}
   23.20 +  where "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
   23.21 +
   23.22 +
   23.23 +instantiation real :: ln
   23.24 +begin
   23.25 +
   23.26 +definition ln_real :: "real \<Rightarrow> real"
   23.27 +  where "ln_real x = (THE u. exp u = x)"
   23.28 +
   23.29 +instance 
   23.30 +by intro_classes (simp add: ln_real_def)
   23.31 +
   23.32 +end
   23.33 +
   23.34 +lemma powr_eq_0_iff [simp]: "w powr z = 0 \<longleftrightarrow> w = 0"
   23.35 +  by (simp add: powr_def)
   23.36 +
   23.37 +lemma ln_exp [simp]: 
   23.38 +  fixes x::real shows "ln (exp x) = x"
   23.39 +  by (simp add: ln_real_def)
   23.40 +
   23.41 +lemma exp_ln [simp]: 
   23.42 +  fixes x::real shows "0 < x \<Longrightarrow> exp (ln x) = x"
   23.43    by (auto dest: exp_total)
   23.44  
   23.45 -lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
   23.46 +lemma exp_ln_iff [simp]: 
   23.47 +  fixes x::real shows "exp (ln x) = x \<longleftrightarrow> 0 < x"
   23.48    by (metis exp_gt_zero exp_ln)
   23.49  
   23.50 -lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
   23.51 +lemma ln_unique: 
   23.52 +  fixes x::real shows "exp y = x \<Longrightarrow> ln x = y"
   23.53    by (erule subst, rule ln_exp)
   23.54  
   23.55 -lemma ln_one [simp]: "ln 1 = 0"
   23.56 -  by (rule ln_unique) simp
   23.57 -
   23.58 -lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   23.59 +lemma ln_mult:  
   23.60 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   23.61    by (rule ln_unique) (simp add: exp_add)
   23.62  
   23.63 -lemma ln_setprod:
   23.64 +lemma ln_setprod: 
   23.65 +  fixes f:: "'a => real" 
   23.66 +  shows
   23.67      "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> f i > 0\<rbrakk> \<Longrightarrow> ln(setprod f I) = setsum (\<lambda>x. ln(f x)) I"
   23.68    by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
   23.69  
   23.70 -lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   23.71 +lemma ln_inverse: 
   23.72 +  fixes x::real shows "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   23.73    by (rule ln_unique) (simp add: exp_minus)
   23.74  
   23.75 -lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
   23.76 +lemma ln_div: 
   23.77 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
   23.78    by (rule ln_unique) (simp add: exp_diff)
   23.79  
   23.80  lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   23.81    by (rule ln_unique) (simp add: exp_real_of_nat_mult)
   23.82  
   23.83 -lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   23.84 +lemma ln_less_cancel_iff [simp]: 
   23.85 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   23.86    by (subst exp_less_cancel_iff [symmetric]) simp
   23.87  
   23.88 -lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
   23.89 +lemma ln_le_cancel_iff [simp]: 
   23.90 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
   23.91    by (simp add: linorder_not_less [symmetric])
   23.92  
   23.93 -lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
   23.94 +lemma ln_inj_iff [simp]: 
   23.95 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
   23.96    by (simp add: order_eq_iff)
   23.97  
   23.98 -lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
   23.99 +lemma ln_add_one_self_le_self [simp]: 
  23.100 +  fixes x::real shows "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
  23.101    apply (rule exp_le_cancel_iff [THEN iffD1])
  23.102    apply (simp add: exp_ge_add_one_self_aux)
  23.103    done
  23.104  
  23.105 -lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
  23.106 +lemma ln_less_self [simp]: 
  23.107 +  fixes x::real shows "0 < x \<Longrightarrow> ln x < x"
  23.108    by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
  23.109  
  23.110 -lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  23.111 +lemma ln_ge_zero [simp]: 
  23.112 +  fixes x::real shows "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
  23.113    using ln_le_cancel_iff [of 1 x] by simp
  23.114  
  23.115 -lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  23.116 +lemma ln_ge_zero_imp_ge_one: 
  23.117 +  fixes x::real shows "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
  23.118    using ln_le_cancel_iff [of 1 x] by simp
  23.119  
  23.120 -lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  23.121 +lemma ln_ge_zero_iff [simp]: 
  23.122 +  fixes x::real shows "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
  23.123    using ln_le_cancel_iff [of 1 x] by simp
  23.124  
  23.125 -lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  23.126 +lemma ln_less_zero_iff [simp]: 
  23.127 +  fixes x::real shows "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
  23.128    using ln_less_cancel_iff [of x 1] by simp
  23.129  
  23.130 -lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
  23.131 +lemma ln_gt_zero: 
  23.132 +  fixes x::real shows "1 < x \<Longrightarrow> 0 < ln x"
  23.133    using ln_less_cancel_iff [of 1 x] by simp
  23.134  
  23.135 -lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  23.136 +lemma ln_gt_zero_imp_gt_one: 
  23.137 +  fixes x::real shows "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
  23.138    using ln_less_cancel_iff [of 1 x] by simp
  23.139  
  23.140 -lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  23.141 +lemma ln_gt_zero_iff [simp]: 
  23.142 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
  23.143    using ln_less_cancel_iff [of 1 x] by simp
  23.144  
  23.145 -lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  23.146 +lemma ln_eq_zero_iff [simp]: 
  23.147 +  fixes x::real shows "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
  23.148    using ln_inj_iff [of x 1] by simp
  23.149  
  23.150 -lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  23.151 +lemma ln_less_zero: 
  23.152 +  fixes x::real shows "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
  23.153    by simp
  23.154  
  23.155 -lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  23.156 -  by (auto simp add: ln_def intro!: arg_cong[where f=The])
  23.157 -
  23.158 -lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
  23.159 +lemma ln_neg_is_const: 
  23.160 +  fixes x::real shows "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
  23.161 +  by (auto simp add: ln_real_def intro!: arg_cong[where f=The])
  23.162 +
  23.163 +lemma isCont_ln: 
  23.164 +  fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
  23.165  proof cases
  23.166    assume "0 < x"
  23.167    moreover then have "isCont ln (exp (ln x))"
  23.168 @@ -1381,32 +1423,35 @@
  23.169                  intro!: exI[of _ "\<bar>x\<bar>"])
  23.170  qed
  23.171  
  23.172 -lemma tendsto_ln [tendsto_intros]:
  23.173 +lemma tendsto_ln [tendsto_intros]: 
  23.174 +  fixes a::real shows
  23.175    "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
  23.176    by (rule isCont_tendsto_compose [OF isCont_ln])
  23.177  
  23.178  lemma continuous_ln:
  23.179 -  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
  23.180 +  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x :: real))"
  23.181    unfolding continuous_def by (rule tendsto_ln)
  23.182  
  23.183  lemma isCont_ln' [continuous_intros]:
  23.184 -  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
  23.185 +  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x :: real))"
  23.186    unfolding continuous_at by (rule tendsto_ln)
  23.187  
  23.188  lemma continuous_within_ln [continuous_intros]:
  23.189 -  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
  23.190 +  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x :: real))"
  23.191    unfolding continuous_within by (rule tendsto_ln)
  23.192  
  23.193  lemma continuous_on_ln [continuous_intros]:
  23.194 -  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
  23.195 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x :: real))"
  23.196    unfolding continuous_on_def by (auto intro: tendsto_ln)
  23.197  
  23.198 -lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  23.199 +lemma DERIV_ln:
  23.200 +  fixes x::real shows "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
  23.201    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
  23.202    apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
  23.203    done
  23.204  
  23.205 -lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  23.206 +lemma DERIV_ln_divide:
  23.207 +  fixes x::real shows "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
  23.208    by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
  23.209  
  23.210  declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
  23.211 @@ -1533,13 +1578,13 @@
  23.212      unfolding power2_eq_square
  23.213      apply (rule mult_left_mono)
  23.214      using assms
  23.215 -    apply (auto simp: )
  23.216 +    apply auto
  23.217      done
  23.218    show ?thesis
  23.219      apply (rule order_trans [OF norm_exp])
  23.220      apply (rule order_trans [OF exp_bound])
  23.221      using assms n
  23.222 -    apply (auto simp: )
  23.223 +    apply auto
  23.224      done
  23.225  qed
  23.226  
  23.227 @@ -1549,7 +1594,8 @@
  23.228  using exp_bound_lemma [of x]
  23.229  by simp
  23.230  
  23.231 -lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  23.232 +lemma ln_one_minus_pos_upper_bound:
  23.233 +  fixes x::real shows "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
  23.234  proof -
  23.235    assume a: "0 <= (x::real)" and b: "x < 1"
  23.236    have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
  23.237 @@ -1590,7 +1636,8 @@
  23.238    apply auto
  23.239  done
  23.240  
  23.241 -lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  23.242 +lemma ln_one_plus_pos_lower_bound:
  23.243 +  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
  23.244  proof -
  23.245    assume a: "0 <= x" and b: "x <= 1"
  23.246    have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
  23.247 @@ -1614,7 +1661,8 @@
  23.248  qed
  23.249  
  23.250  lemma ln_one_minus_pos_lower_bound:
  23.251 -  "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  23.252 +  fixes x::real 
  23.253 +  shows "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
  23.254  proof -
  23.255    assume a: "0 <= x" and b: "x <= (1 / 2)"
  23.256    from b have c: "x < 1" by auto
  23.257 @@ -1642,14 +1690,15 @@
  23.258      by (rule order_trans)
  23.259  qed
  23.260  
  23.261 -lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  23.262 +lemma ln_add_one_self_le_self2:
  23.263 +  fixes x::real shows "-1 < x \<Longrightarrow> ln(1 + x) <= x"
  23.264    apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
  23.265    apply (subst ln_le_cancel_iff)
  23.266    apply auto
  23.267    done
  23.268  
  23.269  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
  23.270 -  "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  23.271 +  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
  23.272  proof -
  23.273    assume x: "0 <= x"
  23.274    assume x1: "x <= 1"
  23.275 @@ -1672,7 +1721,7 @@
  23.276  qed
  23.277  
  23.278  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
  23.279 -  "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  23.280 +  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  23.281  proof -
  23.282    assume a: "-(1 / 2) <= x"
  23.283    assume b: "x <= 0"
  23.284 @@ -1692,7 +1741,7 @@
  23.285  qed
  23.286  
  23.287  lemma abs_ln_one_plus_x_minus_x_bound:
  23.288 -    "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  23.289 +  fixes x::real shows "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
  23.290    apply (case_tac "0 <= x")
  23.291    apply (rule order_trans)
  23.292    apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
  23.293 @@ -1701,7 +1750,8 @@
  23.294    apply auto
  23.295    done
  23.296  
  23.297 -lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  23.298 +lemma ln_x_over_x_mono:
  23.299 +  fixes x::real shows "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
  23.300  proof -
  23.301    assume x: "exp 1 <= x" "x <= y"
  23.302    moreover have "0 < exp (1::real)" by simp
  23.303 @@ -1737,15 +1787,17 @@
  23.304    finally show ?thesis using b by (simp add: field_simps)
  23.305  qed
  23.306  
  23.307 -lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
  23.308 +lemma ln_le_minus_one:
  23.309 +  fixes x::real shows "0 < x \<Longrightarrow> ln x \<le> x - 1"
  23.310    using exp_ge_add_one_self[of "ln x"] by simp
  23.311  
  23.312  lemma ln_eq_minus_one:
  23.313 +  fixes x::real 
  23.314    assumes "0 < x" "ln x = x - 1"
  23.315    shows "x = 1"
  23.316  proof -
  23.317    let ?l = "\<lambda>y. ln y - y + 1"
  23.318 -  have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  23.319 +  have D: "\<And>x::real. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
  23.320      by (auto intro!: derivative_eq_intros)
  23.321  
  23.322    show ?thesis
  23.323 @@ -1814,11 +1866,11 @@
  23.324      by (simp add: Deriv.DERIV_iff2)
  23.325  qed
  23.326  
  23.327 -lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
  23.328 +lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot"
  23.329    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  23.330       (auto simp: eventually_at_filter)
  23.331  
  23.332 -lemma ln_at_top: "LIM x at_top. ln x :> at_top"
  23.333 +lemma ln_at_top: "LIM x at_top. ln (x::real) :> at_top"
  23.334    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
  23.335       (auto intro: eventually_gt_at_top)
  23.336  
  23.337 @@ -1846,10 +1898,6 @@
  23.338  qed
  23.339  
  23.340  
  23.341 -definition powr :: "[real,real] => real"  (infixr "powr" 80)
  23.342 -  -- {*exponentation with real exponent*}
  23.343 -  where "x powr a = exp(a * ln x)"
  23.344 -
  23.345  definition log :: "[real,real] => real"
  23.346    -- {*logarithm of @{term x} to base @{term a}*}
  23.347    where "log a x = ln x / ln a"
  23.348 @@ -1891,67 +1939,77 @@
  23.349  lemma powr_one_eq_one [simp]: "1 powr a = 1"
  23.350    by (simp add: powr_def)
  23.351  
  23.352 -lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
  23.353 +lemma powr_zero_eq_one [simp]: "x powr 0 = (if x=0 then 0 else 1)"
  23.354    by (simp add: powr_def)
  23.355  
  23.356 -lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
  23.357 -  by (simp add: powr_def)
  23.358 +lemma powr_one_gt_zero_iff [simp]:
  23.359 +  fixes x::real shows "(x powr 1 = x) = (0 \<le> x)"
  23.360 +  by (auto simp: powr_def)
  23.361  declare powr_one_gt_zero_iff [THEN iffD2, simp]
  23.362  
  23.363 -lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  23.364 +lemma powr_mult:
  23.365 +  fixes x::real shows "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
  23.366    by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
  23.367  
  23.368 -lemma powr_gt_zero [simp]: "0 < x powr a"
  23.369 +lemma powr_ge_pzero [simp]:
  23.370 +  fixes x::real shows "0 <= x powr y"
  23.371    by (simp add: powr_def)
  23.372  
  23.373 -lemma powr_ge_pzero [simp]: "0 <= x powr y"
  23.374 -  by (rule order_less_imp_le, rule powr_gt_zero)
  23.375 -
  23.376 -lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
  23.377 -  by (simp add: powr_def)
  23.378 -
  23.379 -lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  23.380 +lemma powr_divide:
  23.381 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
  23.382    apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
  23.383    apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
  23.384    done
  23.385  
  23.386 -lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
  23.387 +lemma powr_divide2:
  23.388 +  fixes x::real shows "x powr a / x powr b = x powr (a - b)"
  23.389    apply (simp add: powr_def)
  23.390    apply (subst exp_diff [THEN sym])
  23.391    apply (simp add: left_diff_distrib)
  23.392    done
  23.393  
  23.394 -lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
  23.395 +lemma powr_add:
  23.396 +  fixes x::real shows "x powr (a + b) = (x powr a) * (x powr b)"
  23.397    by (simp add: powr_def exp_add [symmetric] distrib_right)
  23.398  
  23.399 -lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  23.400 +lemma powr_mult_base:
  23.401 +  fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
  23.402    using assms by (auto simp: powr_add)
  23.403  
  23.404 -lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
  23.405 +lemma powr_powr:
  23.406 +  fixes x::real shows "(x powr a) powr b = x powr (a * b)"
  23.407    by (simp add: powr_def)
  23.408  
  23.409 -lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
  23.410 +lemma powr_powr_swap:
  23.411 +  fixes x::real shows "(x powr a) powr b = (x powr b) powr a"
  23.412    by (simp add: powr_powr mult.commute)
  23.413  
  23.414 -lemma powr_minus: "x powr (-a) = inverse (x powr a)"
  23.415 +lemma powr_minus:
  23.416 +  fixes x::real shows "x powr (-a) = inverse (x powr a)"
  23.417    by (simp add: powr_def exp_minus [symmetric])
  23.418  
  23.419 -lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
  23.420 +lemma powr_minus_divide:
  23.421 +  fixes x::real shows "x powr (-a) = 1/(x powr a)"
  23.422    by (simp add: divide_inverse powr_minus)
  23.423  
  23.424 -lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
  23.425 +lemma divide_powr_uminus:
  23.426 +  fixes a::real shows "a / b powr c = a * b powr (- c)"
  23.427    by (simp add: powr_minus_divide)
  23.428  
  23.429 -lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  23.430 +lemma powr_less_mono:
  23.431 +  fixes x::real shows "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
  23.432    by (simp add: powr_def)
  23.433  
  23.434 -lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  23.435 +lemma powr_less_cancel:
  23.436 +  fixes x::real shows "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
  23.437    by (simp add: powr_def)
  23.438  
  23.439 -lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  23.440 +lemma powr_less_cancel_iff [simp]:
  23.441 +  fixes x::real shows "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
  23.442    by (blast intro: powr_less_cancel powr_less_mono)
  23.443  
  23.444 -lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  23.445 +lemma powr_le_cancel_iff [simp]:
  23.446 +  fixes x::real shows "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
  23.447    by (simp add: linorder_not_less [symmetric])
  23.448  
  23.449  lemma log_ln: "ln x = log (exp(1)) x"
  23.450 @@ -2007,6 +2065,9 @@
  23.451  lemma log_divide: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> log a (x/y) = log a x - log a y"
  23.452    by (simp add: log_mult divide_inverse log_inverse)
  23.453  
  23.454 +lemma powr_gt_zero [simp]: "0 < x powr a \<longleftrightarrow> (x::real) \<noteq> 0"
  23.455 +  by (simp add: powr_def)
  23.456 +
  23.457  lemma log_add_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x + y = log b (x * b powr y)"
  23.458    and add_log_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> y + log b x = log b (b powr y * x)"
  23.459    and log_minus_eq_powr: "0 < b \<Longrightarrow> b \<noteq> 1 \<Longrightarrow> 0 < x \<Longrightarrow> log b x - y = log b (x * b powr -y)"
  23.460 @@ -2071,14 +2132,18 @@
  23.461  
  23.462  lemma le_log_iff:
  23.463    assumes "1 < b" "x > 0"
  23.464 -  shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> x"
  23.465 -  by (metis assms(1) assms(2) dual_order.strict_trans powr_le_cancel_iff powr_log_cancel
  23.466 -    powr_one_eq_one powr_one_gt_zero_iff)
  23.467 +  shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> (x::real)"
  23.468 +  using assms 
  23.469 +  apply auto
  23.470 +  apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff
  23.471 +               powr_log_cancel zero_less_one)
  23.472 +  apply (metis not_less order.trans order_refl powr_le_cancel_iff powr_log_cancel zero_le_one)
  23.473 +  done
  23.474  
  23.475  lemma less_log_iff:
  23.476    assumes "1 < b" "x > 0"
  23.477    shows "y < log b x \<longleftrightarrow> b powr y < x"
  23.478 -  by (metis assms(1) assms(2) dual_order.strict_trans less_irrefl powr_less_cancel_iff
  23.479 +  by (metis assms dual_order.strict_trans less_irrefl powr_less_cancel_iff
  23.480      powr_log_cancel zero_less_one)
  23.481  
  23.482  lemma
  23.483 @@ -2136,22 +2201,28 @@
  23.484      else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
  23.485    by (auto simp: powr_int)
  23.486  
  23.487 -lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
  23.488 -  using powr_realpow [of x 1] by simp
  23.489 -
  23.490 -lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  23.491 +lemma powr_one:
  23.492 +  fixes x::real shows "0 \<le> x \<Longrightarrow> x powr 1 = x"
  23.493 +  using powr_realpow [of x 1]
  23.494 +  by simp
  23.495 +
  23.496 +lemma powr_numeral:
  23.497 +  fixes x::real shows "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
  23.498    by (fact powr_realpow_numeral)
  23.499  
  23.500 -lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  23.501 +lemma powr_neg_one:
  23.502 +  fixes x::real shows "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
  23.503    using powr_int [of x "- 1"] by simp
  23.504  
  23.505 -lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  23.506 +lemma powr_neg_numeral:
  23.507 +  fixes x::real shows "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
  23.508    using powr_int [of x "- numeral n"] by simp
  23.509  
  23.510  lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
  23.511    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
  23.512  
  23.513 -lemma ln_powr: "ln (x powr y) = y * ln x"
  23.514 +lemma ln_powr:
  23.515 +  fixes x::real shows "x \<noteq> 0 \<Longrightarrow> ln (x powr y) = y * ln x"
  23.516    by (simp add: powr_def)
  23.517  
  23.518  lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
  23.519 @@ -2163,7 +2234,7 @@
  23.520  lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
  23.521  by(simp add: log_def ln_root)
  23.522  
  23.523 -lemma log_powr: "log b (x powr y) = y * log b x"
  23.524 +lemma log_powr: "x \<noteq> 0 \<Longrightarrow> log b (x powr y) = y * log b x"
  23.525    by (simp add: log_def ln_powr)
  23.526  
  23.527  lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
  23.528 @@ -2175,65 +2246,58 @@
  23.529  lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
  23.530    by (simp add: log_def ln_realpow)
  23.531  
  23.532 -lemma log_base_powr: "log (a powr b) x = log a x / b"
  23.533 +lemma log_base_powr: "a \<noteq> 0 \<Longrightarrow> log (a powr b) x = log a x / b"
  23.534    by (simp add: log_def ln_powr)
  23.535  
  23.536  lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
  23.537  by(simp add: log_def ln_root)
  23.538  
  23.539 -lemma ln_bound: "1 <= x ==> ln x <= x"
  23.540 +lemma ln_bound:
  23.541 +  fixes x::real shows "1 <= x ==> ln x <= x"
  23.542    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
  23.543    apply simp
  23.544    apply (rule ln_add_one_self_le_self, simp)
  23.545    done
  23.546  
  23.547 -lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  23.548 +lemma powr_mono:
  23.549 +  fixes x::real shows "a <= b ==> 1 <= x ==> x powr a <= x powr b"
  23.550    apply (cases "x = 1", simp)
  23.551    apply (cases "a = b", simp)
  23.552    apply (rule order_less_imp_le)
  23.553    apply (rule powr_less_mono, auto)
  23.554    done
  23.555  
  23.556 -lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  23.557 -  apply (subst powr_zero_eq_one [THEN sym])
  23.558 -  apply (rule powr_mono, assumption+)
  23.559 -  done
  23.560 -
  23.561 -lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  23.562 -  apply (unfold powr_def)
  23.563 -  apply (rule exp_less_mono)
  23.564 -  apply (rule mult_strict_left_mono)
  23.565 -  apply (subst ln_less_cancel_iff, assumption)
  23.566 -  apply (rule order_less_trans)
  23.567 -  prefer 2
  23.568 -  apply assumption+
  23.569 -  done
  23.570 -
  23.571 -lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  23.572 -  apply (unfold powr_def)
  23.573 -  apply (rule exp_less_mono)
  23.574 -  apply (rule mult_strict_left_mono_neg)
  23.575 -  apply (subst ln_less_cancel_iff)
  23.576 -  apply assumption
  23.577 -  apply (rule order_less_trans)
  23.578 -  prefer 2
  23.579 -  apply assumption+
  23.580 -  done
  23.581 -
  23.582 -lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  23.583 +lemma ge_one_powr_ge_zero:
  23.584 +  fixes x::real shows "1 <= x ==> 0 <= a ==> 1 <= x powr a"
  23.585 +using powr_mono by fastforce
  23.586 +
  23.587 +lemma powr_less_mono2:
  23.588 +  fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
  23.589 +  by (simp add: powr_def)
  23.590 +
  23.591 +
  23.592 +lemma powr_less_mono2_neg:
  23.593 +  fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
  23.594 +  by (simp add: powr_def)
  23.595 +
  23.596 +lemma powr_mono2:
  23.597 +  fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
  23.598    apply (case_tac "a = 0", simp)
  23.599    apply (case_tac "x = y", simp)
  23.600    apply (metis less_eq_real_def powr_less_mono2)
  23.601    done
  23.602  
  23.603 -lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  23.604 +lemma powr_inj:
  23.605 +  fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
  23.606    unfolding powr_def exp_inj_iff by simp
  23.607  
  23.608 -lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  23.609 -  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
  23.610 -            powr_gt_zero)
  23.611 +lemma ln_powr_bound:
  23.612 +  fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
  23.613 +by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero)
  23.614 +
  23.615  
  23.616  lemma ln_powr_bound2:
  23.617 +  fixes x::real
  23.618    assumes "1 < x" and "0 < a"
  23.619    shows "(ln x) powr a <= (a powr a) * x"
  23.620  proof -
  23.621 @@ -2244,7 +2308,7 @@
  23.622    finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
  23.623      by (metis assms less_imp_le ln_gt_zero powr_mono2)
  23.624    also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
  23.625 -    by (metis assms(2) powr_mult powr_gt_zero)
  23.626 +    using assms powr_mult by auto
  23.627    also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
  23.628      by (rule powr_powr)
  23.629    also have "... = x" using assms
  23.630 @@ -2252,37 +2316,56 @@
  23.631    finally show ?thesis .
  23.632  qed
  23.633  
  23.634 -lemma tendsto_powr [tendsto_intros]:
  23.635 -  "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  23.636 -  unfolding powr_def by (intro tendsto_intros)
  23.637 +lemma tendsto_powr [tendsto_intros]:  (*FIXME a mess, suggests a general rule about exceptions*)
  23.638 +  fixes a::real 
  23.639 +  shows "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
  23.640 +  apply (simp add: powr_def)
  23.641 +  apply (simp add: tendsto_def)
  23.642 +  apply (simp add: Topological_Spaces.eventually_conj_iff )
  23.643 +  apply safe
  23.644 +  apply (case_tac "0 \<in> S")
  23.645 +  apply (auto simp: )
  23.646 +  apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T")
  23.647 +  apply clarify
  23.648 +  apply (drule_tac x="T" in spec)
  23.649 +  apply (simp add: )
  23.650 +  apply (metis (mono_tags, lifting) eventually_mono)
  23.651 +  apply (simp add: separation_t1)
  23.652 +  apply (subgoal_tac "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F")
  23.653 +  apply (simp add: tendsto_def)
  23.654 +  apply (metis (mono_tags, lifting) eventually_mono)
  23.655 +  apply (simp add: tendsto_def [symmetric])
  23.656 +  apply (intro tendsto_intros)
  23.657 +  apply (auto simp: )
  23.658 +  done
  23.659  
  23.660  lemma continuous_powr:
  23.661    assumes "continuous F f"
  23.662      and "continuous F g"
  23.663      and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
  23.664 -  shows "continuous F (\<lambda>x. (f x) powr (g x))"
  23.665 +  shows "continuous F (\<lambda>x. (f x) powr (g x :: real))"
  23.666    using assms unfolding continuous_def by (rule tendsto_powr)
  23.667  
  23.668  lemma continuous_at_within_powr[continuous_intros]:
  23.669    assumes "continuous (at a within s) f"
  23.670      and "continuous (at a within s) g"
  23.671      and "f a \<noteq> 0"
  23.672 -  shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
  23.673 +  shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x :: real))"
  23.674    using assms unfolding continuous_within by (rule tendsto_powr)
  23.675  
  23.676  lemma isCont_powr[continuous_intros, simp]:
  23.677 -  assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
  23.678 +  assumes "isCont f a" "isCont g a" "f a \<noteq> (0::real)"
  23.679    shows "isCont (\<lambda>x. (f x) powr g x) a"
  23.680    using assms unfolding continuous_at by (rule tendsto_powr)
  23.681  
  23.682  lemma continuous_on_powr[continuous_intros]:
  23.683 -  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
  23.684 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> (0::real)"
  23.685    shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
  23.686    using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
  23.687  
  23.688  (* FIXME: generalize by replacing d by with g x and g ---> d? *)
  23.689  lemma tendsto_zero_powrI:
  23.690 -  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
  23.691 +  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> (0::real)) F"
  23.692      and "0 < d"
  23.693    shows "((\<lambda>x. f x powr d) ---> 0) F"
  23.694  proof (rule tendstoI)
  23.695 @@ -2303,14 +2386,17 @@
  23.696  lemma tendsto_neg_powr:
  23.697    assumes "s < 0"
  23.698      and "LIM x F. f x :> at_top"
  23.699 -  shows "((\<lambda>x. f x powr s) ---> 0) F"
  23.700 +  shows "((\<lambda>x. f x powr s) ---> (0::real)) F"
  23.701  proof (rule tendstoI)
  23.702    fix e :: real assume "0 < e"
  23.703    def Z \<equiv> "e powr (1 / s)"
  23.704 +  have "Z > 0"
  23.705 +    using Z_def `0 < e` by auto
  23.706    from assms have "eventually (\<lambda>x. Z < f x) F"
  23.707      by (simp add: filterlim_at_top_dense)
  23.708    moreover
  23.709 -  from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
  23.710 +  from assms have "\<And>x::real. Z < x \<Longrightarrow> x powr s < Z powr s"
  23.711 +    using `Z > 0`
  23.712      by (auto simp: Z_def intro!: powr_less_mono2_neg)
  23.713    with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
  23.714      by (simp add: powr_powr Z_def dist_real_def)
  23.715 @@ -2318,13 +2404,11 @@
  23.716    show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
  23.717  qed
  23.718  
  23.719 -(* it is funny that this isn't in the library! It could go in Transcendental *)
  23.720  lemma tendsto_exp_limit_at_right:
  23.721    fixes x :: real
  23.722    shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
  23.723  proof cases
  23.724    assume "x \<noteq> 0"
  23.725 -
  23.726    have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
  23.727      by (auto intro!: derivative_eq_intros)
  23.728    then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
  23.729 @@ -2335,7 +2419,10 @@
  23.730    proof (rule filterlim_mono_eventually)
  23.731      show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
  23.732        unfolding eventually_at_right[OF zero_less_one]
  23.733 -      using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
  23.734 +      using `x \<noteq> 0`
  23.735 +      apply  (intro exI[of _ "1 / \<bar>x\<bar>"])
  23.736 +      apply (auto simp: field_simps powr_def abs_if)
  23.737 +      by (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one)
  23.738    qed (simp_all add: at_eq_sup_left_right)
  23.739  qed simp
  23.740  
  23.741 @@ -4445,7 +4532,7 @@
  23.742  lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
  23.743    apply (rule trans [OF sin_mono_less_eq [symmetric]])
  23.744    using arcsin_ubound arcsin_lbound
  23.745 -  apply (auto simp: )
  23.746 +  apply auto
  23.747    done
  23.748  
  23.749  lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
  23.750 @@ -4460,7 +4547,7 @@
  23.751  lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
  23.752    apply (rule trans [OF cos_mono_less_eq [symmetric]])
  23.753    using arccos_ubound arccos_lbound
  23.754 -  apply (auto simp: )
  23.755 +  apply auto
  23.756    done
  23.757  
  23.758  lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
  23.759 @@ -5009,4 +5096,253 @@
  23.760    qed
  23.761  qed
  23.762  
  23.763 +
  23.764 +subsection{*Basics about polynomial functions: extremal behaviour and root counts*}
  23.765 +(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*)
  23.766 +
  23.767 +lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)
  23.768 +    fixes x :: "'a::idom"
  23.769 +  assumes "1 \<le> n"
  23.770 +    shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
  23.771 +           (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
  23.772 +proof -
  23.773 +  have h: "bij_betw (\<lambda>(i,j). (j,i)) ((SIGMA i : atMost n. lessThan i)) (SIGMA j : lessThan n. {Suc j..n})"
  23.774 +    by (auto simp: bij_betw_def inj_on_def)
  23.775 +  have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
  23.776 +        (\<Sum>i\<le>n. a i * (x^i - y^i))"
  23.777 +    by (simp add: right_diff_distrib setsum_subtractf)
  23.778 +  also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
  23.779 +    by (simp add: power_diff_sumr2 mult.assoc)
  23.780 +  also have "... = (\<Sum>i\<le>n. \<Sum>j<i. a i * (x - y) * (y^(i - Suc j) * x^j))"
  23.781 +    by (simp add: setsum_right_distrib)
  23.782 +  also have "... = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
  23.783 +    by (simp add: setsum.Sigma)
  23.784 +  also have "... = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
  23.785 +    by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong)
  23.786 +  also have "... = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
  23.787 +    by (simp add: setsum.Sigma)
  23.788 +  also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
  23.789 +    by (simp add: setsum_right_distrib mult_ac)
  23.790 +  finally show ?thesis .
  23.791 +qed
  23.792 +
  23.793 +lemma polyfun_diff_alt: (*COMPLEX_SUB_POLYFUN_ALT in HOL Light*)
  23.794 +    fixes x :: "'a::idom"
  23.795 +  assumes "1 \<le> n"
  23.796 +    shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
  23.797 +           (x - y) * ((\<Sum>j<n. \<Sum>k<n-j. a(j+k+1) * y^k * x^j))"
  23.798 +proof -
  23.799 +  { fix j::nat
  23.800 +    assume "j<n"
  23.801 +    have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
  23.802 +      apply (auto simp: bij_betw_def inj_on_def)
  23.803 +      apply (rule_tac x="x + Suc j" in image_eqI)
  23.804 +      apply (auto simp: )
  23.805 +      done
  23.806 +    have "(\<Sum>i=Suc j..n. a i * y^(i - j - 1)) = (\<Sum>k<n-j. a(j+k+1) * y^k)"
  23.807 +      by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong)
  23.808 +  }
  23.809 +  then show ?thesis
  23.810 +    by (simp add: polyfun_diff [OF assms] setsum_left_distrib)
  23.811 +qed
  23.812 +
  23.813 +lemma polyfun_linear_factor:  (*COMPLEX_POLYFUN_LINEAR_FACTOR in HOL Light*)
  23.814 +  fixes a :: "'a::idom"
  23.815 +  shows "\<exists>b. \<forall>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i) + (\<Sum>i\<le>n. c(i) * a^i)"
  23.816 +proof (cases "n=0")
  23.817 +  case True then show ?thesis
  23.818 +    by simp
  23.819 +next
  23.820 +  case False
  23.821 +  have "(\<exists>b. \<forall>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i) + (\<Sum>i\<le>n. c(i) * a^i)) =
  23.822 +        (\<exists>b. \<forall>z. (\<Sum>i\<le>n. c(i) * z^i) - (\<Sum>i\<le>n. c(i) * a^i) = (z - a) * (\<Sum>i<n. b(i) * z^i))"
  23.823 +    by (simp add: algebra_simps)
  23.824 +  also have "... = (\<exists>b. \<forall>z. (z - a) * (\<Sum>j<n. (\<Sum>i = Suc j..n. c i * a^(i - Suc j)) * z^j) = (z - a) * (\<Sum>i<n. b(i) * z^i))"
  23.825 +    using False by (simp add: polyfun_diff)
  23.826 +  also have "... = True"
  23.827 +    by auto
  23.828 +  finally show ?thesis
  23.829 +    by simp
  23.830 +qed
  23.831 +
  23.832 +lemma polyfun_linear_factor_root:  (*COMPLEX_POLYFUN_LINEAR_FACTOR_ROOT in HOL Light*)
  23.833 +  fixes a :: "'a::idom"
  23.834 +  assumes "(\<Sum>i\<le>n. c(i) * a^i) = 0"
  23.835 +  obtains b where "\<And>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i)"
  23.836 +  using polyfun_linear_factor [of c n a] assms
  23.837 +  by auto
  23.838 +
  23.839 +lemma isCont_polynom:
  23.840 +  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
  23.841 +  shows "isCont (\<lambda>w. \<Sum>i\<le>n. c i * w^i) a"
  23.842 +  by simp
  23.843 +
  23.844 +lemma zero_polynom_imp_zero_coeffs:
  23.845 +    fixes c :: "nat \<Rightarrow> 'a::{ab_semigroup_mult,real_normed_div_algebra}"
  23.846 +  assumes "\<And>w. (\<Sum>i\<le>n. c i * w^i) = 0"  "k \<le> n"
  23.847 +    shows "c k = 0"
  23.848 +using assms
  23.849 +proof (induction n arbitrary: c k)
  23.850 +  case 0
  23.851 +  then show ?case
  23.852 +    by simp
  23.853 +next
  23.854 +  case (Suc n c k)
  23.855 +  have [simp]: "c 0 = 0" using Suc.prems(1) [of 0]
  23.856 +    by simp
  23.857 +  { fix w
  23.858 +    have "(\<Sum>i\<le>Suc n. c i * w^i) = (\<Sum>i\<le>n. c (Suc i) * w ^ Suc i)"
  23.859 +      unfolding Set_Interval.setsum_atMost_Suc_shift
  23.860 +      by simp
  23.861 +    also have "... = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
  23.862 +      by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc)
  23.863 +    finally have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" .
  23.864 +  }
  23.865 +  then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
  23.866 +    using Suc  by auto
  23.867 +  then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
  23.868 +    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity}*}
  23.869 +  then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
  23.870 +    using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
  23.871 +    by (force simp add: Limits.isCont_iff)
  23.872 +  then have "\<And>w. (\<Sum>i\<le>n. c (Suc i) * w^i) = 0" using wnz
  23.873 +    by metis
  23.874 +  then have "\<And>i. i\<le>n \<Longrightarrow> c (Suc i) = 0"
  23.875 +    using Suc.IH [of "\<lambda>i. c (Suc i)"]
  23.876 +    by blast
  23.877 +  then show ?case using `k \<le> Suc n`
  23.878 +    by (cases k) auto
  23.879 +qed
  23.880 +
  23.881 +lemma polyfun_rootbound: (*COMPLEX_POLYFUN_ROOTBOUND in HOL Light*)
  23.882 +    fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
  23.883 +  assumes "c k \<noteq> 0" "k\<le>n"
  23.884 +    shows "finite {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<and>
  23.885 +             card {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<le> n"
  23.886 +using assms
  23.887 +proof (induction n arbitrary: c k)
  23.888 +  case 0
  23.889 +  then show ?case
  23.890 +    by simp
  23.891 +next
  23.892 +  case (Suc m c k)
  23.893 +  let ?succase = ?case
  23.894 +  show ?case
  23.895 +  proof (cases "{z. (\<Sum>i\<le>Suc m. c(i) * z^i) = 0} = {}")
  23.896 +    case True
  23.897 +    then show ?succase
  23.898 +      by simp
  23.899 +  next
  23.900 +    case False
  23.901 +    then obtain z0 where z0: "(\<Sum>i\<le>Suc m. c(i) * z0^i) = 0"
  23.902 +      by blast
  23.903 +    then obtain b where b: "\<And>w. (\<Sum>i\<le>Suc m. c i * w^i) = (w - z0) * (\<Sum>i\<le>m. b i * w^i)"
  23.904 +      using polyfun_linear_factor_root [OF z0, unfolded lessThan_Suc_atMost]
  23.905 +      by blast
  23.906 +    then have eq: "{z. (\<Sum>i\<le>Suc m. c(i) * z^i) = 0} = insert z0 {z. (\<Sum>i\<le>m. b(i) * z^i) = 0}"
  23.907 +      by auto
  23.908 +    have "~(\<forall>k\<le>m. b k = 0)"
  23.909 +    proof
  23.910 +      assume [simp]: "\<forall>k\<le>m. b k = 0"
  23.911 +      then have "\<And>w. (\<Sum>i\<le>m. b i * w^i) = 0"
  23.912 +        by simp
  23.913 +      then have "\<And>w. (\<Sum>i\<le>Suc m. c i * w^i) = 0"
  23.914 +        using b by simp
  23.915 +      then have "\<And>k. k \<le> Suc m \<Longrightarrow> c k = 0"
  23.916 +        using zero_polynom_imp_zero_coeffs
  23.917 +        by blast
  23.918 +      then show False using Suc.prems
  23.919 +        by blast
  23.920 +    qed
  23.921 +    then obtain k' where bk': "b k' \<noteq> 0" "k' \<le> m"
  23.922 +      by blast
  23.923 +    show ?succase
  23.924 +      using Suc.IH [of b k'] bk'
  23.925 +      by (simp add: eq card_insert_if del: setsum_atMost_Suc)
  23.926 +    qed
  23.927 +qed
  23.928 +
  23.929 +lemma
  23.930 +    fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
  23.931 +  assumes "c k \<noteq> 0" "k\<le>n"
  23.932 +    shows polyfun_roots_finite: "finite {z. (\<Sum>i\<le>n. c(i) * z^i) = 0}"
  23.933 +      and polyfun_roots_card:   "card {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<le> n"
  23.934 +using polyfun_rootbound assms
  23.935 +  by auto
  23.936 +
  23.937 +lemma polyfun_finite_roots: (*COMPLEX_POLYFUN_FINITE_ROOTS in HOL Light*)
  23.938 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
  23.939 +  shows "finite {x. (\<Sum>i\<le>n. c i * x^i) = 0} \<longleftrightarrow> (\<exists>i\<le>n. c i \<noteq> 0)"
  23.940 +        (is "?lhs = ?rhs")
  23.941 +proof
  23.942 +  assume ?lhs
  23.943 +  moreover
  23.944 +  { assume "\<forall>i\<le>n. c i = 0"
  23.945 +    then have "\<And>x. (\<Sum>i\<le>n. c i * x^i) = 0"
  23.946 +      by simp
  23.947 +    then have "\<not> finite {x. (\<Sum>i\<le>n. c i * x^i) = 0}"
  23.948 +      using ex_new_if_finite [OF infinite_UNIV_char_0 [where 'a='a]]
  23.949 +      by auto
  23.950 +  }
  23.951 +  ultimately show ?rhs
  23.952 +  by metis
  23.953 +next
  23.954 +  assume ?rhs
  23.955 +  then show ?lhs
  23.956 +    using polyfun_rootbound
  23.957 +    by blast
  23.958 +qed
  23.959 +
  23.960 +lemma polyfun_eq_0: (*COMPLEX_POLYFUN_EQ_0 in HOL Light*)
  23.961 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
  23.962 +  shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = 0) \<longleftrightarrow> (\<forall>i\<le>n. c i = 0)"
  23.963 +  using zero_polynom_imp_zero_coeffs by auto
  23.964 +
  23.965 +lemma polyfun_eq_coeffs:
  23.966 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
  23.967 +  shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = (\<Sum>i\<le>n. d i * x^i)) \<longleftrightarrow> (\<forall>i\<le>n. c i = d i)"
  23.968 +proof -
  23.969 +  have "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = (\<Sum>i\<le>n. d i * x^i)) \<longleftrightarrow> (\<forall>x. (\<Sum>i\<le>n. (c i - d i) * x^i) = 0)"
  23.970 +    by (simp add: left_diff_distrib Groups_Big.setsum_subtractf)
  23.971 +  also have "... \<longleftrightarrow> (\<forall>i\<le>n. c i - d i = 0)"
  23.972 +    by (rule polyfun_eq_0)
  23.973 +  finally show ?thesis
  23.974 +    by simp
  23.975 +qed
  23.976 +
  23.977 +lemma polyfun_eq_const: (*COMPLEX_POLYFUN_EQ_CONST in HOL Light*)
  23.978 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
  23.979 +  shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = k) \<longleftrightarrow> c 0 = k \<and> (\<forall>i \<in> {1..n}. c i = 0)"
  23.980 +        (is "?lhs = ?rhs")
  23.981 +proof -
  23.982 +  have *: "\<forall>x. (\<Sum>i\<le>n. (if i=0 then k else 0) * x^i) = k"
  23.983 +    by (induct n) auto
  23.984 +  show ?thesis
  23.985 +  proof
  23.986 +    assume ?lhs
  23.987 +    with * have "(\<forall>i\<le>n. c i = (if i=0 then k else 0))"
  23.988 +      by (simp add: polyfun_eq_coeffs [symmetric])
  23.989 +    then show ?rhs
  23.990 +      by simp
  23.991 +  next
  23.992 +    assume ?rhs then show ?lhs
  23.993 +      by (induct n) auto
  23.994 +  qed
  23.995 +qed
  23.996 +
  23.997 +lemma root_polyfun:
  23.998 +  fixes z:: "'a::idom"
  23.999 +  assumes "1 \<le> n"
 23.1000 +    shows "z^n = a \<longleftrightarrow> (\<Sum>i\<le>n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0"
 23.1001 +  using assms
 23.1002 +  by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric])
 23.1003 +
 23.1004 +lemma
 23.1005 +    fixes zz :: "'a::{idom,real_normed_div_algebra}"
 23.1006 +  assumes "1 \<le> n"
 23.1007 +    shows finite_roots_unity: "finite {z::'a. z^n = 1}"
 23.1008 +      and card_roots_unity:   "card {z::'a. z^n = 1} \<le> n"
 23.1009 +  using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms
 23.1010 +  by (auto simp add: root_polyfun [OF assms])
 23.1011 +
 23.1012  end