author hoelzl Fri Mar 22 10:41:43 2013 +0100 (2013-03-22) changeset 51483 dc39d69774bb 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 file | annotate | diff | revisions src/HOL/NthRoot.thy file | annotate | diff | revisions
```     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.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.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.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.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.186 -apply (subgoal_tac "root n (- y) < root n (- x)")
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.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.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.343 -apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
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.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"
```