modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
authorhoelzl
Fri Mar 22 10:41:43 2013 +0100 (2013-03-22)
changeset 51483dc39d69774bb
parent 51482 80efd8c49f52
child 51486 0a0c9a45d294
modernized definition of root: use the_inv, handle positive and negative case uniformly, and 0-th root is constant 0
src/HOL/Log.thy
src/HOL/NthRoot.thy
     1.1 --- a/src/HOL/Log.thy	Fri Mar 22 10:41:43 2013 +0100
     1.2 +++ b/src/HOL/Log.thy	Fri Mar 22 10:41:43 2013 +0100
     1.3 @@ -244,7 +244,7 @@
     1.4  
     1.5  lemma root_powr_inverse:
     1.6    "0 < n \<Longrightarrow> 0 < x \<Longrightarrow> root n x = x powr (1/n)"
     1.7 -by (auto simp: root_def powr_realpow[symmetric] powr_powr)
     1.8 +  by (rule real_root_pos_unique) (auto simp: powr_realpow[symmetric] powr_powr)
     1.9  
    1.10  lemma ln_powr: "0 < x ==> 0 < y ==> ln(x powr y) = y * ln x"
    1.11  by (unfold powr_def, simp)
     2.1 --- a/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
     2.2 +++ b/src/HOL/NthRoot.thy	Fri Mar 22 10:41:43 2013 +0100
     2.3 @@ -10,6 +10,17 @@
     2.4  imports Parity Deriv
     2.5  begin
     2.6  
     2.7 +lemma abs_sgn_eq: "abs (sgn x :: real) = (if x = 0 then 0 else 1)"
     2.8 +  by (simp add: sgn_real_def)
     2.9 +
    2.10 +lemma inverse_sgn: "sgn (inverse a) = inverse (sgn a :: real)"
    2.11 +  by (simp add: sgn_real_def)
    2.12 +
    2.13 +lemma power_eq_iff_eq_base: 
    2.14 +  fixes a b :: "_ :: linordered_semidom"
    2.15 +  shows "0 < n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a ^ n = b ^ n \<longleftrightarrow> a = b"
    2.16 +  using power_eq_imp_eq_base[of a n b] by auto
    2.17 +
    2.18  subsection {* Existence of Nth Root *}
    2.19  
    2.20  text {* Existence follows from the Intermediate Value Theorem *}
    2.21 @@ -43,11 +54,8 @@
    2.22  
    2.23  text {* Uniqueness of nth positive root *}
    2.24  
    2.25 -lemma realpow_pos_nth_unique:
    2.26 -  "\<lbrakk>0 < n; 0 < a\<rbrakk> \<Longrightarrow> \<exists>!r. 0 < r \<and> r ^ n = (a::real)"
    2.27 -apply (auto intro!: realpow_pos_nth)
    2.28 -apply (rule_tac n=n in power_eq_imp_eq_base, simp_all)
    2.29 -done
    2.30 +lemma realpow_pos_nth_unique: "\<lbrakk>0 < n; 0 < a\<rbrakk> \<Longrightarrow> \<exists>!r. 0 < r \<and> r ^ n = (a::real)"
    2.31 +  by (auto intro!: realpow_pos_nth simp: power_eq_iff_eq_base)
    2.32  
    2.33  subsection {* Nth Root *}
    2.34  
    2.35 @@ -55,66 +63,86 @@
    2.36    @{term "root n (- x) = - root n x"}. This allows
    2.37    us to omit side conditions from many theorems. *}
    2.38  
    2.39 -definition
    2.40 -  root :: "[nat, real] \<Rightarrow> real" where
    2.41 -  "root n x = (if 0 < x then (THE u. 0 < u \<and> u ^ n = x) else
    2.42 -               if x < 0 then - (THE u. 0 < u \<and> u ^ n = - x) else 0)"
    2.43 +lemma inj_sgn_power: assumes "0 < n" shows "inj (\<lambda>y. sgn y * \<bar>y\<bar>^n :: real)" (is "inj ?f")
    2.44 +proof (rule injI)
    2.45 +  have x: "\<And>a b :: real. (0 < a \<and> b < 0) \<or> (a < 0 \<and> 0 < b) \<Longrightarrow> a \<noteq> b" by auto
    2.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"
    2.47 +    by (cases rule: linorder_cases[of 0 x, case_product linorder_cases[of 0 y]])
    2.48 +       (simp_all add: x)
    2.49 +qed
    2.50 +
    2.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)"
    2.52 +  using inj_sgn_power[THEN injD, of n a b] by simp
    2.53 +
    2.54 +definition root :: "nat \<Rightarrow> real \<Rightarrow> real" where
    2.55 +  "root n x = (if n = 0 then 0 else the_inv (\<lambda>y. sgn y * \<bar>y\<bar>^n) x)"
    2.56 +
    2.57 +lemma root_0 [simp]: "root 0 x = 0"
    2.58 +  by (simp add: root_def)
    2.59 +
    2.60 +lemma root_sgn_power: "0 < n \<Longrightarrow> root n (sgn y * \<bar>y\<bar>^n) = y"
    2.61 +  using the_inv_f_f[OF inj_sgn_power] by (simp add: root_def)
    2.62 +
    2.63 +lemma sgn_power_root:
    2.64 +  assumes "0 < n" shows "sgn (root n x) * \<bar>(root n x)\<bar>^n = x" (is "?f (root n x) = x")
    2.65 +proof cases
    2.66 +  assume "x \<noteq> 0"
    2.67 +  with realpow_pos_nth[OF `0 < n`, of "\<bar>x\<bar>"] obtain r where "0 < r" "r ^ n = \<bar>x\<bar>" by auto
    2.68 +  with `x \<noteq> 0` have S: "x \<in> range ?f"
    2.69 +    by (intro image_eqI[of _ _ "sgn x * r"])
    2.70 +       (auto simp: abs_mult sgn_mult power_mult_distrib abs_sgn_eq mult_sgn_abs)
    2.71 +  from `0 < n` f_the_inv_into_f[OF inj_sgn_power[OF `0 < n`] this]  show ?thesis
    2.72 +    by (simp add: root_def)
    2.73 +qed (insert `0 < n` root_sgn_power[of n 0], simp)
    2.74 +
    2.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))"
    2.76 +  apply (cases "n = 0")
    2.77 +  apply simp_all
    2.78 +  apply (metis root_sgn_power sgn_power_root)
    2.79 +  done
    2.80  
    2.81  lemma real_root_zero [simp]: "root n 0 = 0"
    2.82 -unfolding root_def by simp
    2.83 +  by (simp split: split_root add: sgn_zero_iff)
    2.84 +
    2.85 +lemma real_root_minus: "root n (- x) = - root n x"
    2.86 +  by (clarsimp split: split_root elim!: sgn_power_injE simp: sgn_minus)
    2.87  
    2.88 -lemma real_root_minus: "0 < n \<Longrightarrow> root n (- x) = - root n x"
    2.89 -unfolding root_def by simp
    2.90 +lemma real_root_less_mono: "\<lbrakk>0 < n; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
    2.91 +proof (clarsimp split: split_root)
    2.92 +  have x: "\<And>a b :: real. (0 < b \<and> a < 0) \<Longrightarrow> \<not> a > b" by auto
    2.93 +  fix a b :: real assume "0 < n" "sgn a * \<bar>a\<bar> ^ n < sgn b * \<bar>b\<bar> ^ n" then show "a < b"
    2.94 +    using power_less_imp_less_base[of a n b]  power_less_imp_less_base[of "-b" n "-a"]
    2.95 +    by (simp add: sgn_real_def power_less_zero_eq x[of "a ^ n" "- ((- b) ^ n)"] split: split_if_asm)
    2.96 +qed
    2.97  
    2.98  lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
    2.99 -apply (simp add: root_def)
   2.100 -apply (drule (1) realpow_pos_nth_unique)
   2.101 -apply (erule theI' [THEN conjunct1])
   2.102 -done
   2.103 +  using real_root_less_mono[of n 0 x] by simp
   2.104 +
   2.105 +lemma real_root_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> root n x"
   2.106 +  using real_root_gt_zero[of n x] by (cases "n = 0") (auto simp add: le_less)
   2.107  
   2.108  lemma real_root_pow_pos: (* TODO: rename *)
   2.109    "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
   2.110 -apply (simp add: root_def)
   2.111 -apply (drule (1) realpow_pos_nth_unique)
   2.112 -apply (erule theI' [THEN conjunct2])
   2.113 -done
   2.114 +  using sgn_power_root[of n x] real_root_gt_zero[of n x] by simp
   2.115  
   2.116  lemma real_root_pow_pos2 [simp]: (* TODO: rename *)
   2.117    "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
   2.118  by (auto simp add: order_le_less real_root_pow_pos)
   2.119  
   2.120 +lemma sgn_root: "0 < n \<Longrightarrow> sgn (root n x) = sgn x"
   2.121 +  by (auto split: split_root simp: sgn_real_def power_less_zero_eq)
   2.122 +
   2.123  lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
   2.124 -apply (rule_tac x=0 and y=x in linorder_le_cases)
   2.125 -apply (erule (1) real_root_pow_pos2 [OF odd_pos])
   2.126 -apply (subgoal_tac "root n (- x) ^ n = - x")
   2.127 -apply (simp add: real_root_minus odd_pos)
   2.128 -apply (simp add: odd_pos)
   2.129 -done
   2.130 -
   2.131 -lemma real_root_ge_zero: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> root n x"
   2.132 -by (auto simp add: order_le_less real_root_gt_zero)
   2.133 +  using sgn_power_root[of n x] by (simp add: odd_pos sgn_real_def split: split_if_asm)
   2.134  
   2.135  lemma real_root_power_cancel: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (x ^ n) = x"
   2.136 -apply (subgoal_tac "0 \<le> x ^ n")
   2.137 -apply (subgoal_tac "0 \<le> root n (x ^ n)")
   2.138 -apply (subgoal_tac "root n (x ^ n) ^ n = x ^ n")
   2.139 -apply (erule (3) power_eq_imp_eq_base)
   2.140 -apply (erule (1) real_root_pow_pos2)
   2.141 -apply (erule (1) real_root_ge_zero)
   2.142 -apply (erule zero_le_power)
   2.143 -done
   2.144 +  using root_sgn_power[of n x] by (auto simp add: le_less power_0_left)
   2.145  
   2.146  lemma odd_real_root_power_cancel: "odd n \<Longrightarrow> root n (x ^ n) = x"
   2.147 -apply (rule_tac x=0 and y=x in linorder_le_cases)
   2.148 -apply (erule (1) real_root_power_cancel [OF odd_pos])
   2.149 -apply (subgoal_tac "root n ((- x) ^ n) = - x")
   2.150 -apply (simp add: real_root_minus odd_pos)
   2.151 -apply (erule real_root_power_cancel [OF odd_pos], simp)
   2.152 -done
   2.153 +  using root_sgn_power[of n x] by (simp add: odd_pos sgn_real_def power_0_left split: split_if_asm)
   2.154  
   2.155 -lemma real_root_pos_unique:
   2.156 -  "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   2.157 -by (erule subst, rule real_root_power_cancel)
   2.158 +lemma real_root_pos_unique: "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   2.159 +  using root_sgn_power[of n y] by (auto simp add: le_less power_0_left)
   2.160  
   2.161  lemma odd_real_root_unique:
   2.162    "\<lbrakk>odd n; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   2.163 @@ -125,32 +153,8 @@
   2.164  
   2.165  text {* Root function is strictly monotonic, hence injective *}
   2.166  
   2.167 -lemma real_root_less_mono_lemma:
   2.168 -  "\<lbrakk>0 < n; 0 \<le> x; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   2.169 -apply (subgoal_tac "0 \<le> y")
   2.170 -apply (subgoal_tac "root n x ^ n < root n y ^ n")
   2.171 -apply (erule power_less_imp_less_base)
   2.172 -apply (erule (1) real_root_ge_zero)
   2.173 -apply simp
   2.174 -apply simp
   2.175 -done
   2.176 -
   2.177 -lemma real_root_less_mono: "\<lbrakk>0 < n; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   2.178 -apply (cases "0 \<le> x")
   2.179 -apply (erule (2) real_root_less_mono_lemma)
   2.180 -apply (cases "0 \<le> y")
   2.181 -apply (rule_tac y=0 in order_less_le_trans)
   2.182 -apply (subgoal_tac "0 < root n (- x)")
   2.183 -apply (simp add: real_root_minus)
   2.184 -apply (simp add: real_root_gt_zero)
   2.185 -apply (simp add: real_root_ge_zero)
   2.186 -apply (subgoal_tac "root n (- y) < root n (- x)")
   2.187 -apply (simp add: real_root_minus)
   2.188 -apply (simp add: real_root_less_mono_lemma)
   2.189 -done
   2.190 -
   2.191  lemma real_root_le_mono: "\<lbrakk>0 < n; x \<le> y\<rbrakk> \<Longrightarrow> root n x \<le> root n y"
   2.192 -by (auto simp add: order_le_less real_root_less_mono)
   2.193 +  by (auto simp add: order_le_less real_root_less_mono)
   2.194  
   2.195  lemma real_root_less_iff [simp]:
   2.196    "0 < n \<Longrightarrow> (root n x < root n y) = (x < y)"
   2.197 @@ -191,26 +195,34 @@
   2.198  lemma real_root_eq_1_iff [simp]: "0 < n \<Longrightarrow> (root n x = 1) = (x = 1)"
   2.199  by (insert real_root_eq_iff [where y=1], simp)
   2.200  
   2.201 +text {* Roots of multiplication and division *}
   2.202 +
   2.203 +lemma real_root_mult: "root n (x * y) = root n x * root n y"
   2.204 +  by (auto split: split_root elim!: sgn_power_injE simp: sgn_mult abs_mult power_mult_distrib)
   2.205 +
   2.206 +lemma real_root_inverse: "root n (inverse x) = inverse (root n x)"
   2.207 +  by (auto split: split_root elim!: sgn_power_injE simp: inverse_sgn power_inverse)
   2.208 +
   2.209 +lemma real_root_divide: "root n (x / y) = root n x / root n y"
   2.210 +  by (simp add: divide_inverse real_root_mult real_root_inverse)
   2.211 +
   2.212 +lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
   2.213 +  by (simp add: abs_if real_root_minus)
   2.214 +
   2.215 +lemma real_root_power: "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   2.216 +  by (induct k) (simp_all add: real_root_mult)
   2.217 +
   2.218  text {* Roots of roots *}
   2.219  
   2.220  lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x"
   2.221  by (simp add: odd_real_root_unique)
   2.222  
   2.223 -lemma real_root_pos_mult_exp:
   2.224 -  "\<lbrakk>0 < m; 0 < n; 0 < x\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
   2.225 -by (rule real_root_pos_unique, simp_all add: power_mult)
   2.226 +lemma real_root_mult_exp: "root (m * n) x = root m (root n x)"
   2.227 +  by (auto split: split_root elim!: sgn_power_injE
   2.228 +           simp: sgn_zero_iff sgn_mult power_mult[symmetric] abs_mult power_mult_distrib abs_sgn_eq)
   2.229  
   2.230 -lemma real_root_mult_exp:
   2.231 -  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
   2.232 -apply (rule linorder_cases [where x=x and y=0])
   2.233 -apply (subgoal_tac "root (m * n) (- x) = root m (root n (- x))")
   2.234 -apply (simp add: real_root_minus)
   2.235 -apply (simp_all add: real_root_pos_mult_exp)
   2.236 -done
   2.237 -
   2.238 -lemma real_root_commute:
   2.239 -  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root m (root n x) = root n (root m x)"
   2.240 -by (simp add: real_root_mult_exp [symmetric] mult_commute)
   2.241 +lemma real_root_commute: "root m (root n x) = root n (root m x)"
   2.242 +  by (simp add: real_root_mult_exp [symmetric] mult_commute)
   2.243  
   2.244  text {* Monotonicity in first argument *}
   2.245  
   2.246 @@ -236,118 +248,35 @@
   2.247    "\<lbrakk>0 < n; n < N; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> root n x \<le> root N x"
   2.248  by (auto simp add: order_le_less real_root_strict_increasing)
   2.249  
   2.250 -text {* Roots of multiplication and division *}
   2.251 -
   2.252 -lemma real_root_mult_lemma:
   2.253 -  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> root n (x * y) = root n x * root n y"
   2.254 -by (simp add: real_root_pos_unique mult_nonneg_nonneg power_mult_distrib)
   2.255 -
   2.256 -lemma real_root_inverse_lemma:
   2.257 -  "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (inverse x) = inverse (root n x)"
   2.258 -by (simp add: real_root_pos_unique power_inverse [symmetric])
   2.259 -
   2.260 -lemma real_root_mult:
   2.261 -  assumes n: "0 < n"
   2.262 -  shows "root n (x * y) = root n x * root n y"
   2.263 -proof (rule linorder_le_cases, rule_tac [!] linorder_le_cases)
   2.264 -  assume "0 \<le> x" and "0 \<le> y"
   2.265 -  thus ?thesis by (rule real_root_mult_lemma [OF n])
   2.266 -next
   2.267 -  assume "0 \<le> x" and "y \<le> 0"
   2.268 -  hence "0 \<le> x" and "0 \<le> - y" by simp_all
   2.269 -  hence "root n (x * - y) = root n x * root n (- y)"
   2.270 -    by (rule real_root_mult_lemma [OF n])
   2.271 -  thus ?thesis by (simp add: real_root_minus [OF n])
   2.272 -next
   2.273 -  assume "x \<le> 0" and "0 \<le> y"
   2.274 -  hence "0 \<le> - x" and "0 \<le> y" by simp_all
   2.275 -  hence "root n (- x * y) = root n (- x) * root n y"
   2.276 -    by (rule real_root_mult_lemma [OF n])
   2.277 -  thus ?thesis by (simp add: real_root_minus [OF n])
   2.278 -next
   2.279 -  assume "x \<le> 0" and "y \<le> 0"
   2.280 -  hence "0 \<le> - x" and "0 \<le> - y" by simp_all
   2.281 -  hence "root n (- x * - y) = root n (- x) * root n (- y)"
   2.282 -    by (rule real_root_mult_lemma [OF n])
   2.283 -  thus ?thesis by (simp add: real_root_minus [OF n])
   2.284 -qed
   2.285 -
   2.286 -lemma real_root_inverse:
   2.287 -  assumes n: "0 < n"
   2.288 -  shows "root n (inverse x) = inverse (root n x)"
   2.289 -proof (rule linorder_le_cases)
   2.290 -  assume "0 \<le> x"
   2.291 -  thus ?thesis by (rule real_root_inverse_lemma [OF n])
   2.292 -next
   2.293 -  assume "x \<le> 0"
   2.294 -  hence "0 \<le> - x" by simp
   2.295 -  hence "root n (inverse (- x)) = inverse (root n (- x))"
   2.296 -    by (rule real_root_inverse_lemma [OF n])
   2.297 -  thus ?thesis by (simp add: real_root_minus [OF n])
   2.298 -qed
   2.299 -
   2.300 -lemma real_root_divide:
   2.301 -  "0 < n \<Longrightarrow> root n (x / y) = root n x / root n y"
   2.302 -by (simp add: divide_inverse real_root_mult real_root_inverse)
   2.303 -
   2.304 -lemma real_root_power:
   2.305 -  "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   2.306 -by (induct k, simp_all add: real_root_mult)
   2.307 -
   2.308 -lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
   2.309 -by (simp add: abs_if real_root_minus)
   2.310 -
   2.311  text {* Continuity and derivatives *}
   2.312  
   2.313 -lemma isCont_root_pos:
   2.314 -  assumes n: "0 < n"
   2.315 -  assumes x: "0 < x"
   2.316 -  shows "isCont (root n) x"
   2.317 -proof -
   2.318 -  have "isCont (root n) (root n x ^ n)"
   2.319 -  proof (rule isCont_inverse_function [where f="\<lambda>a. a ^ n"])
   2.320 -    show "0 < root n x" using n x by simp
   2.321 -    show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
   2.322 -      by (simp add: abs_le_iff real_root_power_cancel n)
   2.323 -    show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
   2.324 -      by simp
   2.325 -  qed
   2.326 -  thus ?thesis using n x by simp
   2.327 -qed
   2.328 +lemma isCont_real_root: "isCont (root n) x"
   2.329 +proof cases
   2.330 +  assume n: "0 < n"
   2.331 +  let ?f = "\<lambda>y::real. sgn y * \<bar>y\<bar>^n"
   2.332 +  have "continuous_on ({0..} \<union> {.. 0}) (\<lambda>x. if 0 < x then x ^ n else - ((-x) ^ n) :: real)"
   2.333 +    using n by (intro continuous_on_If continuous_on_intros) auto
   2.334 +  then have "continuous_on UNIV ?f"
   2.335 +    by (rule continuous_on_cong[THEN iffD1, rotated 2]) (auto simp: not_less real_sgn_neg le_less n)
   2.336 +  then have [simp]: "\<And>x. isCont ?f x"
   2.337 +    by (simp add: continuous_on_eq_continuous_at)
   2.338  
   2.339 -lemma isCont_root_neg:
   2.340 -  "\<lbrakk>0 < n; x < 0\<rbrakk> \<Longrightarrow> isCont (root n) x"
   2.341 -apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
   2.342 -apply (simp add: real_root_minus)
   2.343 -apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
   2.344 -apply (simp add: isCont_root_pos)
   2.345 -done
   2.346 -
   2.347 -lemma isCont_root_zero:
   2.348 -  "0 < n \<Longrightarrow> isCont (root n) 0"
   2.349 -unfolding isCont_def
   2.350 -apply (rule LIM_I)
   2.351 -apply (rule_tac x="r ^ n" in exI, safe)
   2.352 -apply (simp)
   2.353 -apply (simp add: real_root_abs [symmetric])
   2.354 -apply (rule_tac n="n" in power_less_imp_less_base, simp_all)
   2.355 -done
   2.356 -
   2.357 -lemma isCont_real_root: "0 < n \<Longrightarrow> isCont (root n) x"
   2.358 -apply (rule_tac x=x and y=0 in linorder_cases)
   2.359 -apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero)
   2.360 -done
   2.361 +  have "isCont (root n) (?f (root n x))"
   2.362 +    by (rule isCont_inverse_function [where f="?f" and d=1]) (auto simp: root_sgn_power n)
   2.363 +  then show ?thesis
   2.364 +    by (simp add: sgn_power_root n)
   2.365 +qed (simp add: root_def[abs_def])
   2.366  
   2.367  lemma tendsto_real_root[tendsto_intros]:
   2.368 -  "(f ---> x) F \<Longrightarrow> 0 < n \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
   2.369 -  using isCont_tendsto_compose[OF isCont_real_root, of n f x F] .
   2.370 +  "(f ---> x) F \<Longrightarrow> ((\<lambda>x. root n (f x)) ---> root n x) F"
   2.371 +  using isCont_tendsto_compose[OF isCont_real_root, of f x F] .
   2.372  
   2.373  lemma continuous_real_root[continuous_intros]:
   2.374 -  "continuous F f \<Longrightarrow> 0 < n \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
   2.375 +  "continuous F f \<Longrightarrow> continuous F (\<lambda>x. root n (f x))"
   2.376    unfolding continuous_def by (rule tendsto_real_root)
   2.377    
   2.378  lemma continuous_on_real_root[continuous_on_intros]:
   2.379 -  "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
   2.380 +  "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. root n (f x))"
   2.381    unfolding continuous_on_def by (auto intro: tendsto_real_root)
   2.382  
   2.383  lemma DERIV_real_root:
   2.384 @@ -363,9 +292,7 @@
   2.385      by (rule DERIV_pow)
   2.386    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
   2.387      using n x by simp
   2.388 -  show "isCont (root n) x"
   2.389 -    using n by (rule isCont_real_root)
   2.390 -qed
   2.391 +qed (rule isCont_real_root)
   2.392  
   2.393  lemma DERIV_odd_real_root:
   2.394    assumes n: "odd n"
   2.395 @@ -380,9 +307,7 @@
   2.396      by (rule DERIV_pow)
   2.397    show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
   2.398      using odd_pos [OF n] x by simp
   2.399 -  show "isCont (root n) x"
   2.400 -    using odd_pos [OF n] by (rule isCont_real_root)
   2.401 -qed
   2.402 +qed (rule isCont_real_root)
   2.403  
   2.404  lemma DERIV_even_real_root:
   2.405    assumes n: "0 < n" and "even n"
   2.406 @@ -396,7 +321,7 @@
   2.407    proof (rule allI, rule impI, erule conjE)
   2.408      fix y assume "x - 1 < y" and "y < 0"
   2.409      hence "root n (-y) ^ n = -y" using `0 < n` by simp
   2.410 -    with real_root_minus[OF `0 < n`] and `even n`
   2.411 +    with real_root_minus and `even n`
   2.412      show "- (root n y ^ n) = y" by simp
   2.413    qed
   2.414  next
   2.415 @@ -404,9 +329,7 @@
   2.416      by  (auto intro!: DERIV_intros)
   2.417    show "- real n * root n x ^ (n - Suc 0) \<noteq> 0"
   2.418      using n x by simp
   2.419 -  show "isCont (root n) x"
   2.420 -    using n by (rule isCont_real_root)
   2.421 -qed
   2.422 +qed (rule isCont_real_root)
   2.423  
   2.424  lemma DERIV_real_root_generic:
   2.425    assumes "0 < n" and "x \<noteq> 0"
   2.426 @@ -421,8 +344,7 @@
   2.427  
   2.428  subsection {* Square Root *}
   2.429  
   2.430 -definition
   2.431 -  sqrt :: "real \<Rightarrow> real" where
   2.432 +definition sqrt :: "real \<Rightarrow> real" where
   2.433    "sqrt = root 2"
   2.434  
   2.435  lemma pos2: "0 < (2::nat)" by simp
   2.436 @@ -453,16 +375,16 @@
   2.437  unfolding sqrt_def by (rule real_root_one [OF pos2])
   2.438  
   2.439  lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
   2.440 -unfolding sqrt_def by (rule real_root_minus [OF pos2])
   2.441 +unfolding sqrt_def by (rule real_root_minus)
   2.442  
   2.443  lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
   2.444 -unfolding sqrt_def by (rule real_root_mult [OF pos2])
   2.445 +unfolding sqrt_def by (rule real_root_mult)
   2.446  
   2.447  lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
   2.448 -unfolding sqrt_def by (rule real_root_inverse [OF pos2])
   2.449 +unfolding sqrt_def by (rule real_root_inverse)
   2.450  
   2.451  lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y"
   2.452 -unfolding sqrt_def by (rule real_root_divide [OF pos2])
   2.453 +unfolding sqrt_def by (rule real_root_divide)
   2.454  
   2.455  lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k"
   2.456  unfolding sqrt_def by (rule real_root_power [OF pos2])
   2.457 @@ -471,7 +393,7 @@
   2.458  unfolding sqrt_def by (rule real_root_gt_zero [OF pos2])
   2.459  
   2.460  lemma real_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> sqrt x"
   2.461 -unfolding sqrt_def by (rule real_root_ge_zero [OF pos2])
   2.462 +unfolding sqrt_def by (rule real_root_ge_zero)
   2.463  
   2.464  lemma real_sqrt_less_mono: "x < y \<Longrightarrow> sqrt x < sqrt y"
   2.465  unfolding sqrt_def by (rule real_root_less_mono [OF pos2])
   2.466 @@ -501,19 +423,19 @@
   2.467  lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified]
   2.468  
   2.469  lemma isCont_real_sqrt: "isCont sqrt x"
   2.470 -unfolding sqrt_def by (rule isCont_real_root [OF pos2])
   2.471 +unfolding sqrt_def by (rule isCont_real_root)
   2.472  
   2.473  lemma tendsto_real_sqrt[tendsto_intros]:
   2.474    "(f ---> x) F \<Longrightarrow> ((\<lambda>x. sqrt (f x)) ---> sqrt x) F"
   2.475 -  unfolding sqrt_def by (rule tendsto_real_root [OF _ pos2])
   2.476 +  unfolding sqrt_def by (rule tendsto_real_root)
   2.477  
   2.478  lemma continuous_real_sqrt[continuous_intros]:
   2.479    "continuous F f \<Longrightarrow> continuous F (\<lambda>x. sqrt (f x))"
   2.480 -  unfolding sqrt_def by (rule continuous_real_root [OF _ pos2])
   2.481 +  unfolding sqrt_def by (rule continuous_real_root)
   2.482    
   2.483  lemma continuous_on_real_sqrt[continuous_on_intros]:
   2.484    "continuous_on s f \<Longrightarrow> 0 < n \<Longrightarrow> continuous_on s (\<lambda>x. sqrt (f x))"
   2.485 -  unfolding sqrt_def by (rule continuous_on_real_root [OF _ pos2])
   2.486 +  unfolding sqrt_def by (rule continuous_on_real_root)
   2.487  
   2.488  lemma DERIV_real_sqrt_generic:
   2.489    assumes "x \<noteq> 0"