src/HOL/Real/RealPow.thy
changeset 14348 744c868ee0b7
parent 14334 6137d24eef79
child 14352 a8b1a44d8264
     1.1 --- a/src/HOL/Real/RealPow.thy	Fri Jan 09 01:28:24 2004 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Fri Jan 09 10:46:18 2004 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  theory RealPow = RealArith:
     1.6  
     1.7 +declare abs_mult_self [simp]
     1.8 +
     1.9  instance real :: power ..
    1.10  
    1.11  primrec (realpow)
    1.12 @@ -15,118 +17,45 @@
    1.13       realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    1.14  
    1.15  
    1.16 -lemma realpow_zero [simp]: "(0::real) ^ (Suc n) = 0"
    1.17 -by auto
    1.18 +instance real :: ringpower
    1.19 +proof
    1.20 +  fix z :: real
    1.21 +  fix n :: nat
    1.22 +  show "z^0 = 1" by simp
    1.23 +  show "z^(Suc n) = z * (z^n)" by simp
    1.24 +qed
    1.25  
    1.26 -lemma realpow_not_zero [rule_format]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
    1.27 -by (induct_tac "n", auto)
    1.28 +
    1.29 +lemma realpow_not_zero: "r \<noteq> (0::real) ==> r ^ n \<noteq> 0"
    1.30 +  by (rule field_power_not_zero)
    1.31  
    1.32  lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
    1.33 -apply (rule ccontr)
    1.34 -apply (auto dest: realpow_not_zero)
    1.35 -done
    1.36 -
    1.37 -lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
    1.38 -apply (induct_tac "n")
    1.39 -apply (auto simp add: inverse_mult_distrib)
    1.40 -done
    1.41 -
    1.42 -lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
    1.43 -apply (induct_tac "n")
    1.44 -apply (auto simp add: abs_mult)
    1.45 -done
    1.46 -
    1.47 -lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
    1.48 -apply (induct_tac "n")
    1.49 -apply (auto simp add: mult_ac)
    1.50 -done
    1.51 -
    1.52 -lemma realpow_one [simp]: "(r::real) ^ 1 = r"
    1.53  by simp
    1.54  
    1.55  lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
    1.56  by simp
    1.57  
    1.58 -lemma realpow_gt_zero [rule_format]: "(0::real) < r --> 0 < r ^ n"
    1.59 -apply (induct_tac "n")
    1.60 -apply (auto intro: real_mult_order simp add: zero_less_one)
    1.61 -done
    1.62 -
    1.63 -lemma realpow_ge_zero [rule_format]: "(0::real) \<le> r --> 0 \<le> r ^ n"
    1.64 -apply (induct_tac "n")
    1.65 -apply (auto simp add: zero_le_mult_iff)
    1.66 -done
    1.67 -
    1.68 -lemma realpow_le [rule_format]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
    1.69 -apply (induct_tac "n")
    1.70 -apply (auto intro!: mult_mono)
    1.71 -apply (simp (no_asm_simp) add: realpow_ge_zero)
    1.72 -done
    1.73 -
    1.74 -lemma realpow_0_left [rule_format, simp]:
    1.75 -     "0 < n --> 0 ^ n = (0::real)"
    1.76 -apply (induct_tac "n", auto) 
    1.77 +text{*Legacy: weaker version of the theorem @{text power_strict_mono},
    1.78 +used 6 times in NthRoot and Transcendental*}
    1.79 +lemma realpow_less:
    1.80 +     "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
    1.81 +apply (rule power_strict_mono, auto) 
    1.82  done
    1.83  
    1.84 -lemma realpow_less' [rule_format]:
    1.85 -     "[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
    1.86 -apply (induct n) 
    1.87 -apply (auto simp add: real_mult_less_mono' realpow_ge_zero) 
    1.88 -done
    1.89 -
    1.90 -text{*Legacy: weaker version of the theorem above*}
    1.91 -lemma realpow_less:
    1.92 -     "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
    1.93 -apply (rule realpow_less', auto) 
    1.94 -done
    1.95 -
    1.96 -lemma realpow_eq_one [simp]: "1 ^ n = (1::real)"
    1.97 -by (induct_tac "n", auto)
    1.98 -
    1.99  lemma abs_realpow_minus_one [simp]: "abs((-1) ^ n) = (1::real)"
   1.100 -apply (induct_tac "n")
   1.101 -apply (auto simp add: abs_mult)
   1.102 -done
   1.103 -
   1.104 -lemma realpow_mult: "((r::real) * s) ^ n = (r ^ n) * (s ^ n)"
   1.105 -apply (induct_tac "n")
   1.106 -apply (auto simp add: mult_ac)
   1.107 -done
   1.108 +by (simp add: power_abs)
   1.109  
   1.110  lemma realpow_two_le [simp]: "(0::real) \<le> r^ Suc (Suc 0)"
   1.111  by (simp add: real_le_square)
   1.112  
   1.113  lemma abs_realpow_two [simp]: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
   1.114 -by (simp add: abs_eqI1 real_le_square)
   1.115 +by (simp add: abs_mult)
   1.116  
   1.117  lemma realpow_two_abs [simp]: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
   1.118 -by (simp add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
   1.119 -
   1.120 -lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
   1.121 -apply auto
   1.122 -apply (cut_tac real_zero_less_one)
   1.123 -apply (frule_tac x = 0 in order_less_trans, assumption)
   1.124 -apply (frule_tac c = r and a = 1 in mult_strict_right_mono)
   1.125 -apply assumption; 
   1.126 -apply (simp add: ); 
   1.127 -done
   1.128 -
   1.129 -lemma realpow_ge_one [rule_format]: "(1::real) < r --> 1 \<le> r ^ n"
   1.130 -apply (induct_tac "n", auto)
   1.131 -apply (subgoal_tac "1*1 \<le> r * r^n")
   1.132 -apply (rule_tac [2] mult_mono, auto)
   1.133 -done
   1.134 -
   1.135 -lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
   1.136 -apply (drule order_le_imp_less_or_eq)
   1.137 -apply (auto dest: realpow_ge_one)
   1.138 -done
   1.139 +by (simp add: power_abs [symmetric] abs_eqI1 del: realpow_Suc)
   1.140  
   1.141  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
   1.142 -apply (rule_tac y = "1 ^ n" in order_trans)
   1.143 -apply (rule_tac [2] realpow_le)
   1.144 -apply (auto intro: order_less_imp_le)
   1.145 -done
   1.146 +by (insert power_increasing [of 0 n "2::real"], simp)
   1.147  
   1.148  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
   1.149  apply (induct_tac "n")
   1.150 @@ -145,111 +74,38 @@
   1.151  lemma realpow_minus_one_even [simp]: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
   1.152  by auto
   1.153  
   1.154 -lemma realpow_Suc_less [rule_format]:
   1.155 -     "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
   1.156 -  by (induct_tac "n", auto simp add: mult_less_cancel_left)
   1.157 -
   1.158 -lemma realpow_Suc_le [rule_format]:
   1.159 -     "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
   1.160 -apply (induct_tac "n")
   1.161 -apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
   1.162 -done
   1.163 -
   1.164 -lemma realpow_zero_le [simp]: "(0::real) \<le> 0 ^ n"
   1.165 -by (case_tac "n", auto)
   1.166 -
   1.167 -lemma realpow_Suc_le2 [rule_format]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
   1.168 -by (blast intro!: order_less_imp_le realpow_Suc_less)
   1.169 +lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
   1.170 +by (insert power_decreasing [of 1 "Suc n" r], simp)
   1.171  
   1.172 -lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
   1.173 -apply (erule order_le_imp_less_or_eq [THEN disjE])
   1.174 -apply (rule realpow_Suc_le2, auto)
   1.175 -done
   1.176 +text{*Used ONCE in Transcendental*}
   1.177 +lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
   1.178 +by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
   1.179  
   1.180 -lemma realpow_less_le [rule_format]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
   1.181 -apply (induct_tac "N")
   1.182 -apply (simp_all (no_asm_simp))
   1.183 -apply clarify
   1.184 -apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n", simp)
   1.185 -apply (rule mult_mono)
   1.186 -apply (auto simp add: realpow_ge_zero less_Suc_eq)
   1.187 -done
   1.188 -
   1.189 -lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
   1.190 -apply (drule_tac n = N in le_imp_less_or_eq)
   1.191 -apply (auto intro: realpow_less_le)
   1.192 +text{*Used ONCE in Lim.ML*}
   1.193 +lemma realpow_minus_mult [rule_format]:
   1.194 +     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
   1.195 +apply (simp split add: nat_diff_split)
   1.196  done
   1.197  
   1.198 -lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
   1.199 -by (drule_tac n = 1 and N = "Suc n" in order_less_imp_le [THEN realpow_le_le], auto)
   1.200 -
   1.201 -lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
   1.202 -by (blast intro: realpow_Suc_le_self order_le_less_trans)
   1.203 -
   1.204 -lemma realpow_le_Suc [rule_format]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
   1.205 -by (induct_tac "n", auto)
   1.206 -
   1.207 -lemma realpow_less_Suc [rule_format]: "(1::real) < r --> r ^ n < r ^ Suc n"
   1.208 -by (induct_tac "n", auto simp add: mult_less_cancel_left)
   1.209 -
   1.210 -lemma realpow_le_Suc2 [rule_format]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
   1.211 -by (blast intro!: order_less_imp_le realpow_less_Suc)
   1.212 -
   1.213 -(*One use in RealPow.thy*)
   1.214 -lemma real_mult_self_le2: "[| (1::real) \<le> r; (1::real) \<le> x |]  ==> x \<le> r * x"
   1.215 -apply (subgoal_tac "1 * x \<le> r * x", simp) 
   1.216 -apply (rule mult_right_mono, auto) 
   1.217 -done
   1.218 -
   1.219 -lemma realpow_gt_ge2 [rule_format]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
   1.220 -apply (induct_tac "N", auto)
   1.221 -apply (frule_tac [!] n = na in realpow_ge_one2)
   1.222 -apply (drule_tac [!] real_mult_self_le2, assumption)
   1.223 -prefer 2 apply assumption
   1.224 -apply (auto intro: order_trans simp add: less_Suc_eq)
   1.225 -done
   1.226 -
   1.227 -lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
   1.228 -apply (drule_tac n = N in le_imp_less_or_eq)
   1.229 -apply (auto intro: realpow_gt_ge2)
   1.230 -done
   1.231 -
   1.232 -lemma realpow_Suc_ge_self2: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
   1.233 -by (drule_tac n = 1 and N = "Suc n" in realpow_ge_ge2, auto)
   1.234 -
   1.235 -(*Used ONCE in Hyperreal/NthRoot.ML*)
   1.236 -lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
   1.237 -apply (drule less_not_refl2 [THEN not0_implies_Suc])
   1.238 -apply (auto intro!: realpow_Suc_ge_self2)
   1.239 -done
   1.240 -
   1.241 -lemma realpow_minus_mult [rule_format, simp]:
   1.242 -     "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
   1.243 -apply (induct_tac "n")
   1.244 -apply (auto simp add: real_mult_commute)
   1.245 -done
   1.246 -
   1.247 -lemma realpow_two_mult_inverse [simp]: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
   1.248 +lemma realpow_two_mult_inverse [simp]:
   1.249 +     "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
   1.250  by (simp add: realpow_two real_mult_assoc [symmetric])
   1.251  
   1.252 -(* 05/00 *)
   1.253  lemma realpow_two_minus [simp]: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
   1.254  by simp
   1.255  
   1.256 -lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
   1.257 +lemma realpow_two_diff:
   1.258 +     "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
   1.259  apply (unfold real_diff_def)
   1.260  apply (simp add: right_distrib left_distrib mult_ac)
   1.261  done
   1.262  
   1.263 -lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
   1.264 +lemma realpow_two_disj:
   1.265 +     "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
   1.266  apply (cut_tac x = x and y = y in realpow_two_diff)
   1.267  apply (auto simp del: realpow_Suc)
   1.268  done
   1.269  
   1.270 -(* used in Transc *)
   1.271 -lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
   1.272 -by (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero mult_ac)
   1.273 -
   1.274  lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
   1.275  apply (induct_tac "n")
   1.276  apply (auto simp add: real_of_nat_one real_of_nat_mult)
   1.277 @@ -261,29 +117,12 @@
   1.278  done
   1.279  
   1.280  lemma realpow_increasing:
   1.281 -  assumes xnonneg: "(0::real) \<le> x"
   1.282 -      and ynonneg: "0 \<le> y"
   1.283 -      and le: "x ^ Suc n \<le> y ^ Suc n"
   1.284 -  shows "x \<le> y"
   1.285 - proof (rule ccontr)
   1.286 -   assume "~ x \<le> y"
   1.287 -   then have "y<x" by simp
   1.288 -   then have "y ^ Suc n < x ^ Suc n"
   1.289 -     by (simp only: prems realpow_less') 
   1.290 -   from le and this show "False"
   1.291 -     by simp
   1.292 - qed
   1.293 -  
   1.294 -lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
   1.295 -by (blast intro: realpow_increasing order_antisym order_eq_refl sym)
   1.296 +     "[|(0::real) \<le> x; 0 \<le> y; x ^ Suc n \<le> y ^ Suc n|] ==> x \<le> y"
   1.297 +  by (rule power_le_imp_le_base)
   1.298  
   1.299  
   1.300 -(*** Logical equivalences for inequalities ***)
   1.301 -
   1.302 -lemma realpow_eq_0_iff [simp]: "(x^n = 0) = (x = (0::real) & 0<n)"
   1.303 -by (induct_tac "n", auto)
   1.304 -
   1.305 -lemma zero_less_realpow_abs_iff [simp]: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
   1.306 +lemma zero_less_realpow_abs_iff [simp]:
   1.307 +     "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)" 
   1.308  apply (induct_tac "n")
   1.309  apply (auto simp add: zero_less_mult_iff)
   1.310  done
   1.311 @@ -294,7 +133,7 @@
   1.312  done
   1.313  
   1.314  
   1.315 -(*** Literal arithmetic involving powers, type real ***)
   1.316 +subsection{*Literal Arithmetic Involving Powers, Type @{typ real}*}
   1.317  
   1.318  lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
   1.319  apply (induct_tac "n")
   1.320 @@ -302,7 +141,8 @@
   1.321  done
   1.322  declare real_of_int_power [symmetric, simp]
   1.323  
   1.324 -lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
   1.325 +lemma power_real_number_of:
   1.326 +     "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
   1.327  by (simp only: real_number_of_def real_of_int_power)
   1.328  
   1.329  declare power_real_number_of [of _ "number_of w", standard, simp]
   1.330 @@ -311,20 +151,6 @@
   1.331  lemma real_power_two: "(r::real)\<twosuperior> = r * r"
   1.332    by (simp add: numeral_2_eq_2)
   1.333  
   1.334 -lemma real_sqr_ge_zero [iff]: "0 \<le> (r::real)\<twosuperior>"
   1.335 -  by (simp add: real_power_two)
   1.336 -
   1.337 -lemma real_sqr_gt_zero: "(r::real) \<noteq> 0 ==> 0 < r\<twosuperior>"
   1.338 -proof -
   1.339 -  assume "r \<noteq> 0"
   1.340 -  hence "0 \<noteq> r\<twosuperior>" by simp
   1.341 -  also have "0 \<le> r\<twosuperior>" by (simp add: real_sqr_ge_zero)
   1.342 -  finally show ?thesis .
   1.343 -qed
   1.344 -
   1.345 -lemma real_sqr_not_zero: "r \<noteq> 0 ==> (r::real)\<twosuperior> \<noteq> 0"
   1.346 -  by simp
   1.347 -
   1.348  
   1.349  subsection{*Various Other Theorems*}
   1.350  
   1.351 @@ -333,25 +159,19 @@
   1.352    by (auto intro: real_sum_squares_cancel)
   1.353  
   1.354  lemma real_squared_diff_one_factored: "x*x - (1::real) = (x + 1)*(x - 1)"
   1.355 -apply (auto simp add: left_distrib right_distrib real_diff_def)
   1.356 -done
   1.357 +by (auto simp add: left_distrib right_distrib real_diff_def)
   1.358  
   1.359 -lemma real_mult_is_one: "(x*x = (1::real)) = (x = 1 | x = - 1)"
   1.360 +lemma real_mult_is_one [simp]: "(x*x = (1::real)) = (x = 1 | x = - 1)"
   1.361  apply auto
   1.362  apply (drule right_minus_eq [THEN iffD2]) 
   1.363  apply (auto simp add: real_squared_diff_one_factored)
   1.364  done
   1.365 -declare real_mult_is_one [iff]
   1.366  
   1.367  lemma real_le_add_half_cancel: "(x + y/2 \<le> (y::real)) = (x \<le> y /2)"
   1.368 -apply auto
   1.369 -done
   1.370 -declare real_le_add_half_cancel [simp]
   1.371 +by auto
   1.372  
   1.373 -lemma real_minus_half_eq: "(x::real) - x/2 = x/2"
   1.374 -apply auto
   1.375 -done
   1.376 -declare real_minus_half_eq [simp]
   1.377 +lemma real_minus_half_eq [simp]: "(x::real) - x/2 = x/2"
   1.378 +by auto
   1.379  
   1.380  lemma real_mult_inverse_cancel:
   1.381       "[|(0::real) < x; 0 < x1; x1 * y < x * u |] 
   1.382 @@ -364,34 +184,22 @@
   1.383  done
   1.384  
   1.385  text{*Used once: in Hyperreal/Transcendental.ML*}
   1.386 -lemma real_mult_inverse_cancel2: "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
   1.387 +lemma real_mult_inverse_cancel2:
   1.388 +     "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
   1.389  apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
   1.390  done
   1.391  
   1.392 -lemma inverse_real_of_nat_gt_zero: "0 < inverse (real (Suc n))"
   1.393 -apply auto
   1.394 -done
   1.395 -declare inverse_real_of_nat_gt_zero [simp]
   1.396 +lemma inverse_real_of_nat_gt_zero [simp]: "0 < inverse (real (Suc n))"
   1.397 +by auto
   1.398  
   1.399 -lemma inverse_real_of_nat_ge_zero: "0 \<le> inverse (real (Suc n))"
   1.400 -apply auto
   1.401 -done
   1.402 -declare inverse_real_of_nat_ge_zero [simp]
   1.403 +lemma inverse_real_of_nat_ge_zero [simp]: "0 \<le> inverse (real (Suc n))"
   1.404 +by auto
   1.405  
   1.406  lemma real_sum_squares_not_zero: "x ~= 0 ==> x * x + y * y ~= (0::real)"
   1.407 -apply (blast dest!: real_sum_squares_cancel) 
   1.408 -done
   1.409 +by (blast dest!: real_sum_squares_cancel)
   1.410  
   1.411  lemma real_sum_squares_not_zero2: "y ~= 0 ==> x * x + y * y ~= (0::real)"
   1.412 -apply (blast dest!: real_sum_squares_cancel2) 
   1.413 -done
   1.414 -
   1.415 -(* nice theorem *)
   1.416 -lemma abs_mult_abs: "abs x * abs x = x * (x::real)"
   1.417 -apply (insert linorder_less_linear [of x 0]) 
   1.418 -apply (auto simp add: abs_eqI2 abs_minus_eqI2)
   1.419 -done
   1.420 -declare abs_mult_abs [simp]
   1.421 +by (blast dest!: real_sum_squares_cancel2)
   1.422  
   1.423  
   1.424  subsection {*Various Other Theorems*}
   1.425 @@ -399,50 +207,29 @@
   1.426  lemma realpow_divide: 
   1.427      "(x/y) ^ n = ((x::real) ^ n/ y ^ n)"
   1.428  apply (unfold real_divide_def)
   1.429 -apply (auto simp add: realpow_mult realpow_inverse)
   1.430 -done
   1.431 -
   1.432 -lemma realpow_ge_zero2 [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
   1.433 -apply (induct_tac "n")
   1.434 -apply (auto simp add: zero_le_mult_iff)
   1.435 +apply (auto simp add: power_mult_distrib power_inverse)
   1.436  done
   1.437  
   1.438 -lemma realpow_le2 [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
   1.439 -apply (induct_tac "n")
   1.440 -apply (auto intro!: mult_mono simp add: realpow_ge_zero2)
   1.441 -done
   1.442 -
   1.443 -lemma realpow_Suc_gt_one: "(1::real) < r ==> 1 < r ^ (Suc n)"
   1.444 -apply (frule_tac n = "n" in realpow_ge_one)
   1.445 -apply (drule real_le_imp_less_or_eq, safe)
   1.446 -apply (frule zero_less_one [THEN real_less_trans])
   1.447 -apply (drule_tac y = "r ^ n" in real_mult_less_mono2)
   1.448 -apply assumption
   1.449 -apply (auto dest: real_less_trans)
   1.450 +lemma realpow_two_sum_zero_iff [simp]:
   1.451 +     "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
   1.452 +apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 
   1.453 +                   simp add: real_power_two)
   1.454  done
   1.455  
   1.456 -lemma realpow_two_sum_zero_iff: "(x ^ 2 + y ^ 2 = (0::real)) = (x = 0 & y = 0)"
   1.457 -apply (auto intro: real_sum_squares_cancel real_sum_squares_cancel2 simp add: numeral_2_eq_2)
   1.458 -done
   1.459 -declare realpow_two_sum_zero_iff [simp]
   1.460 -
   1.461 -lemma realpow_two_le_add_order: "(0::real) \<le> u ^ 2 + v ^ 2"
   1.462 +lemma realpow_two_le_add_order [simp]: "(0::real) \<le> u ^ 2 + v ^ 2"
   1.463  apply (rule real_le_add_order)
   1.464 -apply (auto simp add: numeral_2_eq_2)
   1.465 +apply (auto simp add: real_power_two)
   1.466  done
   1.467 -declare realpow_two_le_add_order [simp]
   1.468  
   1.469 -lemma realpow_two_le_add_order2: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
   1.470 +lemma realpow_two_le_add_order2 [simp]: "(0::real) \<le> u ^ 2 + v ^ 2 + w ^ 2"
   1.471  apply (rule real_le_add_order)+
   1.472 -apply (auto simp add: numeral_2_eq_2)
   1.473 +apply (auto simp add: real_power_two)
   1.474  done
   1.475 -declare realpow_two_le_add_order2 [simp]
   1.476  
   1.477  lemma real_sum_square_gt_zero: "x ~= 0 ==> (0::real) < x * x + y * y"
   1.478 -apply (cut_tac x = "x" and y = "y" in real_mult_self_sum_ge_zero)
   1.479 +apply (cut_tac x = x and y = y in real_mult_self_sum_ge_zero)
   1.480  apply (drule real_le_imp_less_or_eq)
   1.481 -apply (drule_tac y = "y" in real_sum_squares_not_zero)
   1.482 -apply auto
   1.483 +apply (drule_tac y = y in real_sum_squares_not_zero, auto)
   1.484  done
   1.485  
   1.486  lemma real_sum_square_gt_zero2: "y ~= 0 ==> (0::real) < x * x + y * y"
   1.487 @@ -450,48 +237,29 @@
   1.488  apply (erule real_sum_square_gt_zero)
   1.489  done
   1.490  
   1.491 -lemma real_minus_mult_self_le: "-(u * u) \<le> (x * (x::real))"
   1.492 -apply (rule_tac j = "0" in real_le_trans)
   1.493 -apply auto
   1.494 -done
   1.495 -declare real_minus_mult_self_le [simp]
   1.496 +lemma real_minus_mult_self_le [simp]: "-(u * u) \<le> (x * (x::real))"
   1.497 +by (rule_tac j = 0 in real_le_trans, auto)
   1.498  
   1.499 -lemma realpow_square_minus_le: "-(u ^ 2) \<le> (x::real) ^ 2"
   1.500 -apply (auto simp add: numeral_2_eq_2)
   1.501 -done
   1.502 -declare realpow_square_minus_le [simp]
   1.503 +lemma realpow_square_minus_le [simp]: "-(u ^ 2) \<le> (x::real) ^ 2"
   1.504 +by (auto simp add: real_power_two)
   1.505  
   1.506  lemma realpow_num_eq_if: "(m::real) ^ n = (if n=0 then 1 else m * m ^ (n - 1))"
   1.507 -apply (case_tac "n")
   1.508 -apply auto
   1.509 -done
   1.510 +by (case_tac "n", auto)
   1.511  
   1.512 -lemma real_num_zero_less_two_pow: "0 < (2::real) ^ (4*d)"
   1.513 +lemma real_num_zero_less_two_pow [simp]: "0 < (2::real) ^ (4*d)"
   1.514  apply (induct_tac "d")
   1.515  apply (auto simp add: realpow_num_eq_if)
   1.516  done
   1.517 -declare real_num_zero_less_two_pow [simp]
   1.518  
   1.519 -lemma lemma_realpow_num_two_mono: "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
   1.520 +lemma lemma_realpow_num_two_mono:
   1.521 +     "x * (4::real)   < y ==> x * (2 ^ 8) < y * (2 ^ 6)"
   1.522  apply (subgoal_tac " (2::real) ^ 8 = 4 * (2 ^ 6) ")
   1.523  apply (simp (no_asm_simp) add: real_mult_assoc [symmetric])
   1.524  apply (auto simp add: realpow_num_eq_if)
   1.525  done
   1.526  
   1.527 -lemma lemma_realpow_4: "2 ^ 2 = (4::real)"
   1.528 -apply (simp (no_asm) add: realpow_num_eq_if)
   1.529 -done
   1.530 -declare lemma_realpow_4 [simp]
   1.531 -
   1.532 -lemma lemma_realpow_16: "2 ^ 4 = (16::real)"
   1.533 -apply (simp (no_asm) add: realpow_num_eq_if)
   1.534 -done
   1.535 -declare lemma_realpow_16 [simp]
   1.536 -
   1.537 -lemma zero_le_x_squared: "(0::real) \<le> x^2"
   1.538 -apply (simp add: numeral_2_eq_2)
   1.539 -done
   1.540 -declare zero_le_x_squared [simp]
   1.541 +lemma zero_le_x_squared [simp]: "(0::real) \<le> x^2"
   1.542 +by (simp add: real_power_two)
   1.543  
   1.544  
   1.545  
   1.546 @@ -500,67 +268,33 @@
   1.547  val realpow_0 = thm "realpow_0";
   1.548  val realpow_Suc = thm "realpow_Suc";
   1.549  
   1.550 -val realpow_zero = thm "realpow_zero";
   1.551  val realpow_not_zero = thm "realpow_not_zero";
   1.552  val realpow_zero_zero = thm "realpow_zero_zero";
   1.553 -val realpow_inverse = thm "realpow_inverse";
   1.554 -val realpow_abs = thm "realpow_abs";
   1.555 -val realpow_add = thm "realpow_add";
   1.556 -val realpow_one = thm "realpow_one";
   1.557  val realpow_two = thm "realpow_two";
   1.558 -val realpow_gt_zero = thm "realpow_gt_zero";
   1.559 -val realpow_ge_zero = thm "realpow_ge_zero";
   1.560 -val realpow_le = thm "realpow_le";
   1.561 -val realpow_0_left = thm "realpow_0_left";
   1.562  val realpow_less = thm "realpow_less";
   1.563 -val realpow_eq_one = thm "realpow_eq_one";
   1.564  val abs_realpow_minus_one = thm "abs_realpow_minus_one";
   1.565 -val realpow_mult = thm "realpow_mult";
   1.566  val realpow_two_le = thm "realpow_two_le";
   1.567  val abs_realpow_two = thm "abs_realpow_two";
   1.568  val realpow_two_abs = thm "realpow_two_abs";
   1.569 -val realpow_two_gt_one = thm "realpow_two_gt_one";
   1.570 -val realpow_ge_one = thm "realpow_ge_one";
   1.571 -val realpow_ge_one2 = thm "realpow_ge_one2";
   1.572  val two_realpow_ge_one = thm "two_realpow_ge_one";
   1.573  val two_realpow_gt = thm "two_realpow_gt";
   1.574  val realpow_minus_one = thm "realpow_minus_one";
   1.575  val realpow_minus_one_odd = thm "realpow_minus_one_odd";
   1.576  val realpow_minus_one_even = thm "realpow_minus_one_even";
   1.577 -val realpow_Suc_less = thm "realpow_Suc_less";
   1.578 -val realpow_Suc_le = thm "realpow_Suc_le";
   1.579 -val realpow_zero_le = thm "realpow_zero_le";
   1.580 -val realpow_Suc_le2 = thm "realpow_Suc_le2";
   1.581 -val realpow_Suc_le3 = thm "realpow_Suc_le3";
   1.582 -val realpow_less_le = thm "realpow_less_le";
   1.583 -val realpow_le_le = thm "realpow_le_le";
   1.584  val realpow_Suc_le_self = thm "realpow_Suc_le_self";
   1.585  val realpow_Suc_less_one = thm "realpow_Suc_less_one";
   1.586 -val realpow_le_Suc = thm "realpow_le_Suc";
   1.587 -val realpow_less_Suc = thm "realpow_less_Suc";
   1.588 -val realpow_le_Suc2 = thm "realpow_le_Suc2";
   1.589 -val realpow_gt_ge2 = thm "realpow_gt_ge2";
   1.590 -val realpow_ge_ge2 = thm "realpow_ge_ge2";
   1.591 -val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
   1.592 -val realpow_ge_self2 = thm "realpow_ge_self2";
   1.593  val realpow_minus_mult = thm "realpow_minus_mult";
   1.594  val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
   1.595  val realpow_two_minus = thm "realpow_two_minus";
   1.596  val realpow_two_disj = thm "realpow_two_disj";
   1.597 -val realpow_diff = thm "realpow_diff";
   1.598  val realpow_real_of_nat = thm "realpow_real_of_nat";
   1.599  val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
   1.600  val realpow_increasing = thm "realpow_increasing";
   1.601 -val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq";
   1.602 -val realpow_eq_0_iff = thm "realpow_eq_0_iff";
   1.603  val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
   1.604  val zero_le_realpow_abs = thm "zero_le_realpow_abs";
   1.605  val real_of_int_power = thm "real_of_int_power";
   1.606  val power_real_number_of = thm "power_real_number_of";
   1.607  val real_power_two = thm "real_power_two";
   1.608 -val real_sqr_ge_zero = thm "real_sqr_ge_zero";
   1.609 -val real_sqr_gt_zero = thm "real_sqr_gt_zero";
   1.610 -val real_sqr_not_zero = thm "real_sqr_not_zero";
   1.611  val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
   1.612  val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
   1.613  val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
   1.614 @@ -573,12 +307,8 @@
   1.615  val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
   1.616  val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
   1.617  val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
   1.618 -val abs_mult_abs = thm "abs_mult_abs";
   1.619  
   1.620  val realpow_divide = thm "realpow_divide";
   1.621 -val realpow_ge_zero2 = thm "realpow_ge_zero2";
   1.622 -val realpow_le2 = thm "realpow_le2";
   1.623 -val realpow_Suc_gt_one = thm "realpow_Suc_gt_one";
   1.624  val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
   1.625  val realpow_two_le_add_order = thm "realpow_two_le_add_order";
   1.626  val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
   1.627 @@ -589,8 +319,6 @@
   1.628  val realpow_num_eq_if = thm "realpow_num_eq_if";
   1.629  val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
   1.630  val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
   1.631 -val lemma_realpow_4 = thm "lemma_realpow_4";
   1.632 -val lemma_realpow_16 = thm "lemma_realpow_16";
   1.633  val zero_le_x_squared = thm "zero_le_x_squared";
   1.634  *}
   1.635