# HG changeset patch # User paulson # Date 1428749800 -3600 # Node ID b785d6d064305efd9bbc5af955897cc7bc96b81d # Parent 09be0495dcc2015aea497ca978d59bbd1e672822 Overloading of ln and powr, but "approximation" no longer works for powr. Code generation also fails due to type ambiguity in scala. diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Complex.thy --- a/src/HOL/Complex.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Complex.thy Sat Apr 11 11:56:40 2015 +0100 @@ -167,6 +167,10 @@ lemma Im_divide_numeral [simp]: "Im (z / numeral w) = Im z / numeral w" by (simp add: Im_divide sqr_conv_mult) +lemma of_real_Re [simp]: + "z \ \ \ of_real (Re z) = z" + by (auto simp: Reals_def) + subsection {* The Complex Number $i$ *} primcorec "ii" :: complex ("\") where diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Apr 11 11:56:40 2015 +0100 @@ -241,7 +241,9 @@ show ?case proof (cases x) case (Float m e) - hence "0 < m" using assms powr_gt_zero[of 2 e] by (auto simp: sign_simps) + hence "0 < m" using assms + apply (auto simp: sign_simps) + by (meson not_less powr_ge_pzero) hence "0 < sqrt m" by auto have int_nat_bl: "(nat (bitlen m)) = bitlen m" using bitlen_nonneg by auto @@ -1858,7 +1860,8 @@ finally show "?ln \ ?ub" . qed -lemma ln_add: assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)" +lemma ln_add: + fixes x::real assumes "0 < x" and "0 < y" shows "ln (x + y) = ln x + ln (1 + y / x)" proof - have "x \ 0" using assms by auto have "x + y = x * (1 + y / x)" unfolding distrib_left times_divide_eq_right nonzero_mult_divide_cancel_left[OF `x \ 0`] by auto @@ -1885,7 +1888,7 @@ let ?uthird = "rapprox_rat (max prec 1) 1 3" let ?lthird = "lapprox_rat prec 1 3" - have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1)" + have ln2_sum: "ln 2 = ln (1/2 + 1) + ln (1 / 3 + 1::real)" using ln_add[of "3 / 2" "1 / 2"] by auto have lb3: "?lthird \ 1 / 3" using lapprox_rat[of prec 1 3] by auto hence lb3_ub: "real ?lthird < 1" by auto @@ -1955,10 +1958,8 @@ lemma float_pos_eq_mantissa_pos: "x > 0 \ mantissa x > 0" apply (subst Float_mantissa_exponent[of x, symmetric]) - apply (auto simp add: zero_less_mult_iff zero_float_def powr_gt_zero[of 2 "exponent x"] dest: less_zeroE) - using powr_gt_zero[of 2 "exponent x"] - apply simp - done + apply (auto simp add: zero_less_mult_iff zero_float_def dest: less_zeroE) + by (metis not_le powr_ge_pzero) lemma Float_pos_eq_mantissa_pos: "Float m e > 0 \ m > 0" using powr_gt_zero[of 2 "e"] @@ -2140,8 +2141,9 @@ let ?s = "Float (e + (bitlen m - 1)) 0" let ?x = "Float m (- (bitlen m - 1))" - have "0 < m" and "m \ 0" using `0 < x` Float powr_gt_zero[of 2 e] - by (auto simp: zero_less_mult_iff) + have "0 < m" and "m \ 0" using `0 < x` Float powr_gt_zero[of 2 e] + apply (auto simp add: zero_less_mult_iff) + using not_le powr_ge_pzero by blast def bl \ "bitlen m - 1" hence "bl \ 0" using `m > 0` by (simp add: bitlen_def) have "1 \ Float m e" using `1 \ x` Float unfolding less_eq_float_def by auto from bitlen_div[OF `0 < m`] float_gt1_scale[OF `1 \ Float m e`] `bl \ 0` @@ -2180,7 +2182,7 @@ from float_gt1_scale[OF `1 \ Float m e`] show "0 \ real (e + (bitlen m - 1))" by auto next - have "0 \ ln 2" by simp + have "0 \ ln (2 :: real)" by simp thus "0 \ real (ub_ln2 prec)" using ub_ln2[of prec] by arith qed auto ultimately have "ln x \ float_plus_up prec ?ub2 ?ub_horner" @@ -2333,10 +2335,9 @@ unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse by auto -lemma interpret_floatarith_powr: "interpret_floatarith (Exp (Mult b (Ln a))) vs = (interpret_floatarith a vs) powr (interpret_floatarith b vs)" - unfolding powr_def interpret_floatarith.simps .. - -lemma interpret_floatarith_log: "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = log (interpret_floatarith b vs) (interpret_floatarith x vs)" +lemma interpret_floatarith_log: + "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = + log (interpret_floatarith b vs) (interpret_floatarith x vs)" unfolding log_def interpret_floatarith.simps divide_inverse .. lemma interpret_floatarith_num: @@ -3481,7 +3482,7 @@ subsection {* Implement proof method \texttt{approximation} *} lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num - interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_powr interpret_floatarith_log + interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log interpret_floatarith_sin oracle approximation_oracle = {* fn (thy, t) => diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Sat Apr 11 11:56:40 2015 +0100 @@ -35,7 +35,7 @@ section "Compute some transcendental values" -lemma "\ ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \ < inverse (2^51) " +lemma "\ ln 2 - 544531980202654583340825686620847 / 785593587443817081832229725798400 \ < (inverse (2^51) :: real)" by (approximation 60) lemma "\ exp 1.626 - 5.083499996273 \ < (inverse 10 ^ 10 :: real)" diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy --- a/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy Sat Apr 11 11:56:40 2015 +0100 @@ -28,7 +28,7 @@ lemma fixes x::real - shows "x > 1 \ x \ 2 powr 20 * log 2 x + 1 \ (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" + shows "x > 1 \ x \ 2 ^ 20 * log 2 x + 1 \ (sin x)\<^sup>2 + (cos x)\<^sup>2 = 1" using [[quickcheck_approximation_custom_seed = 1]] using [[quickcheck_approximation_epsilon = 0.00000001]] --\avoids spurious counterexamples in approximate computation of @{term "(sin x)\<^sup>2 + (cos x)\<^sup>2"} diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Library/Code_Real_Approx_By_Float.thy --- a/src/HOL/Library/Code_Real_Approx_By_Float.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Library/Code_Real_Approx_By_Float.thy Sat Apr 11 11:56:40 2015 +0100 @@ -103,7 +103,7 @@ constant ln \ (SML) "Math.ln" and (OCaml) "Pervasives.ln" -declare ln_def[code del] +declare ln_real_def[code del] code_printing constant cos \ diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Library/Float.thy --- a/src/HOL/Library/Float.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Library/Float.thy Sat Apr 11 11:56:40 2015 +0100 @@ -82,16 +82,18 @@ lemma uminus_float[simp]: "x \ float \ -x \ float" apply (auto simp: float_def) apply hypsubst_thin - apply (rule_tac x="-x" in exI) - apply (rule_tac x="xa" in exI) + apply (rename_tac m e) + apply (rule_tac x="-m" in exI) + apply (rule_tac x="e" in exI) apply (simp add: field_simps) done lemma times_float[simp]: "x \ float \ y \ float \ x * y \ float" apply (auto simp: float_def) apply hypsubst_thin - apply (rule_tac x="x * xa" in exI) - apply (rule_tac x="xb + xc" in exI) + apply (rename_tac mx my ex ey) + apply (rule_tac x="mx * my" in exI) + apply (rule_tac x="ex + ey" in exI) apply (simp add: powr_add) done @@ -107,16 +109,18 @@ lemma div_power_2_float[simp]: "x \ float \ x / 2^d \ float" apply (auto simp add: float_def) apply hypsubst_thin - apply (rule_tac x="x" in exI) - apply (rule_tac x="xa - d" in exI) + apply (rename_tac m e) + apply (rule_tac x="m" in exI) + apply (rule_tac x="e - d" in exI) apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric]) done lemma div_power_2_int_float[simp]: "x \ float \ x / (2::int)^d \ float" apply (auto simp add: float_def) apply hypsubst_thin - apply (rule_tac x="x" in exI) - apply (rule_tac x="xa - d" in exI) + apply (rename_tac m e) + apply (rule_tac x="m" in exI) + apply (rule_tac x="e - d" in exI) apply (simp add: powr_realpow[symmetric] field_simps powr_add[symmetric]) done @@ -687,8 +691,9 @@ from neg have "2 powr real p \ 2 powr 0" by (intro powr_mono) auto - also have "\ \ \2 powr 0\" by simp - also have "\ \ \x * 2 powr real p\" unfolding real_of_int_le_iff + also have "\ \ \2 powr 0::real\" by simp + also have "... \ \x * 2 powr (real p)\" + unfolding real_of_int_le_iff using x x_le by (intro floor_mono) (simp add: powr_minus_divide field_simps) finally show ?thesis using prec x @@ -723,7 +728,7 @@ proof have "round_up e f - f \ round_up e f - round_down e f" using round_down by simp also have "\ \ 2 powr -e" using round_up_diff_round_down by simp - finally show "round_up e f - f \ 2 powr real (- e)" + finally show "round_up e f - f \ 2 powr - (real e)" by simp qed (simp add: algebra_simps round_up) @@ -740,7 +745,7 @@ proof have "f - round_down e f \ round_up e f - round_down e f" using round_up by simp also have "\ \ 2 powr -e" using round_up_diff_round_down by simp - finally show "f - round_down e f \ 2 powr real (- e)" + finally show "f - round_down e f \ 2 powr - (real e)" by simp qed (simp add: algebra_simps round_down) @@ -923,8 +928,9 @@ shows "0 \ e + (bitlen m - 1)" proof - have "0 < Float m e" using assms by auto - hence "0 < m" using powr_gt_zero[of 2 e] - by (auto simp: zero_less_mult_iff) + hence "0 < m" using powr_gt_zero[of 2 e] + apply (auto simp: zero_less_mult_iff) + using not_le powr_ge_pzero by blast hence "m \ 0" by auto show ?thesis proof (cases "0 \ e") @@ -2017,8 +2023,7 @@ by (simp add: truncate_up_eq_truncate_down truncate_down_mono) lemma Float_le_zero_iff: "Float a b \ 0 \ a \ 0" - apply (auto simp: zero_float_def mult_le_0_iff) - using powr_gt_zero[of 2 b] by simp + by (auto simp: zero_float_def mult_le_0_iff) (simp add: not_less [symmetric]) lemma real_of_float_pprt[simp]: fixes a::float shows "real (pprt a) = pprt (real a)" unfolding pprt_def sup_float_def max_def sup_real_def by auto diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Library/Formal_Power_Series.thy --- a/src/HOL/Library/Formal_Power_Series.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Library/Formal_Power_Series.thy Sat Apr 11 11:56:40 2015 +0100 @@ -624,7 +624,7 @@ by blast } then show ?thesis - unfolding LIMSEQ_def by blast + unfolding lim_sequentially by blast qed diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Limits.thy --- a/src/HOL/Limits.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Limits.thy Sat Apr 11 11:56:40 2015 +0100 @@ -1287,7 +1287,7 @@ lemma LIMSEQ_iff: fixes L :: "'a::real_normed_vector" shows "(X ----> L) = (\r>0. \no. \n \ no. norm (X n - L) < r)" -unfolding LIMSEQ_def dist_norm .. +unfolding lim_sequentially dist_norm .. lemma LIMSEQ_I: fixes L :: "'a::real_normed_vector" diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/MacLaurin.thy --- a/src/HOL/MacLaurin.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/MacLaurin.thy Sat Apr 11 11:56:40 2015 +0100 @@ -389,6 +389,12 @@ (exp t / (fact n)) * x ^ n" by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto) +lemma exp_lower_taylor_quadratic: + fixes x::real + shows "0 \ x \ 1 + x + x\<^sup>2 / 2 \ exp x" + using Maclaurin_exp_le [of x 3] + by (auto simp: numeral_3_eq_3 power2_eq_square power_Suc) + subsection{*Version for Sine Function*} diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Matrix_LP/ComputeFloat.thy --- a/src/HOL/Matrix_LP/ComputeFloat.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy Sat Apr 11 11:56:40 2015 +0100 @@ -189,18 +189,15 @@ lemma zero_le_float: "(0 <= float (a,b)) = (0 <= a)" - using powr_gt_zero[of 2 "real b", arith] - by (simp add: float_def zero_le_mult_iff) + by (simp add: float_def zero_le_mult_iff) (simp add: not_less [symmetric]) lemma float_le_zero: "(float (a,b) <= 0) = (a <= 0)" - using powr_gt_zero[of 2 "real b", arith] - by (simp add: float_def mult_le_0_iff) + by (simp add: float_def mult_le_0_iff) (simp add: not_less [symmetric]) lemma float_abs: "abs (float (a,b)) = (if 0 <= a then (float (a,b)) else (float (-a,b)))" - using powr_gt_zero[of 2 "real b", arith] - by (simp add: float_def abs_if mult_less_0_iff) + by (simp add: float_def abs_if mult_less_0_iff not_less) lemma float_zero: "float (0, b) = 0" diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy --- a/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy Sat Apr 11 11:56:40 2015 +0100 @@ -188,7 +188,7 @@ by simp qed show "convergent f" - proof (rule convergentI, subst LIMSEQ_def, safe) + proof (rule convergentI, subst lim_sequentially, safe) --{* The limit function converges according to its norm *} fix e::real assume "e > 0" hence "e/2 > 0" by simp diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy --- a/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics.thy Sat Apr 11 11:56:40 2015 +0100 @@ -250,6 +250,21 @@ by (metis closed_halfspace_Im_eq) qed +lemma closed_Real_halfspace_Re_le: "closed (\ \ {w. Re w \ x})" + by (simp add: closed_Int closed_complex_Reals closed_halfspace_Re_le) + +lemma closed_Real_halfspace_Re_ge: "closed (\ \ {w. x \ Re(w)})" + using closed_halfspace_Re_ge + by (simp add: closed_Int closed_complex_Reals) + +lemma closed_real_abs_le: "closed {w \ \. \Re w\ \ r}" +proof - + have "{w \ \. \Re w\ \ r} = (\ \ {w. Re w \ r}) \ (\ \ {w. Re w \ -r})" + by auto + then show "closed {w \ \. \Re w\ \ r}" + by (simp add: closed_Int closed_Real_halfspace_Re_ge closed_Real_halfspace_Re_le) +qed + lemma real_lim: fixes l::complex assumes "(f ---> l) F" and "~(trivial_limit F)" and "eventually P F" and "\a. P a \ f a \ \" @@ -1151,4 +1166,93 @@ done qed + +subsection {* Polynomal function extremal theorem, from HOL Light*} + +lemma polyfun_extremal_lemma: (*COMPLEX_POLYFUN_EXTREMAL_LEMMA in HOL Light*) + fixes c :: "nat \ 'a::real_normed_div_algebra" + assumes "0 < e" + shows "\M. \z. M \ norm(z) \ norm (\i\n. c(i) * z^i) \ e * norm(z) ^ (Suc n)" +proof (induct n) + case 0 with assms + show ?case + apply (rule_tac x="norm (c 0) / e" in exI) + apply (auto simp: field_simps) + done +next + case (Suc n) + obtain M where M: "\z. M \ norm z \ norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" + using Suc assms by blast + show ?case + proof (rule exI [where x= "max M (1 + norm(c(Suc n)) / e)"], clarsimp simp del: power_Suc) + fix z::'a + assume z1: "M \ norm z" and "1 + norm (c (Suc n)) / e \ norm z" + then have z2: "e + norm (c (Suc n)) \ e * norm z" + using assms by (simp add: field_simps) + have "norm (\i\n. c i * z^i) \ e * norm z ^ Suc n" + using M [OF z1] by simp + then have "norm (\i\n. c i * z^i) + norm (c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" + by simp + then have "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc n + norm (c (Suc n) * z ^ Suc n)" + by (blast intro: norm_triangle_le elim: ) + also have "... \ (e + norm (c (Suc n))) * norm z ^ Suc n" + by (simp add: norm_power norm_mult algebra_simps) + also have "... \ (e * norm z) * norm z ^ Suc n" + by (metis z2 mult.commute mult_left_mono norm_ge_zero norm_power) + finally show "norm ((\i\n. c i * z^i) + c (Suc n) * z ^ Suc n) \ e * norm z ^ Suc (Suc n)" + by (simp add: power_Suc) + qed +qed + +lemma polyfun_extremal: (*COMPLEX_POLYFUN_EXTREMAL in HOL Light*) + fixes c :: "nat \ 'a::real_normed_div_algebra" + assumes k: "c k \ 0" "1\k" and kn: "k\n" + shows "eventually (\z. norm (\i\n. c(i) * z^i) \ B) at_infinity" +using kn +proof (induction n) + case 0 + then show ?case + using k by simp +next + case (Suc m) + let ?even = ?case + show ?even + proof (cases "c (Suc m) = 0") + case True + then show ?even using Suc k + by auto (metis antisym_conv less_eq_Suc_le not_le) + next + case False + then obtain M where M: + "\z. M \ norm z \ norm (\i\m. c i * z^i) \ norm (c (Suc m)) / 2 * norm z ^ Suc m" + using polyfun_extremal_lemma [of "norm(c (Suc m)) / 2" c m] Suc + by auto + have "\b. \z. b \ norm z \ B \ norm (\i\Suc m. c i * z^i)" + proof (rule exI [where x="max M (max 1 (\B\ / (norm(c (Suc m)) / 2)))"], clarsimp simp del: power_Suc) + fix z::'a + assume z1: "M \ norm z" "1 \ norm z" + and "\B\ * 2 / norm (c (Suc m)) \ norm z" + then have z2: "\B\ \ norm (c (Suc m)) * norm z / 2" + using False by (simp add: field_simps) + have nz: "norm z \ norm z ^ Suc m" + by (metis `1 \ norm z` One_nat_def less_eq_Suc_le power_increasing power_one_right zero_less_Suc) + have *: "\y x. norm (c (Suc m)) * norm z / 2 \ norm y - norm x \ B \ norm (x + y)" + by (metis abs_le_iff add.commute norm_diff_ineq order_trans z2) + have "norm z * norm (c (Suc m)) + 2 * norm (\i\m. c i * z^i) + \ norm (c (Suc m)) * norm z + norm (c (Suc m)) * norm z ^ Suc m" + using M [of z] Suc z1 by auto + also have "... \ 2 * (norm (c (Suc m)) * norm z ^ Suc m)" + using nz by (simp add: mult_mono del: power_Suc) + finally show "B \ norm ((\i\m. c i * z^i) + c (Suc m) * z ^ Suc m)" + using Suc.IH + apply (auto simp: eventually_at_infinity) + apply (rule *) + apply (simp add: field_simps norm_mult norm_power) + done + qed + then show ?even + by (simp add: eventually_at_infinity) + qed +qed + end diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Multivariate_Analysis/Complex_Transcendental.thy --- a/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Complex_Transcendental.thy Sat Apr 11 11:56:40 2015 +0100 @@ -8,7 +8,6 @@ imports "~~/src/HOL/Multivariate_Analysis/Complex_Analysis_Basics" begin - lemma cmod_add_real_less: assumes "Im z \ 0" "r\0" shows "cmod (z + r) < cmod z + abs r" @@ -613,6 +612,14 @@ apply (simp only: pos_le_divide_eq [symmetric], linarith) done +lemma e_less_3: "exp 1 < (3::real)" + using e_approx_32 + by (simp add: abs_if split: split_if_asm) + +lemma ln3_gt_1: "ln 3 > (1::real)" + by (metis e_less_3 exp_less_cancel_iff exp_ln_iff less_trans ln_exp) + + subsection{*The argument of a complex number*} definition Arg :: "complex \ real" where @@ -892,8 +899,9 @@ subsection{*Complex logarithms (the conventional principal value)*} -definition Ln where - "Ln \ \z. THE w. exp w = z & -pi < Im(w) & Im(w) \ pi" +definition Ln :: "complex \ complex" + where "Ln \ \z. THE w. exp w = z & -pi < Im(w) & Im(w) \ pi" + lemma assumes "z \ 0" @@ -941,6 +949,7 @@ apply (auto simp: exp_of_nat_mult [symmetric]) done + subsection{*The Unwinding Number and the Ln-product Formula*} text{*Note that in this special case the unwinding number is -1, 0 or 1.*} @@ -1128,8 +1137,8 @@ apply (cases "z=0", auto) apply (rule exp_complex_eqI) apply (auto simp: abs_if split: split_if_asm) - 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) - 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) + apply (metis Im_Ln_less_pi add_mono_thms_linordered_field(5) cnj.simps mult_2 neg_equal_0_iff_equal) + 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) by (metis exp_Ln exp_cnj) lemma Ln_inverse: "(Im(z) = 0 \ 0 < Re z) \ Ln(inverse z) = -(Ln z)" @@ -1141,7 +1150,7 @@ inverse_inverse_eq inverse_zero le_less mult.commute mult_2_right) done -lemma Ln_1 [simp]: "Ln(1) = 0" +lemma Ln_1 [simp]: "Ln 1 = 0" proof - have "Ln (exp 0) = 0" by (metis exp_zero ln_exp Ln_of_real of_real_0 of_real_1 zero_less_one) @@ -1149,6 +1158,18 @@ by simp qed +instantiation complex :: ln +begin + +definition ln_complex :: "complex \ complex" + where "ln_complex \ Ln" + +instance + by intro_classes (simp add: ln_complex_def) + +end + + lemma Ln_minus1 [simp]: "Ln(-1) = ii * pi" apply (rule exp_complex_eqI) using Im_Ln_le_pi [of "-1"] mpi_less_Im_Ln [of "-1"] cis_conv_exp cis_pi @@ -1242,6 +1263,93 @@ by (auto simp: of_real_numeral Ln_times) + +subsection{*Complex Powers*} + +lemma powr_0 [simp]: "0 powr z = 0" + by (simp add: powr_def) + +lemma powr_to_1 [simp]: "z powr 1 = (z::complex)" + by (simp add: powr_def ln_complex_def) + +lemma powr_nat: + fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)" + by (simp add: exp_of_nat_mult powr_def ln_complex_def) + +lemma powr_add: + fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2" + by (simp add: powr_def algebra_simps exp_add) + +lemma powr_minus: + fixes w::complex shows "w powr (-z) = inverse(w powr z)" + by (simp add: powr_def exp_minus) + +lemma powr_diff: + fixes w::complex shows "w powr (z1 - z2) = w powr z1 / w powr z2" + by (simp add: powr_def algebra_simps exp_diff) + +lemma norm_powr_real: "w \ \ \ 0 < Re w \ norm(w powr z) = exp(Re z * ln(Re w))" + apply (simp add: powr_def ln_complex_def) + using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def + by auto + +lemma powr_real_real: + "\w \ \; z \ \; 0 < Re w\ \ w powr z = exp(Re z * ln(Re w))" + apply (simp add: powr_def ln_complex_def) + by (metis complex_eq complex_is_Real_iff diff_0 diff_0_right diff_minus_eq_add exp_ln exp_not_eq_zero + exp_of_real Ln_of_real mult_zero_right of_real_0 of_real_mult) + +lemma powr_of_real: + fixes x::real + shows "0 < x \ x powr y = x powr y" + by (simp add: powr_def powr_real_real) + +lemma norm_powr_real_mono: + "w \ \ \ 1 < Re w + \ norm(w powr z1) \ norm(w powr z2) \ Re z1 \ Re z2" + by (auto simp: powr_def ln_complex_def algebra_simps Reals_def Ln_of_real) + +lemma powr_times_real: + "\x \ \; y \ \; 0 \ Re x; 0 \ Re y\ + \ (x * y) powr z = x powr z * y powr z" + by (auto simp: Reals_def powr_def ln_complex_def Ln_times exp_add algebra_simps less_eq_real_def Ln_of_real) + +lemma has_field_derivative_powr: + "(Im z = 0 \ 0 < Re z) + \ ((\z. z powr s) has_field_derivative (s * z powr (s - 1))) (at z)" + apply (cases "z=0", auto) + apply (simp add: powr_def ln_complex_def) + apply (rule DERIV_transform_at [where d = "norm z" and f = "\z. exp (s * Ln z)"]) + apply (auto simp: dist_complex_def ln_complex_def) + apply (intro derivative_eq_intros | simp add: assms)+ + apply (simp add: field_simps exp_diff) + done + +lemma has_field_derivative_powr_right: + "w \ 0 \ ((\z. w powr z) has_field_derivative Ln w * w powr z) (at z)" + apply (simp add: powr_def ln_complex_def) + apply (intro derivative_eq_intros | simp add: assms)+ + done + +lemma complex_differentiable_powr_right: + "w \ 0 \ (\z. w powr z) complex_differentiable (at z)" +using complex_differentiable_def has_field_derivative_powr_right by blast + + +lemma holomorphic_on_powr_right: + "f holomorphic_on s \ w \ 0 \ (\z. w powr (f z)) holomorphic_on s" + unfolding holomorphic_on_def + using DERIV_chain' complex_differentiable_def has_field_derivative_powr_right by fastforce + + +lemma norm_powr_real_powr: + "w \ \ \ 0 < Re w \ norm(w powr z) = Re w powr Re z" + by (auto simp add: norm_powr_real powr_def Im_Ln_eq_0 complex_is_Real_iff in_Reals_norm ln_complex_def) + +lemma cmod_Ln_Reals [simp]:"z \ Reals \ 0 < Re z \ cmod (Ln z) = norm (ln (Re z))" + using Ln_of_real by force + + subsection{*Relation between Square Root and exp/ln, hence its derivative*} lemma csqrt_exp_Ln: @@ -1336,10 +1444,6 @@ using open_Compl by (force simp add: continuous_def eventually_at_topological filterlim_iff open_Collect_neg) -lemma closed_Real_halfspace_Re_ge: "closed (\ \ {w. x \ Re(w)})" - using closed_halfspace_Re_ge - by (simp add: closed_Int closed_complex_Reals) - lemma continuous_within_csqrt_posreal: "continuous (at z within (\ \ {w. 0 \ Re(w)})) csqrt" proof (cases "Im z = 0 --> 0 < Re(z)") @@ -1867,15 +1971,15 @@ Re z = pi & Im z \ 0" shows "Arccos(cos z) = z" proof - - have *: "((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z))) = sin z" + have *: "((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z))) = sin z" by (simp add: sin_exp_eq exp_minus field_simps power2_eq_square) - have "1 - (exp (\ * z) + inverse (exp (\ * z)))\<^sup>2 / 4 = ((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z)))\<^sup>2" + have "1 - (exp (\ * z) + inverse (exp (\ * z)))\<^sup>2 / 4 = ((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z)))\<^sup>2" by (simp add: field_simps power2_eq_square) then have "Arccos(cos z) = - (\ * Ln ((exp (\ * z) + inverse (exp (\ * z))) / 2 + - \ * csqrt (((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z)))\<^sup>2)))" + \ * csqrt (((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z)))\<^sup>2)))" by (simp add: cos_exp_eq Arccos_def exp_minus) also have "... = - (\ * Ln ((exp (\ * z) + inverse (exp (\ * z))) / 2 + - \ * ((\ - (Exp (\ * z))\<^sup>2 * \) / (2 * Exp (\ * z)))))" + \ * ((\ - (exp (\ * z))\<^sup>2 * \) / (2 * exp (\ * z)))))" apply (subst csqrt_square) using assms Re_sin_pos [of z] Im_sin_nonneg [of z] Im_sin_nonneg2 [of z] apply (auto simp: * Re_sin Im_sin) @@ -2177,4 +2281,129 @@ lemma of_real_arccos: "abs x \ 1 \ of_real(arccos x) = Arccos(of_real x)" by (metis Im_Arccos_of_real add.right_neutral arccos_eq_Re_Arccos complex_eq mult_zero_right of_real_0) +subsection{*Some interrelationships among the real inverse trig functions.*} + +lemma arccos_arctan: + assumes "-1 < x" "x < 1" + shows "arccos x = pi/2 - arctan(x / sqrt(1 - x\<^sup>2))" +proof - + have "arctan(x / sqrt(1 - x\<^sup>2)) - (pi/2 - arccos x) = 0" + proof (rule sin_eq_0_pi) + show "- pi < arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)" + using arctan_lbound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms + by (simp add: algebra_simps) + next + show "arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x) < pi" + using arctan_ubound [of "x / sqrt(1 - x\<^sup>2)"] arccos_bounded [of x] assms + by (simp add: algebra_simps) + next + show "sin (arctan (x / sqrt (1 - x\<^sup>2)) - (pi / 2 - arccos x)) = 0" + using assms + by (simp add: algebra_simps sin_diff cos_add sin_arccos sin_arctan cos_arctan + power2_eq_square square_eq_1_iff) + qed + then show ?thesis + by simp +qed + +lemma arcsin_plus_arccos: + assumes "-1 \ x" "x \ 1" + shows "arcsin x + arccos x = pi/2" +proof - + have "arcsin x = pi/2 - arccos x" + apply (rule sin_inj_pi) + using assms arcsin [OF assms] arccos [OF assms] + apply (auto simp: algebra_simps sin_diff) + done + then show ?thesis + by (simp add: algebra_simps) +qed + +lemma arcsin_arccos_eq: "-1 \ x \ x \ 1 \ arcsin x = pi/2 - arccos x" + using arcsin_plus_arccos by force + +lemma arccos_arcsin_eq: "-1 \ x \ x \ 1 \ arccos x = pi/2 - arcsin x" + using arcsin_plus_arccos by force + +lemma arcsin_arctan: "-1 < x \ x < 1 \ arcsin x = arctan(x / sqrt(1 - x\<^sup>2))" + by (simp add: arccos_arctan arcsin_arccos_eq) + +lemma zz: "csqrt (1 - (of_real x)\<^sup>2) = (if x^2 \ 1 then sqrt (1 - x^2) else \ * sqrt (x^2 - 1))" + by ( simp add: of_real_sqrt del: csqrt_of_real_nonneg) + +lemma arcsin_arccos_sqrt_pos: "0 \ x \ x \ 1 \ arcsin x = arccos(sqrt(1 - x\<^sup>2))" + apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos) + apply (subst Arcsin_Arccos_csqrt_pos) + apply (auto simp: power_le_one zz) + done + +lemma arcsin_arccos_sqrt_neg: "-1 \ x \ x \ 0 \ arcsin x = -arccos(sqrt(1 - x\<^sup>2))" + using arcsin_arccos_sqrt_pos [of "-x"] + by (simp add: arcsin_minus) + +lemma arccos_arcsin_sqrt_pos: "0 \ x \ x \ 1 \ arccos x = arcsin(sqrt(1 - x\<^sup>2))" + apply (simp add: abs_square_le_1 diff_le_iff arcsin_eq_Re_Arcsin arccos_eq_Re_Arccos) + apply (subst Arccos_Arcsin_csqrt_pos) + apply (auto simp: power_le_one zz) + done + +lemma arccos_arcsin_sqrt_neg: "-1 \ x \ x \ 0 \ arccos x = pi - arcsin(sqrt(1 - x\<^sup>2))" + using arccos_arcsin_sqrt_pos [of "-x"] + by (simp add: arccos_minus) + +subsection{*continuity results for arcsin and arccos.*} + +lemma continuous_on_Arcsin_real [continuous_intros]: + "continuous_on {w \ \. \Re w\ \ 1} Arcsin" +proof - + have "continuous_on {w \ \. \Re w\ \ 1} (\x. complex_of_real (arcsin (Re x))) = + continuous_on {w \ \. \Re w\ \ 1} (\x. complex_of_real (Re (Arcsin (of_real (Re x)))))" + by (rule continuous_on_cong [OF refl]) (simp add: arcsin_eq_Re_Arcsin) + also have "... = ?thesis" + by (rule continuous_on_cong [OF refl]) simp + finally show ?thesis + using continuous_on_arcsin [OF continuous_on_Re [OF continuous_on_id], of "{w \ \. \Re w\ \ 1}"] + continuous_on_of_real + by fastforce +qed + +lemma continuous_within_Arcsin_real: + "continuous (at z within {w \ \. \Re w\ \ 1}) Arcsin" +proof (cases "z \ {w \ \. \Re w\ \ 1}") + case True then show ?thesis + using continuous_on_Arcsin_real continuous_on_eq_continuous_within + by blast +next + case False + with closed_real_abs_le [of 1] show ?thesis + by (rule continuous_within_closed_nontrivial) +qed + +lemma continuous_on_Arccos_real: + "continuous_on {w \ \. \Re w\ \ 1} Arccos" +proof - + have "continuous_on {w \ \. \Re w\ \ 1} (\x. complex_of_real (arccos (Re x))) = + continuous_on {w \ \. \Re w\ \ 1} (\x. complex_of_real (Re (Arccos (of_real (Re x)))))" + by (rule continuous_on_cong [OF refl]) (simp add: arccos_eq_Re_Arccos) + also have "... = ?thesis" + by (rule continuous_on_cong [OF refl]) simp + finally show ?thesis + using continuous_on_arccos [OF continuous_on_Re [OF continuous_on_id], of "{w \ \. \Re w\ \ 1}"] + continuous_on_of_real + by fastforce +qed + +lemma continuous_within_Arccos_real: + "continuous (at z within {w \ \. \Re w\ \ 1}) Arccos" +proof (cases "z \ {w \ \. \Re w\ \ 1}") + case True then show ?thesis + using continuous_on_Arccos_real continuous_on_eq_continuous_within + by blast +next + case False + with closed_real_abs_le [of 1] show ?thesis + by (rule continuous_within_closed_nontrivial) +qed + + end diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Sat Apr 11 11:56:40 2015 +0100 @@ -4077,7 +4077,7 @@ apply (erule_tac x="e/2" in allE) apply auto done - from lr(3)[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] + from lr(3)[unfolded lim_sequentially, THEN spec[where x="e/2"]] obtain M where M:"\n\M. dist ((f \ r) n) l < e/2" using `e > 0` by auto { @@ -4096,7 +4096,7 @@ then have "\N. \n\N. dist (f n) l < e" by blast } then have "\l\s. (f ---> l) sequentially" using `l\s` - unfolding LIMSEQ_def by auto + unfolding lim_sequentially by auto } then show ?thesis unfolding complete_def by auto qed @@ -4442,7 +4442,7 @@ fix e :: real assume "e > 0" then obtain N :: nat where N: "\n\N. dist (t n) l < e" - using l[unfolded LIMSEQ_def] by auto + using l[unfolded lim_sequentially] by auto have "t (max n N) \ s n" using assms(3) unfolding subset_eq @@ -4542,7 +4542,7 @@ fix x assume "P x" then obtain M where M:"\n\M. dist (s n x) (l x) < e/2" - using l[THEN spec[where x=x], unfolded LIMSEQ_def] and `e > 0` + using l[THEN spec[where x=x], unfolded lim_sequentially] and `e > 0` by (auto elim!: allE[where x="e/2"]) fix n :: nat assume "n \ N" @@ -4571,7 +4571,7 @@ assume "P x" then have "l x = l' x" using tendsto_unique[OF trivial_limit_sequentially, of "\n. s n x" "l x" "l' x"] - using l and assms(2) unfolding LIMSEQ_def by blast + using l and assms(2) unfolding lim_sequentially by blast } ultimately show ?thesis by auto qed @@ -4809,7 +4809,7 @@ then obtain d where "d > 0" and d: "\x\s. \x'\s. dist x' x < d \ dist (f x') (f x) < e" using `?lhs`[unfolded uniformly_continuous_on_def, THEN spec[where x=e]] by auto obtain N where N: "\n\N. dist (x n) (y n) < d" - using xy[unfolded LIMSEQ_def dist_norm] and `d>0` by auto + using xy[unfolded lim_sequentially dist_norm] and `d>0` by auto { fix n assume "n\N" @@ -4824,7 +4824,7 @@ by auto } then have "((\n. dist (f(x n)) (f(y n))) ---> 0) sequentially" - unfolding LIMSEQ_def and dist_real_def by auto + unfolding lim_sequentially and dist_real_def by auto } then show ?rhs by auto next @@ -4864,7 +4864,7 @@ } then have "\e>0. \N. \n\N. dist (f (x n)) (f (y n)) < e" using `?rhs`[THEN spec[where x=x], THEN spec[where x=y]] and xyn - unfolding LIMSEQ_def dist_real_def by auto + unfolding lim_sequentially dist_real_def by auto then have False using fxy and `e>0` by auto } then show ?lhs @@ -6615,7 +6615,7 @@ then have "\N::nat. \n\N. inverse (real n + 1) < e" by auto } then have "((\n. inverse (real n + 1)) ---> 0) sequentially" - unfolding LIMSEQ_def by(auto simp add: dist_norm) + unfolding lim_sequentially by(auto simp add: dist_norm) then have "(f ---> x) sequentially" unfolding f_def using tendsto_add[OF tendsto_const, of "\n::nat. (inverse (real n + 1)) *\<^sub>R ((1 / 2) *\<^sub>R (a + b) - x)" 0 sequentially x] @@ -7446,7 +7446,7 @@ unfolding e_def using zero_le_dist[of "f x" x] by (metis dist_eq_0_iff dist_nz e_def) then obtain N where N:"\n\N. dist (z n) x < e / 2" - using x[unfolded LIMSEQ_def, THEN spec[where x="e/2"]] by auto + using x[unfolded lim_sequentially, THEN spec[where x="e/2"]] by auto then have N':"dist (z N) x < e / 2" by auto have *: "c * dist (z N) x \ dist (z N) x" diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/NSA/HLog.thy --- a/src/HOL/NSA/HLog.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/NSA/HLog.thy Sat Apr 11 11:56:40 2015 +0100 @@ -34,13 +34,13 @@ lemma powhr_mult: "!!a x y. [| 0 < x; 0 < y |] ==> (x * y) powhr a = (x powhr a) * (y powhr a)" -by (transfer, rule powr_mult) +by (transfer, simp add: powr_mult) -lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a" +lemma powhr_gt_zero [simp]: "!!a x. 0 < x powhr a \ x \ 0" by (transfer, simp) -lemma powhr_not_zero [simp]: "x powhr a \ 0" -by (metis less_numeral_extra(3) powhr_gt_zero) +lemma powhr_not_zero [simp]: "\a x. x powhr a \ 0 \ x \ 0" +by transfer simp lemma powhr_divide: "!!a x y. [| 0 < x; 0 < y |] ==> (x / y) powhr a = (x powhr a)/(y powhr a)" @@ -105,8 +105,8 @@ ==> hlog a x = (( *f* ln) b/( *f*ln) a) * hlog b x" by (transfer, rule log_eq_div_ln_mult_log) -lemma powhr_as_starfun: "!!a x. x powhr a = ( *f* exp) (a * ( *f* ln) x)" -by (transfer, simp add: powr_def) +lemma powhr_as_starfun: "!!a x. x powhr a = (if x=0 then 0 else ( *f* exp) (a * ( *f* real_ln) x))" + by (transfer, simp add: powr_def) lemma HInfinite_powhr: "[| x : HInfinite; 0 < x; a : HFinite - Infinitesimal; diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/NSA/HTranscendental.thy --- a/src/HOL/NSA/HTranscendental.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/NSA/HTranscendental.thy Sat Apr 11 11:56:40 2015 +0100 @@ -306,34 +306,37 @@ lemma starfun_exp_gt_one [simp]: "!!x::hypreal. 0 < x ==> 1 < ( *f* exp) x" by transfer (rule exp_gt_one) -lemma starfun_ln_exp [simp]: "!!x. ( *f* ln) (( *f* exp) x) = x" +abbreviation real_ln :: "real \ real" where + "real_ln \ ln" + +lemma starfun_ln_exp [simp]: "!!x. ( *f* real_ln) (( *f* exp) x) = x" by transfer (rule ln_exp) -lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* ln) x) = x) = (0 < x)" +lemma starfun_exp_ln_iff [simp]: "!!x. (( *f* exp)(( *f* real_ln) x) = x) = (0 < x)" by transfer (rule exp_ln_iff) -lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* ln) x = u" +lemma starfun_exp_ln_eq: "!!u x. ( *f* exp) u = x ==> ( *f* real_ln) x = u" by transfer (rule ln_unique) -lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* ln) x < x" +lemma starfun_ln_less_self [simp]: "!!x. 0 < x ==> ( *f* real_ln) x < x" by transfer (rule ln_less_self) -lemma starfun_ln_ge_zero [simp]: "!!x. 1 \ x ==> 0 \ ( *f* ln) x" +lemma starfun_ln_ge_zero [simp]: "!!x. 1 \ x ==> 0 \ ( *f* real_ln) x" by transfer (rule ln_ge_zero) -lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* ln) x" +lemma starfun_ln_gt_zero [simp]: "!!x .1 < x ==> 0 < ( *f* real_ln) x" by transfer (rule ln_gt_zero) -lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \ 1 |] ==> ( *f* ln) x \ 0" +lemma starfun_ln_not_eq_zero [simp]: "!!x. [| 0 < x; x \ 1 |] ==> ( *f* real_ln) x \ 0" by transfer simp -lemma starfun_ln_HFinite: "[| x \ HFinite; 1 \ x |] ==> ( *f* ln) x \ HFinite" +lemma starfun_ln_HFinite: "[| x \ HFinite; 1 \ x |] ==> ( *f* real_ln) x \ HFinite" apply (rule HFinite_bounded) apply assumption apply (simp_all add: starfun_ln_less_self order_less_imp_le) done -lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* ln) (inverse x) = -( *f* ln) x" +lemma starfun_ln_inverse: "!!x. 0 < x ==> ( *f* real_ln) (inverse x) = -( *f* ln) x" by transfer (rule ln_inverse) lemma starfun_abs_exp_cancel: "\x. \( *f* exp) (x::hypreal)\ = ( *f* exp) x" @@ -360,7 +363,7 @@ (* using previous result to get to result *) lemma starfun_ln_HInfinite: - "[| x \ HInfinite; 0 < x |] ==> ( *f* ln) x \ HInfinite" + "[| x \ HInfinite; 0 < x |] ==> ( *f* real_ln) x \ HInfinite" apply (rule ccontr, drule HFinite_HInfinite_iff [THEN iffD2]) apply (drule starfun_exp_HFinite) apply (simp add: starfun_exp_ln_iff [THEN iffD2] HFinite_HInfinite_iff) @@ -374,7 +377,7 @@ (* check out this proof!!! *) lemma starfun_ln_HFinite_not_Infinitesimal: - "[| x \ HFinite - Infinitesimal; 0 < x |] ==> ( *f* ln) x \ HFinite" + "[| x \ HFinite - Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \ HFinite" apply (rule ccontr, drule HInfinite_HFinite_iff [THEN iffD2]) apply (drule starfun_exp_HInfinite_Infinitesimal_disj) apply (simp add: starfun_exp_ln_iff [symmetric] HInfinite_HFinite_iff @@ -383,22 +386,22 @@ (* we do proof by considering ln of 1/x *) lemma starfun_ln_Infinitesimal_HInfinite: - "[| x \ Infinitesimal; 0 < x |] ==> ( *f* ln) x \ HInfinite" + "[| x \ Infinitesimal; 0 < x |] ==> ( *f* real_ln) x \ HInfinite" apply (drule Infinitesimal_inverse_HInfinite) apply (frule positive_imp_inverse_positive) apply (drule_tac [2] starfun_ln_HInfinite) apply (auto simp add: starfun_ln_inverse HInfinite_minus_iff) done -lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* ln) x < 0" +lemma starfun_ln_less_zero: "!!x. [| 0 < x; x < 1 |] ==> ( *f* real_ln) x < 0" by transfer (rule ln_less_zero) lemma starfun_ln_Infinitesimal_less_zero: - "[| x \ Infinitesimal; 0 < x |] ==> ( *f* ln) x < 0" + "[| x \ Infinitesimal; 0 < x |] ==> ( *f* real_ln) x < 0" by (auto intro!: starfun_ln_less_zero simp add: Infinitesimal_def) lemma starfun_ln_HInfinite_gt_zero: - "[| x \ HInfinite; 0 < x |] ==> 0 < ( *f* ln) x" + "[| x \ HInfinite; 0 < x |] ==> 0 < ( *f* real_ln) x" by (auto intro!: starfun_ln_gt_zero simp add: HInfinite_def) diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/NSA/NSComplex.thy --- a/src/HOL/NSA/NSComplex.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/NSA/NSComplex.thy Sat Apr 11 11:56:40 2015 +0100 @@ -72,7 +72,7 @@ (*------------ e ^ (x + iy) ------------*) definition hExp :: "hcomplex => hcomplex" where - "hExp = *f* Exp" + "hExp = *f* exp" definition HComplex :: "[hypreal,hypreal] => hcomplex" where @@ -485,7 +485,7 @@ by transfer (rule rcis_Ex) lemma hRe_hcomplex_polar [simp]: - "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = + "!!r a. hRe (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = r * ( *f* cos) a" by transfer simp @@ -493,7 +493,7 @@ by transfer (rule Re_rcis) lemma hIm_hcomplex_polar [simp]: - "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = + "!!r a. hIm (hcomplex_of_hypreal r * HComplex (( *f* cos) a) (( *f* sin) a)) = r * ( *f* sin) a" by transfer simp @@ -621,8 +621,8 @@ subsection{*Numerals and Arithmetic*} -lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: - "hcomplex_of_hypreal (hypreal_of_real x) = +lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: + "hcomplex_of_hypreal (hypreal_of_real x) = hcomplex_of_complex (complex_of_real x)" by transfer (rule refl) @@ -642,15 +642,15 @@ "hcmod(numeral v :: hcomplex) = (numeral v :: hypreal)" by transfer (rule norm_numeral) -lemma hcomplex_neg_numeral_hcmod [simp]: +lemma hcomplex_neg_numeral_hcmod [simp]: "hcmod(- numeral v :: hcomplex) = (numeral v :: hypreal)" by transfer (rule norm_neg_numeral) -lemma hcomplex_numeral_hRe [simp]: +lemma hcomplex_numeral_hRe [simp]: "hRe(numeral v :: hcomplex) = numeral v" by transfer (rule complex_Re_numeral) -lemma hcomplex_numeral_hIm [simp]: +lemma hcomplex_numeral_hIm [simp]: "hIm(numeral v :: hcomplex) = 0" by transfer (rule complex_Im_numeral) diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Probability/Borel_Space.thy --- a/src/HOL/Probability/Borel_Space.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Probability/Borel_Space.thy Sat Apr 11 11:56:40 2015 +0100 @@ -1038,7 +1038,7 @@ lemma borel_measurable_ln[measurable (raw)]: assumes f: "f \ borel_measurable M" - shows "(\x. ln (f x)) \ borel_measurable M" + shows "(\x. ln (f x :: real)) \ borel_measurable M" apply (rule measurable_compose[OF f]) apply (rule borel_measurable_continuous_countable_exceptions[of "{0}"]) apply (auto intro!: continuous_on_ln continuous_on_id) diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Probability/Information.thy --- a/src/HOL/Probability/Information.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Probability/Information.thy Sat Apr 11 11:56:40 2015 +0100 @@ -46,7 +46,7 @@ finally have "exp u \ x" by auto } then show "log b x = log b 0" - by (simp add: log_def ln_def) + by (simp add: log_def ln_real_def) qed lemma log_mult_eq: diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Probability/Regularity.thy --- a/src/HOL/Probability/Regularity.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Probability/Regularity.thy Sat Apr 11 11:56:40 2015 +0100 @@ -363,7 +363,7 @@ fix e::real assume "e > 0" with measure_LIMSEQ have "\no. \n\no. \(\ix. D x)\ < e/2" - by (auto simp: LIMSEQ_def dist_real_def simp del: less_divide_eq_numeral1) + by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1) hence "\n0. \(\ix. D x)\ < e/2" by auto then obtain n0 where n0: "\(\ii. D i)\ < e/2" unfolding choice_iff by blast diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Real_Vector_Spaces.thy --- a/src/HOL/Real_Vector_Spaces.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Real_Vector_Spaces.thy Sat Apr 11 11:56:40 2015 +0100 @@ -1544,19 +1544,19 @@ subsubsection {* Limits of Sequences *} -lemma LIMSEQ_def: "X ----> (L::'a::metric_space) \ (\r>0. \no. \n\no. dist (X n) L < r)" +lemma lim_sequentially: "X ----> (L::'a::metric_space) \ (\r>0. \no. \n\no. dist (X n) L < r)" unfolding tendsto_iff eventually_sequentially .. lemma LIMSEQ_iff_nz: "X ----> (L::'a::metric_space) = (\r>0. \no>0. \n\no. dist (X n) L < r)" - unfolding LIMSEQ_def by (metis Suc_leD zero_less_Suc) + unfolding lim_sequentially by (metis Suc_leD zero_less_Suc) lemma metric_LIMSEQ_I: "(\r. 0 < r \ \no. \n\no. dist (X n) L < r) \ X ----> (L::'a::metric_space)" -by (simp add: LIMSEQ_def) +by (simp add: lim_sequentially) lemma metric_LIMSEQ_D: "\X ----> (L::'a::metric_space); 0 < r\ \ \no. \n\no. dist (X n) L < r" -by (simp add: LIMSEQ_def) +by (simp add: lim_sequentially) subsubsection {* Limits of Functions *} @@ -1823,7 +1823,7 @@ proof (rule tendstoI) fix e :: real assume "0 < e" with limseq obtain N :: nat where N: "\n. N \ n \ \f (real n) - y\ < e" - by (auto simp: LIMSEQ_def dist_real_def) + by (auto simp: lim_sequentially dist_real_def) { fix x :: real obtain n where "x \ real_of_nat n" using ex_le_of_nat[of x] .. diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Set_Interval.thy Sat Apr 11 11:56:40 2015 +0100 @@ -1562,12 +1562,6 @@ "(\i\n. (\jji = Suc j..n. a i j)" by (induction n) (auto simp: setsum.distrib) -lemma setsum_zero_power [simp]: - fixes c :: "nat \ 'a::division_ring" - shows "(\i\A. c i * 0^i) = (if finite A \ 0 \ A then c 0 else 0)" -apply (cases "finite A") - by (induction A rule: finite_induct) auto - lemma setsum_zero_power' [simp]: fixes c :: "nat \ 'a::field" shows "(\i\A. c i * 0^i / d i) = (if finite A \ 0 \ A then c 0 / d 0 else 0)" diff -r 09be0495dcc2 -r b785d6d06430 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Thu Apr 09 20:42:38 2015 +0200 +++ b/src/HOL/Transcendental.thy Sat Apr 11 11:56:40 2015 +0100 @@ -1285,88 +1285,130 @@ subsection {* Natural Logarithm *} -definition ln :: "real \ real" - where "ln x = (THE u. exp u = x)" - -lemma ln_exp [simp]: "ln (exp x) = x" - by (simp add: ln_def) - -lemma exp_ln [simp]: "0 < x \ exp (ln x) = x" +class ln = real_normed_algebra_1 + banach + + fixes ln :: "'a \ 'a" + assumes ln_one [simp]: "ln 1 = 0" + +definition powr :: "['a,'a] => 'a::ln" (infixr "powr" 80) + -- {*exponentation via ln and exp*} + where "x powr a \ if x = 0 then 0 else exp(a * ln x)" + + +instantiation real :: ln +begin + +definition ln_real :: "real \ real" + where "ln_real x = (THE u. exp u = x)" + +instance +by intro_classes (simp add: ln_real_def) + +end + +lemma powr_eq_0_iff [simp]: "w powr z = 0 \ w = 0" + by (simp add: powr_def) + +lemma ln_exp [simp]: + fixes x::real shows "ln (exp x) = x" + by (simp add: ln_real_def) + +lemma exp_ln [simp]: + fixes x::real shows "0 < x \ exp (ln x) = x" by (auto dest: exp_total) -lemma exp_ln_iff [simp]: "exp (ln x) = x \ 0 < x" +lemma exp_ln_iff [simp]: + fixes x::real shows "exp (ln x) = x \ 0 < x" by (metis exp_gt_zero exp_ln) -lemma ln_unique: "exp y = x \ ln x = y" +lemma ln_unique: + fixes x::real shows "exp y = x \ ln x = y" by (erule subst, rule ln_exp) -lemma ln_one [simp]: "ln 1 = 0" - by (rule ln_unique) simp - -lemma ln_mult: "0 < x \ 0 < y \ ln (x * y) = ln x + ln y" +lemma ln_mult: + fixes x::real shows "0 < x \ 0 < y \ ln (x * y) = ln x + ln y" by (rule ln_unique) (simp add: exp_add) -lemma ln_setprod: +lemma ln_setprod: + fixes f:: "'a => real" + shows "\finite I; \i. i \ I \ f i > 0\ \ ln(setprod f I) = setsum (\x. ln(f x)) I" by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos) -lemma ln_inverse: "0 < x \ ln (inverse x) = - ln x" +lemma ln_inverse: + fixes x::real shows "0 < x \ ln (inverse x) = - ln x" by (rule ln_unique) (simp add: exp_minus) -lemma ln_div: "0 < x \ 0 < y \ ln (x / y) = ln x - ln y" +lemma ln_div: + fixes x::real shows "0 < x \ 0 < y \ ln (x / y) = ln x - ln y" by (rule ln_unique) (simp add: exp_diff) lemma ln_realpow: "0 < x \ ln (x^n) = real n * ln x" by (rule ln_unique) (simp add: exp_real_of_nat_mult) -lemma ln_less_cancel_iff [simp]: "0 < x \ 0 < y \ ln x < ln y \ x < y" +lemma ln_less_cancel_iff [simp]: + fixes x::real shows "0 < x \ 0 < y \ ln x < ln y \ x < y" by (subst exp_less_cancel_iff [symmetric]) simp -lemma ln_le_cancel_iff [simp]: "0 < x \ 0 < y \ ln x \ ln y \ x \ y" +lemma ln_le_cancel_iff [simp]: + fixes x::real shows "0 < x \ 0 < y \ ln x \ ln y \ x \ y" by (simp add: linorder_not_less [symmetric]) -lemma ln_inj_iff [simp]: "0 < x \ 0 < y \ ln x = ln y \ x = y" +lemma ln_inj_iff [simp]: + fixes x::real shows "0 < x \ 0 < y \ ln x = ln y \ x = y" by (simp add: order_eq_iff) -lemma ln_add_one_self_le_self [simp]: "0 \ x \ ln (1 + x) \ x" +lemma ln_add_one_self_le_self [simp]: + fixes x::real shows "0 \ x \ ln (1 + x) \ x" apply (rule exp_le_cancel_iff [THEN iffD1]) apply (simp add: exp_ge_add_one_self_aux) done -lemma ln_less_self [simp]: "0 < x \ ln x < x" +lemma ln_less_self [simp]: + fixes x::real shows "0 < x \ ln x < x" by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all -lemma ln_ge_zero [simp]: "1 \ x \ 0 \ ln x" +lemma ln_ge_zero [simp]: + fixes x::real shows "1 \ x \ 0 \ ln x" using ln_le_cancel_iff [of 1 x] by simp -lemma ln_ge_zero_imp_ge_one: "0 \ ln x \ 0 < x \ 1 \ x" +lemma ln_ge_zero_imp_ge_one: + fixes x::real shows "0 \ ln x \ 0 < x \ 1 \ x" using ln_le_cancel_iff [of 1 x] by simp -lemma ln_ge_zero_iff [simp]: "0 < x \ 0 \ ln x \ 1 \ x" +lemma ln_ge_zero_iff [simp]: + fixes x::real shows "0 < x \ 0 \ ln x \ 1 \ x" using ln_le_cancel_iff [of 1 x] by simp -lemma ln_less_zero_iff [simp]: "0 < x \ ln x < 0 \ x < 1" +lemma ln_less_zero_iff [simp]: + fixes x::real shows "0 < x \ ln x < 0 \ x < 1" using ln_less_cancel_iff [of x 1] by simp -lemma ln_gt_zero: "1 < x \ 0 < ln x" +lemma ln_gt_zero: + fixes x::real shows "1 < x \ 0 < ln x" using ln_less_cancel_iff [of 1 x] by simp -lemma ln_gt_zero_imp_gt_one: "0 < ln x \ 0 < x \ 1 < x" +lemma ln_gt_zero_imp_gt_one: + fixes x::real shows "0 < ln x \ 0 < x \ 1 < x" using ln_less_cancel_iff [of 1 x] by simp -lemma ln_gt_zero_iff [simp]: "0 < x \ 0 < ln x \ 1 < x" +lemma ln_gt_zero_iff [simp]: + fixes x::real shows "0 < x \ 0 < ln x \ 1 < x" using ln_less_cancel_iff [of 1 x] by simp -lemma ln_eq_zero_iff [simp]: "0 < x \ ln x = 0 \ x = 1" +lemma ln_eq_zero_iff [simp]: + fixes x::real shows "0 < x \ ln x = 0 \ x = 1" using ln_inj_iff [of x 1] by simp -lemma ln_less_zero: "0 < x \ x < 1 \ ln x < 0" +lemma ln_less_zero: + fixes x::real shows "0 < x \ x < 1 \ ln x < 0" by simp -lemma ln_neg_is_const: "x \ 0 \ ln x = (THE x. False)" - by (auto simp add: ln_def intro!: arg_cong[where f=The]) - -lemma isCont_ln: assumes "x \ 0" shows "isCont ln x" +lemma ln_neg_is_const: + fixes x::real shows "x \ 0 \ ln x = (THE x. False)" + by (auto simp add: ln_real_def intro!: arg_cong[where f=The]) + +lemma isCont_ln: + fixes x::real assumes "x \ 0" shows "isCont ln x" proof cases assume "0 < x" moreover then have "isCont ln (exp (ln x))" @@ -1381,32 +1423,35 @@ intro!: exI[of _ "\x\"]) qed -lemma tendsto_ln [tendsto_intros]: +lemma tendsto_ln [tendsto_intros]: + fixes a::real shows "(f ---> a) F \ a \ 0 \ ((\x. ln (f x)) ---> ln a) F" by (rule isCont_tendsto_compose [OF isCont_ln]) lemma continuous_ln: - "continuous F f \ f (Lim F (\x. x)) \ 0 \ continuous F (\x. ln (f x))" + "continuous F f \ f (Lim F (\x. x)) \ 0 \ continuous F (\x. ln (f x :: real))" unfolding continuous_def by (rule tendsto_ln) lemma isCont_ln' [continuous_intros]: - "continuous (at x) f \ f x \ 0 \ continuous (at x) (\x. ln (f x))" + "continuous (at x) f \ f x \ 0 \ continuous (at x) (\x. ln (f x :: real))" unfolding continuous_at by (rule tendsto_ln) lemma continuous_within_ln [continuous_intros]: - "continuous (at x within s) f \ f x \ 0 \ continuous (at x within s) (\x. ln (f x))" + "continuous (at x within s) f \ f x \ 0 \ continuous (at x within s) (\x. ln (f x :: real))" unfolding continuous_within by (rule tendsto_ln) lemma continuous_on_ln [continuous_intros]: - "continuous_on s f \ (\x\s. f x \ 0) \ continuous_on s (\x. ln (f x))" + "continuous_on s f \ (\x\s. f x \ 0) \ continuous_on s (\x. ln (f x :: real))" unfolding continuous_on_def by (auto intro: tendsto_ln) -lemma DERIV_ln: "0 < x \ DERIV ln x :> inverse x" +lemma DERIV_ln: + fixes x::real shows "0 < x \ DERIV ln x :> inverse x" apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"]) apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln) done -lemma DERIV_ln_divide: "0 < x \ DERIV ln x :> 1 / x" +lemma DERIV_ln_divide: + fixes x::real shows "0 < x \ DERIV ln x :> 1 / x" by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse) declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros] @@ -1533,13 +1578,13 @@ unfolding power2_eq_square apply (rule mult_left_mono) using assms - apply (auto simp: ) + apply auto done show ?thesis apply (rule order_trans [OF norm_exp]) apply (rule order_trans [OF exp_bound]) using assms n - apply (auto simp: ) + apply auto done qed @@ -1549,7 +1594,8 @@ using exp_bound_lemma [of x] by simp -lemma ln_one_minus_pos_upper_bound: "0 <= x \ x < 1 \ ln (1 - x) <= - x" +lemma ln_one_minus_pos_upper_bound: + fixes x::real shows "0 <= x \ x < 1 \ ln (1 - x) <= - x" proof - assume a: "0 <= (x::real)" and b: "x < 1" have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)" @@ -1590,7 +1636,8 @@ apply auto done -lemma ln_one_plus_pos_lower_bound: "0 <= x \ x <= 1 \ x - x\<^sup>2 <= ln (1 + x)" +lemma ln_one_plus_pos_lower_bound: + fixes x::real shows "0 <= x \ x <= 1 \ x - x\<^sup>2 <= ln (1 + x)" proof - assume a: "0 <= x" and b: "x <= 1" have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)" @@ -1614,7 +1661,8 @@ qed lemma ln_one_minus_pos_lower_bound: - "0 <= x \ x <= (1 / 2) \ - x - 2 * x\<^sup>2 <= ln (1 - x)" + fixes x::real + shows "0 <= x \ x <= (1 / 2) \ - x - 2 * x\<^sup>2 <= ln (1 - x)" proof - assume a: "0 <= x" and b: "x <= (1 / 2)" from b have c: "x < 1" by auto @@ -1642,14 +1690,15 @@ by (rule order_trans) qed -lemma ln_add_one_self_le_self2: "-1 < x \ ln(1 + x) <= x" +lemma ln_add_one_self_le_self2: + fixes x::real shows "-1 < x \ ln(1 + x) <= x" apply (subgoal_tac "ln (1 + x) \ ln (exp x)", simp) apply (subst ln_le_cancel_iff) apply auto done lemma abs_ln_one_plus_x_minus_x_bound_nonneg: - "0 <= x \ x <= 1 \ abs(ln (1 + x) - x) <= x\<^sup>2" + fixes x::real shows "0 <= x \ x <= 1 \ abs(ln (1 + x) - x) <= x\<^sup>2" proof - assume x: "0 <= x" assume x1: "x <= 1" @@ -1672,7 +1721,7 @@ qed lemma abs_ln_one_plus_x_minus_x_bound_nonpos: - "-(1 / 2) <= x \ x <= 0 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" + fixes x::real shows "-(1 / 2) <= x \ x <= 0 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" proof - assume a: "-(1 / 2) <= x" assume b: "x <= 0" @@ -1692,7 +1741,7 @@ qed lemma abs_ln_one_plus_x_minus_x_bound: - "abs x <= 1 / 2 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" + fixes x::real shows "abs x <= 1 / 2 \ abs(ln (1 + x) - x) <= 2 * x\<^sup>2" apply (case_tac "0 <= x") apply (rule order_trans) apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg) @@ -1701,7 +1750,8 @@ apply auto done -lemma ln_x_over_x_mono: "exp 1 <= x \ x <= y \ (ln y / y) <= (ln x / x)" +lemma ln_x_over_x_mono: + fixes x::real shows "exp 1 <= x \ x <= y \ (ln y / y) <= (ln x / x)" proof - assume x: "exp 1 <= x" "x <= y" moreover have "0 < exp (1::real)" by simp @@ -1737,15 +1787,17 @@ finally show ?thesis using b by (simp add: field_simps) qed -lemma ln_le_minus_one: "0 < x \ ln x \ x - 1" +lemma ln_le_minus_one: + fixes x::real shows "0 < x \ ln x \ x - 1" using exp_ge_add_one_self[of "ln x"] by simp lemma ln_eq_minus_one: + fixes x::real assumes "0 < x" "ln x = x - 1" shows "x = 1" proof - let ?l = "\y. ln y - y + 1" - have D: "\x. 0 < x \ DERIV ?l x :> (1 / x - 1)" + have D: "\x::real. 0 < x \ DERIV ?l x :> (1 / x - 1)" by (auto intro!: derivative_eq_intros) show ?thesis @@ -1814,11 +1866,11 @@ by (simp add: Deriv.DERIV_iff2) qed -lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot" +lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot" by (rule filterlim_at_bot_at_right[where Q="\x. 0 < x" and P="\x. True" and g="exp"]) (auto simp: eventually_at_filter) -lemma ln_at_top: "LIM x at_top. ln x :> at_top" +lemma ln_at_top: "LIM x at_top. ln (x::real) :> at_top" by (rule filterlim_at_top_at_top[where Q="\x. 0 < x" and P="\x. True" and g="exp"]) (auto intro: eventually_gt_at_top) @@ -1846,10 +1898,6 @@ qed -definition powr :: "[real,real] => real" (infixr "powr" 80) - -- {*exponentation with real exponent*} - where "x powr a = exp(a * ln x)" - definition log :: "[real,real] => real" -- {*logarithm of @{term x} to base @{term a}*} where "log a x = ln x / ln a" @@ -1891,67 +1939,77 @@ lemma powr_one_eq_one [simp]: "1 powr a = 1" by (simp add: powr_def) -lemma powr_zero_eq_one [simp]: "x powr 0 = 1" +lemma powr_zero_eq_one [simp]: "x powr 0 = (if x=0 then 0 else 1)" by (simp add: powr_def) -lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)" - by (simp add: powr_def) +lemma powr_one_gt_zero_iff [simp]: + fixes x::real shows "(x powr 1 = x) = (0 \ x)" + by (auto simp: powr_def) declare powr_one_gt_zero_iff [THEN iffD2, simp] -lemma powr_mult: "0 < x \ 0 < y \ (x * y) powr a = (x powr a) * (y powr a)" +lemma powr_mult: + fixes x::real shows "0 \ x \ 0 \ y \ (x * y) powr a = (x powr a) * (y powr a)" by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left) -lemma powr_gt_zero [simp]: "0 < x powr a" +lemma powr_ge_pzero [simp]: + fixes x::real shows "0 <= x powr y" by (simp add: powr_def) -lemma powr_ge_pzero [simp]: "0 <= x powr y" - by (rule order_less_imp_le, rule powr_gt_zero) - -lemma powr_not_zero [simp]: "x powr a \ 0" - by (simp add: powr_def) - -lemma powr_divide: "0 < x \ 0 < y \ (x / y) powr a = (x powr a) / (y powr a)" +lemma powr_divide: + fixes x::real shows "0 < x \ 0 < y \ (x / y) powr a = (x powr a) / (y powr a)" apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult) apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse) done -lemma powr_divide2: "x powr a / x powr b = x powr (a - b)" +lemma powr_divide2: + fixes x::real shows "x powr a / x powr b = x powr (a - b)" apply (simp add: powr_def) apply (subst exp_diff [THEN sym]) apply (simp add: left_diff_distrib) done -lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)" +lemma powr_add: + fixes x::real shows "x powr (a + b) = (x powr a) * (x powr b)" by (simp add: powr_def exp_add [symmetric] distrib_right) -lemma powr_mult_base: "0 < x \x * x powr y = x powr (1 + y)" +lemma powr_mult_base: + fixes x::real shows "0 < x \x * x powr y = x powr (1 + y)" using assms by (auto simp: powr_add) -lemma powr_powr: "(x powr a) powr b = x powr (a * b)" +lemma powr_powr: + fixes x::real shows "(x powr a) powr b = x powr (a * b)" by (simp add: powr_def) -lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a" +lemma powr_powr_swap: + fixes x::real shows "(x powr a) powr b = (x powr b) powr a" by (simp add: powr_powr mult.commute) -lemma powr_minus: "x powr (-a) = inverse (x powr a)" +lemma powr_minus: + fixes x::real shows "x powr (-a) = inverse (x powr a)" by (simp add: powr_def exp_minus [symmetric]) -lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)" +lemma powr_minus_divide: + fixes x::real shows "x powr (-a) = 1/(x powr a)" by (simp add: divide_inverse powr_minus) -lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)" +lemma divide_powr_uminus: + fixes a::real shows "a / b powr c = a * b powr (- c)" by (simp add: powr_minus_divide) -lemma powr_less_mono: "a < b \ 1 < x \ x powr a < x powr b" +lemma powr_less_mono: + fixes x::real shows "a < b \ 1 < x \ x powr a < x powr b" by (simp add: powr_def) -lemma powr_less_cancel: "x powr a < x powr b \ 1 < x \ a < b" +lemma powr_less_cancel: + fixes x::real shows "x powr a < x powr b \ 1 < x \ a < b" by (simp add: powr_def) -lemma powr_less_cancel_iff [simp]: "1 < x \ (x powr a < x powr b) = (a < b)" +lemma powr_less_cancel_iff [simp]: + fixes x::real shows "1 < x \ (x powr a < x powr b) = (a < b)" by (blast intro: powr_less_cancel powr_less_mono) -lemma powr_le_cancel_iff [simp]: "1 < x \ (x powr a \ x powr b) = (a \ b)" +lemma powr_le_cancel_iff [simp]: + fixes x::real shows "1 < x \ (x powr a \ x powr b) = (a \ b)" by (simp add: linorder_not_less [symmetric]) lemma log_ln: "ln x = log (exp(1)) x" @@ -2007,6 +2065,9 @@ lemma log_divide: "0 < a \ a \ 1 \ 0 < x \ 0 < y \ log a (x/y) = log a x - log a y" by (simp add: log_mult divide_inverse log_inverse) +lemma powr_gt_zero [simp]: "0 < x powr a \ (x::real) \ 0" + by (simp add: powr_def) + lemma log_add_eq_powr: "0 < b \ b \ 1 \ 0 < x \ log b x + y = log b (x * b powr y)" and add_log_eq_powr: "0 < b \ b \ 1 \ 0 < x \ y + log b x = log b (b powr y * x)" and log_minus_eq_powr: "0 < b \ b \ 1 \ 0 < x \ log b x - y = log b (x * b powr -y)" @@ -2071,14 +2132,18 @@ lemma le_log_iff: assumes "1 < b" "x > 0" - shows "y \ log b x \ b powr y \ x" - by (metis assms(1) assms(2) dual_order.strict_trans powr_le_cancel_iff powr_log_cancel - powr_one_eq_one powr_one_gt_zero_iff) + shows "y \ log b x \ b powr y \ (x::real)" + using assms + apply auto + apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff + powr_log_cancel zero_less_one) + apply (metis not_less order.trans order_refl powr_le_cancel_iff powr_log_cancel zero_le_one) + done lemma less_log_iff: assumes "1 < b" "x > 0" shows "y < log b x \ b powr y < x" - by (metis assms(1) assms(2) dual_order.strict_trans less_irrefl powr_less_cancel_iff + by (metis assms dual_order.strict_trans less_irrefl powr_less_cancel_iff powr_log_cancel zero_less_one) lemma @@ -2136,22 +2201,28 @@ else Code.abort (STR ''op powr with non-integer exponent'') (\_. b powr i))" by (auto simp: powr_int) -lemma powr_one: "0 < x \ x powr 1 = x" - using powr_realpow [of x 1] by simp - -lemma powr_numeral: "0 < x \ x powr numeral n = x ^ numeral n" +lemma powr_one: + fixes x::real shows "0 \ x \ x powr 1 = x" + using powr_realpow [of x 1] + by simp + +lemma powr_numeral: + fixes x::real shows "0 < x \ x powr numeral n = x ^ numeral n" by (fact powr_realpow_numeral) -lemma powr_neg_one: "0 < x \ x powr - 1 = 1 / x" +lemma powr_neg_one: + fixes x::real shows "0 < x \ x powr - 1 = 1 / x" using powr_int [of x "- 1"] by simp -lemma powr_neg_numeral: "0 < x \ x powr - numeral n = 1 / x ^ numeral n" +lemma powr_neg_numeral: + fixes x::real shows "0 < x \ x powr - numeral n = 1 / x ^ numeral n" using powr_int [of x "- numeral n"] by simp lemma root_powr_inverse: "0 < n \ 0 < x \ root n x = x powr (1/n)" by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr) -lemma ln_powr: "ln (x powr y) = y * ln x" +lemma ln_powr: + fixes x::real shows "x \ 0 \ ln (x powr y) = y * ln x" by (simp add: powr_def) lemma ln_root: "\ n > 0; b > 0 \ \ ln (root n b) = ln b / n" @@ -2163,7 +2234,7 @@ lemma log_root: "\ n > 0; a > 0 \ \ log b (root n a) = log b a / n" by(simp add: log_def ln_root) -lemma log_powr: "log b (x powr y) = y * log b x" +lemma log_powr: "x \ 0 \ log b (x powr y) = y * log b x" by (simp add: log_def ln_powr) lemma log_nat_power: "0 < x \ log b (x^n) = real n * log b x" @@ -2175,65 +2246,58 @@ lemma log_base_pow: "0 < a \ log (a ^ n) x = log a x / n" by (simp add: log_def ln_realpow) -lemma log_base_powr: "log (a powr b) x = log a x / b" +lemma log_base_powr: "a \ 0 \ log (a powr b) x = log a x / b" by (simp add: log_def ln_powr) lemma log_base_root: "\ n > 0; b > 0 \ \ log (root n b) x = n * (log b x)" by(simp add: log_def ln_root) -lemma ln_bound: "1 <= x ==> ln x <= x" +lemma ln_bound: + fixes x::real shows "1 <= x ==> ln x <= x" apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1") apply simp apply (rule ln_add_one_self_le_self, simp) done -lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b" +lemma powr_mono: + fixes x::real shows "a <= b ==> 1 <= x ==> x powr a <= x powr b" apply (cases "x = 1", simp) apply (cases "a = b", simp) apply (rule order_less_imp_le) apply (rule powr_less_mono, auto) done -lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a" - apply (subst powr_zero_eq_one [THEN sym]) - apply (rule powr_mono, assumption+) - done - -lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a" - apply (unfold powr_def) - apply (rule exp_less_mono) - apply (rule mult_strict_left_mono) - apply (subst ln_less_cancel_iff, assumption) - apply (rule order_less_trans) - prefer 2 - apply assumption+ - done - -lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a" - apply (unfold powr_def) - apply (rule exp_less_mono) - apply (rule mult_strict_left_mono_neg) - apply (subst ln_less_cancel_iff) - apply assumption - apply (rule order_less_trans) - prefer 2 - apply assumption+ - done - -lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a" +lemma ge_one_powr_ge_zero: + fixes x::real shows "1 <= x ==> 0 <= a ==> 1 <= x powr a" +using powr_mono by fastforce + +lemma powr_less_mono2: + fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a" + by (simp add: powr_def) + + +lemma powr_less_mono2_neg: + fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a" + by (simp add: powr_def) + +lemma powr_mono2: + fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a" apply (case_tac "a = 0", simp) apply (case_tac "x = y", simp) apply (metis less_eq_real_def powr_less_mono2) done -lemma powr_inj: "0 < a \ a \ 1 \ a powr x = a powr y \ x = y" +lemma powr_inj: + fixes x::real shows "0 < a \ a \ 1 \ a powr x = a powr y \ x = y" unfolding powr_def exp_inj_iff by simp -lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a" - by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute - powr_gt_zero) +lemma ln_powr_bound: + fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a" +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) + lemma ln_powr_bound2: + fixes x::real assumes "1 < x" and "0 < a" shows "(ln x) powr a <= (a powr a) * x" proof - @@ -2244,7 +2308,7 @@ finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a" by (metis assms less_imp_le ln_gt_zero powr_mono2) also have "... = (a powr a) * ((x powr (1 / a)) powr a)" - by (metis assms(2) powr_mult powr_gt_zero) + using assms powr_mult by auto also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)" by (rule powr_powr) also have "... = x" using assms @@ -2252,37 +2316,56 @@ finally show ?thesis . qed -lemma tendsto_powr [tendsto_intros]: - "\(f ---> a) F; (g ---> b) F; a \ 0\ \ ((\x. f x powr g x) ---> a powr b) F" - unfolding powr_def by (intro tendsto_intros) +lemma tendsto_powr [tendsto_intros]: (*FIXME a mess, suggests a general rule about exceptions*) + fixes a::real + shows "\(f ---> a) F; (g ---> b) F; a \ 0\ \ ((\x. f x powr g x) ---> a powr b) F" + apply (simp add: powr_def) + apply (simp add: tendsto_def) + apply (simp add: Topological_Spaces.eventually_conj_iff ) + apply safe + apply (case_tac "0 \ S") + apply (auto simp: ) + apply (subgoal_tac "\T. open T & a : T & 0 \ T") + apply clarify + apply (drule_tac x="T" in spec) + apply (simp add: ) + apply (metis (mono_tags, lifting) eventually_mono) + apply (simp add: separation_t1) + apply (subgoal_tac "((\x. exp (g x * ln (f x))) ---> exp (b * ln a)) F") + apply (simp add: tendsto_def) + apply (metis (mono_tags, lifting) eventually_mono) + apply (simp add: tendsto_def [symmetric]) + apply (intro tendsto_intros) + apply (auto simp: ) + done lemma continuous_powr: assumes "continuous F f" and "continuous F g" and "f (Lim F (\x. x)) \ 0" - shows "continuous F (\x. (f x) powr (g x))" + shows "continuous F (\x. (f x) powr (g x :: real))" using assms unfolding continuous_def by (rule tendsto_powr) lemma continuous_at_within_powr[continuous_intros]: assumes "continuous (at a within s) f" and "continuous (at a within s) g" and "f a \ 0" - shows "continuous (at a within s) (\x. (f x) powr (g x))" + shows "continuous (at a within s) (\x. (f x) powr (g x :: real))" using assms unfolding continuous_within by (rule tendsto_powr) lemma isCont_powr[continuous_intros, simp]: - assumes "isCont f a" "isCont g a" "f a \ 0" + assumes "isCont f a" "isCont g a" "f a \ (0::real)" shows "isCont (\x. (f x) powr g x) a" using assms unfolding continuous_at by (rule tendsto_powr) lemma continuous_on_powr[continuous_intros]: - assumes "continuous_on s f" "continuous_on s g" and "\x\s. f x \ 0" + assumes "continuous_on s f" "continuous_on s g" and "\x\s. f x \ (0::real)" shows "continuous_on s (\x. (f x) powr (g x))" using assms unfolding continuous_on_def by (fast intro: tendsto_powr) (* FIXME: generalize by replacing d by with g x and g ---> d? *) lemma tendsto_zero_powrI: - assumes "eventually (\x. 0 < f x ) F" and "(f ---> 0) F" + assumes "eventually (\x. 0 < f x ) F" and "(f ---> (0::real)) F" and "0 < d" shows "((\x. f x powr d) ---> 0) F" proof (rule tendstoI) @@ -2303,14 +2386,17 @@ lemma tendsto_neg_powr: assumes "s < 0" and "LIM x F. f x :> at_top" - shows "((\x. f x powr s) ---> 0) F" + shows "((\x. f x powr s) ---> (0::real)) F" proof (rule tendstoI) fix e :: real assume "0 < e" def Z \ "e powr (1 / s)" + have "Z > 0" + using Z_def `0 < e` by auto from assms have "eventually (\x. Z < f x) F" by (simp add: filterlim_at_top_dense) moreover - from assms have "\x. Z < x \ x powr s < Z powr s" + from assms have "\x::real. Z < x \ x powr s < Z powr s" + using `Z > 0` by (auto simp: Z_def intro!: powr_less_mono2_neg) with assms `0 < e` have "\x. Z < x \ dist (x powr s) 0 < e" by (simp add: powr_powr Z_def dist_real_def) @@ -2318,13 +2404,11 @@ show "eventually (\x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1) qed -(* it is funny that this isn't in the library! It could go in Transcendental *) lemma tendsto_exp_limit_at_right: fixes x :: real shows "((\y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)" proof cases assume "x \ 0" - have "((\y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)" by (auto intro!: derivative_eq_intros) then have "((\y. ln (1 + x * y) / y) ---> x) (at 0)" @@ -2335,7 +2419,10 @@ proof (rule filterlim_mono_eventually) show "eventually (\xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)" unfolding eventually_at_right[OF zero_less_one] - using `x \ 0` by (intro exI[of _ "1 / \x\"]) (auto simp: field_simps powr_def) + using `x \ 0` + apply (intro exI[of _ "1 / \x\"]) + apply (auto simp: field_simps powr_def abs_if) + by (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one) qed (simp_all add: at_eq_sup_left_right) qed simp @@ -4445,7 +4532,7 @@ lemma arcsin_less_mono: "abs x \ 1 \ abs y \ 1 \ arcsin x < arcsin y \ x < y" apply (rule trans [OF sin_mono_less_eq [symmetric]]) using arcsin_ubound arcsin_lbound - apply (auto simp: ) + apply auto done lemma arcsin_le_mono: "abs x \ 1 \ abs y \ 1 \ arcsin x \ arcsin y \ x \ y" @@ -4460,7 +4547,7 @@ lemma arccos_less_mono: "abs x \ 1 \ abs y \ 1 \ (arccos x < arccos y \ y < x)" apply (rule trans [OF cos_mono_less_eq [symmetric]]) using arccos_ubound arccos_lbound - apply (auto simp: ) + apply auto done lemma arccos_le_mono: "abs x \ 1 \ abs y \ 1 \ arccos x \ arccos y \ y \ x" @@ -5009,4 +5096,253 @@ qed qed + +subsection{*Basics about polynomial functions: extremal behaviour and root counts*} +(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*) + +lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*) + fixes x :: "'a::idom" + assumes "1 \ n" + shows "(\i\n. a i * x^i) - (\i\n. a i * y^i) = + (x - y) * (\ji=Suc j..n. a i * y^(i - j - 1)) * x^j)" +proof - + have h: "bij_betw (\(i,j). (j,i)) ((SIGMA i : atMost n. lessThan i)) (SIGMA j : lessThan n. {Suc j..n})" + by (auto simp: bij_betw_def inj_on_def) + have "(\i\n. a i * x^i) - (\i\n. a i * y^i) = + (\i\n. a i * (x^i - y^i))" + by (simp add: right_diff_distrib setsum_subtractf) + also have "... = (\i\n. a i * (x - y) * (\ji\n. \j(i,j) \ (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))" + by (simp add: setsum.Sigma) + also have "... = (\(j,i) \ (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))" + by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong) + also have "... = (\ji=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))" + by (simp add: setsum.Sigma) + also have "... = (x - y) * (\ji=Suc j..n. a i * y^(i - j - 1)) * x^j)" + by (simp add: setsum_right_distrib mult_ac) + finally show ?thesis . +qed + +lemma polyfun_diff_alt: (*COMPLEX_SUB_POLYFUN_ALT in HOL Light*) + fixes x :: "'a::idom" + assumes "1 \ n" + shows "(\i\n. a i * x^i) - (\i\n. a i * y^i) = + (x - y) * ((\jki. i - (j + 1)) {Suc j..n} (lessThan (n-j))" + apply (auto simp: bij_betw_def inj_on_def) + apply (rule_tac x="x + Suc j" in image_eqI) + apply (auto simp: ) + done + have "(\i=Suc j..n. a i * y^(i - j - 1)) = (\kb. \z. (\i\n. c(i) * z^i) = (z - a) * (\ii\n. c(i) * a^i)" +proof (cases "n=0") + case True then show ?thesis + by simp +next + case False + have "(\b. \z. (\i\n. c(i) * z^i) = (z - a) * (\ii\n. c(i) * a^i)) = + (\b. \z. (\i\n. c(i) * z^i) - (\i\n. c(i) * a^i) = (z - a) * (\ib. \z. (z - a) * (\ji = Suc j..n. c i * a^(i - Suc j)) * z^j) = (z - a) * (\ii\n. c(i) * a^i) = 0" + obtains b where "\z. (\i\n. c(i) * z^i) = (z - a) * (\i 'a::real_normed_div_algebra" + shows "isCont (\w. \i\n. c i * w^i) a" + by simp + +lemma zero_polynom_imp_zero_coeffs: + fixes c :: "nat \ 'a::{ab_semigroup_mult,real_normed_div_algebra}" + assumes "\w. (\i\n. c i * w^i) = 0" "k \ n" + shows "c k = 0" +using assms +proof (induction n arbitrary: c k) + case 0 + then show ?case + by simp +next + case (Suc n c k) + have [simp]: "c 0 = 0" using Suc.prems(1) [of 0] + by simp + { fix w + have "(\i\Suc n. c i * w^i) = (\i\n. c (Suc i) * w ^ Suc i)" + unfolding Set_Interval.setsum_atMost_Suc_shift + by simp + also have "... = w * (\i\n. c (Suc i) * w^i)" + by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc) + finally have "(\i\Suc n. c i * w^i) = w * (\i\n. c (Suc i) * w^i)" . + } + then have wnz: "\w. w \ 0 \ (\i\n. c (Suc i) * w^i) = 0" + using Suc by auto + then have "(\h. \i\n. c (Suc i) * h^i) -- 0 --> 0" + by (simp cong: LIM_cong) --{*the case @{term"w=0"} by continuity}*} + then have "(\i\n. c (Suc i) * 0^i) = 0" + using isCont_polynom [of 0 "\i. c (Suc i)" n] LIM_unique + by (force simp add: Limits.isCont_iff) + then have "\w. (\i\n. c (Suc i) * w^i) = 0" using wnz + by metis + then have "\i. i\n \ c (Suc i) = 0" + using Suc.IH [of "\i. c (Suc i)"] + by blast + then show ?case using `k \ Suc n` + by (cases k) auto +qed + +lemma polyfun_rootbound: (*COMPLEX_POLYFUN_ROOTBOUND in HOL Light*) + fixes c :: "nat \ 'a::{idom,real_normed_div_algebra}" + assumes "c k \ 0" "k\n" + shows "finite {z. (\i\n. c(i) * z^i) = 0} \ + card {z. (\i\n. c(i) * z^i) = 0} \ n" +using assms +proof (induction n arbitrary: c k) + case 0 + then show ?case + by simp +next + case (Suc m c k) + let ?succase = ?case + show ?case + proof (cases "{z. (\i\Suc m. c(i) * z^i) = 0} = {}") + case True + then show ?succase + by simp + next + case False + then obtain z0 where z0: "(\i\Suc m. c(i) * z0^i) = 0" + by blast + then obtain b where b: "\w. (\i\Suc m. c i * w^i) = (w - z0) * (\i\m. b i * w^i)" + using polyfun_linear_factor_root [OF z0, unfolded lessThan_Suc_atMost] + by blast + then have eq: "{z. (\i\Suc m. c(i) * z^i) = 0} = insert z0 {z. (\i\m. b(i) * z^i) = 0}" + by auto + have "~(\k\m. b k = 0)" + proof + assume [simp]: "\k\m. b k = 0" + then have "\w. (\i\m. b i * w^i) = 0" + by simp + then have "\w. (\i\Suc m. c i * w^i) = 0" + using b by simp + then have "\k. k \ Suc m \ c k = 0" + using zero_polynom_imp_zero_coeffs + by blast + then show False using Suc.prems + by blast + qed + then obtain k' where bk': "b k' \ 0" "k' \ m" + by blast + show ?succase + using Suc.IH [of b k'] bk' + by (simp add: eq card_insert_if del: setsum_atMost_Suc) + qed +qed + +lemma + fixes c :: "nat \ 'a::{idom,real_normed_div_algebra}" + assumes "c k \ 0" "k\n" + shows polyfun_roots_finite: "finite {z. (\i\n. c(i) * z^i) = 0}" + and polyfun_roots_card: "card {z. (\i\n. c(i) * z^i) = 0} \ n" +using polyfun_rootbound assms + by auto + +lemma polyfun_finite_roots: (*COMPLEX_POLYFUN_FINITE_ROOTS in HOL Light*) + fixes c :: "nat \ 'a::{idom,real_normed_div_algebra}" + shows "finite {x. (\i\n. c i * x^i) = 0} \ (\i\n. c i \ 0)" + (is "?lhs = ?rhs") +proof + assume ?lhs + moreover + { assume "\i\n. c i = 0" + then have "\x. (\i\n. c i * x^i) = 0" + by simp + then have "\ finite {x. (\i\n. c i * x^i) = 0}" + using ex_new_if_finite [OF infinite_UNIV_char_0 [where 'a='a]] + by auto + } + ultimately show ?rhs + by metis +next + assume ?rhs + then show ?lhs + using polyfun_rootbound + by blast +qed + +lemma polyfun_eq_0: (*COMPLEX_POLYFUN_EQ_0 in HOL Light*) + fixes c :: "nat \ 'a::{idom,real_normed_div_algebra}" + shows "(\x. (\i\n. c i * x^i) = 0) \ (\i\n. c i = 0)" + using zero_polynom_imp_zero_coeffs by auto + +lemma polyfun_eq_coeffs: + fixes c :: "nat \ 'a::{idom,real_normed_div_algebra}" + shows "(\x. (\i\n. c i * x^i) = (\i\n. d i * x^i)) \ (\i\n. c i = d i)" +proof - + have "(\x. (\i\n. c i * x^i) = (\i\n. d i * x^i)) \ (\x. (\i\n. (c i - d i) * x^i) = 0)" + by (simp add: left_diff_distrib Groups_Big.setsum_subtractf) + also have "... \ (\i\n. c i - d i = 0)" + by (rule polyfun_eq_0) + finally show ?thesis + by simp +qed + +lemma polyfun_eq_const: (*COMPLEX_POLYFUN_EQ_CONST in HOL Light*) + fixes c :: "nat \ 'a::{idom,real_normed_div_algebra}" + shows "(\x. (\i\n. c i * x^i) = k) \ c 0 = k \ (\i \ {1..n}. c i = 0)" + (is "?lhs = ?rhs") +proof - + have *: "\x. (\i\n. (if i=0 then k else 0) * x^i) = k" + by (induct n) auto + show ?thesis + proof + assume ?lhs + with * have "(\i\n. c i = (if i=0 then k else 0))" + by (simp add: polyfun_eq_coeffs [symmetric]) + then show ?rhs + by simp + next + assume ?rhs then show ?lhs + by (induct n) auto + qed +qed + +lemma root_polyfun: + fixes z:: "'a::idom" + assumes "1 \ n" + shows "z^n = a \ (\i\n. (if i = 0 then -a else if i=n then 1 else 0) * z^i) = 0" + using assms + by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric]) + +lemma + fixes zz :: "'a::{idom,real_normed_div_algebra}" + assumes "1 \ n" + shows finite_roots_unity: "finite {z::'a. z^n = 1}" + and card_roots_unity: "card {z::'a. z^n = 1} \ n" + using polyfun_rootbound [of "\i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms + by (auto simp add: root_polyfun [OF assms]) + end