src/HOL/Power.thy
 changeset 30996 648d02b124d8 parent 30960 fec1a04b7220 child 30997 081e825c2218
```     1.1 --- a/src/HOL/Power.thy	Sun Apr 26 00:42:59 2009 +0200
1.2 +++ b/src/HOL/Power.thy	Sun Apr 26 08:45:37 2009 +0200
1.3 @@ -11,85 +11,169 @@
1.4
1.5  subsection {* Powers for Arbitrary Monoids *}
1.6
1.7 -class recpower = monoid_mult
1.8 +class power = one + times
1.9  begin
1.10
1.11  primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
1.12      power_0: "a ^ 0 = 1"
1.13    | power_Suc: "a ^ Suc n = a * a ^ n"
1.14
1.15 +notation (latex output)
1.16 +  power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
1.17 +
1.18 +notation (HTML output)
1.19 +  power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
1.20 +
1.21  end
1.22
1.23 -lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0"
1.24 -  by simp
1.25 +context monoid_mult
1.26 +begin
1.27
1.28 -text{*It looks plausible as a simprule, but its effect can be strange.*}
1.29 -lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))"
1.30 -  by (induct n) simp_all
1.31 +subclass power ..
1.32
1.33 -lemma power_one [simp]: "1^n = (1::'a::recpower)"
1.34 +lemma power_one [simp]:
1.35 +  "1 ^ n = 1"
1.36    by (induct n) simp_all
1.37
1.38 -lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
1.39 -  unfolding One_nat_def by simp
1.40 +lemma power_one_right [simp]:
1.41 +  "a ^ 1 = a * 1"
1.42 +  by simp
1.43
1.44 -lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
1.45 +lemma power_commutes:
1.46 +  "a ^ n * a = a * a ^ n"
1.47    by (induct n) (simp_all add: mult_assoc)
1.48
1.49 -lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a"
1.50 +lemma power_Suc2:
1.51 +  "a ^ Suc n = a ^ n * a"
1.53
1.54 -lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)"
1.55 -  by (induct m) (simp_all add: mult_ac)
1.57 +  "a ^ (m + n) = a ^ m * a ^ n"
1.58 +  by (induct m) (simp_all add: algebra_simps)
1.59
1.60 -lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n"
1.61 +lemma power_mult:
1.62 +  "a ^ (m * n) = (a ^ m) ^ n"
1.64
1.65 -lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)"
1.66 +end
1.67 +
1.68 +context comm_monoid_mult
1.69 +begin
1.70 +
1.71 +lemma power_mult_distrib:
1.72 +  "(a * b) ^ n = (a ^ n) * (b ^ n)"
1.73    by (induct n) (simp_all add: mult_ac)
1.74
1.75 -lemma zero_less_power[simp]:
1.76 -     "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n"
1.77 -by (induct n) (simp_all add: mult_pos_pos)
1.78 +end
1.79 +
1.80 +context semiring_1
1.81 +begin
1.82 +
1.83 +lemma of_nat_power:
1.84 +  "of_nat (m ^ n) = of_nat m ^ n"
1.85 +  by (induct n) (simp_all add: of_nat_mult)
1.86 +
1.87 +end
1.88 +
1.89 +context comm_semiring_1
1.90 +begin
1.91 +
1.92 +text {* The divides relation *}
1.93 +
1.94 +lemma le_imp_power_dvd:
1.95 +  assumes "m \<le> n" shows "a ^ m dvd a ^ n"
1.96 +proof
1.97 +  have "a ^ n = a ^ (m + (n - m))"
1.98 +    using `m \<le> n` by simp
1.99 +  also have "\<dots> = a ^ m * a ^ (n - m)"
1.101 +  finally show "a ^ n = a ^ m * a ^ (n - m)" .
1.102 +qed
1.103 +
1.104 +lemma power_le_dvd:
1.105 +  "a ^ n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a ^ m dvd b"
1.106 +  by (rule dvd_trans [OF le_imp_power_dvd])
1.107 +
1.108 +lemma dvd_power_same:
1.109 +  "x dvd y \<Longrightarrow> x ^ n dvd y ^ n"
1.110 +  by (induct n) (auto simp add: mult_dvd_mono)
1.111 +
1.112 +lemma dvd_power_le:
1.113 +  "x dvd y \<Longrightarrow> m \<ge> n \<Longrightarrow> x ^ n dvd y ^ m"
1.114 +  by (rule power_le_dvd [OF dvd_power_same])
1.115
1.116 -lemma zero_le_power[simp]:
1.117 -     "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n"
1.118 -by (induct n) (simp_all add: mult_nonneg_nonneg)
1.119 +lemma dvd_power [simp]:
1.120 +  assumes "n > (0::nat) \<or> x = 1"
1.121 +  shows "x dvd (x ^ n)"
1.122 +using assms proof
1.123 +  assume "0 < n"
1.124 +  then have "x ^ n = x ^ Suc (n - 1)" by simp
1.125 +  then show "x dvd (x ^ n)" by simp
1.126 +next
1.127 +  assume "x = 1"
1.128 +  then show "x dvd (x ^ n)" by simp
1.129 +qed
1.130 +
1.131 +end
1.132 +
1.133 +context ring_1
1.134 +begin
1.135 +
1.136 +lemma power_minus:
1.137 +  "(- a) ^ n = (- 1) ^ n * a ^ n"
1.138 +proof (induct n)
1.139 +  case 0 show ?case by simp
1.140 +next
1.141 +  case (Suc n) then show ?case
1.142 +    by (simp del: power_Suc add: power_Suc2 mult_assoc)
1.143 +qed
1.144 +
1.145 +end
1.146 +
1.147 +context ordered_semidom
1.148 +begin
1.149 +
1.150 +lemma zero_less_power [simp]:
1.151 +  "0 < a \<Longrightarrow> 0 < a ^ n"
1.152 +  by (induct n) (simp_all add: mult_pos_pos)
1.153 +
1.154 +lemma zero_le_power [simp]:
1.155 +  "0 \<le> a \<Longrightarrow> 0 \<le> a ^ n"
1.156 +  by (induct n) (simp_all add: mult_nonneg_nonneg)
1.157
1.158  lemma one_le_power[simp]:
1.159 -     "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n"
1.160 -apply (induct "n")
1.161 -apply simp_all
1.162 -apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
1.163 -apply (simp_all add: order_trans [OF zero_le_one])
1.164 -done
1.165 -
1.166 -lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semidom)"
1.167 -  by (simp add: order_trans [OF zero_le_one order_less_imp_le])
1.168 +  "1 \<le> a \<Longrightarrow> 1 \<le> a ^ n"
1.169 +  apply (induct n)
1.170 +  apply simp_all
1.171 +  apply (rule order_trans [OF _ mult_mono [of 1 _ 1]])
1.172 +  apply (simp_all add: order_trans [OF zero_le_one])
1.173 +  done
1.174
1.175  lemma power_gt1_lemma:
1.176 -  assumes gt1: "1 < (a::'a::{ordered_semidom,recpower})"
1.177 -  shows "1 < a * a^n"
1.178 +  assumes gt1: "1 < a"
1.179 +  shows "1 < a * a ^ n"
1.180  proof -
1.181 -  have "1*1 < a*1" using gt1 by simp
1.182 -  also have "\<dots> \<le> a * a^n" using gt1
1.183 -    by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le
1.184 +  from gt1 have "0 \<le> a"
1.185 +    by (fact order_trans [OF zero_le_one less_imp_le])
1.186 +  have "1 * 1 < a * 1" using gt1 by simp
1.187 +  also have "\<dots> \<le> a * a ^ n" using gt1
1.188 +    by (simp only: mult_mono `0 \<le> a` one_le_power order_less_imp_le
1.189          zero_le_one order_refl)
1.190    finally show ?thesis by simp
1.191  qed
1.192
1.193 -lemma one_less_power[simp]:
1.194 -  "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n"
1.195 -by (cases n, simp_all add: power_gt1_lemma)
1.196 +lemma power_gt1:
1.197 +  "1 < a \<Longrightarrow> 1 < a ^ Suc n"
1.198 +  by (simp add: power_gt1_lemma)
1.199
1.200 -lemma power_gt1:
1.201 -     "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)"
1.203 +lemma one_less_power [simp]:
1.204 +  "1 < a \<Longrightarrow> 0 < n \<Longrightarrow> 1 < a ^ n"
1.205 +  by (cases n) (simp_all add: power_gt1_lemma)
1.206
1.207  lemma power_le_imp_le_exp:
1.208 -  assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a"
1.209 -  shows "!!n. a^m \<le> a^n ==> m \<le> n"
1.210 -proof (induct m)
1.211 +  assumes gt1: "1 < a"
1.212 +  shows "a ^ m \<le> a ^ n \<Longrightarrow> m \<le> n"
1.213 +proof (induct m arbitrary: n)
1.214    case 0
1.215    show ?case by simp
1.216  next
1.217 @@ -97,212 +181,128 @@
1.218    show ?case
1.219    proof (cases n)
1.220      case 0
1.221 -    from prems have "a * a^m \<le> 1" by simp
1.222 +    with Suc.prems Suc.hyps have "a * a ^ m \<le> 1" by simp
1.223      with gt1 show ?thesis
1.224        by (force simp only: power_gt1_lemma
1.225 -          linorder_not_less [symmetric])
1.226 +          not_less [symmetric])
1.227    next
1.228      case (Suc n)
1.229 -    from prems show ?thesis
1.230 +    with Suc.prems Suc.hyps show ?thesis
1.231        by (force dest: mult_left_le_imp_le
1.232 -          simp add: order_less_trans [OF zero_less_one gt1])
1.233 +          simp add: less_trans [OF zero_less_one gt1])
1.234    qed
1.235  qed
1.236
1.237  text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*}
1.238  lemma power_inject_exp [simp]:
1.239 -     "1 < (a::'a::{ordered_semidom,recpower}) ==> (a^m = a^n) = (m=n)"
1.240 +  "1 < a \<Longrightarrow> a ^ m = a ^ n \<longleftrightarrow> m = n"
1.241    by (force simp add: order_antisym power_le_imp_le_exp)
1.242
1.243  text{*Can relax the first premise to @{term "0<a"} in the case of the
1.244  natural numbers.*}
1.245  lemma power_less_imp_less_exp:
1.246 -     "[| (1::'a::{recpower,ordered_semidom}) < a; a^m < a^n |] ==> m < n"
1.247 -by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"]
1.248 -              power_le_imp_le_exp)
1.249 -
1.250 +  "1 < a \<Longrightarrow> a ^ m < a ^ n \<Longrightarrow> m < n"
1.251 +  by (simp add: order_less_le [of m n] less_le [of "a^m" "a^n"]
1.252 +    power_le_imp_le_exp)
1.253
1.254  lemma power_mono:
1.255 -     "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n"
1.256 -apply (induct "n")
1.257 -apply simp_all
1.258 -apply (auto intro: mult_mono order_trans [of 0 a b])
1.259 -done
1.260 +  "a \<le> b \<Longrightarrow> 0 \<le> a \<Longrightarrow> a ^ n \<le> b ^ n"
1.261 +  by (induct n)
1.262 +    (auto intro: mult_mono order_trans [of 0 a b])
1.263
1.264  lemma power_strict_mono [rule_format]:
1.265 -     "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|]
1.266 -      ==> 0 < n --> a^n < b^n"
1.267 -apply (induct "n")
1.268 -apply (auto simp add: mult_strict_mono order_le_less_trans [of 0 a b])
1.269 -done
1.270 -
1.271 -lemma power_eq_0_iff [simp]:
1.272 -  "(a^n = 0) \<longleftrightarrow>
1.273 -   (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
1.274 -apply (induct "n")
1.275 -apply (auto simp add: no_zero_divisors)
1.276 -done
1.277 -
1.278 -
1.279 -lemma field_power_not_zero:
1.280 -  "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
1.281 -by force
1.282 -
1.283 -lemma nonzero_power_inverse:
1.284 -  fixes a :: "'a::{division_ring,recpower}"
1.285 -  shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n"
1.286 -apply (induct "n")
1.287 -apply (auto simp add: nonzero_inverse_mult_distrib power_commutes)
1.288 -done (* TODO: reorient or rename to nonzero_inverse_power *)
1.289 -
1.290 -text{*Perhaps these should be simprules.*}
1.291 -lemma power_inverse:
1.292 -  fixes a :: "'a::{division_ring,division_by_zero,recpower}"
1.293 -  shows "inverse (a ^ n) = (inverse a) ^ n"
1.294 -apply (cases "a = 0")
1.297 -done (* TODO: reorient or rename to inverse_power *)
1.298 -
1.299 -lemma power_one_over: "1 / (a::'a::{field,division_by_zero,recpower})^n =
1.300 -    (1 / a)^n"
1.302 -apply (rule power_inverse)
1.303 -done
1.304 -
1.305 -lemma nonzero_power_divide:
1.306 -    "b \<noteq> 0 ==> (a/b) ^ n = ((a::'a::{field,recpower}) ^ n) / (b ^ n)"
1.307 -by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
1.308 -
1.309 -lemma power_divide:
1.310 -    "(a/b) ^ n = ((a::'a::{field,division_by_zero,recpower}) ^ n / b ^ n)"
1.311 -apply (case_tac "b=0", simp add: power_0_left)
1.312 -apply (rule nonzero_power_divide)
1.313 -apply assumption
1.314 -done
1.315 -
1.316 -lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n"
1.317 -apply (induct "n")
1.318 -apply (auto simp add: abs_mult)
1.319 -done
1.320 -
1.321 -lemma abs_power_minus [simp]:
1.322 -  fixes a:: "'a::{ordered_idom,recpower}" shows "abs((-a) ^ n) = abs(a ^ n)"
1.323 -  by (simp add: abs_minus_cancel power_abs)
1.324 -
1.325 -lemma zero_less_power_abs_iff [simp,noatp]:
1.326 -     "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)"
1.327 -proof (induct "n")
1.328 -  case 0
1.329 -    show ?case by simp
1.330 -next
1.331 -  case (Suc n)
1.332 -    show ?case by (auto simp add: prems zero_less_mult_iff)
1.333 -qed
1.334 -
1.335 -lemma zero_le_power_abs [simp]:
1.336 -     "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n"
1.337 -by (rule zero_le_power [OF abs_ge_zero])
1.338 -
1.339 -lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring_1,recpower}) ^ n"
1.340 -proof (induct n)
1.341 -  case 0 show ?case by simp
1.342 -next
1.343 -  case (Suc n) then show ?case
1.344 -    by (simp del: power_Suc add: power_Suc2 mult_assoc)
1.345 -qed
1.346 +  "a < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<longrightarrow> a ^ n < b ^ n"
1.347 +  by (induct n)
1.348 +   (auto simp add: mult_strict_mono le_less_trans [of 0 a b])
1.349
1.350  text{*Lemma for @{text power_strict_decreasing}*}
1.351  lemma power_Suc_less:
1.352 -     "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|]
1.353 -      ==> a * a^n < a^n"
1.354 -apply (induct n)
1.355 -apply (auto simp add: mult_strict_left_mono)
1.356 -done
1.357 +  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a * a ^ n < a ^ n"
1.358 +  by (induct n)
1.359 +    (auto simp add: mult_strict_left_mono)
1.360
1.361 -lemma power_strict_decreasing:
1.362 -     "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|]
1.363 -      ==> a^N < a^n"
1.364 -apply (erule rev_mp)
1.365 -apply (induct "N")
1.366 -apply (auto simp add: power_Suc_less less_Suc_eq)
1.367 -apply (rename_tac m)
1.368 -apply (subgoal_tac "a * a^m < 1 * a^n", simp)
1.369 -apply (rule mult_strict_mono)
1.370 -apply (auto simp add: order_less_imp_le)
1.371 -done
1.372 +lemma power_strict_decreasing [rule_format]:
1.373 +  "n < N \<Longrightarrow> 0 < a \<Longrightarrow> a < 1 \<longrightarrow> a ^ N < a ^ n"
1.374 +proof (induct N)
1.375 +  case 0 then show ?case by simp
1.376 +next
1.377 +  case (Suc N) then show ?case
1.378 +  apply (auto simp add: power_Suc_less less_Suc_eq)
1.379 +  apply (subgoal_tac "a * a^N < 1 * a^n")
1.380 +  apply simp
1.381 +  apply (rule mult_strict_mono) apply auto
1.382 +  done
1.383 +qed
1.384
1.385  text{*Proof resembles that of @{text power_strict_decreasing}*}
1.386 -lemma power_decreasing:
1.387 -     "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|]
1.388 -      ==> a^N \<le> a^n"
1.389 -apply (erule rev_mp)
1.390 -apply (induct "N")
1.391 -apply (auto simp add: le_Suc_eq)
1.392 -apply (rename_tac m)
1.393 -apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp)
1.394 -apply (rule mult_mono)
1.395 -apply auto
1.396 -done
1.397 +lemma power_decreasing [rule_format]:
1.398 +  "n \<le> N \<Longrightarrow> 0 \<le> a \<Longrightarrow> a \<le> 1 \<longrightarrow> a ^ N \<le> a ^ n"
1.399 +proof (induct N)
1.400 +  case 0 then show ?case by simp
1.401 +next
1.402 +  case (Suc N) then show ?case
1.403 +  apply (auto simp add: le_Suc_eq)
1.404 +  apply (subgoal_tac "a * a^N \<le> 1 * a^n", simp)
1.405 +  apply (rule mult_mono) apply auto
1.406 +  done
1.407 +qed
1.408
1.409  lemma power_Suc_less_one:
1.410 -     "[| 0 < a; a < (1::'a::{ordered_semidom,recpower}) |] ==> a ^ Suc n < 1"
1.411 -apply (insert power_strict_decreasing [of 0 "Suc n" a], simp)
1.412 -done
1.413 +  "0 < a \<Longrightarrow> a < 1 \<Longrightarrow> a ^ Suc n < 1"
1.414 +  using power_strict_decreasing [of 0 "Suc n" a] by simp
1.415
1.416  text{*Proof again resembles that of @{text power_strict_decreasing}*}
1.417 -lemma power_increasing:
1.418 -     "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N"
1.419 -apply (erule rev_mp)
1.420 -apply (induct "N")
1.421 -apply (auto simp add: le_Suc_eq)
1.422 -apply (rename_tac m)
1.423 -apply (subgoal_tac "1 * a^n \<le> a * a^m", simp)
1.424 -apply (rule mult_mono)
1.425 -apply (auto simp add: order_trans [OF zero_le_one])
1.426 -done
1.427 +lemma power_increasing [rule_format]:
1.428 +  "n \<le> N \<Longrightarrow> 1 \<le> a \<Longrightarrow> a ^ n \<le> a ^ N"
1.429 +proof (induct N)
1.430 +  case 0 then show ?case by simp
1.431 +next
1.432 +  case (Suc N) then show ?case
1.433 +  apply (auto simp add: le_Suc_eq)
1.434 +  apply (subgoal_tac "1 * a^n \<le> a * a^N", simp)
1.435 +  apply (rule mult_mono) apply (auto simp add: order_trans [OF zero_le_one])
1.436 +  done
1.437 +qed
1.438
1.439  text{*Lemma for @{text power_strict_increasing}*}
1.440  lemma power_less_power_Suc:
1.441 -     "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n"
1.442 -apply (induct n)
1.443 -apply (auto simp add: mult_strict_left_mono order_less_trans [OF zero_less_one])
1.444 -done
1.445 +  "1 < a \<Longrightarrow> a ^ n < a * a ^ n"
1.446 +  by (induct n) (auto simp add: mult_strict_left_mono less_trans [OF zero_less_one])
1.447
1.448 -lemma power_strict_increasing:
1.449 -     "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N"
1.450 -apply (erule rev_mp)
1.451 -apply (induct "N")
1.452 -apply (auto simp add: power_less_power_Suc less_Suc_eq)
1.453 -apply (rename_tac m)
1.454 -apply (subgoal_tac "1 * a^n < a * a^m", simp)
1.455 -apply (rule mult_strict_mono)
1.456 -apply (auto simp add: order_less_trans [OF zero_less_one] order_less_imp_le)
1.457 -done
1.458 +lemma power_strict_increasing [rule_format]:
1.459 +  "n < N \<Longrightarrow> 1 < a \<longrightarrow> a ^ n < a ^ N"
1.460 +proof (induct N)
1.461 +  case 0 then show ?case by simp
1.462 +next
1.463 +  case (Suc N) then show ?case
1.464 +  apply (auto simp add: power_less_power_Suc less_Suc_eq)
1.465 +  apply (subgoal_tac "1 * a^n < a * a^N", simp)
1.466 +  apply (rule mult_strict_mono) apply (auto simp add: less_trans [OF zero_less_one] less_imp_le)
1.467 +  done
1.468 +qed
1.469
1.470  lemma power_increasing_iff [simp]:
1.471 -  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x \<le> b ^ y) = (x \<le> y)"
1.472 -by (blast intro: power_le_imp_le_exp power_increasing order_less_imp_le)
1.473 +  "1 < b \<Longrightarrow> b ^ x \<le> b ^ y \<longleftrightarrow> x \<le> y"
1.474 +  by (blast intro: power_le_imp_le_exp power_increasing less_imp_le)
1.475
1.476  lemma power_strict_increasing_iff [simp]:
1.477 -  "1 < (b::'a::{ordered_semidom,recpower}) ==> (b ^ x < b ^ y) = (x < y)"
1.478 +  "1 < b \<Longrightarrow> b ^ x < b ^ y \<longleftrightarrow> x < y"
1.479  by (blast intro: power_less_imp_less_exp power_strict_increasing)
1.480
1.481  lemma power_le_imp_le_base:
1.482 -assumes le: "a ^ Suc n \<le> b ^ Suc n"
1.483 -    and ynonneg: "(0::'a::{ordered_semidom,recpower}) \<le> b"
1.484 -shows "a \<le> b"
1.485 +  assumes le: "a ^ Suc n \<le> b ^ Suc n"
1.486 +    and ynonneg: "0 \<le> b"
1.487 +  shows "a \<le> b"
1.488  proof (rule ccontr)
1.489    assume "~ a \<le> b"
1.490    then have "b < a" by (simp only: linorder_not_le)
1.491    then have "b ^ Suc n < a ^ Suc n"
1.492      by (simp only: prems power_strict_mono)
1.493 -  from le and this show "False"
1.494 +  from le and this show False
1.495      by (simp add: linorder_not_less [symmetric])
1.496  qed
1.497
1.498  lemma power_less_imp_less_base:
1.499 -  fixes a b :: "'a::{ordered_semidom,recpower}"
1.500    assumes less: "a ^ n < b ^ n"
1.501    assumes nonneg: "0 \<le> b"
1.502    shows "a < b"
1.503 @@ -310,83 +310,144 @@
1.504    assume "~ a < b"
1.505    hence "b \<le> a" by (simp only: linorder_not_less)
1.506    hence "b ^ n \<le> a ^ n" using nonneg by (rule power_mono)
1.507 -  thus "~ a ^ n < b ^ n" by (simp only: linorder_not_less)
1.508 +  thus "\<not> a ^ n < b ^ n" by (simp only: linorder_not_less)
1.509  qed
1.510
1.511  lemma power_inject_base:
1.512 -     "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |]
1.513 -      ==> a = (b::'a::{ordered_semidom,recpower})"
1.514 -by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym)
1.515 +  "a ^ Suc n = b ^ Suc n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> a = b"
1.516 +by (blast intro: power_le_imp_le_base antisym eq_refl sym)
1.517
1.518  lemma power_eq_imp_eq_base:
1.519 -  fixes a b :: "'a::{ordered_semidom,recpower}"
1.520 -  shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
1.521 -by (cases n, simp_all del: power_Suc, rule power_inject_base)
1.522 +  "a ^ n = b ^ n \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 \<le> b \<Longrightarrow> 0 < n \<Longrightarrow> a = b"
1.523 +  by (cases n) (simp_all del: power_Suc, rule power_inject_base)
1.524
1.525 -text {* The divides relation *}
1.526 +end
1.527 +
1.528 +context ordered_idom
1.529 +begin
1.530
1.531 -lemma le_imp_power_dvd:
1.532 -  fixes a :: "'a::{comm_semiring_1,recpower}"
1.533 -  assumes "m \<le> n" shows "a^m dvd a^n"
1.534 -proof
1.535 -  have "a^n = a^(m + (n - m))"
1.536 -    using `m \<le> n` by simp
1.537 -  also have "\<dots> = a^m * a^(n - m)"
1.539 -  finally show "a^n = a^m * a^(n - m)" .
1.540 +lemma power_abs:
1.541 +  "abs (a ^ n) = abs a ^ n"
1.542 +  by (induct n) (auto simp add: abs_mult)
1.543 +
1.544 +lemma abs_power_minus [simp]:
1.545 +  "abs ((-a) ^ n) = abs (a ^ n)"
1.546 +  by (simp add: abs_minus_cancel power_abs)
1.547 +
1.548 +lemma zero_less_power_abs_iff [simp, noatp]:
1.549 +  "0 < abs a ^ n \<longleftrightarrow> a \<noteq> 0 \<or> n = 0"
1.550 +proof (induct n)
1.551 +  case 0 show ?case by simp
1.552 +next
1.553 +  case (Suc n) show ?case by (auto simp add: Suc zero_less_mult_iff)
1.554  qed
1.555
1.556 -lemma power_le_dvd:
1.557 -  fixes a b :: "'a::{comm_semiring_1,recpower}"
1.558 -  shows "a^n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a^m dvd b"
1.559 -  by (rule dvd_trans [OF le_imp_power_dvd])
1.560 +lemma zero_le_power_abs [simp]:
1.561 +  "0 \<le> abs a ^ n"
1.562 +  by (rule zero_le_power [OF abs_ge_zero])
1.563 +
1.564 +end
1.565 +
1.566 +context ring_1_no_zero_divisors
1.567 +begin
1.568 +
1.569 +lemma field_power_not_zero:
1.570 +  "a \<noteq> 0 \<Longrightarrow> a ^ n \<noteq> 0"
1.571 +  by (induct n) auto
1.572 +
1.573 +end
1.574 +
1.575 +context division_ring
1.576 +begin
1.577
1.578 +text {* FIXME reorient or rename to nonzero_inverse_power *}
1.579 +lemma nonzero_power_inverse:
1.580 +  "a \<noteq> 0 \<Longrightarrow> inverse (a ^ n) = (inverse a) ^ n"
1.581 +  by (induct n)
1.582 +    (simp_all add: nonzero_inverse_mult_distrib power_commutes field_power_not_zero)
1.583
1.584 -lemma dvd_power_same:
1.585 -  "(x::'a::{comm_semiring_1,recpower}) dvd y \<Longrightarrow> x^n dvd y^n"
1.586 -by (induct n) (auto simp add: mult_dvd_mono)
1.587 +end
1.588 +
1.589 +context field
1.590 +begin
1.591 +
1.592 +lemma nonzero_power_divide:
1.593 +  "b \<noteq> 0 \<Longrightarrow> (a / b) ^ n = a ^ n / b ^ n"
1.594 +  by (simp add: divide_inverse power_mult_distrib nonzero_power_inverse)
1.595 +
1.596 +end
1.597 +
1.598 +lemma power_0_Suc [simp]:
1.599 +  "(0::'a::{power, semiring_0}) ^ Suc n = 0"
1.600 +  by simp
1.601
1.602 -lemma dvd_power_le:
1.603 -  "(x::'a::{comm_semiring_1,recpower}) dvd y \<Longrightarrow> m >= n \<Longrightarrow> x^n dvd y^m"
1.604 -by(rule power_le_dvd[OF dvd_power_same])
1.605 +text{*It looks plausible as a simprule, but its effect can be strange.*}
1.606 +lemma power_0_left:
1.607 +  "0 ^ n = (if n = 0 then 1 else (0::'a::{power, semiring_0}))"
1.608 +  by (induct n) simp_all
1.609 +
1.610 +lemma power_eq_0_iff [simp]:
1.611 +  "a ^ n = 0 \<longleftrightarrow>
1.612 +     a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,power}) \<and> n \<noteq> 0"
1.613 +  by (induct n)
1.614 +    (auto simp add: no_zero_divisors elim: contrapos_pp)
1.615 +
1.616 +lemma power_diff:
1.617 +  fixes a :: "'a::field"
1.618 +  assumes nz: "a \<noteq> 0"
1.619 +  shows "n \<le> m \<Longrightarrow> a ^ (m - n) = a ^ m / a ^ n"
1.620 +  by (induct m n rule: diff_induct) (simp_all add: nz)
1.621
1.622 -lemma dvd_power [simp]:
1.623 -  "n > 0 | (x::'a::{comm_semiring_1,recpower}) = 1 \<Longrightarrow> x dvd x^n"
1.624 -apply (erule disjE)
1.625 - apply (subgoal_tac "x ^ n = x^(Suc (n - 1))")
1.626 -  apply (erule ssubst)
1.627 -  apply (subst power_Suc)
1.628 -  apply auto
1.629 +text{*Perhaps these should be simprules.*}
1.630 +lemma power_inverse:
1.631 +  fixes a :: "'a::{division_ring,division_by_zero,power}"
1.632 +  shows "inverse (a ^ n) = (inverse a) ^ n"
1.633 +apply (cases "a = 0")
1.636 +done (* TODO: reorient or rename to inverse_power *)
1.637 +
1.638 +lemma power_one_over:
1.639 +  "1 / (a::'a::{field,division_by_zero, power}) ^ n =  (1 / a) ^ n"
1.640 +  by (simp add: divide_inverse) (rule power_inverse)
1.641 +
1.642 +lemma power_divide:
1.643 +  "(a / b) ^ n = (a::'a::{field,division_by_zero}) ^ n / b ^ n"
1.644 +apply (cases "b = 0")
1.646 +apply (rule nonzero_power_divide)
1.647 +apply assumption
1.648  done
1.649
1.650 +class recpower = monoid_mult
1.651 +
1.652
1.653  subsection {* Exponentiation for the Natural Numbers *}
1.654
1.655  instance nat :: recpower ..
1.656
1.657 -lemma of_nat_power:
1.658 -  "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
1.659 -by (induct n, simp_all add: of_nat_mult)
1.660 +lemma nat_one_le_power [simp]:
1.661 +  "Suc 0 \<le> i \<Longrightarrow> Suc 0 \<le> i ^ n"
1.662 +  by (rule one_le_power [of i n, unfolded One_nat_def])
1.663
1.664 -lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
1.665 -by (rule one_le_power [of i n, unfolded One_nat_def])
1.666 -
1.667 -lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
1.668 -by (induct "n", auto)
1.669 +lemma nat_zero_less_power_iff [simp]:
1.670 +  "x ^ n > 0 \<longleftrightarrow> x > (0::nat) \<or> n = 0"
1.671 +  by (induct n) auto
1.672
1.673  lemma nat_power_eq_Suc_0_iff [simp]:
1.674 -  "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
1.675 -by (induct m, auto)
1.676 +  "x ^ m = Suc 0 \<longleftrightarrow> m = 0 \<or> x = Suc 0"
1.677 +  by (induct m) auto
1.678
1.679 -lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
1.680 -by simp
1.681 +lemma power_Suc_0 [simp]:
1.682 +  "Suc 0 ^ n = Suc 0"
1.683 +  by simp
1.684
1.685  text{*Valid for the naturals, but what if @{text"0<i<1"}?
1.686  Premises cannot be weakened: consider the case where @{term "i=0"},
1.687  @{term "m=1"} and @{term "n=0"}.*}
1.688  lemma nat_power_less_imp_less:
1.689    assumes nonneg: "0 < (i\<Colon>nat)"
1.690 -  assumes less: "i^m < i^n"
1.691 +  assumes less: "i ^ m < i ^ n"
1.692    shows "m < n"
1.693  proof (cases "i = 1")
1.694    case True with less power_one [where 'a = nat] show ?thesis by simp
1.695 @@ -395,10 +456,4 @@
1.696    from power_strict_increasing_iff [OF this] less show ?thesis ..
1.697  qed
1.698
1.699 -lemma power_diff:
1.700 -  assumes nz: "a ~= 0"
1.701 -  shows "n <= m ==> (a::'a::{recpower, field}) ^ (m-n) = (a^m) / (a^n)"
1.702 -  by (induct m n rule: diff_induct)
1.703 -    (simp_all add: nonzero_mult_divide_cancel_left nz)
1.704 -
1.705  end
```