src/HOL/NthRoot.thy
changeset 51483 dc39d69774bb
parent 51478 270b21f3ae0a
child 53015 a1119cf551e8
     1.1 --- a/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -10,6 +10,17 @@
     1.4  imports Parity Deriv
     1.5  begin
     1.6  
     1.7 +lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
     1.8 +  by (simp add: sgn_real_def)
     1.9 +
    1.10 +lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
    1.11 +  by (simp add: sgn_real_def)
    1.12 +
    1.13 +lemma power_eq_iff_eq_base: 
    1.14 +  fixes a b :: "_ :: linordered_semidom"
    1.15 +  shows "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
    1.16 +  using power_eq_imp_eq_base[of a n b] by auto
    1.17 +
    1.18  subsection {* Existence of Nth Root *}
    1.19  
    1.20  text {* Existence follows from the Intermediate Value Theorem *}
    1.21 @@ -43,11 +54,8 @@
    1.22  
    1.23  text {* Uniqueness of nth positive root *}
    1.24  
    1.25 -lemma realpow_pos_nth_unique:
    1.26 -  "\<lbrakk>0 < n; 0 < a\<rbrakk> \<Longrightarrow> \<exists>!r. 0 < r \<and> r ^ n = (a::real)"
    1.27 -apply (auto intro!: realpow_pos_nth)
    1.28 -apply (rule_tac n=n in power_eq_imp_eq_base, simp_all)
    1.29 -done
    1.30 +lemma realpow_pos_nth_unique: "\<lbrakk>0 < n; 0 < a\<rbrakk> \<Longrightarrow> \<exists>!r. 0 < r \<and> r ^ n = (a::real)"
    1.31 +  by (auto intro!: realpow_pos_nth simp: power_eq_iff_eq_base)
    1.32  
    1.33  subsection {* Nth Root *}
    1.34  
    1.35 @@ -55,66 +63,86 @@
    1.36    @{term "root n (- x) = - root n x"}. This allows
    1.37    us to omit side conditions from many theorems. *}
    1.38  
    1.39 -definition
    1.40 -  root :: "[nat, real] \<Rightarrow> real" where
    1.41 -  "root n x = (if 0 < x then (THE u. 0 < u \<and> u ^ n = x) else
    1.42 -               if x < 0 then - (THE u. 0 < u \<and> u ^ n = - x) else 0)"
    1.43 +lemma inj_sgn_power: assumes "0 < n" shows "inj (\<lambda>y. sgn y * \<bar>y\<bar>^n :: real)" (is "inj ?f")
    1.44 +proof (rule injI)
    1.45 +  have x: "\<And>a b :: real. (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b) \<Longrightarrow> a \<noteq> b" by auto
    1.46 +  fix x y assume "?f x = ?f y" with power_eq_iff_eq_base[of n "\<bar>x\<bar>" "\<bar>y\<bar>"] `0<n` show "x = y"
    1.47 +    by (cases rule: linorder_cases[of 0 x, case_product linorder_cases[of 0 y]])
    1.48 +       (simp_all add: x)
    1.49 +qed
    1.50 +
    1.51 +lemma sgn_power_injE: "sgn a * \<bar>a\<bar> ^ n = x \<Longrightarrow> x = sgn b * \<bar>b\<bar> ^ n \<Longrightarrow> 0 < n \<Longrightarrow> a = (b::real)"
    1.52 +  using inj_sgn_power[THEN injD, of n a b] by simp
    1.53 +
    1.54 +definition root :: "nat \<Rightarrow> real \<Rightarrow> real" where
    1.55 +  "root n x = (if n = 0 then 0 else the_inv (\<lambda>y. sgn y * \<bar>y\<bar>^n) x)"
    1.56 +
    1.57 +lemma root_0 [simp]: "root 0 x = 0"
    1.58 +  by (simp add: root_def)
    1.59 +
    1.60 +lemma root_sgn_power: "0 < n \<Longrightarrow> root n (sgn y * \<bar>y\<bar>^n) = y"
    1.61 +  using the_inv_f_f[OF inj_sgn_power] by (simp add: root_def)
    1.62 +
    1.63 +lemma sgn_power_root:
    1.64 +  assumes "0 < n" shows "sgn (root n x) * \<bar>(root n x)\<bar>^n = x" (is "?f (root n x) = x")
    1.65 +proof cases
    1.66 +  assume "x \<noteq> 0"
    1.67 +  with realpow_pos_nth[OF `0 < n`, of "\<bar>x\<bar>"] obtain r where "0 < r" "r ^ n = \<bar>x\<bar>" by auto
    1.68 +  with `x \<noteq> 0` have S: "x \<in> range ?f"
    1.69 +    by (intro image_eqI[of _ _ "sgn x * r"])
    1.70 +       (auto simp: abs_mult sgn_mult power_mult_distrib abs_sgn_eq mult_sgn_abs)
    1.71 +  from `0 < n` f_the_inv_into_f[OF inj_sgn_power[OF `0 < n`] this]  show ?thesis
    1.72 +    by (simp add: root_def)
    1.73 +qed (insert `0 < n` root_sgn_power[of n 0], simp)
    1.74 +
    1.75 +lemma split_root: "P (root n x) \<longleftrightarrow> (n = 0 \<longrightarrow> P 0) \<and> (0 < n \<longrightarrow> (\<forall>y. sgn y * \<bar>y\<bar>^n = x \<longrightarrow> P y))"
    1.76 +  apply (cases "n = 0")
    1.77 +  apply simp_all
    1.78 +  apply (metis root_sgn_power sgn_power_root)
    1.79 +  done
    1.80  
    1.81  lemma real_root_zero [simp]: "root n 0 = 0"
    1.82 -unfolding root_def by simp
    1.83 +  by (simp split: split_root add: sgn_zero_iff)
    1.84 +
    1.85 +lemma real_root_minus: "root n (- x) = - root n x"
    1.86 +  by (clarsimp split: split_root elim!: sgn_power_injE simp: sgn_minus)
    1.87  
    1.88 -lemma real_root_minus: "0 < n \<Longrightarrow> root n (- x) = - root n x"
    1.89 -unfolding root_def by simp
    1.90 +lemma real_root_less_mono: "\<lbrakk>0 < n; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
    1.91 +proof (clarsimp split: split_root)
    1.92 +  have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
    1.93 +  fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
    1.94 +    using power_less_imp_less_base[of a n b]  power_less_imp_less_base[of "-b" n "-a"]
    1.95 +    by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
    1.96 +qed
    1.97  
    1.98  lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
    1.99 -apply (simp add: root_def)
   1.100 -apply (drule (1) realpow_pos_nth_unique)
   1.101 -apply (erule theI' [THEN conjunct1])
   1.102 -done
   1.103 +  using real_root_less_mono[of n 0 x] by simp
   1.104 +
   1.105 +lemma real_root_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> root n x"
   1.106 +  using real_root_gt_zero[of n x] by (cases "n = 0") (auto simp add: le_less)
   1.107  
   1.108  lemma real_root_pow_pos: (* TODO: rename *)
   1.109    "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
   1.110 -apply (simp add: root_def)
   1.111 -apply (drule (1) realpow_pos_nth_unique)
   1.112 -apply (erule theI' [THEN conjunct2])
   1.113 -done
   1.114 +  using sgn_power_root[of n x] real_root_gt_zero[of n x] by simp
   1.115  
   1.116  lemma real_root_pow_pos2 [simp]: (* TODO: rename *)
   1.117    "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
   1.118  by (auto simp add: order_le_less real_root_pow_pos)
   1.119  
   1.120 +lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x"
   1.121 +  by (auto split: split_root simp: sgn_real_def power_less_zero_eq)
   1.122 +
   1.123  lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
   1.124 -apply (rule_tac x=0 and y=x in linorder_le_cases)
   1.125 -apply (erule (1) real_root_pow_pos2 [OF odd_pos])
   1.126 -apply (subgoal_tac "root n (- x) ^ n = - x")
   1.127 -apply (simp add: real_root_minus odd_pos)
   1.128 -apply (simp add: odd_pos)
   1.129 -done
   1.130 -
   1.131 -lemma real_root_ge_zero: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> root n x"
   1.132 -by (auto simp add: order_le_less real_root_gt_zero)
   1.133 +  using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
   1.134  
   1.135  lemma real_root_power_cancel: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (x ^ n) = x"
   1.136 -apply (subgoal_tac "0 \<le> x ^ n")
   1.137 -apply (subgoal_tac "0 \<le> root n (x ^ n)")
   1.138 -apply (subgoal_tac "root n (x ^ n) ^ n = x ^ n")
   1.139 -apply (erule (3) power_eq_imp_eq_base)
   1.140 -apply (erule (1) real_root_pow_pos2)
   1.141 -apply (erule (1) real_root_ge_zero)
   1.142 -apply (erule zero_le_power)
   1.143 -done
   1.144 +  using root_sgn_power[of n x] by (auto simp add: le_less power_0_left)
   1.145  
   1.146  lemma odd_real_root_power_cancel: "odd n \<Longrightarrow> root n (x ^ n) = x"
   1.147 -apply (rule_tac x=0 and y=x in linorder_le_cases)
   1.148 -apply (erule (1) real_root_power_cancel [OF odd_pos])
   1.149 -apply (subgoal_tac "root n ((- x) ^ n) = - x")
   1.150 -apply (simp add: real_root_minus odd_pos)
   1.151 -apply (erule real_root_power_cancel [OF odd_pos], simp)
   1.152 -done
   1.153 +  using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: split_if_asm)
   1.154  
   1.155 -lemma real_root_pos_unique:
   1.156 -  "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   1.157 -by (erule subst, rule real_root_power_cancel)
   1.158 +lemma real_root_pos_unique: "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   1.159 +  using root_sgn_power[of n y] by (auto simp add: le_less power_0_left)
   1.160  
   1.161  lemma odd_real_root_unique:
   1.162    "\<lbrakk>odd n; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   1.163 @@ -125,32 +153,8 @@
   1.164  
   1.165  text {* Root function is strictly monotonic, hence injective *}
   1.166  
   1.167 -lemma real_root_less_mono_lemma:
   1.168 -  "\<lbrakk>0 < n; 0 \<le> x; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   1.169 -apply (subgoal_tac "0 \<le> y")
   1.170 -apply (subgoal_tac "root n x ^ n < root n y ^ n")
   1.171 -apply (erule power_less_imp_less_base)
   1.172 -apply (erule (1) real_root_ge_zero)
   1.173 -apply simp
   1.174 -apply simp
   1.175 -done
   1.176 -
   1.177 -lemma real_root_less_mono: "\<lbrakk>0 < n; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   1.178 -apply (cases "0 \<le> x")
   1.179 -apply (erule (2) real_root_less_mono_lemma)
   1.180 -apply (cases "0 \<le> y")
   1.181 -apply (rule_tac y=0 in order_less_le_trans)
   1.182 -apply (subgoal_tac "0 < root n (- x)")
   1.183 -apply (simp add: real_root_minus)
   1.184 -apply (simp add: real_root_gt_zero)
   1.185 -apply (simp add: real_root_ge_zero)
   1.186 -apply (subgoal_tac "root n (- y) < root n (- x)")
   1.187 -apply (simp add: real_root_minus)
   1.188 -apply (simp add: real_root_less_mono_lemma)
   1.189 -done
   1.190 -
   1.191  lemma real_root_le_mono: "\<lbrakk>0 < n; x \<le> y\<rbrakk> \<Longrightarrow> root n x \<le> root n y"
   1.192 -by (auto simp add: order_le_less real_root_less_mono)
   1.193 +  by (auto simp add: order_le_less real_root_less_mono)
   1.194  
   1.195  lemma real_root_less_iff [simp]:
   1.196    "0 < n \<Longrightarrow> (root n x < root n y) = (x < y)"
   1.197 @@ -191,26 +195,34 @@
   1.198  lemma real_root_eq_1_iff [simp]: "0 < n \<Longrightarrow> (root n x = 1) = (x = 1)"
   1.199  by (insert real_root_eq_iff [where y=1], simp)
   1.200  
   1.201 +text {* Roots of multiplication and division *}
   1.202 +
   1.203 +lemma real_root_mult: "root n (x * y) = root n x * root n y"
   1.204 +  by (auto split: split_root elim!: sgn_power_injE simp: sgn_mult abs_mult power_mult_distrib)
   1.205 +
   1.206 +lemma real_root_inverse: "root n (inverse x) = inverse (root n x)"
   1.207 +  by (auto split: split_root elim!: sgn_power_injE simp: inverse_sgn power_inverse)
   1.208 +
   1.209 +lemma real_root_divide: "root n (x / y) = root n x / root n y"
   1.210 +  by (simp add: divide_inverse real_root_mult real_root_inverse)
   1.211 +
   1.212 +lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
   1.213 +  by (simp add: abs_if real_root_minus)
   1.214 +
   1.215 +lemma real_root_power: "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   1.216 +  by (induct k) (simp_all add: real_root_mult)
   1.217 +
   1.218  text {* Roots of roots *}
   1.219  
   1.220  lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x"
   1.221  by (simp add: odd_real_root_unique)
   1.222  
   1.223 -lemma real_root_pos_mult_exp:
   1.224 -  "\<lbrakk>0 < m; 0 < n; 0 < x\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
   1.225 -by (rule real_root_pos_unique, simp_all add: power_mult)
   1.226 +lemma real_root_mult_exp: "root (m * n) x = root m (root n x)"
   1.227 +  by (auto split: split_root elim!: sgn_power_injE
   1.228 +           simp: sgn_zero_iff sgn_mult power_mult[symmetric] abs_mult power_mult_distrib abs_sgn_eq)
   1.229  
   1.230 -lemma real_root_mult_exp:
   1.231 -  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
   1.232 -apply (rule linorder_cases [where x=x and y=0])
   1.233 -apply (subgoal_tac "root (m * n) (- x) = root m (root n (- x))")
   1.234 -apply (simp add: real_root_minus)
   1.235 -apply (simp_all add: real_root_pos_mult_exp)
   1.236 -done
   1.237 -
   1.238 -lemma real_root_commute:
   1.239 -  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root m (root n x) = root n (root m x)"
   1.240 -by (simp add: real_root_mult_exp [symmetric] mult_commute)
   1.241 +lemma real_root_commute: "root m (root n x) = root n (root m x)"
   1.242 +  by (simp add: real_root_mult_exp [symmetric] mult_commute)
   1.243  
   1.244  text {* Monotonicity in first argument *}
   1.245  
   1.246 @@ -236,118 +248,35 @@
   1.247    "\<lbrakk>0 < n; n < N; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> root n x \<le> root N x"
   1.248  by (auto simp add: order_le_less real_root_strict_increasing)
   1.249  
   1.250 -text {* Roots of multiplication and division *}
   1.251 -
   1.252 -lemma real_root_mult_lemma:
   1.253 -  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> root n (x * y) = root n x * root n y"
   1.254 -by (simp add: real_root_pos_unique mult_nonneg_nonneg power_mult_distrib)
   1.255 -
   1.256 -lemma real_root_inverse_lemma:
   1.257 -  "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (inverse x) = inverse (root n x)"
   1.258 -by (simp add: real_root_pos_unique power_inverse [symmetric])
   1.259 -
   1.260 -lemma real_root_mult:
   1.261 -  assumes n: "0 < n"
   1.262 -  shows "root n (x * y) = root n x * root n y"
   1.263 -proof (rule linorder_le_cases, rule_tac [!] linorder_le_cases)
   1.264 -  assume "0 \<le> x" and "0 \<le> y"
   1.265 -  thus ?thesis by (rule real_root_mult_lemma [OF n])
   1.266 -next
   1.267 -  assume "0 \<le> x" and "y \<le> 0"
   1.268 -  hence "0 \<le> x" and "0 \<le> - y" by simp_all
   1.269 -  hence "root n (x * - y) = root n x * root n (- y)"
   1.270 -    by (rule real_root_mult_lemma [OF n])
   1.271 -  thus ?thesis by (simp add: real_root_minus [OF n])
   1.272 -next
   1.273 -  assume "x \<le> 0" and "0 \<le> y"
   1.274 -  hence "0 \<le> - x" and "0 \<le> y" by simp_all
   1.275 -  hence "root n (- x * y) = root n (- x) * root n y"
   1.276 -    by (rule real_root_mult_lemma [OF n])
   1.277 -  thus ?thesis by (simp add: real_root_minus [OF n])
   1.278 -next
   1.279 -  assume "x \<le> 0" and "y \<le> 0"
   1.280 -  hence "0 \<le> - x" and "0 \<le> - y" by simp_all
   1.281 -  hence "root n (- x * - y) = root n (- x) * root n (- y)"
   1.282 -    by (rule real_root_mult_lemma [OF n])
   1.283 -  thus ?thesis by (simp add: real_root_minus [OF n])
   1.284 -qed
   1.285 -
   1.286 -lemma real_root_inverse:
   1.287 -  assumes n: "0 < n"
   1.288 -  shows "root n (inverse x) = inverse (root n x)"
   1.289 -proof (rule linorder_le_cases)
   1.290 -  assume "0 \<le> x"
   1.291 -  thus ?thesis by (rule real_root_inverse_lemma [OF n])
   1.292 -next
   1.293 -  assume "x \<le> 0"
   1.294 -  hence "0 \<le> - x" by simp
   1.295 -  hence "root n (inverse (- x)) = inverse (root n (- x))"
   1.296 -    by (rule real_root_inverse_lemma [OF n])
   1.297 -  thus ?thesis by (simp add: real_root_minus [OF n])
   1.298 -qed
   1.299 -
   1.300 -lemma real_root_divide:
   1.301 -  "0 < n \<Longrightarrow> root n (x / y) = root n x / root n y"
   1.302 -by (simp add: divide_inverse real_root_mult real_root_inverse)
   1.303 -
   1.304 -lemma real_root_power:
   1.305 -  "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   1.306 -by (induct k, simp_all add: real_root_mult)
   1.307 -
   1.308 -lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
   1.309 -by (simp add: abs_if real_root_minus)
   1.310 -
   1.311  text {* Continuity and derivatives *}
   1.312  
   1.313 -lemma isCont_root_pos:
   1.314 -  assumes n: "0 < n"
   1.315 -  assumes x: "0 < x"
   1.316 -  shows "isCont (root n) x"
   1.317 -proof -
   1.318 -  have "isCont (root n) (root n x ^ n)"
   1.319 -  proof (rule isCont_inverse_function [where f="\<lambda>a. a ^ n"])
   1.320 -    show "0 < root n x" using n x by simp
   1.321 -    show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
   1.322 -      by (simp add: abs_le_iff real_root_power_cancel n)
   1.323 -    show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
   1.324 -      by simp
   1.325 -  qed
   1.326 -  thus ?thesis using n x by simp
   1.327 -qed
   1.328 +lemma isCont_real_root: "isCont (root n) x"
   1.329 +proof cases
   1.330 +  assume n: "0 < n"
   1.331 +  let ?f = "\<lambda>y::real. sgn y * \<bar>y\<bar>^n"
   1.332 +  have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
   1.333 +    using n by (intro continuous_on_If continuous_on_intros) auto
   1.334 +  then have "continuous_on UNIV ?f"
   1.335 +    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
   1.336 +  then have [simp]: "\<And>x. isCont ?f x"
   1.337 +    by (simp add: continuous_on_eq_continuous_at)
   1.338  
   1.339 -lemma isCont_root_neg:
   1.340 -  "\<lbrakk>0 < n; x < 0\<rbrakk> \<Longrightarrow> isCont (root n) x"
   1.341 -apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
   1.342 -apply (simp add: real_root_minus)
   1.343 -apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
   1.344 -apply (simp add: isCont_root_pos)
   1.345 -done
   1.346 -
   1.347 -lemma isCont_root_zero:
   1.348 -  "0 < n \<Longrightarrow> isCont (root n) 0"
   1.349 -unfolding isCont_def
   1.350 -apply (rule LIM_I)
   1.351 -apply (rule_tac x="r ^ n" in exI, safe)
   1.352 -apply (simp)
   1.353 -apply (simp add: real_root_abs [symmetric])
   1.354 -apply (rule_tac n="n" in power_less_imp_less_base, simp_all)
   1.355 -done
   1.356 -
   1.357 -lemma isCont_real_root: "0 < n \<Longrightarrow> isCont (root n) x"
   1.358 -apply (rule_tac x=x and y=0 in linorder_cases)
   1.359 -apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero)
   1.360 -done
   1.361 +  have "isCont (root n) (?f (root n x))"
   1.362 +    by (rule isCont_inverse_function [where f="?f" and d=1]) (auto simp: root_sgn_power n)
   1.363 +  then show ?thesis
   1.364 +    by (simp add: sgn_power_root n)
   1.365 +qed (simp add: root_def[abs_def])
   1.366  
   1.367  lemma tendsto_real_root[tendsto_intros]:
   1.368 -  "(f ---> x) F \<Longrightarrow> 0 < n \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
   1.369 -  using isCont_tendsto_compose[OF isCont_real_root, of n f x F] .
   1.370 +  "(f ---> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
   1.371 +  using isCont_tendsto_compose[OF isCont_real_root, of f x F] .
   1.372  
   1.373  lemma continuous_real_root[continuous_intros]:
   1.374 -  "continuous F f \<Longrightarrow> 0 < n \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
   1.375 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
   1.376    unfolding continuous_def by (rule tendsto_real_root)
   1.377    
   1.378  lemma continuous_on_real_root[continuous_on_intros]:
   1.379 -  "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
   1.380 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
   1.381    unfolding continuous_on_def by (auto intro: tendsto_real_root)
   1.382  
   1.383  lemma DERIV_real_root:
   1.384 @@ -363,9 +292,7 @@
   1.385      by (rule DERIV_pow)
   1.386    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
   1.387      using n x by simp
   1.388 -  show "isCont (root n) x"
   1.389 -    using n by (rule isCont_real_root)
   1.390 -qed
   1.391 +qed (rule isCont_real_root)
   1.392  
   1.393  lemma DERIV_odd_real_root:
   1.394    assumes n: "odd n"
   1.395 @@ -380,9 +307,7 @@
   1.396      by (rule DERIV_pow)
   1.397    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
   1.398      using odd_pos [OF n] x by simp
   1.399 -  show "isCont (root n) x"
   1.400 -    using odd_pos [OF n] by (rule isCont_real_root)
   1.401 -qed
   1.402 +qed (rule isCont_real_root)
   1.403  
   1.404  lemma DERIV_even_real_root:
   1.405    assumes n: "0 < n" and "even n"
   1.406 @@ -396,7 +321,7 @@
   1.407    proof (rule allI, rule impI, erule conjE)
   1.408      fix y assume "x - 1 < y" and "y < 0"
   1.409      hence "root n (-y) ^ n = -y" using `0 < n` by simp
   1.410 -    with real_root_minus[OF `0 < n`] and `even n`
   1.411 +    with real_root_minus and `even n`
   1.412      show "- (root n y ^ n) = y" by simp
   1.413    qed
   1.414  next
   1.415 @@ -404,9 +329,7 @@
   1.416      by  (auto intro!: DERIV_intros)
   1.417    show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
   1.418      using n x by simp
   1.419 -  show "isCont (root n) x"
   1.420 -    using n by (rule isCont_real_root)
   1.421 -qed
   1.422 +qed (rule isCont_real_root)
   1.423  
   1.424  lemma DERIV_real_root_generic:
   1.425    assumes "0 < n" and "x \<noteq> 0"
   1.426 @@ -421,8 +344,7 @@
   1.427  
   1.428  subsection {* Square Root *}
   1.429  
   1.430 -definition
   1.431 -  sqrt :: "real \<Rightarrow> real" where
   1.432 +definition sqrt :: "real \<Rightarrow> real" where
   1.433    "sqrt = root 2"
   1.434  
   1.435  lemma pos2: "0 < (2::nat)" by simp
   1.436 @@ -453,16 +375,16 @@
   1.437  unfolding sqrt_def by (rule real_root_one [OF pos2])
   1.438  
   1.439  lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
   1.440 -unfolding sqrt_def by (rule real_root_minus [OF pos2])
   1.441 +unfolding sqrt_def by (rule real_root_minus)
   1.442  
   1.443  lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
   1.444 -unfolding sqrt_def by (rule real_root_mult [OF pos2])
   1.445 +unfolding sqrt_def by (rule real_root_mult)
   1.446  
   1.447  lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
   1.448 -unfolding sqrt_def by (rule real_root_inverse [OF pos2])
   1.449 +unfolding sqrt_def by (rule real_root_inverse)
   1.450  
   1.451  lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y"
   1.452 -unfolding sqrt_def by (rule real_root_divide [OF pos2])
   1.453 +unfolding sqrt_def by (rule real_root_divide)
   1.454  
   1.455  lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k"
   1.456  unfolding sqrt_def by (rule real_root_power [OF pos2])
   1.457 @@ -471,7 +393,7 @@
   1.458  unfolding sqrt_def by (rule real_root_gt_zero [OF pos2])
   1.459  
   1.460  lemma real_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> sqrt x"
   1.461 -unfolding sqrt_def by (rule real_root_ge_zero [OF pos2])
   1.462 +unfolding sqrt_def by (rule real_root_ge_zero)
   1.463  
   1.464  lemma real_sqrt_less_mono: "x < y \<Longrightarrow> sqrt x < sqrt y"
   1.465  unfolding sqrt_def by (rule real_root_less_mono [OF pos2])
   1.466 @@ -501,19 +423,19 @@
   1.467  lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified]
   1.468  
   1.469  lemma isCont_real_sqrt: "isCont sqrt x"
   1.470 -unfolding sqrt_def by (rule isCont_real_root [OF pos2])
   1.471 +unfolding sqrt_def by (rule isCont_real_root)
   1.472  
   1.473  lemma tendsto_real_sqrt[tendsto_intros]:
   1.474    "(f ---> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
   1.475 -  unfolding sqrt_def by (rule tendsto_real_root [OF _ pos2])
   1.476 +  unfolding sqrt_def by (rule tendsto_real_root)
   1.477  
   1.478  lemma continuous_real_sqrt[continuous_intros]:
   1.479    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
   1.480 -  unfolding sqrt_def by (rule continuous_real_root [OF _ pos2])
   1.481 +  unfolding sqrt_def by (rule continuous_real_root)
   1.482    
   1.483  lemma continuous_on_real_sqrt[continuous_on_intros]:
   1.484    "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
   1.485 -  unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2])
   1.486 +  unfolding sqrt_def by (rule continuous_on_real_root)
   1.487  
   1.488  lemma DERIV_real_sqrt_generic:
   1.489    assumes "x \<noteq> 0"