src/HOL/Transcendental.thy
 changeset 60017 b785d6d06430 parent 59869 3b5b53eb78ba child 60020 065ecea354d0
```     1.1 --- a/src/HOL/Transcendental.thy	Thu Apr 09 20:42:38 2015 +0200
1.2 +++ b/src/HOL/Transcendental.thy	Sat Apr 11 11:56:40 2015 +0100
1.3 @@ -1285,88 +1285,130 @@
1.4
1.5  subsection {* Natural Logarithm *}
1.6
1.7 -definition ln :: "real \<Rightarrow> real"
1.8 -  where "ln x = (THE u. exp u = x)"
1.9 -
1.10 -lemma ln_exp [simp]: "ln (exp x) = x"
1.11 -  by (simp add: ln_def)
1.12 -
1.13 -lemma exp_ln [simp]: "0 < x \<Longrightarrow> exp (ln x) = x"
1.14 +class ln = real_normed_algebra_1 + banach +
1.15 +  fixes ln :: "'a \<Rightarrow> 'a"
1.16 +  assumes ln_one [simp]: "ln 1 = 0"
1.17 +
1.18 +definition powr :: "['a,'a] => 'a::ln"     (infixr "powr" 80)
1.19 +  -- {*exponentation via ln and exp*}
1.20 +  where "x powr a \<equiv> if x = 0 then 0 else exp(a * ln x)"
1.21 +
1.22 +
1.23 +instantiation real :: ln
1.24 +begin
1.25 +
1.26 +definition ln_real :: "real \<Rightarrow> real"
1.27 +  where "ln_real x = (THE u. exp u = x)"
1.28 +
1.29 +instance
1.30 +by intro_classes (simp add: ln_real_def)
1.31 +
1.32 +end
1.33 +
1.34 +lemma powr_eq_0_iff [simp]: "w powr z = 0 \<longleftrightarrow> w = 0"
1.35 +  by (simp add: powr_def)
1.36 +
1.37 +lemma ln_exp [simp]:
1.38 +  fixes x::real shows "ln (exp x) = x"
1.39 +  by (simp add: ln_real_def)
1.40 +
1.41 +lemma exp_ln [simp]:
1.42 +  fixes x::real shows "0 < x \<Longrightarrow> exp (ln x) = x"
1.43    by (auto dest: exp_total)
1.44
1.45 -lemma exp_ln_iff [simp]: "exp (ln x) = x \<longleftrightarrow> 0 < x"
1.46 +lemma exp_ln_iff [simp]:
1.47 +  fixes x::real shows "exp (ln x) = x \<longleftrightarrow> 0 < x"
1.48    by (metis exp_gt_zero exp_ln)
1.49
1.50 -lemma ln_unique: "exp y = x \<Longrightarrow> ln x = y"
1.51 +lemma ln_unique:
1.52 +  fixes x::real shows "exp y = x \<Longrightarrow> ln x = y"
1.53    by (erule subst, rule ln_exp)
1.54
1.55 -lemma ln_one [simp]: "ln 1 = 0"
1.56 -  by (rule ln_unique) simp
1.57 -
1.58 -lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
1.59 +lemma ln_mult:
1.60 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
1.62
1.63 -lemma ln_setprod:
1.64 +lemma ln_setprod:
1.65 +  fixes f:: "'a => real"
1.66 +  shows
1.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"
1.68    by (induction I rule: finite_induct) (auto simp: ln_mult setprod_pos)
1.69
1.70 -lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.71 +lemma ln_inverse:
1.72 +  fixes x::real shows "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
1.73    by (rule ln_unique) (simp add: exp_minus)
1.74
1.75 -lemma ln_div: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
1.76 +lemma ln_div:
1.77 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x / y) = ln x - ln y"
1.78    by (rule ln_unique) (simp add: exp_diff)
1.79
1.80  lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
1.81    by (rule ln_unique) (simp add: exp_real_of_nat_mult)
1.82
1.83 -lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.84 +lemma ln_less_cancel_iff [simp]:
1.85 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
1.86    by (subst exp_less_cancel_iff [symmetric]) simp
1.87
1.88 -lemma ln_le_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
1.89 +lemma ln_le_cancel_iff [simp]:
1.90 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x \<le> ln y \<longleftrightarrow> x \<le> y"
1.91    by (simp add: linorder_not_less [symmetric])
1.92
1.93 -lemma ln_inj_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
1.94 +lemma ln_inj_iff [simp]:
1.95 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x = ln y \<longleftrightarrow> x = y"
1.97
1.98 -lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
1.100 +  fixes x::real shows "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
1.101    apply (rule exp_le_cancel_iff [THEN iffD1])
1.103    done
1.104
1.105 -lemma ln_less_self [simp]: "0 < x \<Longrightarrow> ln x < x"
1.106 +lemma ln_less_self [simp]:
1.107 +  fixes x::real shows "0 < x \<Longrightarrow> ln x < x"
1.108    by (rule order_less_le_trans [where y="ln (1 + x)"]) simp_all
1.109
1.110 -lemma ln_ge_zero [simp]: "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
1.111 +lemma ln_ge_zero [simp]:
1.112 +  fixes x::real shows "1 \<le> x \<Longrightarrow> 0 \<le> ln x"
1.113    using ln_le_cancel_iff [of 1 x] by simp
1.114
1.115 -lemma ln_ge_zero_imp_ge_one: "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
1.116 +lemma ln_ge_zero_imp_ge_one:
1.117 +  fixes x::real shows "0 \<le> ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 \<le> x"
1.118    using ln_le_cancel_iff [of 1 x] by simp
1.119
1.120 -lemma ln_ge_zero_iff [simp]: "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
1.121 +lemma ln_ge_zero_iff [simp]:
1.122 +  fixes x::real shows "0 < x \<Longrightarrow> 0 \<le> ln x \<longleftrightarrow> 1 \<le> x"
1.123    using ln_le_cancel_iff [of 1 x] by simp
1.124
1.125 -lemma ln_less_zero_iff [simp]: "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
1.126 +lemma ln_less_zero_iff [simp]:
1.127 +  fixes x::real shows "0 < x \<Longrightarrow> ln x < 0 \<longleftrightarrow> x < 1"
1.128    using ln_less_cancel_iff [of x 1] by simp
1.129
1.130 -lemma ln_gt_zero: "1 < x \<Longrightarrow> 0 < ln x"
1.131 +lemma ln_gt_zero:
1.132 +  fixes x::real shows "1 < x \<Longrightarrow> 0 < ln x"
1.133    using ln_less_cancel_iff [of 1 x] by simp
1.134
1.135 -lemma ln_gt_zero_imp_gt_one: "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
1.136 +lemma ln_gt_zero_imp_gt_one:
1.137 +  fixes x::real shows "0 < ln x \<Longrightarrow> 0 < x \<Longrightarrow> 1 < x"
1.138    using ln_less_cancel_iff [of 1 x] by simp
1.139
1.140 -lemma ln_gt_zero_iff [simp]: "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
1.141 +lemma ln_gt_zero_iff [simp]:
1.142 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < ln x \<longleftrightarrow> 1 < x"
1.143    using ln_less_cancel_iff [of 1 x] by simp
1.144
1.145 -lemma ln_eq_zero_iff [simp]: "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
1.146 +lemma ln_eq_zero_iff [simp]:
1.147 +  fixes x::real shows "0 < x \<Longrightarrow> ln x = 0 \<longleftrightarrow> x = 1"
1.148    using ln_inj_iff [of x 1] by simp
1.149
1.150 -lemma ln_less_zero: "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
1.151 +lemma ln_less_zero:
1.152 +  fixes x::real shows "0 < x \<Longrightarrow> x < 1 \<Longrightarrow> ln x < 0"
1.153    by simp
1.154
1.155 -lemma ln_neg_is_const: "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
1.156 -  by (auto simp add: ln_def intro!: arg_cong[where f=The])
1.157 -
1.158 -lemma isCont_ln: assumes "x \<noteq> 0" shows "isCont ln x"
1.159 +lemma ln_neg_is_const:
1.160 +  fixes x::real shows "x \<le> 0 \<Longrightarrow> ln x = (THE x. False)"
1.161 +  by (auto simp add: ln_real_def intro!: arg_cong[where f=The])
1.162 +
1.163 +lemma isCont_ln:
1.164 +  fixes x::real assumes "x \<noteq> 0" shows "isCont ln x"
1.165  proof cases
1.166    assume "0 < x"
1.167    moreover then have "isCont ln (exp (ln x))"
1.168 @@ -1381,32 +1423,35 @@
1.169                  intro!: exI[of _ "\<bar>x\<bar>"])
1.170  qed
1.171
1.172 -lemma tendsto_ln [tendsto_intros]:
1.173 +lemma tendsto_ln [tendsto_intros]:
1.174 +  fixes a::real shows
1.175    "(f ---> a) F \<Longrightarrow> a \<noteq> 0 \<Longrightarrow> ((\<lambda>x. ln (f x)) ---> ln a) F"
1.176    by (rule isCont_tendsto_compose [OF isCont_ln])
1.177
1.178  lemma continuous_ln:
1.179 -  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x))"
1.180 +  "continuous F f \<Longrightarrow> f (Lim F (\<lambda>x. x)) \<noteq> 0 \<Longrightarrow> continuous F (\<lambda>x. ln (f x :: real))"
1.181    unfolding continuous_def by (rule tendsto_ln)
1.182
1.183  lemma isCont_ln' [continuous_intros]:
1.184 -  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x))"
1.185 +  "continuous (at x) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x) (\<lambda>x. ln (f x :: real))"
1.186    unfolding continuous_at by (rule tendsto_ln)
1.187
1.188  lemma continuous_within_ln [continuous_intros]:
1.189 -  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x))"
1.190 +  "continuous (at x within s) f \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow> continuous (at x within s) (\<lambda>x. ln (f x :: real))"
1.191    unfolding continuous_within by (rule tendsto_ln)
1.192
1.193  lemma continuous_on_ln [continuous_intros]:
1.194 -  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x))"
1.195 +  "continuous_on s f \<Longrightarrow> (\<forall>x\<in>s. f x \<noteq> 0) \<Longrightarrow> continuous_on s (\<lambda>x. ln (f x :: real))"
1.196    unfolding continuous_on_def by (auto intro: tendsto_ln)
1.197
1.198 -lemma DERIV_ln: "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
1.199 +lemma DERIV_ln:
1.200 +  fixes x::real shows "0 < x \<Longrightarrow> DERIV ln x :> inverse x"
1.201    apply (rule DERIV_inverse_function [where f=exp and a=0 and b="x+1"])
1.202    apply (auto intro: DERIV_cong [OF DERIV_exp exp_ln] isCont_ln)
1.203    done
1.204
1.205 -lemma DERIV_ln_divide: "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
1.206 +lemma DERIV_ln_divide:
1.207 +  fixes x::real shows "0 < x \<Longrightarrow> DERIV ln x :> 1 / x"
1.208    by (rule DERIV_ln[THEN DERIV_cong], simp, simp add: divide_inverse)
1.209
1.210  declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
1.211 @@ -1533,13 +1578,13 @@
1.212      unfolding power2_eq_square
1.213      apply (rule mult_left_mono)
1.214      using assms
1.215 -    apply (auto simp: )
1.216 +    apply auto
1.217      done
1.218    show ?thesis
1.219      apply (rule order_trans [OF norm_exp])
1.220      apply (rule order_trans [OF exp_bound])
1.221      using assms n
1.222 -    apply (auto simp: )
1.223 +    apply auto
1.224      done
1.225  qed
1.226
1.227 @@ -1549,7 +1594,8 @@
1.228  using exp_bound_lemma [of x]
1.229  by simp
1.230
1.231 -lemma ln_one_minus_pos_upper_bound: "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
1.232 +lemma ln_one_minus_pos_upper_bound:
1.233 +  fixes x::real shows "0 <= x \<Longrightarrow> x < 1 \<Longrightarrow> ln (1 - x) <= - x"
1.234  proof -
1.235    assume a: "0 <= (x::real)" and b: "x < 1"
1.236    have "(1 - x) * (1 + x + x\<^sup>2) = (1 - x^3)"
1.237 @@ -1590,7 +1636,8 @@
1.238    apply auto
1.239  done
1.240
1.241 -lemma ln_one_plus_pos_lower_bound: "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
1.242 +lemma ln_one_plus_pos_lower_bound:
1.243 +  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> x - x\<^sup>2 <= ln (1 + x)"
1.244  proof -
1.245    assume a: "0 <= x" and b: "x <= 1"
1.246    have "exp (x - x\<^sup>2) = exp x / exp (x\<^sup>2)"
1.247 @@ -1614,7 +1661,8 @@
1.248  qed
1.249
1.250  lemma ln_one_minus_pos_lower_bound:
1.251 -  "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
1.252 +  fixes x::real
1.253 +  shows "0 <= x \<Longrightarrow> x <= (1 / 2) \<Longrightarrow> - x - 2 * x\<^sup>2 <= ln (1 - x)"
1.254  proof -
1.255    assume a: "0 <= x" and b: "x <= (1 / 2)"
1.256    from b have c: "x < 1" by auto
1.257 @@ -1642,14 +1690,15 @@
1.258      by (rule order_trans)
1.259  qed
1.260
1.261 -lemma ln_add_one_self_le_self2: "-1 < x \<Longrightarrow> ln(1 + x) <= x"
1.263 +  fixes x::real shows "-1 < x \<Longrightarrow> ln(1 + x) <= x"
1.264    apply (subgoal_tac "ln (1 + x) \<le> ln (exp x)", simp)
1.265    apply (subst ln_le_cancel_iff)
1.266    apply auto
1.267    done
1.268
1.269  lemma abs_ln_one_plus_x_minus_x_bound_nonneg:
1.270 -  "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
1.271 +  fixes x::real shows "0 <= x \<Longrightarrow> x <= 1 \<Longrightarrow> abs(ln (1 + x) - x) <= x\<^sup>2"
1.272  proof -
1.273    assume x: "0 <= x"
1.274    assume x1: "x <= 1"
1.275 @@ -1672,7 +1721,7 @@
1.276  qed
1.277
1.278  lemma abs_ln_one_plus_x_minus_x_bound_nonpos:
1.279 -  "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.280 +  fixes x::real shows "-(1 / 2) <= x \<Longrightarrow> x <= 0 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.281  proof -
1.282    assume a: "-(1 / 2) <= x"
1.283    assume b: "x <= 0"
1.284 @@ -1692,7 +1741,7 @@
1.285  qed
1.286
1.287  lemma abs_ln_one_plus_x_minus_x_bound:
1.288 -    "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.289 +  fixes x::real shows "abs x <= 1 / 2 \<Longrightarrow> abs(ln (1 + x) - x) <= 2 * x\<^sup>2"
1.290    apply (case_tac "0 <= x")
1.291    apply (rule order_trans)
1.292    apply (rule abs_ln_one_plus_x_minus_x_bound_nonneg)
1.293 @@ -1701,7 +1750,8 @@
1.294    apply auto
1.295    done
1.296
1.297 -lemma ln_x_over_x_mono: "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
1.298 +lemma ln_x_over_x_mono:
1.299 +  fixes x::real shows "exp 1 <= x \<Longrightarrow> x <= y \<Longrightarrow> (ln y / y) <= (ln x / x)"
1.300  proof -
1.301    assume x: "exp 1 <= x" "x <= y"
1.302    moreover have "0 < exp (1::real)" by simp
1.303 @@ -1737,15 +1787,17 @@
1.304    finally show ?thesis using b by (simp add: field_simps)
1.305  qed
1.306
1.307 -lemma ln_le_minus_one: "0 < x \<Longrightarrow> ln x \<le> x - 1"
1.308 +lemma ln_le_minus_one:
1.309 +  fixes x::real shows "0 < x \<Longrightarrow> ln x \<le> x - 1"
1.310    using exp_ge_add_one_self[of "ln x"] by simp
1.311
1.312  lemma ln_eq_minus_one:
1.313 +  fixes x::real
1.314    assumes "0 < x" "ln x = x - 1"
1.315    shows "x = 1"
1.316  proof -
1.317    let ?l = "\<lambda>y. ln y - y + 1"
1.318 -  have D: "\<And>x. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
1.319 +  have D: "\<And>x::real. 0 < x \<Longrightarrow> DERIV ?l x :> (1 / x - 1)"
1.320      by (auto intro!: derivative_eq_intros)
1.321
1.322    show ?thesis
1.323 @@ -1814,11 +1866,11 @@
1.325  qed
1.326
1.327 -lemma ln_at_0: "LIM x at_right 0. ln x :> at_bot"
1.328 +lemma ln_at_0: "LIM x at_right 0. ln (x::real) :> at_bot"
1.329    by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
1.330       (auto simp: eventually_at_filter)
1.331
1.332 -lemma ln_at_top: "LIM x at_top. ln x :> at_top"
1.333 +lemma ln_at_top: "LIM x at_top. ln (x::real) :> at_top"
1.334    by (rule filterlim_at_top_at_top[where Q="\<lambda>x. 0 < x" and P="\<lambda>x. True" and g="exp"])
1.335       (auto intro: eventually_gt_at_top)
1.336
1.337 @@ -1846,10 +1898,6 @@
1.338  qed
1.339
1.340
1.341 -definition powr :: "[real,real] => real"  (infixr "powr" 80)
1.342 -  -- {*exponentation with real exponent*}
1.343 -  where "x powr a = exp(a * ln x)"
1.344 -
1.345  definition log :: "[real,real] => real"
1.346    -- {*logarithm of @{term x} to base @{term a}*}
1.347    where "log a x = ln x / ln a"
1.348 @@ -1891,67 +1939,77 @@
1.349  lemma powr_one_eq_one [simp]: "1 powr a = 1"
1.351
1.352 -lemma powr_zero_eq_one [simp]: "x powr 0 = 1"
1.353 +lemma powr_zero_eq_one [simp]: "x powr 0 = (if x=0 then 0 else 1)"
1.355
1.356 -lemma powr_one_gt_zero_iff [simp]: "(x powr 1 = x) = (0 < x)"
1.357 -  by (simp add: powr_def)
1.358 +lemma powr_one_gt_zero_iff [simp]:
1.359 +  fixes x::real shows "(x powr 1 = x) = (0 \<le> x)"
1.360 +  by (auto simp: powr_def)
1.361  declare powr_one_gt_zero_iff [THEN iffD2, simp]
1.362
1.363 -lemma powr_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
1.364 +lemma powr_mult:
1.365 +  fixes x::real shows "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
1.367
1.368 -lemma powr_gt_zero [simp]: "0 < x powr a"
1.369 +lemma powr_ge_pzero [simp]:
1.370 +  fixes x::real shows "0 <= x powr y"
1.372
1.373 -lemma powr_ge_pzero [simp]: "0 <= x powr y"
1.374 -  by (rule order_less_imp_le, rule powr_gt_zero)
1.375 -
1.376 -lemma powr_not_zero [simp]: "x powr a \<noteq> 0"
1.377 -  by (simp add: powr_def)
1.378 -
1.379 -lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
1.380 +lemma powr_divide:
1.381 +  fixes x::real shows "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
1.382    apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
1.384    done
1.385
1.386 -lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
1.387 +lemma powr_divide2:
1.388 +  fixes x::real shows "x powr a / x powr b = x powr (a - b)"
1.390    apply (subst exp_diff [THEN sym])
1.392    done
1.393
1.394 -lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
1.396 +  fixes x::real shows "x powr (a + b) = (x powr a) * (x powr b)"
1.398
1.399 -lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
1.400 +lemma powr_mult_base:
1.401 +  fixes x::real shows "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
1.402    using assms by (auto simp: powr_add)
1.403
1.404 -lemma powr_powr: "(x powr a) powr b = x powr (a * b)"
1.405 +lemma powr_powr:
1.406 +  fixes x::real shows "(x powr a) powr b = x powr (a * b)"
1.408
1.409 -lemma powr_powr_swap: "(x powr a) powr b = (x powr b) powr a"
1.410 +lemma powr_powr_swap:
1.411 +  fixes x::real shows "(x powr a) powr b = (x powr b) powr a"
1.412    by (simp add: powr_powr mult.commute)
1.413
1.414 -lemma powr_minus: "x powr (-a) = inverse (x powr a)"
1.415 +lemma powr_minus:
1.416 +  fixes x::real shows "x powr (-a) = inverse (x powr a)"
1.417    by (simp add: powr_def exp_minus [symmetric])
1.418
1.419 -lemma powr_minus_divide: "x powr (-a) = 1/(x powr a)"
1.420 +lemma powr_minus_divide:
1.421 +  fixes x::real shows "x powr (-a) = 1/(x powr a)"
1.422    by (simp add: divide_inverse powr_minus)
1.423
1.424 -lemma divide_powr_uminus: "a / b powr c = a * b powr (- c)"
1.425 +lemma divide_powr_uminus:
1.426 +  fixes a::real shows "a / b powr c = a * b powr (- c)"
1.428
1.429 -lemma powr_less_mono: "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
1.430 +lemma powr_less_mono:
1.431 +  fixes x::real shows "a < b \<Longrightarrow> 1 < x \<Longrightarrow> x powr a < x powr b"
1.433
1.434 -lemma powr_less_cancel: "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
1.435 +lemma powr_less_cancel:
1.436 +  fixes x::real shows "x powr a < x powr b \<Longrightarrow> 1 < x \<Longrightarrow> a < b"
1.438
1.439 -lemma powr_less_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
1.440 +lemma powr_less_cancel_iff [simp]:
1.441 +  fixes x::real shows "1 < x \<Longrightarrow> (x powr a < x powr b) = (a < b)"
1.442    by (blast intro: powr_less_cancel powr_less_mono)
1.443
1.444 -lemma powr_le_cancel_iff [simp]: "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
1.445 +lemma powr_le_cancel_iff [simp]:
1.446 +  fixes x::real shows "1 < x \<Longrightarrow> (x powr a \<le> x powr b) = (a \<le> b)"
1.447    by (simp add: linorder_not_less [symmetric])
1.448
1.449  lemma log_ln: "ln x = log (exp(1)) x"
1.450 @@ -2007,6 +2065,9 @@
1.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"
1.452    by (simp add: log_mult divide_inverse log_inverse)
1.453
1.454 +lemma powr_gt_zero [simp]: "0 < x powr a \<longleftrightarrow> (x::real) \<noteq> 0"
1.455 +  by (simp add: powr_def)
1.456 +
1.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)"
1.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)"
1.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)"
1.460 @@ -2071,14 +2132,18 @@
1.461
1.462  lemma le_log_iff:
1.463    assumes "1 < b" "x > 0"
1.464 -  shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> x"
1.465 -  by (metis assms(1) assms(2) dual_order.strict_trans powr_le_cancel_iff powr_log_cancel
1.466 -    powr_one_eq_one powr_one_gt_zero_iff)
1.467 +  shows "y \<le> log b x \<longleftrightarrow> b powr y \<le> (x::real)"
1.468 +  using assms
1.469 +  apply auto
1.470 +  apply (metis (no_types, hide_lams) less_irrefl less_le_trans linear powr_le_cancel_iff
1.471 +               powr_log_cancel zero_less_one)
1.472 +  apply (metis not_less order.trans order_refl powr_le_cancel_iff powr_log_cancel zero_le_one)
1.473 +  done
1.474
1.475  lemma less_log_iff:
1.476    assumes "1 < b" "x > 0"
1.477    shows "y < log b x \<longleftrightarrow> b powr y < x"
1.478 -  by (metis assms(1) assms(2) dual_order.strict_trans less_irrefl powr_less_cancel_iff
1.479 +  by (metis assms dual_order.strict_trans less_irrefl powr_less_cancel_iff
1.480      powr_log_cancel zero_less_one)
1.481
1.482  lemma
1.483 @@ -2136,22 +2201,28 @@
1.484      else Code.abort (STR ''op powr with non-integer exponent'') (\<lambda>_. b powr i))"
1.485    by (auto simp: powr_int)
1.486
1.487 -lemma powr_one: "0 < x \<Longrightarrow> x powr 1 = x"
1.488 -  using powr_realpow [of x 1] by simp
1.489 -
1.490 -lemma powr_numeral: "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
1.491 +lemma powr_one:
1.492 +  fixes x::real shows "0 \<le> x \<Longrightarrow> x powr 1 = x"
1.493 +  using powr_realpow [of x 1]
1.494 +  by simp
1.495 +
1.496 +lemma powr_numeral:
1.497 +  fixes x::real shows "0 < x \<Longrightarrow> x powr numeral n = x ^ numeral n"
1.498    by (fact powr_realpow_numeral)
1.499
1.500 -lemma powr_neg_one: "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
1.501 +lemma powr_neg_one:
1.502 +  fixes x::real shows "0 < x \<Longrightarrow> x powr - 1 = 1 / x"
1.503    using powr_int [of x "- 1"] by simp
1.504
1.505 -lemma powr_neg_numeral: "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
1.506 +lemma powr_neg_numeral:
1.507 +  fixes x::real shows "0 < x \<Longrightarrow> x powr - numeral n = 1 / x ^ numeral n"
1.508    using powr_int [of x "- numeral n"] by simp
1.509
1.510  lemma root_powr_inverse: "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
1.511    by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
1.512
1.513 -lemma ln_powr: "ln (x powr y) = y * ln x"
1.514 +lemma ln_powr:
1.515 +  fixes x::real shows "x \<noteq> 0 \<Longrightarrow> ln (x powr y) = y * ln x"
1.517
1.518  lemma ln_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> ln (root n b) =  ln b / n"
1.519 @@ -2163,7 +2234,7 @@
1.520  lemma log_root: "\<lbrakk> n > 0; a > 0 \<rbrakk> \<Longrightarrow> log b (root n a) =  log b a / n"
1.522
1.523 -lemma log_powr: "log b (x powr y) = y * log b x"
1.524 +lemma log_powr: "x \<noteq> 0 \<Longrightarrow> log b (x powr y) = y * log b x"
1.525    by (simp add: log_def ln_powr)
1.526
1.527  lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
1.528 @@ -2175,65 +2246,58 @@
1.529  lemma log_base_pow: "0 < a \<Longrightarrow> log (a ^ n) x = log a x / n"
1.530    by (simp add: log_def ln_realpow)
1.531
1.532 -lemma log_base_powr: "log (a powr b) x = log a x / b"
1.533 +lemma log_base_powr: "a \<noteq> 0 \<Longrightarrow> log (a powr b) x = log a x / b"
1.534    by (simp add: log_def ln_powr)
1.535
1.536  lemma log_base_root: "\<lbrakk> n > 0; b > 0 \<rbrakk> \<Longrightarrow> log (root n b) x = n * (log b x)"
1.538
1.539 -lemma ln_bound: "1 <= x ==> ln x <= x"
1.540 +lemma ln_bound:
1.541 +  fixes x::real shows "1 <= x ==> ln x <= x"
1.542    apply (subgoal_tac "ln(1 + (x - 1)) <= x - 1")
1.543    apply simp
1.545    done
1.546
1.547 -lemma powr_mono: "a <= b ==> 1 <= x ==> x powr a <= x powr b"
1.548 +lemma powr_mono:
1.549 +  fixes x::real shows "a <= b ==> 1 <= x ==> x powr a <= x powr b"
1.550    apply (cases "x = 1", simp)
1.551    apply (cases "a = b", simp)
1.552    apply (rule order_less_imp_le)
1.553    apply (rule powr_less_mono, auto)
1.554    done
1.555
1.556 -lemma ge_one_powr_ge_zero: "1 <= x ==> 0 <= a ==> 1 <= x powr a"
1.557 -  apply (subst powr_zero_eq_one [THEN sym])
1.558 -  apply (rule powr_mono, assumption+)
1.559 -  done
1.560 -
1.561 -lemma powr_less_mono2: "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
1.562 -  apply (unfold powr_def)
1.563 -  apply (rule exp_less_mono)
1.564 -  apply (rule mult_strict_left_mono)
1.565 -  apply (subst ln_less_cancel_iff, assumption)
1.566 -  apply (rule order_less_trans)
1.567 -  prefer 2
1.568 -  apply assumption+
1.569 -  done
1.570 -
1.571 -lemma powr_less_mono2_neg: "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
1.572 -  apply (unfold powr_def)
1.573 -  apply (rule exp_less_mono)
1.574 -  apply (rule mult_strict_left_mono_neg)
1.575 -  apply (subst ln_less_cancel_iff)
1.576 -  apply assumption
1.577 -  apply (rule order_less_trans)
1.578 -  prefer 2
1.579 -  apply assumption+
1.580 -  done
1.581 -
1.582 -lemma powr_mono2: "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
1.583 +lemma ge_one_powr_ge_zero:
1.584 +  fixes x::real shows "1 <= x ==> 0 <= a ==> 1 <= x powr a"
1.585 +using powr_mono by fastforce
1.586 +
1.587 +lemma powr_less_mono2:
1.588 +  fixes x::real shows "0 < a ==> 0 < x ==> x < y ==> x powr a < y powr a"
1.589 +  by (simp add: powr_def)
1.590 +
1.591 +
1.592 +lemma powr_less_mono2_neg:
1.593 +  fixes x::real shows "a < 0 ==> 0 < x ==> x < y ==> y powr a < x powr a"
1.594 +  by (simp add: powr_def)
1.595 +
1.596 +lemma powr_mono2:
1.597 +  fixes x::real shows "0 <= a ==> 0 < x ==> x <= y ==> x powr a <= y powr a"
1.598    apply (case_tac "a = 0", simp)
1.599    apply (case_tac "x = y", simp)
1.600    apply (metis less_eq_real_def powr_less_mono2)
1.601    done
1.602
1.603 -lemma powr_inj: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
1.604 +lemma powr_inj:
1.605 +  fixes x::real shows "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> a powr x = a powr y \<longleftrightarrow> x = y"
1.606    unfolding powr_def exp_inj_iff by simp
1.607
1.608 -lemma ln_powr_bound: "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
1.609 -  by (metis less_eq_real_def ln_less_self mult_imp_le_div_pos ln_powr mult.commute
1.610 -            powr_gt_zero)
1.611 +lemma ln_powr_bound:
1.612 +  fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
1.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)
1.614 +
1.615
1.616  lemma ln_powr_bound2:
1.617 +  fixes x::real
1.618    assumes "1 < x" and "0 < a"
1.619    shows "(ln x) powr a <= (a powr a) * x"
1.620  proof -
1.621 @@ -2244,7 +2308,7 @@
1.622    finally have "(ln x) powr a <= (a * (x powr (1 / a))) powr a"
1.623      by (metis assms less_imp_le ln_gt_zero powr_mono2)
1.624    also have "... = (a powr a) * ((x powr (1 / a)) powr a)"
1.625 -    by (metis assms(2) powr_mult powr_gt_zero)
1.626 +    using assms powr_mult by auto
1.627    also have "(x powr (1 / a)) powr a = x powr ((1 / a) * a)"
1.628      by (rule powr_powr)
1.629    also have "... = x" using assms
1.630 @@ -2252,37 +2316,56 @@
1.631    finally show ?thesis .
1.632  qed
1.633
1.634 -lemma tendsto_powr [tendsto_intros]:
1.635 -  "\<lbrakk>(f ---> a) F; (g ---> b) F; a \<noteq> 0\<rbrakk> \<Longrightarrow> ((\<lambda>x. f x powr g x) ---> a powr b) F"
1.636 -  unfolding powr_def by (intro tendsto_intros)
1.637 +lemma tendsto_powr [tendsto_intros]:  (*FIXME a mess, suggests a general rule about exceptions*)
1.638 +  fixes a::real
1.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"
1.640 +  apply (simp add: powr_def)
1.641 +  apply (simp add: tendsto_def)
1.642 +  apply (simp add: Topological_Spaces.eventually_conj_iff )
1.643 +  apply safe
1.644 +  apply (case_tac "0 \<in> S")
1.645 +  apply (auto simp: )
1.646 +  apply (subgoal_tac "\<exists>T. open T & a : T & 0 \<notin> T")
1.647 +  apply clarify
1.648 +  apply (drule_tac x="T" in spec)
1.649 +  apply (simp add: )
1.650 +  apply (metis (mono_tags, lifting) eventually_mono)
1.651 +  apply (simp add: separation_t1)
1.652 +  apply (subgoal_tac "((\<lambda>x. exp (g x * ln (f x))) ---> exp (b * ln a)) F")
1.653 +  apply (simp add: tendsto_def)
1.654 +  apply (metis (mono_tags, lifting) eventually_mono)
1.655 +  apply (simp add: tendsto_def [symmetric])
1.656 +  apply (intro tendsto_intros)
1.657 +  apply (auto simp: )
1.658 +  done
1.659
1.660  lemma continuous_powr:
1.661    assumes "continuous F f"
1.662      and "continuous F g"
1.663      and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
1.664 -  shows "continuous F (\<lambda>x. (f x) powr (g x))"
1.665 +  shows "continuous F (\<lambda>x. (f x) powr (g x :: real))"
1.666    using assms unfolding continuous_def by (rule tendsto_powr)
1.667
1.668  lemma continuous_at_within_powr[continuous_intros]:
1.669    assumes "continuous (at a within s) f"
1.670      and "continuous (at a within s) g"
1.671      and "f a \<noteq> 0"
1.672 -  shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x))"
1.673 +  shows "continuous (at a within s) (\<lambda>x. (f x) powr (g x :: real))"
1.674    using assms unfolding continuous_within by (rule tendsto_powr)
1.675
1.676  lemma isCont_powr[continuous_intros, simp]:
1.677 -  assumes "isCont f a" "isCont g a" "f a \<noteq> 0"
1.678 +  assumes "isCont f a" "isCont g a" "f a \<noteq> (0::real)"
1.679    shows "isCont (\<lambda>x. (f x) powr g x) a"
1.680    using assms unfolding continuous_at by (rule tendsto_powr)
1.681
1.682  lemma continuous_on_powr[continuous_intros]:
1.683 -  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> 0"
1.684 +  assumes "continuous_on s f" "continuous_on s g" and "\<forall>x\<in>s. f x \<noteq> (0::real)"
1.685    shows "continuous_on s (\<lambda>x. (f x) powr (g x))"
1.686    using assms unfolding continuous_on_def by (fast intro: tendsto_powr)
1.687
1.688  (* FIXME: generalize by replacing d by with g x and g ---> d? *)
1.689  lemma tendsto_zero_powrI:
1.690 -  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> 0) F"
1.691 +  assumes "eventually (\<lambda>x. 0 < f x ) F" and "(f ---> (0::real)) F"
1.692      and "0 < d"
1.693    shows "((\<lambda>x. f x powr d) ---> 0) F"
1.694  proof (rule tendstoI)
1.695 @@ -2303,14 +2386,17 @@
1.696  lemma tendsto_neg_powr:
1.697    assumes "s < 0"
1.698      and "LIM x F. f x :> at_top"
1.699 -  shows "((\<lambda>x. f x powr s) ---> 0) F"
1.700 +  shows "((\<lambda>x. f x powr s) ---> (0::real)) F"
1.701  proof (rule tendstoI)
1.702    fix e :: real assume "0 < e"
1.703    def Z \<equiv> "e powr (1 / s)"
1.704 +  have "Z > 0"
1.705 +    using Z_def `0 < e` by auto
1.706    from assms have "eventually (\<lambda>x. Z < f x) F"
1.708    moreover
1.709 -  from assms have "\<And>x. Z < x \<Longrightarrow> x powr s < Z powr s"
1.710 +  from assms have "\<And>x::real. Z < x \<Longrightarrow> x powr s < Z powr s"
1.711 +    using `Z > 0`
1.712      by (auto simp: Z_def intro!: powr_less_mono2_neg)
1.713    with assms `0 < e` have "\<And>x. Z < x \<Longrightarrow> dist (x powr s) 0 < e"
1.714      by (simp add: powr_powr Z_def dist_real_def)
1.715 @@ -2318,13 +2404,11 @@
1.716    show "eventually (\<lambda>x. dist (f x powr s) 0 < e) F" by (rule eventually_elim1)
1.717  qed
1.718
1.719 -(* it is funny that this isn't in the library! It could go in Transcendental *)
1.720  lemma tendsto_exp_limit_at_right:
1.721    fixes x :: real
1.722    shows "((\<lambda>y. (1 + x * y) powr (1 / y)) ---> exp x) (at_right 0)"
1.723  proof cases
1.724    assume "x \<noteq> 0"
1.725 -
1.726    have "((\<lambda>y. ln (1 + x * y)::real) has_real_derivative 1 * x) (at 0)"
1.727      by (auto intro!: derivative_eq_intros)
1.728    then have "((\<lambda>y. ln (1 + x * y) / y) ---> x) (at 0)"
1.729 @@ -2335,7 +2419,10 @@
1.730    proof (rule filterlim_mono_eventually)
1.731      show "eventually (\<lambda>xa. exp (ln (1 + x * xa) / xa) = (1 + x * xa) powr (1 / xa)) (at_right 0)"
1.732        unfolding eventually_at_right[OF zero_less_one]
1.733 -      using `x \<noteq> 0` by (intro exI[of _ "1 / \<bar>x\<bar>"]) (auto simp: field_simps powr_def)
1.734 +      using `x \<noteq> 0`
1.735 +      apply  (intro exI[of _ "1 / \<bar>x\<bar>"])
1.736 +      apply (auto simp: field_simps powr_def abs_if)
1.737 +      by (metis add_less_same_cancel1 mult_less_0_iff not_less_iff_gr_or_eq zero_less_one)
1.739  qed simp
1.740
1.741 @@ -4445,7 +4532,7 @@
1.742  lemma arcsin_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x < arcsin y \<longleftrightarrow> x < y"
1.743    apply (rule trans [OF sin_mono_less_eq [symmetric]])
1.744    using arcsin_ubound arcsin_lbound
1.745 -  apply (auto simp: )
1.746 +  apply auto
1.747    done
1.748
1.749  lemma arcsin_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arcsin x \<le> arcsin y \<longleftrightarrow> x \<le> y"
1.750 @@ -4460,7 +4547,7 @@
1.751  lemma arccos_less_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> (arccos x < arccos y \<longleftrightarrow> y < x)"
1.752    apply (rule trans [OF cos_mono_less_eq [symmetric]])
1.753    using arccos_ubound arccos_lbound
1.754 -  apply (auto simp: )
1.755 +  apply auto
1.756    done
1.757
1.758  lemma arccos_le_mono: "abs x \<le> 1 \<Longrightarrow> abs y \<le> 1 \<Longrightarrow> arccos x \<le> arccos y \<longleftrightarrow> y \<le> x"
1.759 @@ -5009,4 +5096,253 @@
1.760    qed
1.761  qed
1.762
1.763 +
1.764 +subsection{*Basics about polynomial functions: extremal behaviour and root counts*}
1.765 +(*ALL COULD GO TO COMPLEX_MAIN OR EARLIER*)
1.766 +
1.767 +lemma polyfun_diff: (*COMPLEX_SUB_POLYFUN in HOL Light*)
1.768 +    fixes x :: "'a::idom"
1.769 +  assumes "1 \<le> n"
1.770 +    shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
1.771 +           (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
1.772 +proof -
1.773 +  have h: "bij_betw (\<lambda>(i,j). (j,i)) ((SIGMA i : atMost n. lessThan i)) (SIGMA j : lessThan n. {Suc j..n})"
1.774 +    by (auto simp: bij_betw_def inj_on_def)
1.775 +  have "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
1.776 +        (\<Sum>i\<le>n. a i * (x^i - y^i))"
1.777 +    by (simp add: right_diff_distrib setsum_subtractf)
1.778 +  also have "... = (\<Sum>i\<le>n. a i * (x - y) * (\<Sum>j<i. y^(i - Suc j) * x^j))"
1.779 +    by (simp add: power_diff_sumr2 mult.assoc)
1.780 +  also have "... = (\<Sum>i\<le>n. \<Sum>j<i. a i * (x - y) * (y^(i - Suc j) * x^j))"
1.781 +    by (simp add: setsum_right_distrib)
1.782 +  also have "... = (\<Sum>(i,j) \<in> (SIGMA i : atMost n. lessThan i). a i * (x - y) * (y^(i - Suc j) * x^j))"
1.783 +    by (simp add: setsum.Sigma)
1.784 +  also have "... = (\<Sum>(j,i) \<in> (SIGMA j : lessThan n. {Suc j..n}). a i * (x - y) * (y^(i - Suc j) * x^j))"
1.785 +    by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong)
1.786 +  also have "... = (\<Sum>j<n. \<Sum>i=Suc j..n. a i * (x - y) * (y^(i - Suc j) * x^j))"
1.787 +    by (simp add: setsum.Sigma)
1.788 +  also have "... = (x - y) * (\<Sum>j<n. (\<Sum>i=Suc j..n. a i * y^(i - j - 1)) * x^j)"
1.789 +    by (simp add: setsum_right_distrib mult_ac)
1.790 +  finally show ?thesis .
1.791 +qed
1.792 +
1.793 +lemma polyfun_diff_alt: (*COMPLEX_SUB_POLYFUN_ALT in HOL Light*)
1.794 +    fixes x :: "'a::idom"
1.795 +  assumes "1 \<le> n"
1.796 +    shows "(\<Sum>i\<le>n. a i * x^i) - (\<Sum>i\<le>n. a i * y^i) =
1.797 +           (x - y) * ((\<Sum>j<n. \<Sum>k<n-j. a(j+k+1) * y^k * x^j))"
1.798 +proof -
1.799 +  { fix j::nat
1.800 +    assume "j<n"
1.801 +    have h: "bij_betw (\<lambda>i. i - (j + 1)) {Suc j..n} (lessThan (n-j))"
1.802 +      apply (auto simp: bij_betw_def inj_on_def)
1.803 +      apply (rule_tac x="x + Suc j" in image_eqI)
1.804 +      apply (auto simp: )
1.805 +      done
1.806 +    have "(\<Sum>i=Suc j..n. a i * y^(i - j - 1)) = (\<Sum>k<n-j. a(j+k+1) * y^k)"
1.807 +      by (auto simp add: setsum.reindex_bij_betw [OF h, symmetric] intro: setsum.strong_cong)
1.808 +  }
1.809 +  then show ?thesis
1.810 +    by (simp add: polyfun_diff [OF assms] setsum_left_distrib)
1.811 +qed
1.812 +
1.813 +lemma polyfun_linear_factor:  (*COMPLEX_POLYFUN_LINEAR_FACTOR in HOL Light*)
1.814 +  fixes a :: "'a::idom"
1.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)"
1.816 +proof (cases "n=0")
1.817 +  case True then show ?thesis
1.818 +    by simp
1.819 +next
1.820 +  case False
1.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)) =
1.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))"
1.823 +    by (simp add: algebra_simps)
1.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))"
1.825 +    using False by (simp add: polyfun_diff)
1.826 +  also have "... = True"
1.827 +    by auto
1.828 +  finally show ?thesis
1.829 +    by simp
1.830 +qed
1.831 +
1.832 +lemma polyfun_linear_factor_root:  (*COMPLEX_POLYFUN_LINEAR_FACTOR_ROOT in HOL Light*)
1.833 +  fixes a :: "'a::idom"
1.834 +  assumes "(\<Sum>i\<le>n. c(i) * a^i) = 0"
1.835 +  obtains b where "\<And>z. (\<Sum>i\<le>n. c(i) * z^i) = (z - a) * (\<Sum>i<n. b(i) * z^i)"
1.836 +  using polyfun_linear_factor [of c n a] assms
1.837 +  by auto
1.838 +
1.839 +lemma isCont_polynom:
1.840 +  fixes c :: "nat \<Rightarrow> 'a::real_normed_div_algebra"
1.841 +  shows "isCont (\<lambda>w. \<Sum>i\<le>n. c i * w^i) a"
1.842 +  by simp
1.843 +
1.844 +lemma zero_polynom_imp_zero_coeffs:
1.845 +    fixes c :: "nat \<Rightarrow> 'a::{ab_semigroup_mult,real_normed_div_algebra}"
1.846 +  assumes "\<And>w. (\<Sum>i\<le>n. c i * w^i) = 0"  "k \<le> n"
1.847 +    shows "c k = 0"
1.848 +using assms
1.849 +proof (induction n arbitrary: c k)
1.850 +  case 0
1.851 +  then show ?case
1.852 +    by simp
1.853 +next
1.854 +  case (Suc n c k)
1.855 +  have [simp]: "c 0 = 0" using Suc.prems(1) [of 0]
1.856 +    by simp
1.857 +  { fix w
1.858 +    have "(\<Sum>i\<le>Suc n. c i * w^i) = (\<Sum>i\<le>n. c (Suc i) * w ^ Suc i)"
1.859 +      unfolding Set_Interval.setsum_atMost_Suc_shift
1.860 +      by simp
1.861 +    also have "... = w * (\<Sum>i\<le>n. c (Suc i) * w^i)"
1.862 +      by (simp add: power_Suc mult_ac setsum_right_distrib del: setsum_atMost_Suc)
1.863 +    finally have "(\<Sum>i\<le>Suc n. c i * w^i) = w * (\<Sum>i\<le>n. c (Suc i) * w^i)" .
1.864 +  }
1.865 +  then have wnz: "\<And>w. w \<noteq> 0 \<Longrightarrow> (\<Sum>i\<le>n. c (Suc i) * w^i) = 0"
1.866 +    using Suc  by auto
1.867 +  then have "(\<lambda>h. \<Sum>i\<le>n. c (Suc i) * h^i) -- 0 --> 0"
1.868 +    by (simp cong: LIM_cong)                   --{*the case @{term"w=0"} by continuity}*}
1.869 +  then have "(\<Sum>i\<le>n. c (Suc i) * 0^i) = 0"
1.870 +    using isCont_polynom [of 0 "\<lambda>i. c (Suc i)" n] LIM_unique
1.871 +    by (force simp add: Limits.isCont_iff)
1.872 +  then have "\<And>w. (\<Sum>i\<le>n. c (Suc i) * w^i) = 0" using wnz
1.873 +    by metis
1.874 +  then have "\<And>i. i\<le>n \<Longrightarrow> c (Suc i) = 0"
1.875 +    using Suc.IH [of "\<lambda>i. c (Suc i)"]
1.876 +    by blast
1.877 +  then show ?case using `k \<le> Suc n`
1.878 +    by (cases k) auto
1.879 +qed
1.880 +
1.881 +lemma polyfun_rootbound: (*COMPLEX_POLYFUN_ROOTBOUND in HOL Light*)
1.882 +    fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
1.883 +  assumes "c k \<noteq> 0" "k\<le>n"
1.884 +    shows "finite {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<and>
1.885 +             card {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<le> n"
1.886 +using assms
1.887 +proof (induction n arbitrary: c k)
1.888 +  case 0
1.889 +  then show ?case
1.890 +    by simp
1.891 +next
1.892 +  case (Suc m c k)
1.893 +  let ?succase = ?case
1.894 +  show ?case
1.895 +  proof (cases "{z. (\<Sum>i\<le>Suc m. c(i) * z^i) = 0} = {}")
1.896 +    case True
1.897 +    then show ?succase
1.898 +      by simp
1.899 +  next
1.900 +    case False
1.901 +    then obtain z0 where z0: "(\<Sum>i\<le>Suc m. c(i) * z0^i) = 0"
1.902 +      by blast
1.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)"
1.904 +      using polyfun_linear_factor_root [OF z0, unfolded lessThan_Suc_atMost]
1.905 +      by blast
1.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}"
1.907 +      by auto
1.908 +    have "~(\<forall>k\<le>m. b k = 0)"
1.909 +    proof
1.910 +      assume [simp]: "\<forall>k\<le>m. b k = 0"
1.911 +      then have "\<And>w. (\<Sum>i\<le>m. b i * w^i) = 0"
1.912 +        by simp
1.913 +      then have "\<And>w. (\<Sum>i\<le>Suc m. c i * w^i) = 0"
1.914 +        using b by simp
1.915 +      then have "\<And>k. k \<le> Suc m \<Longrightarrow> c k = 0"
1.916 +        using zero_polynom_imp_zero_coeffs
1.917 +        by blast
1.918 +      then show False using Suc.prems
1.919 +        by blast
1.920 +    qed
1.921 +    then obtain k' where bk': "b k' \<noteq> 0" "k' \<le> m"
1.922 +      by blast
1.923 +    show ?succase
1.924 +      using Suc.IH [of b k'] bk'
1.925 +      by (simp add: eq card_insert_if del: setsum_atMost_Suc)
1.926 +    qed
1.927 +qed
1.928 +
1.929 +lemma
1.930 +    fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
1.931 +  assumes "c k \<noteq> 0" "k\<le>n"
1.932 +    shows polyfun_roots_finite: "finite {z. (\<Sum>i\<le>n. c(i) * z^i) = 0}"
1.933 +      and polyfun_roots_card:   "card {z. (\<Sum>i\<le>n. c(i) * z^i) = 0} \<le> n"
1.934 +using polyfun_rootbound assms
1.935 +  by auto
1.936 +
1.937 +lemma polyfun_finite_roots: (*COMPLEX_POLYFUN_FINITE_ROOTS in HOL Light*)
1.938 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
1.939 +  shows "finite {x. (\<Sum>i\<le>n. c i * x^i) = 0} \<longleftrightarrow> (\<exists>i\<le>n. c i \<noteq> 0)"
1.940 +        (is "?lhs = ?rhs")
1.941 +proof
1.942 +  assume ?lhs
1.943 +  moreover
1.944 +  { assume "\<forall>i\<le>n. c i = 0"
1.945 +    then have "\<And>x. (\<Sum>i\<le>n. c i * x^i) = 0"
1.946 +      by simp
1.947 +    then have "\<not> finite {x. (\<Sum>i\<le>n. c i * x^i) = 0}"
1.948 +      using ex_new_if_finite [OF infinite_UNIV_char_0 [where 'a='a]]
1.949 +      by auto
1.950 +  }
1.951 +  ultimately show ?rhs
1.952 +  by metis
1.953 +next
1.954 +  assume ?rhs
1.955 +  then show ?lhs
1.956 +    using polyfun_rootbound
1.957 +    by blast
1.958 +qed
1.959 +
1.960 +lemma polyfun_eq_0: (*COMPLEX_POLYFUN_EQ_0 in HOL Light*)
1.961 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
1.962 +  shows "(\<forall>x. (\<Sum>i\<le>n. c i * x^i) = 0) \<longleftrightarrow> (\<forall>i\<le>n. c i = 0)"
1.963 +  using zero_polynom_imp_zero_coeffs by auto
1.964 +
1.965 +lemma polyfun_eq_coeffs:
1.966 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
1.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)"
1.968 +proof -
1.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)"
1.970 +    by (simp add: left_diff_distrib Groups_Big.setsum_subtractf)
1.971 +  also have "... \<longleftrightarrow> (\<forall>i\<le>n. c i - d i = 0)"
1.972 +    by (rule polyfun_eq_0)
1.973 +  finally show ?thesis
1.974 +    by simp
1.975 +qed
1.976 +
1.977 +lemma polyfun_eq_const: (*COMPLEX_POLYFUN_EQ_CONST in HOL Light*)
1.978 +  fixes c :: "nat \<Rightarrow> 'a::{idom,real_normed_div_algebra}"
1.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)"
1.980 +        (is "?lhs = ?rhs")
1.981 +proof -
1.982 +  have *: "\<forall>x. (\<Sum>i\<le>n. (if i=0 then k else 0) * x^i) = k"
1.983 +    by (induct n) auto
1.984 +  show ?thesis
1.985 +  proof
1.986 +    assume ?lhs
1.987 +    with * have "(\<forall>i\<le>n. c i = (if i=0 then k else 0))"
1.988 +      by (simp add: polyfun_eq_coeffs [symmetric])
1.989 +    then show ?rhs
1.990 +      by simp
1.991 +  next
1.992 +    assume ?rhs then show ?lhs
1.993 +      by (induct n) auto
1.994 +  qed
1.995 +qed
1.996 +
1.997 +lemma root_polyfun:
1.998 +  fixes z:: "'a::idom"
1.999 +  assumes "1 \<le> n"
1.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"
1.1001 +  using assms