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.61    by (rule ln_unique) (simp add: exp_add)
    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.96    by (simp add: order_eq_iff)
    1.97  
    1.98 -lemma ln_add_one_self_le_self [simp]: "0 \<le> x \<Longrightarrow> ln (1 + x) \<le> x"
    1.99 +lemma ln_add_one_self_le_self [simp]: 
   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.102    apply (simp add: exp_ge_add_one_self_aux)
   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.262 +lemma ln_add_one_self_le_self2:
   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.324      by (simp add: Deriv.DERIV_iff2)
   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.350    by (simp add: powr_def)
   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.354    by (simp add: powr_def)
   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.366    by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
   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.371    by (simp add: powr_def)
   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.383    apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
   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.389    apply (simp add: powr_def)
   1.390    apply (subst exp_diff [THEN sym])
   1.391    apply (simp add: left_diff_distrib)
   1.392    done
   1.393  
   1.394 -lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
   1.395 +lemma powr_add:
   1.396 +  fixes x::real shows "x powr (a + b) = (x powr a) * (x powr b)"
   1.397    by (simp add: powr_def exp_add [symmetric] distrib_right)
   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.407    by (simp add: powr_def)
   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.427    by (simp add: powr_minus_divide)
   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.432    by (simp add: powr_def)
   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.437    by (simp add: powr_def)
   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.516    by (simp add: powr_def)
   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.521  by(simp add: log_def ln_root)
   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.537  by(simp add: log_def ln_root)
   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.544    apply (rule ln_add_one_self_le_self, 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.707      by (simp add: filterlim_at_top_dense)
   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.738    qed (simp_all add: at_eq_sup_left_right)
   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
  1.1002 +  by (cases n; simp add: setsum_head_Suc atLeast0AtMost [symmetric])
  1.1003 +
  1.1004 +lemma
  1.1005 +    fixes zz :: "'a::{idom,real_normed_div_algebra}"
  1.1006 +  assumes "1 \<le> n"
  1.1007 +    shows finite_roots_unity: "finite {z::'a. z^n = 1}"
  1.1008 +      and card_roots_unity:   "card {z::'a. z^n = 1} \<le> n"
  1.1009 +  using polyfun_rootbound [of "\<lambda>i. if i = 0 then -1 else if i=n then 1 else 0" n n] assms
  1.1010 +  by (auto simp add: root_polyfun [OF assms])
  1.1011 +
  1.1012  end