src/HOL/Real/RealPow.thy
changeset 14265 95b42e69436c
parent 12018 ec054019c910
child 14268 5cf13e80be0e
     1.1 --- a/src/HOL/Real/RealPow.thy	Thu Nov 20 10:42:00 2003 +0100
     1.2 +++ b/src/HOL/Real/RealPow.thy	Fri Nov 21 11:15:40 2003 +0100
     1.3 @@ -11,11 +11,477 @@
     1.4  (*belongs to theory RealAbs*)
     1.5  lemmas [arith_split] = abs_split
     1.6  
     1.7 -
     1.8  instance real :: power ..
     1.9  
    1.10  primrec (realpow)
    1.11       realpow_0:   "r ^ 0       = 1"
    1.12       realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    1.13  
    1.14 +
    1.15 +(*FIXME: most of the theorems for Suc (Suc 0) are redundant!
    1.16 +*)
    1.17 +
    1.18 +lemma realpow_zero: "(0::real) ^ (Suc n) = 0"
    1.19 +apply auto
    1.20 +done
    1.21 +declare realpow_zero [simp]
    1.22 +
    1.23 +lemma realpow_not_zero [rule_format (no_asm)]: "r \<noteq> (0::real) --> r ^ n \<noteq> 0"
    1.24 +apply (induct_tac "n")
    1.25 +apply auto
    1.26 +done
    1.27 +
    1.28 +lemma realpow_zero_zero: "r ^ n = (0::real) ==> r = 0"
    1.29 +apply (rule ccontr)
    1.30 +apply (auto dest: realpow_not_zero)
    1.31 +done
    1.32 +
    1.33 +lemma realpow_inverse: "inverse ((r::real) ^ n) = (inverse r) ^ n"
    1.34 +apply (induct_tac "n")
    1.35 +apply (auto simp add: real_inverse_distrib)
    1.36 +done
    1.37 +
    1.38 +lemma realpow_abs: "abs(r ^ n) = abs(r::real) ^ n"
    1.39 +apply (induct_tac "n")
    1.40 +apply (auto simp add: abs_mult)
    1.41 +done
    1.42 +
    1.43 +lemma realpow_add: "(r::real) ^ (n + m) = (r ^ n) * (r ^ m)"
    1.44 +apply (induct_tac "n")
    1.45 +apply (auto simp add: real_mult_ac)
    1.46 +done
    1.47 +
    1.48 +lemma realpow_one: "(r::real) ^ 1 = r"
    1.49 +apply (simp (no_asm))
    1.50 +done
    1.51 +declare realpow_one [simp]
    1.52 +
    1.53 +lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
    1.54 +apply (simp (no_asm))
    1.55 +done
    1.56 +
    1.57 +lemma realpow_gt_zero [rule_format (no_asm)]: "(0::real) < r --> 0 < r ^ n"
    1.58 +apply (induct_tac "n")
    1.59 +apply (auto intro: real_mult_order simp add: real_zero_less_one)
    1.60 +done
    1.61 +
    1.62 +lemma realpow_ge_zero [rule_format (no_asm)]: "(0::real) \<le> r --> 0 \<le> r ^ n"
    1.63 +apply (induct_tac "n")
    1.64 +apply (auto simp add: real_0_le_mult_iff)
    1.65 +done
    1.66 +
    1.67 +lemma realpow_le [rule_format (no_asm)]: "(0::real) \<le> x & x \<le> y --> x ^ n \<le> y ^ n"
    1.68 +apply (induct_tac "n")
    1.69 +apply (auto intro!: real_mult_le_mono)
    1.70 +apply (simp (no_asm_simp) add: realpow_ge_zero)
    1.71 +done
    1.72 +
    1.73 +lemma realpow_0_left [rule_format, simp]:
    1.74 +     "0 < n --> 0 ^ n = (0::real)"
    1.75 +apply (induct_tac "n")
    1.76 +apply (auto ); 
    1.77 +done
    1.78 +
    1.79 +lemma realpow_less' [rule_format]:
    1.80 +     "[|(0::real) \<le> x; x < y |] ==> 0 < n --> x ^ n < y ^ n"
    1.81 +apply (induct n) 
    1.82 +apply (auto simp add: real_mult_less_mono' realpow_ge_zero); 
    1.83 +done
    1.84 +
    1.85 +text{*Legacy: weaker version of the theorem above*}
    1.86 +lemma realpow_less [rule_format]:
    1.87 +     "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
    1.88 +apply (rule realpow_less') 
    1.89 +apply (auto ); 
    1.90 +done
    1.91 +
    1.92 +lemma realpow_eq_one: "1 ^ n = (1::real)"
    1.93 +apply (induct_tac "n")
    1.94 +apply auto
    1.95 +done
    1.96 +declare realpow_eq_one [simp]
    1.97 +
    1.98 +lemma abs_realpow_minus_one: "abs((-1) ^ n) = (1::real)"
    1.99 +apply (induct_tac "n")
   1.100 +apply (auto simp add: abs_mult)
   1.101 +done
   1.102 +declare abs_realpow_minus_one [simp]
   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: real_mult_ac)
   1.107 +done
   1.108 +
   1.109 +lemma realpow_two_le: "(0::real) \<le> r^ Suc (Suc 0)"
   1.110 +apply (simp (no_asm) add: real_le_square)
   1.111 +done
   1.112 +declare realpow_two_le [simp]
   1.113 +
   1.114 +lemma abs_realpow_two: "abs((x::real)^Suc (Suc 0)) = x^Suc (Suc 0)"
   1.115 +apply (simp (no_asm) add: abs_eqI1 real_le_square)
   1.116 +done
   1.117 +declare abs_realpow_two [simp]
   1.118 +
   1.119 +lemma realpow_two_abs: "abs(x::real)^Suc (Suc 0) = x^Suc (Suc 0)"
   1.120 +apply (simp (no_asm) add: realpow_abs [symmetric] abs_eqI1 del: realpow_Suc)
   1.121 +done
   1.122 +declare realpow_two_abs [simp]
   1.123 +
   1.124 +lemma realpow_two_gt_one: "(1::real) < r ==> 1 < r^ (Suc (Suc 0))"
   1.125 +apply auto
   1.126 +apply (cut_tac real_zero_less_one)
   1.127 +apply (frule_tac x = "0" in order_less_trans)
   1.128 +apply assumption
   1.129 +apply (drule_tac  z = "r" and x = "1" in real_mult_less_mono1)
   1.130 +apply (auto intro: order_less_trans)
   1.131 +done
   1.132 +
   1.133 +lemma realpow_ge_one [rule_format (no_asm)]: "(1::real) < r --> 1 \<le> r ^ n"
   1.134 +apply (induct_tac "n")
   1.135 +apply auto
   1.136 +apply (subgoal_tac "1*1 \<le> r * r^n")
   1.137 +apply (rule_tac [2] real_mult_le_mono)
   1.138 +apply auto
   1.139 +done
   1.140 +
   1.141 +lemma realpow_ge_one2: "(1::real) \<le> r ==> 1 \<le> r ^ n"
   1.142 +apply (drule order_le_imp_less_or_eq)
   1.143 +apply (auto dest: realpow_ge_one)
   1.144 +done
   1.145 +
   1.146 +lemma two_realpow_ge_one: "(1::real) \<le> 2 ^ n"
   1.147 +apply (rule_tac y = "1 ^ n" in order_trans)
   1.148 +apply (rule_tac [2] realpow_le)
   1.149 +apply (auto intro: order_less_imp_le)
   1.150 +done
   1.151 +
   1.152 +lemma two_realpow_gt: "real (n::nat) < 2 ^ n"
   1.153 +apply (induct_tac "n")
   1.154 +apply (auto simp add: real_of_nat_Suc)
   1.155 +apply (subst real_mult_2)
   1.156 +apply (rule real_add_less_le_mono)
   1.157 +apply (auto simp add: two_realpow_ge_one)
   1.158 +done
   1.159 +declare two_realpow_gt [simp] two_realpow_ge_one [simp]
   1.160 +
   1.161 +lemma realpow_minus_one: "(-1) ^ (2*n) = (1::real)"
   1.162 +apply (induct_tac "n")
   1.163 +apply auto
   1.164 +done
   1.165 +declare realpow_minus_one [simp]
   1.166 +
   1.167 +lemma realpow_minus_one_odd: "(-1) ^ Suc (2*n) = -(1::real)"
   1.168 +apply auto
   1.169 +done
   1.170 +declare realpow_minus_one_odd [simp]
   1.171 +
   1.172 +lemma realpow_minus_one_even: "(-1) ^ Suc (Suc (2*n)) = (1::real)"
   1.173 +apply auto
   1.174 +done
   1.175 +declare realpow_minus_one_even [simp]
   1.176 +
   1.177 +lemma realpow_Suc_less [rule_format (no_asm)]: "(0::real) < r & r < (1::real) --> r ^ Suc n < r ^ n"
   1.178 +apply (induct_tac "n")
   1.179 +apply auto
   1.180 +done
   1.181 +
   1.182 +lemma realpow_Suc_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
   1.183 +apply (induct_tac "n")
   1.184 +apply (auto intro: order_less_imp_le dest!: order_le_imp_less_or_eq)
   1.185 +done
   1.186 +
   1.187 +lemma realpow_zero_le: "(0::real) \<le> 0 ^ n"
   1.188 +apply (case_tac "n")
   1.189 +apply auto
   1.190 +done
   1.191 +declare realpow_zero_le [simp]
   1.192 +
   1.193 +lemma realpow_Suc_le2 [rule_format (no_asm)]: "0 < r & r < (1::real) --> r ^ Suc n \<le> r ^ n"
   1.194 +apply (blast intro!: order_less_imp_le realpow_Suc_less)
   1.195 +done
   1.196 +
   1.197 +lemma realpow_Suc_le3: "[| 0 \<le> r; r < (1::real) |] ==> r ^ Suc n \<le> r ^ n"
   1.198 +apply (erule order_le_imp_less_or_eq [THEN disjE])
   1.199 +apply (rule realpow_Suc_le2)
   1.200 +apply auto
   1.201 +done
   1.202 +
   1.203 +lemma realpow_less_le [rule_format (no_asm)]: "0 \<le> r & r < (1::real) & n < N --> r ^ N \<le> r ^ n"
   1.204 +apply (induct_tac "N")
   1.205 +apply (simp_all (no_asm_simp))
   1.206 +apply clarify
   1.207 +apply (subgoal_tac "r * r ^ na \<le> 1 * r ^ n")
   1.208 +apply simp
   1.209 +apply (rule real_mult_le_mono)
   1.210 +apply (auto simp add: realpow_ge_zero less_Suc_eq)
   1.211 +done
   1.212 +
   1.213 +lemma realpow_le_le: "[| 0 \<le> r; r < (1::real); n \<le> N |] ==> r ^ N \<le> r ^ n"
   1.214 +apply (drule_tac n = "N" in le_imp_less_or_eq)
   1.215 +apply (auto intro: realpow_less_le)
   1.216 +done
   1.217 +
   1.218 +lemma realpow_Suc_le_self: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n \<le> r"
   1.219 +apply (drule_tac n = "1" and N = "Suc n" in order_less_imp_le [THEN realpow_le_le])
   1.220 +apply auto
   1.221 +done
   1.222 +
   1.223 +lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
   1.224 +apply (blast intro: realpow_Suc_le_self order_le_less_trans)
   1.225 +done
   1.226 +
   1.227 +lemma realpow_le_Suc [rule_format (no_asm)]: "(1::real) \<le> r --> r ^ n \<le> r ^ Suc n"
   1.228 +apply (induct_tac "n")
   1.229 +apply auto
   1.230 +done
   1.231 +
   1.232 +lemma realpow_less_Suc [rule_format (no_asm)]: "(1::real) < r --> r ^ n < r ^ Suc n"
   1.233 +apply (induct_tac "n")
   1.234 +apply auto
   1.235 +done
   1.236 +
   1.237 +lemma realpow_le_Suc2 [rule_format (no_asm)]: "(1::real) < r --> r ^ n \<le> r ^ Suc n"
   1.238 +apply (blast intro!: order_less_imp_le realpow_less_Suc)
   1.239 +done
   1.240 +
   1.241 +lemma realpow_gt_ge [rule_format (no_asm)]: "(1::real) < r & n < N --> r ^ n \<le> r ^ N"
   1.242 +apply (induct_tac "N")
   1.243 +apply auto
   1.244 +apply (frule_tac [!] n = "na" in realpow_ge_one)
   1.245 +apply (drule_tac [!] real_mult_self_le)
   1.246 +apply assumption
   1.247 +prefer 2 apply (assumption)
   1.248 +apply (auto intro: order_trans simp add: less_Suc_eq)
   1.249 +done
   1.250 +
   1.251 +lemma realpow_gt_ge2 [rule_format (no_asm)]: "(1::real) \<le> r & n < N --> r ^ n \<le> r ^ N"
   1.252 +apply (induct_tac "N")
   1.253 +apply auto
   1.254 +apply (frule_tac [!] n = "na" in realpow_ge_one2)
   1.255 +apply (drule_tac [!] real_mult_self_le2)
   1.256 +apply assumption
   1.257 +prefer 2 apply (assumption)
   1.258 +apply (auto intro: order_trans simp add: less_Suc_eq)
   1.259 +done
   1.260 +
   1.261 +lemma realpow_ge_ge: "[| (1::real) < r; n \<le> N |] ==> r ^ n \<le> r ^ N"
   1.262 +apply (drule_tac n = "N" in le_imp_less_or_eq)
   1.263 +apply (auto intro: realpow_gt_ge)
   1.264 +done
   1.265 +
   1.266 +lemma realpow_ge_ge2: "[| (1::real) \<le> r; n \<le> N |] ==> r ^ n \<le> r ^ N"
   1.267 +apply (drule_tac n = "N" in le_imp_less_or_eq)
   1.268 +apply (auto intro: realpow_gt_ge2)
   1.269 +done
   1.270 +
   1.271 +lemma realpow_Suc_ge_self [rule_format (no_asm)]: "(1::real) < r ==> r \<le> r ^ Suc n"
   1.272 +apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge)
   1.273 +apply auto
   1.274 +done
   1.275 +
   1.276 +lemma realpow_Suc_ge_self2 [rule_format (no_asm)]: "(1::real) \<le> r ==> r \<le> r ^ Suc n"
   1.277 +apply (drule_tac n = "1" and N = "Suc n" in realpow_ge_ge2)
   1.278 +apply auto
   1.279 +done
   1.280 +
   1.281 +lemma realpow_ge_self: "[| (1::real) < r; 0 < n |] ==> r \<le> r ^ n"
   1.282 +apply (drule less_not_refl2 [THEN not0_implies_Suc])
   1.283 +apply (auto intro!: realpow_Suc_ge_self)
   1.284 +done
   1.285 +
   1.286 +lemma realpow_ge_self2: "[| (1::real) \<le> r; 0 < n |] ==> r \<le> r ^ n"
   1.287 +apply (drule less_not_refl2 [THEN not0_implies_Suc])
   1.288 +apply (auto intro!: realpow_Suc_ge_self2)
   1.289 +done
   1.290 +
   1.291 +lemma realpow_minus_mult [rule_format (no_asm)]: "0 < n --> (x::real) ^ (n - 1) * x = x ^ n"
   1.292 +apply (induct_tac "n")
   1.293 +apply (auto simp add: real_mult_commute)
   1.294 +done
   1.295 +declare realpow_minus_mult [simp]
   1.296 +
   1.297 +lemma realpow_two_mult_inverse: "r \<noteq> 0 ==> r * inverse r ^Suc (Suc 0) = inverse (r::real)"
   1.298 +apply (simp (no_asm_simp) add: realpow_two real_mult_assoc [symmetric])
   1.299 +done
   1.300 +declare realpow_two_mult_inverse [simp]
   1.301 +
   1.302 +(* 05/00 *)
   1.303 +lemma realpow_two_minus: "(-x)^Suc (Suc 0) = (x::real)^Suc (Suc 0)"
   1.304 +apply (simp (no_asm))
   1.305 +done
   1.306 +declare realpow_two_minus [simp]
   1.307 +
   1.308 +lemma realpow_two_diff: "(x::real)^Suc (Suc 0) - y^Suc (Suc 0) = (x - y) * (x + y)"
   1.309 +apply (unfold real_diff_def)
   1.310 +apply (simp add: real_add_mult_distrib2 real_add_mult_distrib real_mult_ac)
   1.311 +done
   1.312 +
   1.313 +lemma realpow_two_disj: "((x::real)^Suc (Suc 0) = y^Suc (Suc 0)) = (x = y | x = -y)"
   1.314 +apply (cut_tac x = "x" and y = "y" in realpow_two_diff)
   1.315 +apply (auto simp del: realpow_Suc)
   1.316 +done
   1.317 +
   1.318 +(* used in Transc *)
   1.319 +lemma realpow_diff: "[|(x::real) \<noteq> 0; m \<le> n |] ==> x ^ (n - m) = x ^ n * inverse (x ^ m)"
   1.320 +apply (auto simp add: le_eq_less_or_eq less_iff_Suc_add realpow_add realpow_not_zero real_mult_ac)
   1.321 +done
   1.322 +
   1.323 +lemma realpow_real_of_nat: "real (m::nat) ^ n = real (m ^ n)"
   1.324 +apply (induct_tac "n")
   1.325 +apply (auto simp add: real_of_nat_one real_of_nat_mult)
   1.326 +done
   1.327 +
   1.328 +lemma realpow_real_of_nat_two_pos: "0 < real (Suc (Suc 0) ^ n)"
   1.329 +apply (induct_tac "n")
   1.330 +apply (auto simp add: real_of_nat_mult real_0_less_mult_iff)
   1.331 +done
   1.332 +declare realpow_real_of_nat_two_pos [simp] 
   1.333 +
   1.334 +lemma realpow_increasing:
   1.335 +  assumes xnonneg: "(0::real) \<le> x"
   1.336 +      and ynonneg: "0 \<le> y"
   1.337 +      and le: "x ^ Suc n \<le> y ^ Suc n"
   1.338 +  shows "x \<le> y"
   1.339 + proof (rule ccontr)
   1.340 +   assume "~ x \<le> y"
   1.341 +   then have "y<x" by simp
   1.342 +   then have "y ^ Suc n < x ^ Suc n"
   1.343 +     by (simp only: prems realpow_less') 
   1.344 +   from le and this show "False"
   1.345 +     by simp
   1.346 + qed
   1.347 +  
   1.348 +lemma realpow_Suc_cancel_eq: "[| (0::real) \<le> x; 0 \<le> y; x ^ Suc n = y ^ Suc n |] ==> x = y"
   1.349 +apply (blast intro: realpow_increasing order_antisym order_eq_refl sym)
   1.350 +done
   1.351 +
   1.352 +
   1.353 +(*** Logical equivalences for inequalities ***)
   1.354 +
   1.355 +lemma realpow_eq_0_iff: "(x^n = 0) = (x = (0::real) & 0<n)"
   1.356 +apply (induct_tac "n")
   1.357 +apply auto
   1.358 +done
   1.359 +declare realpow_eq_0_iff [simp]
   1.360 +
   1.361 +lemma zero_less_realpow_abs_iff: "(0 < (abs x)^n) = (x \<noteq> (0::real) | n=0)"
   1.362 +apply (induct_tac "n")
   1.363 +apply (auto simp add: real_0_less_mult_iff)
   1.364 +done
   1.365 +declare zero_less_realpow_abs_iff [simp]
   1.366 +
   1.367 +lemma zero_le_realpow_abs: "(0::real) \<le> (abs x)^n"
   1.368 +apply (induct_tac "n")
   1.369 +apply (auto simp add: real_0_le_mult_iff)
   1.370 +done
   1.371 +declare zero_le_realpow_abs [simp]
   1.372 +
   1.373 +
   1.374 +(*** Literal arithmetic involving powers, type real ***)
   1.375 +
   1.376 +lemma real_of_int_power: "real (x::int) ^ n = real (x ^ n)"
   1.377 +apply (induct_tac "n")
   1.378 +apply (simp_all (no_asm_simp) add: nat_mult_distrib)
   1.379 +done
   1.380 +declare real_of_int_power [symmetric, simp]
   1.381 +
   1.382 +lemma power_real_number_of: "(number_of v :: real) ^ n = real ((number_of v :: int) ^ n)"
   1.383 +apply (simp only: real_number_of_def real_of_int_power)
   1.384 +done
   1.385 +
   1.386 +declare power_real_number_of [of _ "number_of w", standard, simp]
   1.387 +
   1.388 +
   1.389 +lemma real_power_two: "(r::real)\<twosuperior> = r * r"
   1.390 +  by (simp add: numeral_2_eq_2)
   1.391 +
   1.392 +lemma real_sqr_ge_zero [iff]: "0 \<le> (r::real)\<twosuperior>"
   1.393 +  by (simp add: real_power_two)
   1.394 +
   1.395 +lemma real_sqr_gt_zero: "(r::real) \<noteq> 0 ==> 0 < r\<twosuperior>"
   1.396 +proof -
   1.397 +  assume "r \<noteq> 0"
   1.398 +  hence "0 \<noteq> r\<twosuperior>" by simp
   1.399 +  also have "0 \<le> r\<twosuperior>" by (simp add: real_sqr_ge_zero)
   1.400 +  finally show ?thesis .
   1.401 +qed
   1.402 +
   1.403 +lemma real_sqr_not_zero: "r \<noteq> 0 ==> (r::real)\<twosuperior> \<noteq> 0"
   1.404 +  by simp
   1.405 +
   1.406 +
   1.407 +ML
   1.408 +{*
   1.409 +val realpow_0 = thm "realpow_0";
   1.410 +val realpow_Suc = thm "realpow_Suc";
   1.411 +
   1.412 +val realpow_zero = thm "realpow_zero";
   1.413 +val realpow_not_zero = thm "realpow_not_zero";
   1.414 +val realpow_zero_zero = thm "realpow_zero_zero";
   1.415 +val realpow_inverse = thm "realpow_inverse";
   1.416 +val realpow_abs = thm "realpow_abs";
   1.417 +val realpow_add = thm "realpow_add";
   1.418 +val realpow_one = thm "realpow_one";
   1.419 +val realpow_two = thm "realpow_two";
   1.420 +val realpow_gt_zero = thm "realpow_gt_zero";
   1.421 +val realpow_ge_zero = thm "realpow_ge_zero";
   1.422 +val realpow_le = thm "realpow_le";
   1.423 +val realpow_0_left = thm "realpow_0_left";
   1.424 +val realpow_less = thm "realpow_less";
   1.425 +val realpow_eq_one = thm "realpow_eq_one";
   1.426 +val abs_realpow_minus_one = thm "abs_realpow_minus_one";
   1.427 +val realpow_mult = thm "realpow_mult";
   1.428 +val realpow_two_le = thm "realpow_two_le";
   1.429 +val abs_realpow_two = thm "abs_realpow_two";
   1.430 +val realpow_two_abs = thm "realpow_two_abs";
   1.431 +val realpow_two_gt_one = thm "realpow_two_gt_one";
   1.432 +val realpow_ge_one = thm "realpow_ge_one";
   1.433 +val realpow_ge_one2 = thm "realpow_ge_one2";
   1.434 +val two_realpow_ge_one = thm "two_realpow_ge_one";
   1.435 +val two_realpow_gt = thm "two_realpow_gt";
   1.436 +val realpow_minus_one = thm "realpow_minus_one";
   1.437 +val realpow_minus_one_odd = thm "realpow_minus_one_odd";
   1.438 +val realpow_minus_one_even = thm "realpow_minus_one_even";
   1.439 +val realpow_Suc_less = thm "realpow_Suc_less";
   1.440 +val realpow_Suc_le = thm "realpow_Suc_le";
   1.441 +val realpow_zero_le = thm "realpow_zero_le";
   1.442 +val realpow_Suc_le2 = thm "realpow_Suc_le2";
   1.443 +val realpow_Suc_le3 = thm "realpow_Suc_le3";
   1.444 +val realpow_less_le = thm "realpow_less_le";
   1.445 +val realpow_le_le = thm "realpow_le_le";
   1.446 +val realpow_Suc_le_self = thm "realpow_Suc_le_self";
   1.447 +val realpow_Suc_less_one = thm "realpow_Suc_less_one";
   1.448 +val realpow_le_Suc = thm "realpow_le_Suc";
   1.449 +val realpow_less_Suc = thm "realpow_less_Suc";
   1.450 +val realpow_le_Suc2 = thm "realpow_le_Suc2";
   1.451 +val realpow_gt_ge = thm "realpow_gt_ge";
   1.452 +val realpow_gt_ge2 = thm "realpow_gt_ge2";
   1.453 +val realpow_ge_ge = thm "realpow_ge_ge";
   1.454 +val realpow_ge_ge2 = thm "realpow_ge_ge2";
   1.455 +val realpow_Suc_ge_self = thm "realpow_Suc_ge_self";
   1.456 +val realpow_Suc_ge_self2 = thm "realpow_Suc_ge_self2";
   1.457 +val realpow_ge_self = thm "realpow_ge_self";
   1.458 +val realpow_ge_self2 = thm "realpow_ge_self2";
   1.459 +val realpow_minus_mult = thm "realpow_minus_mult";
   1.460 +val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
   1.461 +val realpow_two_minus = thm "realpow_two_minus";
   1.462 +val realpow_two_diff = thm "realpow_two_diff";
   1.463 +val realpow_two_disj = thm "realpow_two_disj";
   1.464 +val realpow_diff = thm "realpow_diff";
   1.465 +val realpow_real_of_nat = thm "realpow_real_of_nat";
   1.466 +val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
   1.467 +val realpow_increasing = thm "realpow_increasing";
   1.468 +val realpow_Suc_cancel_eq = thm "realpow_Suc_cancel_eq";
   1.469 +val realpow_eq_0_iff = thm "realpow_eq_0_iff";
   1.470 +val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
   1.471 +val zero_le_realpow_abs = thm "zero_le_realpow_abs";
   1.472 +val real_of_int_power = thm "real_of_int_power";
   1.473 +val power_real_number_of = thm "power_real_number_of";
   1.474 +val real_power_two = thm "real_power_two";
   1.475 +val real_sqr_ge_zero = thm "real_sqr_ge_zero";
   1.476 +val real_sqr_gt_zero = thm "real_sqr_gt_zero";
   1.477 +val real_sqr_not_zero = thm "real_sqr_not_zero";
   1.478 +*}
   1.479 +
   1.480 +
   1.481  end