src/HOL/NthRoot.thy
changeset 28952 15a4b2cf8c34
parent 25875 536dfdc25e0a
child 30273 ecd6f0ca62ea
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/NthRoot.thy	Wed Dec 03 15:58:44 2008 +0100
     1.3 @@ -0,0 +1,631 @@
     1.4 +(*  Title       : NthRoot.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     1.8 +*)
     1.9 +
    1.10 +header {* Nth Roots of Real Numbers *}
    1.11 +
    1.12 +theory NthRoot
    1.13 +imports Parity Deriv
    1.14 +begin
    1.15 +
    1.16 +subsection {* Existence of Nth Root *}
    1.17 +
    1.18 +text {* Existence follows from the Intermediate Value Theorem *}
    1.19 +
    1.20 +lemma realpow_pos_nth:
    1.21 +  assumes n: "0 < n"
    1.22 +  assumes a: "0 < a"
    1.23 +  shows "\<exists>r>0. r ^ n = (a::real)"
    1.24 +proof -
    1.25 +  have "\<exists>r\<ge>0. r \<le> (max 1 a) \<and> r ^ n = a"
    1.26 +  proof (rule IVT)
    1.27 +    show "0 ^ n \<le> a" using n a by (simp add: power_0_left)
    1.28 +    show "0 \<le> max 1 a" by simp
    1.29 +    from n have n1: "1 \<le> n" by simp
    1.30 +    have "a \<le> max 1 a ^ 1" by simp
    1.31 +    also have "max 1 a ^ 1 \<le> max 1 a ^ n"
    1.32 +      using n1 by (rule power_increasing, simp)
    1.33 +    finally show "a \<le> max 1 a ^ n" .
    1.34 +    show "\<forall>r. 0 \<le> r \<and> r \<le> max 1 a \<longrightarrow> isCont (\<lambda>x. x ^ n) r"
    1.35 +      by (simp add: isCont_power)
    1.36 +  qed
    1.37 +  then obtain r where r: "0 \<le> r \<and> r ^ n = a" by fast
    1.38 +  with n a have "r \<noteq> 0" by (auto simp add: power_0_left)
    1.39 +  with r have "0 < r \<and> r ^ n = a" by simp
    1.40 +  thus ?thesis ..
    1.41 +qed
    1.42 +
    1.43 +(* Used by Integration/RealRandVar.thy in AFP *)
    1.44 +lemma realpow_pos_nth2: "(0::real) < a \<Longrightarrow> \<exists>r>0. r ^ Suc n = a"
    1.45 +by (blast intro: realpow_pos_nth)
    1.46 +
    1.47 +text {* Uniqueness of nth positive root *}
    1.48 +
    1.49 +lemma realpow_pos_nth_unique:
    1.50 +  "\<lbrakk>0 < n; 0 < a\<rbrakk> \<Longrightarrow> \<exists>!r. 0 < r \<and> r ^ n = (a::real)"
    1.51 +apply (auto intro!: realpow_pos_nth)
    1.52 +apply (rule_tac n=n in power_eq_imp_eq_base, simp_all)
    1.53 +done
    1.54 +
    1.55 +subsection {* Nth Root *}
    1.56 +
    1.57 +text {* We define roots of negative reals such that
    1.58 +  @{term "root n (- x) = - root n x"}. This allows
    1.59 +  us to omit side conditions from many theorems. *}
    1.60 +
    1.61 +definition
    1.62 +  root :: "[nat, real] \<Rightarrow> real" where
    1.63 +  "root n x = (if 0 < x then (THE u. 0 < u \<and> u ^ n = x) else
    1.64 +               if x < 0 then - (THE u. 0 < u \<and> u ^ n = - x) else 0)"
    1.65 +
    1.66 +lemma real_root_zero [simp]: "root n 0 = 0"
    1.67 +unfolding root_def by simp
    1.68 +
    1.69 +lemma real_root_minus: "0 < n \<Longrightarrow> root n (- x) = - root n x"
    1.70 +unfolding root_def by simp
    1.71 +
    1.72 +lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
    1.73 +apply (simp add: root_def)
    1.74 +apply (drule (1) realpow_pos_nth_unique)
    1.75 +apply (erule theI' [THEN conjunct1])
    1.76 +done
    1.77 +
    1.78 +lemma real_root_pow_pos: (* TODO: rename *)
    1.79 +  "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
    1.80 +apply (simp add: root_def)
    1.81 +apply (drule (1) realpow_pos_nth_unique)
    1.82 +apply (erule theI' [THEN conjunct2])
    1.83 +done
    1.84 +
    1.85 +lemma real_root_pow_pos2 [simp]: (* TODO: rename *)
    1.86 +  "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
    1.87 +by (auto simp add: order_le_less real_root_pow_pos)
    1.88 +
    1.89 +lemma odd_real_root_pow: "odd n \<Longrightarrow> root n x ^ n = x"
    1.90 +apply (rule_tac x=0 and y=x in linorder_le_cases)
    1.91 +apply (erule (1) real_root_pow_pos2 [OF odd_pos])
    1.92 +apply (subgoal_tac "root n (- x) ^ n = - x")
    1.93 +apply (simp add: real_root_minus odd_pos)
    1.94 +apply (simp add: odd_pos)
    1.95 +done
    1.96 +
    1.97 +lemma real_root_ge_zero: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> root n x"
    1.98 +by (auto simp add: order_le_less real_root_gt_zero)
    1.99 +
   1.100 +lemma real_root_power_cancel: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (x ^ n) = x"
   1.101 +apply (subgoal_tac "0 \<le> x ^ n")
   1.102 +apply (subgoal_tac "0 \<le> root n (x ^ n)")
   1.103 +apply (subgoal_tac "root n (x ^ n) ^ n = x ^ n")
   1.104 +apply (erule (3) power_eq_imp_eq_base)
   1.105 +apply (erule (1) real_root_pow_pos2)
   1.106 +apply (erule (1) real_root_ge_zero)
   1.107 +apply (erule zero_le_power)
   1.108 +done
   1.109 +
   1.110 +lemma odd_real_root_power_cancel: "odd n \<Longrightarrow> root n (x ^ n) = x"
   1.111 +apply (rule_tac x=0 and y=x in linorder_le_cases)
   1.112 +apply (erule (1) real_root_power_cancel [OF odd_pos])
   1.113 +apply (subgoal_tac "root n ((- x) ^ n) = - x")
   1.114 +apply (simp add: real_root_minus odd_pos)
   1.115 +apply (erule real_root_power_cancel [OF odd_pos], simp)
   1.116 +done
   1.117 +
   1.118 +lemma real_root_pos_unique:
   1.119 +  "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   1.120 +by (erule subst, rule real_root_power_cancel)
   1.121 +
   1.122 +lemma odd_real_root_unique:
   1.123 +  "\<lbrakk>odd n; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   1.124 +by (erule subst, rule odd_real_root_power_cancel)
   1.125 +
   1.126 +lemma real_root_one [simp]: "0 < n \<Longrightarrow> root n 1 = 1"
   1.127 +by (simp add: real_root_pos_unique)
   1.128 +
   1.129 +text {* Root function is strictly monotonic, hence injective *}
   1.130 +
   1.131 +lemma real_root_less_mono_lemma:
   1.132 +  "\<lbrakk>0 < n; 0 \<le> x; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   1.133 +apply (subgoal_tac "0 \<le> y")
   1.134 +apply (subgoal_tac "root n x ^ n < root n y ^ n")
   1.135 +apply (erule power_less_imp_less_base)
   1.136 +apply (erule (1) real_root_ge_zero)
   1.137 +apply simp
   1.138 +apply simp
   1.139 +done
   1.140 +
   1.141 +lemma real_root_less_mono: "\<lbrakk>0 < n; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   1.142 +apply (cases "0 \<le> x")
   1.143 +apply (erule (2) real_root_less_mono_lemma)
   1.144 +apply (cases "0 \<le> y")
   1.145 +apply (rule_tac y=0 in order_less_le_trans)
   1.146 +apply (subgoal_tac "0 < root n (- x)")
   1.147 +apply (simp add: real_root_minus)
   1.148 +apply (simp add: real_root_gt_zero)
   1.149 +apply (simp add: real_root_ge_zero)
   1.150 +apply (subgoal_tac "root n (- y) < root n (- x)")
   1.151 +apply (simp add: real_root_minus)
   1.152 +apply (simp add: real_root_less_mono_lemma)
   1.153 +done
   1.154 +
   1.155 +lemma real_root_le_mono: "\<lbrakk>0 < n; x \<le> y\<rbrakk> \<Longrightarrow> root n x \<le> root n y"
   1.156 +by (auto simp add: order_le_less real_root_less_mono)
   1.157 +
   1.158 +lemma real_root_less_iff [simp]:
   1.159 +  "0 < n \<Longrightarrow> (root n x < root n y) = (x < y)"
   1.160 +apply (cases "x < y")
   1.161 +apply (simp add: real_root_less_mono)
   1.162 +apply (simp add: linorder_not_less real_root_le_mono)
   1.163 +done
   1.164 +
   1.165 +lemma real_root_le_iff [simp]:
   1.166 +  "0 < n \<Longrightarrow> (root n x \<le> root n y) = (x \<le> y)"
   1.167 +apply (cases "x \<le> y")
   1.168 +apply (simp add: real_root_le_mono)
   1.169 +apply (simp add: linorder_not_le real_root_less_mono)
   1.170 +done
   1.171 +
   1.172 +lemma real_root_eq_iff [simp]:
   1.173 +  "0 < n \<Longrightarrow> (root n x = root n y) = (x = y)"
   1.174 +by (simp add: order_eq_iff)
   1.175 +
   1.176 +lemmas real_root_gt_0_iff [simp] = real_root_less_iff [where x=0, simplified]
   1.177 +lemmas real_root_lt_0_iff [simp] = real_root_less_iff [where y=0, simplified]
   1.178 +lemmas real_root_ge_0_iff [simp] = real_root_le_iff [where x=0, simplified]
   1.179 +lemmas real_root_le_0_iff [simp] = real_root_le_iff [where y=0, simplified]
   1.180 +lemmas real_root_eq_0_iff [simp] = real_root_eq_iff [where y=0, simplified]
   1.181 +
   1.182 +lemma real_root_gt_1_iff [simp]: "0 < n \<Longrightarrow> (1 < root n y) = (1 < y)"
   1.183 +by (insert real_root_less_iff [where x=1], simp)
   1.184 +
   1.185 +lemma real_root_lt_1_iff [simp]: "0 < n \<Longrightarrow> (root n x < 1) = (x < 1)"
   1.186 +by (insert real_root_less_iff [where y=1], simp)
   1.187 +
   1.188 +lemma real_root_ge_1_iff [simp]: "0 < n \<Longrightarrow> (1 \<le> root n y) = (1 \<le> y)"
   1.189 +by (insert real_root_le_iff [where x=1], simp)
   1.190 +
   1.191 +lemma real_root_le_1_iff [simp]: "0 < n \<Longrightarrow> (root n x \<le> 1) = (x \<le> 1)"
   1.192 +by (insert real_root_le_iff [where y=1], simp)
   1.193 +
   1.194 +lemma real_root_eq_1_iff [simp]: "0 < n \<Longrightarrow> (root n x = 1) = (x = 1)"
   1.195 +by (insert real_root_eq_iff [where y=1], simp)
   1.196 +
   1.197 +text {* Roots of roots *}
   1.198 +
   1.199 +lemma real_root_Suc_0 [simp]: "root (Suc 0) x = x"
   1.200 +by (simp add: odd_real_root_unique)
   1.201 +
   1.202 +lemma real_root_pos_mult_exp:
   1.203 +  "\<lbrakk>0 < m; 0 < n; 0 < x\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
   1.204 +by (rule real_root_pos_unique, simp_all add: power_mult)
   1.205 +
   1.206 +lemma real_root_mult_exp:
   1.207 +  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root (m * n) x = root m (root n x)"
   1.208 +apply (rule linorder_cases [where x=x and y=0])
   1.209 +apply (subgoal_tac "root (m * n) (- x) = root m (root n (- x))")
   1.210 +apply (simp add: real_root_minus)
   1.211 +apply (simp_all add: real_root_pos_mult_exp)
   1.212 +done
   1.213 +
   1.214 +lemma real_root_commute:
   1.215 +  "\<lbrakk>0 < m; 0 < n\<rbrakk> \<Longrightarrow> root m (root n x) = root n (root m x)"
   1.216 +by (simp add: real_root_mult_exp [symmetric] mult_commute)
   1.217 +
   1.218 +text {* Monotonicity in first argument *}
   1.219 +
   1.220 +lemma real_root_strict_decreasing:
   1.221 +  "\<lbrakk>0 < n; n < N; 1 < x\<rbrakk> \<Longrightarrow> root N x < root n x"
   1.222 +apply (subgoal_tac "root n (root N x) ^ n < root N (root n x) ^ N", simp)
   1.223 +apply (simp add: real_root_commute power_strict_increasing
   1.224 +            del: real_root_pow_pos2)
   1.225 +done
   1.226 +
   1.227 +lemma real_root_strict_increasing:
   1.228 +  "\<lbrakk>0 < n; n < N; 0 < x; x < 1\<rbrakk> \<Longrightarrow> root n x < root N x"
   1.229 +apply (subgoal_tac "root N (root n x) ^ N < root n (root N x) ^ n", simp)
   1.230 +apply (simp add: real_root_commute power_strict_decreasing
   1.231 +            del: real_root_pow_pos2)
   1.232 +done
   1.233 +
   1.234 +lemma real_root_decreasing:
   1.235 +  "\<lbrakk>0 < n; n < N; 1 \<le> x\<rbrakk> \<Longrightarrow> root N x \<le> root n x"
   1.236 +by (auto simp add: order_le_less real_root_strict_decreasing)
   1.237 +
   1.238 +lemma real_root_increasing:
   1.239 +  "\<lbrakk>0 < n; n < N; 0 \<le> x; x \<le> 1\<rbrakk> \<Longrightarrow> root n x \<le> root N x"
   1.240 +by (auto simp add: order_le_less real_root_strict_increasing)
   1.241 +
   1.242 +text {* Roots of multiplication and division *}
   1.243 +
   1.244 +lemma real_root_mult_lemma:
   1.245 +  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> root n (x * y) = root n x * root n y"
   1.246 +by (simp add: real_root_pos_unique mult_nonneg_nonneg power_mult_distrib)
   1.247 +
   1.248 +lemma real_root_inverse_lemma:
   1.249 +  "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (inverse x) = inverse (root n x)"
   1.250 +by (simp add: real_root_pos_unique power_inverse [symmetric])
   1.251 +
   1.252 +lemma real_root_mult:
   1.253 +  assumes n: "0 < n"
   1.254 +  shows "root n (x * y) = root n x * root n y"
   1.255 +proof (rule linorder_le_cases, rule_tac [!] linorder_le_cases)
   1.256 +  assume "0 \<le> x" and "0 \<le> y"
   1.257 +  thus ?thesis by (rule real_root_mult_lemma [OF n])
   1.258 +next
   1.259 +  assume "0 \<le> x" and "y \<le> 0"
   1.260 +  hence "0 \<le> x" and "0 \<le> - y" by simp_all
   1.261 +  hence "root n (x * - y) = root n x * root n (- y)"
   1.262 +    by (rule real_root_mult_lemma [OF n])
   1.263 +  thus ?thesis by (simp add: real_root_minus [OF n])
   1.264 +next
   1.265 +  assume "x \<le> 0" and "0 \<le> y"
   1.266 +  hence "0 \<le> - x" and "0 \<le> y" by simp_all
   1.267 +  hence "root n (- x * y) = root n (- x) * root n y"
   1.268 +    by (rule real_root_mult_lemma [OF n])
   1.269 +  thus ?thesis by (simp add: real_root_minus [OF n])
   1.270 +next
   1.271 +  assume "x \<le> 0" and "y \<le> 0"
   1.272 +  hence "0 \<le> - x" and "0 \<le> - y" by simp_all
   1.273 +  hence "root n (- x * - y) = root n (- x) * root n (- y)"
   1.274 +    by (rule real_root_mult_lemma [OF n])
   1.275 +  thus ?thesis by (simp add: real_root_minus [OF n])
   1.276 +qed
   1.277 +
   1.278 +lemma real_root_inverse:
   1.279 +  assumes n: "0 < n"
   1.280 +  shows "root n (inverse x) = inverse (root n x)"
   1.281 +proof (rule linorder_le_cases)
   1.282 +  assume "0 \<le> x"
   1.283 +  thus ?thesis by (rule real_root_inverse_lemma [OF n])
   1.284 +next
   1.285 +  assume "x \<le> 0"
   1.286 +  hence "0 \<le> - x" by simp
   1.287 +  hence "root n (inverse (- x)) = inverse (root n (- x))"
   1.288 +    by (rule real_root_inverse_lemma [OF n])
   1.289 +  thus ?thesis by (simp add: real_root_minus [OF n])
   1.290 +qed
   1.291 +
   1.292 +lemma real_root_divide:
   1.293 +  "0 < n \<Longrightarrow> root n (x / y) = root n x / root n y"
   1.294 +by (simp add: divide_inverse real_root_mult real_root_inverse)
   1.295 +
   1.296 +lemma real_root_power:
   1.297 +  "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   1.298 +by (induct k, simp_all add: real_root_mult)
   1.299 +
   1.300 +lemma real_root_abs: "0 < n \<Longrightarrow> root n \<bar>x\<bar> = \<bar>root n x\<bar>"
   1.301 +by (simp add: abs_if real_root_minus)
   1.302 +
   1.303 +text {* Continuity and derivatives *}
   1.304 +
   1.305 +lemma isCont_root_pos:
   1.306 +  assumes n: "0 < n"
   1.307 +  assumes x: "0 < x"
   1.308 +  shows "isCont (root n) x"
   1.309 +proof -
   1.310 +  have "isCont (root n) (root n x ^ n)"
   1.311 +  proof (rule isCont_inverse_function [where f="\<lambda>a. a ^ n"])
   1.312 +    show "0 < root n x" using n x by simp
   1.313 +    show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> root n (z ^ n) = z"
   1.314 +      by (simp add: abs_le_iff real_root_power_cancel n)
   1.315 +    show "\<forall>z. \<bar>z - root n x\<bar> \<le> root n x \<longrightarrow> isCont (\<lambda>a. a ^ n) z"
   1.316 +      by (simp add: isCont_power)
   1.317 +  qed
   1.318 +  thus ?thesis using n x by simp
   1.319 +qed
   1.320 +
   1.321 +lemma isCont_root_neg:
   1.322 +  "\<lbrakk>0 < n; x < 0\<rbrakk> \<Longrightarrow> isCont (root n) x"
   1.323 +apply (subgoal_tac "isCont (\<lambda>x. - root n (- x)) x")
   1.324 +apply (simp add: real_root_minus)
   1.325 +apply (rule isCont_o2 [OF isCont_minus [OF isCont_ident]])
   1.326 +apply (simp add: isCont_minus isCont_root_pos)
   1.327 +done
   1.328 +
   1.329 +lemma isCont_root_zero:
   1.330 +  "0 < n \<Longrightarrow> isCont (root n) 0"
   1.331 +unfolding isCont_def
   1.332 +apply (rule LIM_I)
   1.333 +apply (rule_tac x="r ^ n" in exI, safe)
   1.334 +apply (simp)
   1.335 +apply (simp add: real_root_abs [symmetric])
   1.336 +apply (rule_tac n="n" in power_less_imp_less_base, simp_all)
   1.337 +done
   1.338 +
   1.339 +lemma isCont_real_root: "0 < n \<Longrightarrow> isCont (root n) x"
   1.340 +apply (rule_tac x=x and y=0 in linorder_cases)
   1.341 +apply (simp_all add: isCont_root_pos isCont_root_neg isCont_root_zero)
   1.342 +done
   1.343 +
   1.344 +lemma DERIV_real_root:
   1.345 +  assumes n: "0 < n"
   1.346 +  assumes x: "0 < x"
   1.347 +  shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))"
   1.348 +proof (rule DERIV_inverse_function)
   1.349 +  show "0 < x" using x .
   1.350 +  show "x < x + 1" by simp
   1.351 +  show "\<forall>y. 0 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
   1.352 +    using n by simp
   1.353 +  show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
   1.354 +    by (rule DERIV_pow)
   1.355 +  show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
   1.356 +    using n x by simp
   1.357 +  show "isCont (root n) x"
   1.358 +    using n by (rule isCont_real_root)
   1.359 +qed
   1.360 +
   1.361 +lemma DERIV_odd_real_root:
   1.362 +  assumes n: "odd n"
   1.363 +  assumes x: "x \<noteq> 0"
   1.364 +  shows "DERIV (root n) x :> inverse (real n * root n x ^ (n - Suc 0))"
   1.365 +proof (rule DERIV_inverse_function)
   1.366 +  show "x - 1 < x" by simp
   1.367 +  show "x < x + 1" by simp
   1.368 +  show "\<forall>y. x - 1 < y \<and> y < x + 1 \<longrightarrow> root n y ^ n = y"
   1.369 +    using n by (simp add: odd_real_root_pow)
   1.370 +  show "DERIV (\<lambda>x. x ^ n) (root n x) :> real n * root n x ^ (n - Suc 0)"
   1.371 +    by (rule DERIV_pow)
   1.372 +  show "real n * root n x ^ (n - Suc 0) \<noteq> 0"
   1.373 +    using odd_pos [OF n] x by simp
   1.374 +  show "isCont (root n) x"
   1.375 +    using odd_pos [OF n] by (rule isCont_real_root)
   1.376 +qed
   1.377 +
   1.378 +subsection {* Square Root *}
   1.379 +
   1.380 +definition
   1.381 +  sqrt :: "real \<Rightarrow> real" where
   1.382 +  "sqrt = root 2"
   1.383 +
   1.384 +lemma pos2: "0 < (2::nat)" by simp
   1.385 +
   1.386 +lemma real_sqrt_unique: "\<lbrakk>y\<twosuperior> = x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt x = y"
   1.387 +unfolding sqrt_def by (rule real_root_pos_unique [OF pos2])
   1.388 +
   1.389 +lemma real_sqrt_abs [simp]: "sqrt (x\<twosuperior>) = \<bar>x\<bar>"
   1.390 +apply (rule real_sqrt_unique)
   1.391 +apply (rule power2_abs)
   1.392 +apply (rule abs_ge_zero)
   1.393 +done
   1.394 +
   1.395 +lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<twosuperior> = x"
   1.396 +unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2])
   1.397 +
   1.398 +lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
   1.399 +apply (rule iffI)
   1.400 +apply (erule subst)
   1.401 +apply (rule zero_le_power2)
   1.402 +apply (erule real_sqrt_pow2)
   1.403 +done
   1.404 +
   1.405 +lemma real_sqrt_zero [simp]: "sqrt 0 = 0"
   1.406 +unfolding sqrt_def by (rule real_root_zero)
   1.407 +
   1.408 +lemma real_sqrt_one [simp]: "sqrt 1 = 1"
   1.409 +unfolding sqrt_def by (rule real_root_one [OF pos2])
   1.410 +
   1.411 +lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
   1.412 +unfolding sqrt_def by (rule real_root_minus [OF pos2])
   1.413 +
   1.414 +lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
   1.415 +unfolding sqrt_def by (rule real_root_mult [OF pos2])
   1.416 +
   1.417 +lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
   1.418 +unfolding sqrt_def by (rule real_root_inverse [OF pos2])
   1.419 +
   1.420 +lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y"
   1.421 +unfolding sqrt_def by (rule real_root_divide [OF pos2])
   1.422 +
   1.423 +lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k"
   1.424 +unfolding sqrt_def by (rule real_root_power [OF pos2])
   1.425 +
   1.426 +lemma real_sqrt_gt_zero: "0 < x \<Longrightarrow> 0 < sqrt x"
   1.427 +unfolding sqrt_def by (rule real_root_gt_zero [OF pos2])
   1.428 +
   1.429 +lemma real_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> sqrt x"
   1.430 +unfolding sqrt_def by (rule real_root_ge_zero [OF pos2])
   1.431 +
   1.432 +lemma real_sqrt_less_mono: "x < y \<Longrightarrow> sqrt x < sqrt y"
   1.433 +unfolding sqrt_def by (rule real_root_less_mono [OF pos2])
   1.434 +
   1.435 +lemma real_sqrt_le_mono: "x \<le> y \<Longrightarrow> sqrt x \<le> sqrt y"
   1.436 +unfolding sqrt_def by (rule real_root_le_mono [OF pos2])
   1.437 +
   1.438 +lemma real_sqrt_less_iff [simp]: "(sqrt x < sqrt y) = (x < y)"
   1.439 +unfolding sqrt_def by (rule real_root_less_iff [OF pos2])
   1.440 +
   1.441 +lemma real_sqrt_le_iff [simp]: "(sqrt x \<le> sqrt y) = (x \<le> y)"
   1.442 +unfolding sqrt_def by (rule real_root_le_iff [OF pos2])
   1.443 +
   1.444 +lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
   1.445 +unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
   1.446 +
   1.447 +lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, simplified]
   1.448 +lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, simplified]
   1.449 +lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, simplified]
   1.450 +lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, simplified]
   1.451 +lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, simplified]
   1.452 +
   1.453 +lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, simplified]
   1.454 +lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, simplified]
   1.455 +lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, simplified]
   1.456 +lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, simplified]
   1.457 +lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified]
   1.458 +
   1.459 +lemma isCont_real_sqrt: "isCont sqrt x"
   1.460 +unfolding sqrt_def by (rule isCont_real_root [OF pos2])
   1.461 +
   1.462 +lemma DERIV_real_sqrt:
   1.463 +  "0 < x \<Longrightarrow> DERIV sqrt x :> inverse (sqrt x) / 2"
   1.464 +unfolding sqrt_def by (rule DERIV_real_root [OF pos2, simplified])
   1.465 +
   1.466 +lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
   1.467 +apply auto
   1.468 +apply (cut_tac x = x and y = 0 in linorder_less_linear)
   1.469 +apply (simp add: zero_less_mult_iff)
   1.470 +done
   1.471 +
   1.472 +lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \<bar>x\<bar>"
   1.473 +apply (subst power2_eq_square [symmetric])
   1.474 +apply (rule real_sqrt_abs)
   1.475 +done
   1.476 +
   1.477 +lemma real_sqrt_pow2_gt_zero: "0 < x ==> 0 < (sqrt x)\<twosuperior>"
   1.478 +by simp (* TODO: delete *)
   1.479 +
   1.480 +lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 0"
   1.481 +by simp (* TODO: delete *)
   1.482 +
   1.483 +lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
   1.484 +by (simp add: power_inverse [symmetric])
   1.485 +
   1.486 +lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
   1.487 +by simp
   1.488 +
   1.489 +lemma real_sqrt_ge_one: "1 \<le> x ==> 1 \<le> sqrt x"
   1.490 +by simp
   1.491 +
   1.492 +lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2"
   1.493 +by simp
   1.494 +
   1.495 +lemma real_sqrt_two_ge_zero [simp]: "0 \<le> sqrt 2"
   1.496 +by simp
   1.497 +
   1.498 +lemma real_sqrt_two_gt_one [simp]: "1 < sqrt 2"
   1.499 +by simp
   1.500 +
   1.501 +lemma sqrt_divide_self_eq:
   1.502 +  assumes nneg: "0 \<le> x"
   1.503 +  shows "sqrt x / x = inverse (sqrt x)"
   1.504 +proof cases
   1.505 +  assume "x=0" thus ?thesis by simp
   1.506 +next
   1.507 +  assume nz: "x\<noteq>0" 
   1.508 +  hence pos: "0<x" using nneg by arith
   1.509 +  show ?thesis
   1.510 +  proof (rule right_inverse_eq [THEN iffD1, THEN sym]) 
   1.511 +    show "sqrt x / x \<noteq> 0" by (simp add: divide_inverse nneg nz) 
   1.512 +    show "inverse (sqrt x) / (sqrt x / x) = 1"
   1.513 +      by (simp add: divide_inverse mult_assoc [symmetric] 
   1.514 +                  power2_eq_square [symmetric] real_inv_sqrt_pow2 pos nz) 
   1.515 +  qed
   1.516 +qed
   1.517 +
   1.518 +lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
   1.519 +apply (simp add: divide_inverse)
   1.520 +apply (case_tac "r=0")
   1.521 +apply (auto simp add: mult_ac)
   1.522 +done
   1.523 +
   1.524 +lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
   1.525 +by (simp add: divide_less_eq mult_compare_simps)
   1.526 +
   1.527 +lemma four_x_squared: 
   1.528 +  fixes x::real
   1.529 +  shows "4 * x\<twosuperior> = (2 * x)\<twosuperior>"
   1.530 +by (simp add: power2_eq_square)
   1.531 +
   1.532 +subsection {* Square Root of Sum of Squares *}
   1.533 +
   1.534 +lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
   1.535 +by (rule real_sqrt_ge_zero [OF sum_squares_ge_zero])
   1.536 +
   1.537 +lemma real_sqrt_sum_squares_ge_zero [simp]: "0 \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
   1.538 +by simp
   1.539 +
   1.540 +declare real_sqrt_sum_squares_ge_zero [THEN abs_of_nonneg, simp]
   1.541 +
   1.542 +lemma real_sqrt_sum_squares_mult_ge_zero [simp]:
   1.543 +     "0 \<le> sqrt ((x\<twosuperior> + y\<twosuperior>)*(xa\<twosuperior> + ya\<twosuperior>))"
   1.544 +by (auto intro!: real_sqrt_ge_zero simp add: zero_le_mult_iff)
   1.545 +
   1.546 +lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
   1.547 +     "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
   1.548 +by (auto simp add: zero_le_mult_iff)
   1.549 +
   1.550 +lemma real_sqrt_sum_squares_eq_cancel: "sqrt (x\<twosuperior> + y\<twosuperior>) = x \<Longrightarrow> y = 0"
   1.551 +by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
   1.552 +
   1.553 +lemma real_sqrt_sum_squares_eq_cancel2: "sqrt (x\<twosuperior> + y\<twosuperior>) = y \<Longrightarrow> x = 0"
   1.554 +by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, simp)
   1.555 +
   1.556 +lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
   1.557 +by (rule power2_le_imp_le, simp_all)
   1.558 +
   1.559 +lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
   1.560 +by (rule power2_le_imp_le, simp_all)
   1.561 +
   1.562 +lemma real_sqrt_ge_abs1 [simp]: "\<bar>x\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
   1.563 +by (rule power2_le_imp_le, simp_all)
   1.564 +
   1.565 +lemma real_sqrt_ge_abs2 [simp]: "\<bar>y\<bar> \<le> sqrt (x\<twosuperior> + y\<twosuperior>)"
   1.566 +by (rule power2_le_imp_le, simp_all)
   1.567 +
   1.568 +lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
   1.569 +by (simp add: power2_eq_square [symmetric])
   1.570 +
   1.571 +lemma power2_sum:
   1.572 +  fixes x y :: "'a::{number_ring,recpower}"
   1.573 +  shows "(x + y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> + 2 * x * y"
   1.574 +by (simp add: ring_distribs power2_eq_square)
   1.575 +
   1.576 +lemma power2_diff:
   1.577 +  fixes x y :: "'a::{number_ring,recpower}"
   1.578 +  shows "(x - y)\<twosuperior> = x\<twosuperior> + y\<twosuperior> - 2 * x * y"
   1.579 +by (simp add: ring_distribs power2_eq_square)
   1.580 +
   1.581 +lemma real_sqrt_sum_squares_triangle_ineq:
   1.582 +  "sqrt ((a + c)\<twosuperior> + (b + d)\<twosuperior>) \<le> sqrt (a\<twosuperior> + b\<twosuperior>) + sqrt (c\<twosuperior> + d\<twosuperior>)"
   1.583 +apply (rule power2_le_imp_le, simp)
   1.584 +apply (simp add: power2_sum)
   1.585 +apply (simp only: mult_assoc right_distrib [symmetric])
   1.586 +apply (rule mult_left_mono)
   1.587 +apply (rule power2_le_imp_le)
   1.588 +apply (simp add: power2_sum power_mult_distrib)
   1.589 +apply (simp add: ring_distribs)
   1.590 +apply (subgoal_tac "0 \<le> b\<twosuperior> * c\<twosuperior> + a\<twosuperior> * d\<twosuperior> - 2 * (a * c) * (b * d)", simp)
   1.591 +apply (rule_tac b="(a * d - b * c)\<twosuperior>" in ord_le_eq_trans)
   1.592 +apply (rule zero_le_power2)
   1.593 +apply (simp add: power2_diff power_mult_distrib)
   1.594 +apply (simp add: mult_nonneg_nonneg)
   1.595 +apply simp
   1.596 +apply (simp add: add_increasing)
   1.597 +done
   1.598 +
   1.599 +lemma real_sqrt_sum_squares_less:
   1.600 +  "\<lbrakk>\<bar>x\<bar> < u / sqrt 2; \<bar>y\<bar> < u / sqrt 2\<rbrakk> \<Longrightarrow> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
   1.601 +apply (rule power2_less_imp_less, simp)
   1.602 +apply (drule power_strict_mono [OF _ abs_ge_zero pos2])
   1.603 +apply (drule power_strict_mono [OF _ abs_ge_zero pos2])
   1.604 +apply (simp add: power_divide)
   1.605 +apply (drule order_le_less_trans [OF abs_ge_zero])
   1.606 +apply (simp add: zero_less_divide_iff)
   1.607 +done
   1.608 +
   1.609 +text{*Needed for the infinitely close relation over the nonstandard
   1.610 +    complex numbers*}
   1.611 +lemma lemma_sqrt_hcomplex_capprox:
   1.612 +     "[| 0 < u; x < u/2; y < u/2; 0 \<le> x; 0 \<le> y |] ==> sqrt (x\<twosuperior> + y\<twosuperior>) < u"
   1.613 +apply (rule_tac y = "u/sqrt 2" in order_le_less_trans)
   1.614 +apply (erule_tac [2] lemma_real_divide_sqrt_less)
   1.615 +apply (rule power2_le_imp_le)
   1.616 +apply (auto simp add: real_0_le_divide_iff power_divide)
   1.617 +apply (rule_tac t = "u\<twosuperior>" in real_sum_of_halves [THEN subst])
   1.618 +apply (rule add_mono)
   1.619 +apply (auto simp add: four_x_squared simp del: realpow_Suc intro: power_mono)
   1.620 +done
   1.621 +
   1.622 +text "Legacy theorem names:"
   1.623 +lemmas real_root_pos2 = real_root_power_cancel
   1.624 +lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
   1.625 +lemmas real_root_pos_pos_le = real_root_ge_zero
   1.626 +lemmas real_sqrt_mult_distrib = real_sqrt_mult
   1.627 +lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
   1.628 +lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
   1.629 +
   1.630 +(* needed for CauchysMeanTheorem.het_base from AFP *)
   1.631 +lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
   1.632 +by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
   1.633 +
   1.634 +end