define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
authorhuffman
Sun May 13 20:05:42 2007 +0200 (2007-05-13)
changeset 22956617140080e6a
parent 22955 48dc37776d1e
child 22957 82a799ae7579
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
src/HOL/Complex/Complex.thy
src/HOL/Complex/NSCA.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Transcendental.thy
     1.1 --- a/src/HOL/Complex/Complex.thy	Sun May 13 19:15:36 2007 +0200
     1.2 +++ b/src/HOL/Complex/Complex.thy	Sun May 13 20:05:42 2007 +0200
     1.3 @@ -394,7 +394,6 @@
     1.4  lemma complex_mod_mult: "cmod (x * y) = cmod x * cmod y"
     1.5  apply (induct x, induct y)
     1.6  apply (simp add: real_sqrt_mult_distrib [symmetric])
     1.7 -apply (rule_tac f=sqrt in arg_cong)
     1.8  apply (simp add: power2_sum power2_diff power_mult_distrib ring_distrib)
     1.9  done
    1.10  
    1.11 @@ -618,9 +617,7 @@
    1.12  
    1.13  lemma complex_mod_sqrt_Re_mult_cnj: "cmod z = sqrt (Re (z * cnj z))"
    1.14  apply (simp add: cmod_def)
    1.15 -apply (rule real_sqrt_eq_iff [THEN iffD2])
    1.16 -apply (auto simp add: complex_mult_cnj
    1.17 -            simp del: of_real_add)
    1.18 +apply (simp add: complex_mult_cnj del: of_real_add)
    1.19  done
    1.20  
    1.21  lemma complex_Re_cnj [simp]: "Re(cnj z) = Re z"
     2.1 --- a/src/HOL/Complex/NSCA.thy	Sun May 13 19:15:36 2007 +0200
     2.2 +++ b/src/HOL/Complex/NSCA.thy	Sun May 13 20:05:42 2007 +0200
     2.3 @@ -269,11 +269,12 @@
     2.4  apply (erule (1) InfinitesimalD2)
     2.5  done
     2.6  
     2.7 -lemma real_sqrt_lessI: "\<lbrakk>0 \<le> x; 0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> sqrt x < u"
     2.8 -by (frule (1) real_sqrt_less_mono) simp
     2.9 +lemma real_sqrt_lessI: "\<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> sqrt x < u"
    2.10 +(* TODO: this belongs somewhere else *)
    2.11 +by (frule real_sqrt_less_mono) simp
    2.12  
    2.13  lemma hypreal_sqrt_lessI:
    2.14 -  "\<And>x u. \<lbrakk>0 \<le> x; 0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"
    2.15 +  "\<And>x u. \<lbrakk>0 < u; x < u\<twosuperior>\<rbrakk> \<Longrightarrow> ( *f* sqrt) x < u"
    2.16  by transfer (rule real_sqrt_lessI)
    2.17   
    2.18  lemma hypreal_sqrt_ge_zero: "\<And>x. 0 \<le> x \<Longrightarrow> 0 \<le> ( *f* sqrt) x"
     3.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Sun May 13 19:15:36 2007 +0200
     3.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Sun May 13 20:05:42 2007 +0200
     3.3 @@ -4,20 +4,13 @@
     3.4      Conversion to Isar and new proofs by Lawrence C Paulson, 2004
     3.5  *)
     3.6  
     3.7 -header{*Existence of Nth Root*}
     3.8 +header {* Nth Roots of Real Numbers *}
     3.9  
    3.10  theory NthRoot
    3.11  imports SEQ Parity
    3.12  begin
    3.13  
    3.14 -definition
    3.15 -  root :: "[nat, real] \<Rightarrow> real" where
    3.16 -  "root n x = (THE u. (0 < x \<longrightarrow> 0 < u) \<and> (u ^ n = x))"
    3.17 -
    3.18 -definition
    3.19 -  sqrt :: "real \<Rightarrow> real" where
    3.20 -  "sqrt x = root 2 x"
    3.21 -
    3.22 +subsection {* Existence of Nth Root *}
    3.23  
    3.24  text {*
    3.25    Various lemmas needed for this result. We follow the proof given by
    3.26 @@ -65,7 +58,7 @@
    3.27  by (blast intro: lemma_nth_realpow_isUb_ex lemma_nth_realpow_non_empty reals_complete)
    3.28  
    3.29   
    3.30 -subsection{*First Half -- Lemmas First*}
    3.31 +subsubsection {* First Half -- Lemmas First *}
    3.32  
    3.33  lemma lemma_nth_realpow_seq:
    3.34       "isLub (UNIV::real set) {x. x ^ n <= a & (0::real) < x} u  
    3.35 @@ -104,7 +97,7 @@
    3.36  apply (auto simp add: real_of_nat_def)
    3.37  done
    3.38  
    3.39 -subsection{*Second Half*}
    3.40 +subsubsection {* Second Half *}
    3.41  
    3.42  lemma less_isLub_not_isUb:
    3.43       "[| isLub (UNIV::real set) S u; x < u |]  
    3.44 @@ -165,7 +158,7 @@
    3.45  apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym)
    3.46  done
    3.47  
    3.48 -(* positive only *)
    3.49 +text {* positive only *}
    3.50  lemma realpow_pos_nth: "[| (0::real) < a; 0 < n |] ==> \<exists>r. 0 < r & r ^ n = a"
    3.51  apply (frule nth_realpow_isLub_ex, auto)
    3.52  apply (auto intro: realpow_nth_le realpow_nth_ge order_antisym lemma_nth_realpow_isLub_gt_zero)
    3.53 @@ -174,7 +167,7 @@
    3.54  lemma realpow_pos_nth2: "(0::real) < a  ==> \<exists>r. 0 < r & r ^ Suc n = a"
    3.55  by (blast intro: realpow_pos_nth)
    3.56  
    3.57 -(* uniqueness of nth positive root *)
    3.58 +text {* uniqueness of nth positive root *}
    3.59  lemma realpow_pos_nth_unique:
    3.60       "[| (0::real) < a; 0 < n |] ==> EX! r. 0 < r & r ^ n = a"
    3.61  apply (auto intro!: realpow_pos_nth)
    3.62 @@ -185,159 +178,250 @@
    3.63  
    3.64  subsection {* Nth Root *}
    3.65  
    3.66 -lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
    3.67 -apply (simp add: root_def)
    3.68 -apply (safe intro!: the_equality power_0_Suc elim!: realpow_zero_zero)
    3.69 -done
    3.70 +text {* We define roots of negative reals such that
    3.71 +  @{term "root n (- x) = - root n x"}. This allows
    3.72 +  us to omit side conditions from many theorems. *}
    3.73  
    3.74 -lemma real_root_pow_pos: 
    3.75 -     "0 < x ==> (root (Suc n) x) ^ (Suc n) = x"
    3.76 -apply (simp add: root_def del: realpow_Suc)
    3.77 -apply (drule_tac n="Suc n" in realpow_pos_nth_unique, simp)
    3.78 -apply (erule theI' [THEN conjunct2])
    3.79 -done
    3.80 -
    3.81 -lemma real_root_pow_pos2: "0 \<le> x ==> (root (Suc n) x) ^ (Suc n) = x"
    3.82 -by (auto dest!: real_le_imp_less_or_eq dest: real_root_pow_pos)
    3.83 +definition
    3.84 +  root :: "[nat, real] \<Rightarrow> real" where
    3.85 +  "root n x = (if 0 < x then (THE u. 0 < u \<and> u ^ n = x) else
    3.86 +               if x < 0 then - (THE u. 0 < u \<and> u ^ n = - x) else 0)"
    3.87  
    3.88 -lemma real_root_pos: 
    3.89 -     "0 < x ==> root(Suc n) (x ^ (Suc n)) = x"
    3.90 +lemma real_root_zero [simp]: "root n 0 = 0"
    3.91 +unfolding root_def by simp
    3.92 +
    3.93 +lemma real_root_minus: "0 < n \<Longrightarrow> root n (- x) = - root n x"
    3.94 +unfolding root_def by simp
    3.95 +
    3.96 +lemma real_root_gt_zero: "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> 0 < root n x"
    3.97  apply (simp add: root_def)
    3.98 -apply (rule the_equality)
    3.99 -apply (frule_tac [2] n = n in zero_less_power)
   3.100 -apply (auto simp add: zero_less_mult_iff)
   3.101 -apply (rule_tac x = u and y = x in linorder_cases)
   3.102 -apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less])
   3.103 -apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less])
   3.104 -apply (auto)
   3.105 -done
   3.106 -
   3.107 -lemma real_root_pos2: "0 \<le> x ==> root(Suc n) (x ^ (Suc n)) = x"
   3.108 -by (auto dest!: real_le_imp_less_or_eq real_root_pos)
   3.109 -
   3.110 -lemma real_root_gt_zero:
   3.111 -     "0 < x ==> 0 < root (Suc n) x"
   3.112 -apply (simp add: root_def del: realpow_Suc)
   3.113 -apply (drule_tac n="Suc n" in realpow_pos_nth_unique, simp)
   3.114 +apply (drule (1) realpow_pos_nth_unique)
   3.115  apply (erule theI' [THEN conjunct1])
   3.116  done
   3.117  
   3.118 -lemma real_root_pos_pos: 
   3.119 -     "0 < x ==> 0 \<le> root(Suc n) x"
   3.120 -by (rule real_root_gt_zero [THEN order_less_imp_le])
   3.121 +lemma real_root_pow_pos: (* TODO: rename *)
   3.122 +  "\<lbrakk>0 < n; 0 < x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
   3.123 +apply (simp add: root_def)
   3.124 +apply (drule (1) realpow_pos_nth_unique)
   3.125 +apply (erule theI' [THEN conjunct2])
   3.126 +done
   3.127  
   3.128 -lemma real_root_pos_pos_le: "0 \<le> x ==> 0 \<le> root(Suc n) x"
   3.129 +lemma real_root_pow_pos2 [simp]: (* TODO: rename *)
   3.130 +  "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n x ^ n = x"
   3.131 +by (auto simp add: order_le_less real_root_pow_pos)
   3.132 +
   3.133 +lemma real_root_ge_zero: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> 0 \<le> root n x"
   3.134  by (auto simp add: order_le_less real_root_gt_zero)
   3.135  
   3.136 -lemma real_root_one [simp]: "root (Suc n) 1 = 1"
   3.137 -apply (simp add: root_def)
   3.138 -apply (rule the_equality, auto)
   3.139 -apply (rule ccontr)
   3.140 -apply (rule_tac x = u and y = 1 in linorder_cases)
   3.141 -apply (drule_tac n = n in realpow_Suc_less_one)
   3.142 -apply (drule_tac [4] n = n in power_gt1_lemma)
   3.143 -apply (auto)
   3.144 +lemma real_root_power_cancel: "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (x ^ n) = x"
   3.145 +apply (subgoal_tac "0 \<le> x ^ n")
   3.146 +apply (subgoal_tac "0 \<le> root n (x ^ n)")
   3.147 +apply (subgoal_tac "root n (x ^ n) ^ n = x ^ n")
   3.148 +apply (erule (3) power_eq_imp_eq_base)
   3.149 +apply (erule (1) real_root_pow_pos2)
   3.150 +apply (erule (1) real_root_ge_zero)
   3.151 +apply (erule zero_le_power)
   3.152  done
   3.153  
   3.154 -lemma real_root_less_mono:
   3.155 -     "[| 0 \<le> x; x < y |] ==> root(Suc n) x < root(Suc n) y"
   3.156 +lemma real_root_pos_unique:
   3.157 +  "\<lbrakk>0 < n; 0 \<le> y; y ^ n = x\<rbrakk> \<Longrightarrow> root n x = y"
   3.158 +by (erule subst, rule real_root_power_cancel)
   3.159 +
   3.160 +lemma real_root_one [simp]: "0 < n \<Longrightarrow> root n 1 = 1"
   3.161 +by (simp add: real_root_pos_unique)
   3.162 +
   3.163 +text {* Root function is strictly monotonic, hence injective *}
   3.164 +
   3.165 +lemma real_root_less_mono_lemma:
   3.166 +  "\<lbrakk>0 < n; 0 \<le> x; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   3.167  apply (subgoal_tac "0 \<le> y")
   3.168 -apply (rule_tac n="Suc n" in power_less_imp_less_base)
   3.169 -apply (simp only: real_root_pow_pos2)
   3.170 -apply (erule real_root_pos_pos_le)
   3.171 -apply (erule order_trans)
   3.172 -apply (erule order_less_imp_le)
   3.173 +apply (subgoal_tac "root n x ^ n < root n y ^ n")
   3.174 +apply (erule power_less_imp_less_base)
   3.175 +apply (erule (1) real_root_ge_zero)
   3.176 +apply simp
   3.177 +apply simp
   3.178  done
   3.179  
   3.180 -lemma real_root_le_mono:
   3.181 -     "[| 0 \<le> x; x \<le> y |] ==> root(Suc n) x \<le> root(Suc n) y"
   3.182 -apply (drule_tac y = y in order_le_imp_less_or_eq)
   3.183 -apply (auto dest: real_root_less_mono intro: order_less_imp_le)
   3.184 +lemma real_root_less_mono: "\<lbrakk>0 < n; x < y\<rbrakk> \<Longrightarrow> root n x < root n y"
   3.185 +apply (cases "0 \<le> x")
   3.186 +apply (erule (2) real_root_less_mono_lemma)
   3.187 +apply (cases "0 \<le> y")
   3.188 +apply (rule_tac y=0 in order_less_le_trans)
   3.189 +apply (subgoal_tac "0 < root n (- x)")
   3.190 +apply (simp add: real_root_minus)
   3.191 +apply (simp add: real_root_gt_zero)
   3.192 +apply (simp add: real_root_ge_zero)
   3.193 +apply (subgoal_tac "root n (- y) < root n (- x)")
   3.194 +apply (simp add: real_root_minus)
   3.195 +apply (simp add: real_root_less_mono_lemma)
   3.196  done
   3.197  
   3.198 +lemma real_root_le_mono: "\<lbrakk>0 < n; x \<le> y\<rbrakk> \<Longrightarrow> root n x \<le> root n y"
   3.199 +by (auto simp add: order_le_less real_root_less_mono)
   3.200 +
   3.201  lemma real_root_less_iff [simp]:
   3.202 -     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x < root(Suc n) y) = (x < y)"
   3.203 -apply (auto intro: real_root_less_mono)
   3.204 -apply (rule ccontr, drule linorder_not_less [THEN iffD1])
   3.205 -apply (drule_tac x = y and n = n in real_root_le_mono, auto)
   3.206 +  "0 < n \<Longrightarrow> (root n x < root n y) = (x < y)"
   3.207 +apply (cases "x < y")
   3.208 +apply (simp add: real_root_less_mono)
   3.209 +apply (simp add: linorder_not_less real_root_le_mono)
   3.210  done
   3.211  
   3.212  lemma real_root_le_iff [simp]:
   3.213 -     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x \<le> root(Suc n) y) = (x \<le> y)"
   3.214 -apply (auto intro: real_root_le_mono)
   3.215 -apply (simp (no_asm) add: linorder_not_less [symmetric])
   3.216 -apply auto
   3.217 -apply (drule_tac x = y and n = n in real_root_less_mono, auto)
   3.218 +  "0 < n \<Longrightarrow> (root n x \<le> root n y) = (x \<le> y)"
   3.219 +apply (cases "x \<le> y")
   3.220 +apply (simp add: real_root_le_mono)
   3.221 +apply (simp add: linorder_not_le real_root_less_mono)
   3.222  done
   3.223  
   3.224  lemma real_root_eq_iff [simp]:
   3.225 -     "[| 0 \<le> x; 0 \<le> y |] ==> (root(Suc n) x = root(Suc n) y) = (x = y)"
   3.226 -apply (auto intro!: order_antisym [where 'a = real])
   3.227 -apply (rule_tac n1 = n in real_root_le_iff [THEN iffD1])
   3.228 -apply (rule_tac [4] n1 = n in real_root_le_iff [THEN iffD1], auto)
   3.229 -done
   3.230 +  "0 < n \<Longrightarrow> (root n x = root n y) = (x = y)"
   3.231 +by (simp add: order_eq_iff)
   3.232 +
   3.233 +lemmas real_root_gt_0_iff [simp] = real_root_less_iff [where x=0, simplified]
   3.234 +lemmas real_root_lt_0_iff [simp] = real_root_less_iff [where y=0, simplified]
   3.235 +lemmas real_root_ge_0_iff [simp] = real_root_le_iff [where x=0, simplified]
   3.236 +lemmas real_root_le_0_iff [simp] = real_root_le_iff [where y=0, simplified]
   3.237 +lemmas real_root_eq_0_iff [simp] = real_root_eq_iff [where y=0, simplified]
   3.238  
   3.239 -lemma real_root_pos_unique:
   3.240 -     "[| 0 \<le> x; 0 \<le> y; y ^ (Suc n) = x |] ==> root (Suc n) x = y"
   3.241 -by (auto dest: real_root_pos2 simp del: realpow_Suc)
   3.242 +text {* Roots of multiplication and division *}
   3.243 +
   3.244 +lemma real_root_mult_lemma:
   3.245 +  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> root n (x * y) = root n x * root n y"
   3.246 +by (simp add: real_root_pos_unique mult_nonneg_nonneg power_mult_distrib)
   3.247 +
   3.248 +lemma real_root_inverse_lemma:
   3.249 +  "\<lbrakk>0 < n; 0 \<le> x\<rbrakk> \<Longrightarrow> root n (inverse x) = inverse (root n x)"
   3.250 +by (simp add: real_root_pos_unique power_inverse [symmetric])
   3.251  
   3.252  lemma real_root_mult:
   3.253 -     "[| 0 \<le> x; 0 \<le> y |] 
   3.254 -      ==> root(Suc n) (x * y) = root(Suc n) x * root(Suc n) y"
   3.255 -apply (rule real_root_pos_unique)
   3.256 -apply (auto intro!: real_root_pos_pos_le 
   3.257 -            simp add: power_mult_distrib zero_le_mult_iff real_root_pow_pos2 
   3.258 -            simp del: realpow_Suc)
   3.259 -done
   3.260 +  assumes n: "0 < n"
   3.261 +  shows "root n (x * y) = root n x * root n y"
   3.262 +proof (rule linorder_le_cases, rule_tac [!] linorder_le_cases)
   3.263 +  assume "0 \<le> x" and "0 \<le> y"
   3.264 +  thus ?thesis by (rule real_root_mult_lemma [OF n])
   3.265 +next
   3.266 +  assume "0 \<le> x" and "y \<le> 0"
   3.267 +  hence "0 \<le> x" and "0 \<le> - y" by simp_all
   3.268 +  hence "root n (x * - y) = root n x * root n (- y)"
   3.269 +    by (rule real_root_mult_lemma [OF n])
   3.270 +  thus ?thesis by (simp add: real_root_minus [OF n])
   3.271 +next
   3.272 +  assume "x \<le> 0" and "0 \<le> y"
   3.273 +  hence "0 \<le> - x" and "0 \<le> y" by simp_all
   3.274 +  hence "root n (- x * y) = root n (- x) * root n y"
   3.275 +    by (rule real_root_mult_lemma [OF n])
   3.276 +  thus ?thesis by (simp add: real_root_minus [OF n])
   3.277 +next
   3.278 +  assume "x \<le> 0" and "y \<le> 0"
   3.279 +  hence "0 \<le> - x" and "0 \<le> - y" by simp_all
   3.280 +  hence "root n (- x * - y) = root n (- x) * root n (- y)"
   3.281 +    by (rule real_root_mult_lemma [OF n])
   3.282 +  thus ?thesis by (simp add: real_root_minus [OF n])
   3.283 +qed
   3.284  
   3.285  lemma real_root_inverse:
   3.286 -     "0 \<le> x ==> (root(Suc n) (inverse x) = inverse(root(Suc n) x))"
   3.287 -apply (rule real_root_pos_unique)
   3.288 -apply (auto intro: real_root_pos_pos_le 
   3.289 -            simp add: power_inverse [symmetric] real_root_pow_pos2 
   3.290 -            simp del: realpow_Suc)
   3.291 -done
   3.292 +  assumes n: "0 < n"
   3.293 +  shows "root n (inverse x) = inverse (root n x)"
   3.294 +proof (rule linorder_le_cases)
   3.295 +  assume "0 \<le> x"
   3.296 +  thus ?thesis by (rule real_root_inverse_lemma [OF n])
   3.297 +next
   3.298 +  assume "x \<le> 0"
   3.299 +  hence "0 \<le> - x" by simp
   3.300 +  hence "root n (inverse (- x)) = inverse (root n (- x))"
   3.301 +    by (rule real_root_inverse_lemma [OF n])
   3.302 +  thus ?thesis by (simp add: real_root_minus [OF n])
   3.303 +qed
   3.304  
   3.305 -lemma real_root_divide: 
   3.306 -     "[| 0 \<le> x; 0 \<le> y |]  
   3.307 -      ==> (root(Suc n) (x / y) = root(Suc n) x / root(Suc n) y)"
   3.308 -apply (simp add: divide_inverse)
   3.309 -apply (auto simp add: real_root_mult real_root_inverse)
   3.310 -done
   3.311 +lemma real_root_divide:
   3.312 +  "0 < n \<Longrightarrow> root n (x / y) = root n x / root n y"
   3.313 +by (simp add: divide_inverse real_root_mult real_root_inverse)
   3.314 +
   3.315 +lemma real_root_power:
   3.316 +  "0 < n \<Longrightarrow> root n (x ^ k) = root n x ^ k"
   3.317 +by (induct k, simp_all add: real_root_mult)
   3.318  
   3.319  
   3.320 -subsection{*Square Root*}
   3.321 +subsection {* Square Root *}
   3.322  
   3.323 -text{*needed because 2 is a binary numeral!*}
   3.324 -lemma root_2_eq [simp]: "root 2 = root (Suc (Suc 0))"
   3.325 -by (simp only: numeral_2_eq_2)
   3.326 +definition
   3.327 +  sqrt :: "real \<Rightarrow> real" where
   3.328 +  "sqrt = root 2"
   3.329  
   3.330 -lemma real_sqrt_zero [simp]: "sqrt 0 = 0"
   3.331 -by (simp add: sqrt_def)
   3.332 +lemma pos2: "0 < (2::nat)" by simp
   3.333 +
   3.334 +lemma real_sqrt_unique: "\<lbrakk>y\<twosuperior> = x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt x = y"
   3.335 +unfolding sqrt_def by (rule real_root_pos_unique [OF pos2])
   3.336  
   3.337 -lemma real_sqrt_one [simp]: "sqrt 1 = 1"
   3.338 -by (simp add: sqrt_def)
   3.339 +lemma real_sqrt_abs [simp]: "sqrt (x\<twosuperior>) = \<bar>x\<bar>"
   3.340 +apply (rule real_sqrt_unique)
   3.341 +apply (rule power2_abs)
   3.342 +apply (rule abs_ge_zero)
   3.343 +done
   3.344  
   3.345 -lemma real_sqrt_pow2 [simp]: "0 \<le> x ==> (sqrt x)\<twosuperior> = x"
   3.346 -unfolding sqrt_def numeral_2_eq_2
   3.347 -by (rule real_root_pow_pos2)
   3.348 +lemma real_sqrt_pow2 [simp]: "0 \<le> x \<Longrightarrow> (sqrt x)\<twosuperior> = x"
   3.349 +unfolding sqrt_def by (rule real_root_pow_pos2 [OF pos2])
   3.350  
   3.351 -lemma real_sqrt_pow2_iff [iff]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
   3.352 +lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
   3.353  apply (rule iffI)
   3.354  apply (erule subst)
   3.355  apply (rule zero_le_power2)
   3.356  apply (erule real_sqrt_pow2)
   3.357  done
   3.358  
   3.359 -lemma sqrt_eqI: "\<lbrakk>r\<twosuperior> = a; 0 \<le> r\<rbrakk> \<Longrightarrow> sqrt a = r"
   3.360 -unfolding sqrt_def numeral_2_eq_2
   3.361 -by (erule subst, erule real_root_pos2)
   3.362 +lemma real_sqrt_zero [simp]: "sqrt 0 = 0"
   3.363 +unfolding sqrt_def by (rule real_root_zero)
   3.364 +
   3.365 +lemma real_sqrt_one [simp]: "sqrt 1 = 1"
   3.366 +unfolding sqrt_def by (rule real_root_one [OF pos2])
   3.367 +
   3.368 +lemma real_sqrt_minus: "sqrt (- x) = - sqrt x"
   3.369 +unfolding sqrt_def by (rule real_root_minus [OF pos2])
   3.370 +
   3.371 +lemma real_sqrt_mult: "sqrt (x * y) = sqrt x * sqrt y"
   3.372 +unfolding sqrt_def by (rule real_root_mult [OF pos2])
   3.373 +
   3.374 +lemma real_sqrt_inverse: "sqrt (inverse x) = inverse (sqrt x)"
   3.375 +unfolding sqrt_def by (rule real_root_inverse [OF pos2])
   3.376 +
   3.377 +lemma real_sqrt_divide: "sqrt (x / y) = sqrt x / sqrt y"
   3.378 +unfolding sqrt_def by (rule real_root_divide [OF pos2])
   3.379 +
   3.380 +lemma real_sqrt_power: "sqrt (x ^ k) = sqrt x ^ k"
   3.381 +unfolding sqrt_def by (rule real_root_power [OF pos2])
   3.382 +
   3.383 +lemma real_sqrt_gt_zero: "0 < x \<Longrightarrow> 0 < sqrt x"
   3.384 +unfolding sqrt_def by (rule real_root_gt_zero [OF pos2])
   3.385 +
   3.386 +lemma real_sqrt_ge_zero: "0 \<le> x \<Longrightarrow> 0 \<le> sqrt x"
   3.387 +unfolding sqrt_def by (rule real_root_ge_zero [OF pos2])
   3.388  
   3.389 -lemma real_sqrt_abs [simp]: "sqrt (x\<twosuperior>) = \<bar>x\<bar>"
   3.390 -apply (rule sqrt_eqI)
   3.391 -apply (rule power2_abs)
   3.392 -apply (rule abs_ge_zero)
   3.393 -done
   3.394 +lemma real_sqrt_less_mono: "x < y \<Longrightarrow> sqrt x < sqrt y"
   3.395 +unfolding sqrt_def by (rule real_root_less_mono [OF pos2])
   3.396 +
   3.397 +lemma real_sqrt_le_mono: "x \<le> y \<Longrightarrow> sqrt x \<le> sqrt y"
   3.398 +unfolding sqrt_def by (rule real_root_le_mono [OF pos2])
   3.399 +
   3.400 +lemma real_sqrt_less_iff [simp]: "(sqrt x < sqrt y) = (x < y)"
   3.401 +unfolding sqrt_def by (rule real_root_less_iff [OF pos2])
   3.402 +
   3.403 +lemma real_sqrt_le_iff [simp]: "(sqrt x \<le> sqrt y) = (x \<le> y)"
   3.404 +unfolding sqrt_def by (rule real_root_le_iff [OF pos2])
   3.405 +
   3.406 +lemma real_sqrt_eq_iff [simp]: "(sqrt x = sqrt y) = (x = y)"
   3.407 +unfolding sqrt_def by (rule real_root_eq_iff [OF pos2])
   3.408 +
   3.409 +lemmas real_sqrt_gt_0_iff [simp] = real_sqrt_less_iff [where x=0, simplified]
   3.410 +lemmas real_sqrt_lt_0_iff [simp] = real_sqrt_less_iff [where y=0, simplified]
   3.411 +lemmas real_sqrt_ge_0_iff [simp] = real_sqrt_le_iff [where x=0, simplified]
   3.412 +lemmas real_sqrt_le_0_iff [simp] = real_sqrt_le_iff [where y=0, simplified]
   3.413 +lemmas real_sqrt_eq_0_iff [simp] = real_sqrt_eq_iff [where y=0, simplified]
   3.414 +
   3.415 +lemmas real_sqrt_gt_1_iff [simp] = real_sqrt_less_iff [where x=1, simplified]
   3.416 +lemmas real_sqrt_lt_1_iff [simp] = real_sqrt_less_iff [where y=1, simplified]
   3.417 +lemmas real_sqrt_ge_1_iff [simp] = real_sqrt_le_iff [where x=1, simplified]
   3.418 +lemmas real_sqrt_le_1_iff [simp] = real_sqrt_le_iff [where y=1, simplified]
   3.419 +lemmas real_sqrt_eq_1_iff [simp] = real_sqrt_eq_iff [where y=1, simplified]
   3.420  
   3.421  lemma not_real_square_gt_zero [simp]: "(~ (0::real) < x*x) = (x = 0)"
   3.422  apply auto
   3.423 @@ -345,56 +429,25 @@
   3.424  apply (simp add: zero_less_mult_iff)
   3.425  done
   3.426  
   3.427 -lemma real_sqrt_gt_zero: "0 < x ==> 0 < sqrt(x)"
   3.428 -by (simp add: sqrt_def real_root_gt_zero)
   3.429 -
   3.430 -lemma real_sqrt_ge_zero: "0 \<le> x ==> 0 \<le> sqrt(x)"
   3.431 -by (auto intro: real_sqrt_gt_zero simp add: order_le_less)
   3.432 -
   3.433 -
   3.434 -(*we need to prove something like this:
   3.435 -lemma "[|r ^ n = a; 0<n; 0 < a \<longrightarrow> 0 < r|] ==> root n a = r"
   3.436 -apply (case_tac n, simp) 
   3.437 -apply (simp add: root_def) 
   3.438 -apply (rule someI2 [of _ r], safe)
   3.439 -apply (auto simp del: realpow_Suc dest: power_inject_base)
   3.440 -*)
   3.441 -
   3.442 -lemma real_sqrt_mult_distrib: 
   3.443 -     "[| 0 \<le> x; 0 \<le> y |] ==> sqrt(x*y) = sqrt(x) * sqrt(y)"
   3.444 -unfolding sqrt_def numeral_2_eq_2
   3.445 -by (rule real_root_mult)
   3.446 -
   3.447 -lemmas real_sqrt_mult_distrib2 = real_sqrt_mult_distrib
   3.448 -
   3.449  lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \<bar>x\<bar>"
   3.450  apply (subst power2_eq_square [symmetric])
   3.451  apply (rule real_sqrt_abs)
   3.452  done
   3.453  
   3.454  lemma real_sqrt_pow2_gt_zero: "0 < x ==> 0 < (sqrt x)\<twosuperior>"
   3.455 -by simp
   3.456 +by simp (* TODO: delete *)
   3.457  
   3.458  lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 0"
   3.459 -apply (frule real_sqrt_pow2_gt_zero)
   3.460 -apply (auto simp add: numeral_2_eq_2)
   3.461 -done
   3.462 +by simp (* TODO: delete *)
   3.463  
   3.464  lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
   3.465  by (simp add: power_inverse [symmetric])
   3.466  
   3.467  lemma real_sqrt_eq_zero_cancel: "[| 0 \<le> x; sqrt(x) = 0|] ==> x = 0"
   3.468 -apply (drule real_le_imp_less_or_eq)
   3.469 -apply (auto dest: real_sqrt_not_eq_zero)
   3.470 -done
   3.471 -
   3.472 -lemma real_sqrt_eq_zero_cancel_iff [simp]: "0 \<le> x ==> ((sqrt x = 0) = (x=0))"
   3.473 -by (auto simp add: real_sqrt_eq_zero_cancel)
   3.474 +by simp
   3.475  
   3.476  lemma real_sqrt_ge_one: "1 \<le> x ==> 1 \<le> sqrt x"
   3.477 -apply (rule power2_le_imp_le, simp)
   3.478 -apply (simp add: real_sqrt_ge_zero)
   3.479 -done
   3.480 +by simp
   3.481  
   3.482  lemma sqrt_divide_self_eq:
   3.483    assumes nneg: "0 \<le> x"
   3.484 @@ -413,25 +466,6 @@
   3.485    qed
   3.486  qed
   3.487  
   3.488 -
   3.489 -lemma real_sqrt_less_mono: "[| 0 \<le> x; x < y |] ==> sqrt(x) < sqrt(y)"
   3.490 -by (simp add: sqrt_def)
   3.491 -
   3.492 -lemma real_sqrt_le_mono: "[| 0 \<le> x; x \<le> y |] ==> sqrt(x) \<le> sqrt(y)"
   3.493 -by (simp add: sqrt_def)
   3.494 -
   3.495 -lemma real_sqrt_less_iff [simp]:
   3.496 -     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) < sqrt(y)) = (x < y)"
   3.497 -by (simp add: sqrt_def)
   3.498 -
   3.499 -lemma real_sqrt_le_iff [simp]:
   3.500 -     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) \<le> sqrt(y)) = (x \<le> y)"
   3.501 -by (simp add: sqrt_def)
   3.502 -
   3.503 -lemma real_sqrt_eq_iff [simp]:
   3.504 -     "[| 0 \<le> x; 0 \<le> y |] ==> (sqrt(x) = sqrt(y)) = (x = y)"
   3.505 -by (simp add: sqrt_def)
   3.506 -
   3.507  lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
   3.508  apply (simp add: divide_inverse)
   3.509  apply (case_tac "r=0")
   3.510 @@ -441,7 +475,7 @@
   3.511  subsection {* Square Root of Sum of Squares *}
   3.512  
   3.513  lemma "(sqrt (x\<twosuperior> + y\<twosuperior>))\<twosuperior> = x\<twosuperior> + y\<twosuperior>"
   3.514 -by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]])
   3.515 +by simp
   3.516  
   3.517  lemma real_sqrt_mult_self_sum_ge_zero [simp]: "0 \<le> sqrt(x*x + y*y)"
   3.518  by (rule real_sqrt_ge_zero [OF real_mult_self_sum_ge_zero]) 
   3.519 @@ -455,7 +489,7 @@
   3.520  
   3.521  lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
   3.522       "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
   3.523 -by (auto simp add: zero_le_mult_iff simp del: realpow_Suc)
   3.524 +by (auto simp add: zero_le_mult_iff)
   3.525  
   3.526  lemma real_sqrt_sum_squares_ge1 [simp]: "x \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
   3.527  by (rule power2_le_imp_le, simp_all)
   3.528 @@ -463,15 +497,11 @@
   3.529  lemma real_sqrt_sum_squares_ge2 [simp]: "y \<le> sqrt(x\<twosuperior> + y\<twosuperior>)"
   3.530  by (rule power2_le_imp_le, simp_all)
   3.531  
   3.532 -lemma real_sqrt_sos_less_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
   3.533 -apply (subst real_sqrt_one [symmetric])
   3.534 -apply (rule real_sqrt_less_iff, auto)
   3.535 -done
   3.536 +lemma real_sqrt_sos_less_one_iff: "(sqrt (x\<twosuperior> + y\<twosuperior>) < 1) = (x\<twosuperior> + y\<twosuperior> < 1)"
   3.537 +by (rule real_sqrt_lt_1_iff)
   3.538  
   3.539 -lemma real_sqrt_sos_eq_one_iff [simp]: "(sqrt(x\<twosuperior> + y\<twosuperior>) = 1) = (x\<twosuperior> + y\<twosuperior> = 1)"
   3.540 -apply (subst real_sqrt_one [symmetric])
   3.541 -apply (rule real_sqrt_eq_iff, auto)
   3.542 -done
   3.543 +lemma real_sqrt_sos_eq_one_iff: "(sqrt (x\<twosuperior> + y\<twosuperior>) = 1) = (x\<twosuperior> + y\<twosuperior> = 1)"
   3.544 +by (rule real_sqrt_eq_1_iff)
   3.545  
   3.546  lemma power2_sum:
   3.547    fixes x y :: "'a::{number_ring,recpower}"
   3.548 @@ -501,4 +531,24 @@
   3.549  apply (simp add: add_increasing)
   3.550  done
   3.551  
   3.552 +text "Legacy theorem names:"
   3.553 +lemmas real_root_pos2 = real_root_power_cancel
   3.554 +lemmas real_root_pos_pos = real_root_gt_zero [THEN order_less_imp_le]
   3.555 +lemmas real_root_pos_pos_le = real_root_ge_zero
   3.556 +lemmas real_sqrt_mult_distrib = real_sqrt_mult
   3.557 +lemmas real_sqrt_mult_distrib2 = real_sqrt_mult
   3.558 +lemmas real_sqrt_eq_zero_cancel_iff = real_sqrt_eq_0_iff
   3.559 +
   3.560 +(* needed for CauchysMeanTheorem.het_base from AFP *)
   3.561 +lemma real_root_pos: "0 < x \<Longrightarrow> root (Suc n) (x ^ (Suc n)) = x"
   3.562 +by (rule real_root_power_cancel [OF zero_less_Suc order_less_imp_le])
   3.563 +
   3.564 +(* FIXME: the stronger version of real_root_less_iff
   3.565 + breaks CauchysMeanTheorem.list_gmean_gt_iff from AFP. *)
   3.566 +
   3.567 +declare real_root_less_iff [simp del]
   3.568 +lemma real_root_less_iff_nonneg [simp]:
   3.569 +  "\<lbrakk>0 < n; 0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (root n x < root n y) = (x < y)"
   3.570 +by (rule real_root_less_iff)
   3.571 +
   3.572  end
     4.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Sun May 13 19:15:36 2007 +0200
     4.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Sun May 13 20:05:42 2007 +0200
     4.3 @@ -1928,7 +1928,8 @@
     4.4  
     4.5  lemma lemma_real_divide_sqrt_ge_minus_one:
     4.6       "0 < x ==> -1 \<le> x/(sqrt (x * x + y * y))" 
     4.7 -by (simp add: divide_const_simps linorder_not_le [symmetric])
     4.8 +by (simp add: divide_const_simps linorder_not_le [symmetric]
     4.9 +         del: real_sqrt_le_0_iff real_sqrt_ge_0_iff)
    4.10  
    4.11  lemma real_sqrt_sum_squares_gt_zero1: "x < 0 ==> 0 < sqrt (x * x + y * y)"
    4.12  apply (rule real_sqrt_gt_zero)
    4.13 @@ -1943,14 +1944,10 @@
    4.14  done
    4.15  
    4.16  lemma real_sqrt_sum_squares_gt_zero3: "x \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
    4.17 -apply (cut_tac x = x and y = 0 in linorder_less_linear)
    4.18 -apply (auto intro: real_sqrt_sum_squares_gt_zero2 real_sqrt_sum_squares_gt_zero1 simp add: numeral_2_eq_2)
    4.19 -done
    4.20 +by (simp add: add_pos_nonneg)
    4.21  
    4.22  lemma real_sqrt_sum_squares_gt_zero3a: "y \<noteq> 0 ==> 0 < sqrt(x\<twosuperior> + y\<twosuperior>)"
    4.23 -apply (drule_tac y = x in real_sqrt_sum_squares_gt_zero3)
    4.24 -apply (auto simp add: real_add_commute)
    4.25 -done
    4.26 +by (simp add: add_nonneg_pos)
    4.27  
    4.28  lemma real_sqrt_sum_squares_eq_cancel: "sqrt(x\<twosuperior> + y\<twosuperior>) = x ==> y = 0"
    4.29  by (drule_tac f = "%x. x\<twosuperior>" in arg_cong, auto)
    4.30 @@ -1965,7 +1962,8 @@
    4.31  
    4.32  lemma lemma_real_divide_sqrt_ge_minus_one2:
    4.33       "x < 0 ==> -1 \<le> x/(sqrt (x * x + y * y))"
    4.34 -apply (simp add: divide_const_simps) 
    4.35 +apply (simp add: divide_const_simps
    4.36 +            del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff)
    4.37  apply (insert minus_le_real_sqrt_sumsq [of x y], arith)
    4.38  done
    4.39  
    4.40 @@ -1979,10 +1977,12 @@
    4.41  by (subst add_commute, simp add: minus_sqrt_le) 
    4.42  
    4.43  lemma not_neg_sqrt_sumsq: "~ sqrt (x * x + y * y) < 0"
    4.44 -by (simp add: linorder_not_less)
    4.45 +by (simp add: linorder_not_less
    4.46 +         del: real_sqrt_lt_0_iff real_sqrt_ge_0_iff)
    4.47  
    4.48  lemma cos_x_y_ge_minus_one: "-1 \<le> x / sqrt (x * x + y * y)"
    4.49 -by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps)
    4.50 +by (simp add: minus_sqrt_le not_neg_sqrt_sumsq divide_const_simps
    4.51 +         del: real_sqrt_gt_0_iff real_sqrt_lt_0_iff)
    4.52  
    4.53  lemma cos_x_y_ge_minus_one1a [simp]: "-1 \<le> y / sqrt (x * x + y * y)"
    4.54  by (subst add_commute, simp add: cos_x_y_ge_minus_one)
    4.55 @@ -2006,11 +2006,13 @@
    4.56  
    4.57  lemma cos_abs_x_y_ge_minus_one [simp]:
    4.58       "-1 \<le> \<bar>x\<bar> / sqrt (x * x + y * y)"
    4.59 -by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric]) 
    4.60 +by (auto simp add: divide_const_simps abs_if linorder_not_le [symmetric]
    4.61 +         simp del: real_sqrt_ge_0_iff real_sqrt_le_0_iff)
    4.62  
    4.63  lemma cos_abs_x_y_le_one [simp]: "\<bar>x\<bar> / sqrt (x * x + y * y) \<le> 1"
    4.64 -apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y]) 
    4.65 -apply (auto simp add: divide_const_simps abs_if linorder_neq_iff) 
    4.66 +apply (insert minus_le_real_sqrt_sumsq [of x y] le_real_sqrt_sumsq [of x y])
    4.67 +apply (auto simp add: divide_const_simps abs_if linorder_neq_iff
    4.68 +            simp del: real_sqrt_gt_0_iff real_sqrt_eq_0_iff)
    4.69  done
    4.70  
    4.71  declare cos_arcos [OF cos_abs_x_y_ge_minus_one cos_abs_x_y_le_one, simp] 
    4.72 @@ -2165,20 +2167,15 @@
    4.73  apply (rule real_add_commute [THEN subst])
    4.74  apply (rule real_sqrt_ge_abs1)
    4.75  done
    4.76 -declare real_sqrt_ge_abs1 [simp] real_sqrt_ge_abs2 [simp]
    4.77  
    4.78  lemma real_sqrt_two_gt_zero [simp]: "0 < sqrt 2"
    4.79 -by (auto intro: real_sqrt_gt_zero)
    4.80 +by simp
    4.81  
    4.82  lemma real_sqrt_two_ge_zero [simp]: "0 \<le> sqrt 2"
    4.83 -by (auto intro: real_sqrt_ge_zero)
    4.84 +by simp
    4.85  
    4.86  lemma real_sqrt_two_gt_one [simp]: "1 < sqrt 2"
    4.87 -apply (rule order_less_le_trans [of _ "7/5"], simp) 
    4.88 -apply (rule_tac n = 1 in realpow_increasing)
    4.89 -  prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
    4.90 -apply (simp_all add: numeral_2_eq_2)
    4.91 -done
    4.92 +by simp
    4.93  
    4.94  lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
    4.95  by (simp add: divide_less_eq mult_compare_simps)