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.52    by (simp add: power_commutes)
    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.56 +lemma power_add:
    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.63    by (induct n) (simp_all add: power_add)
    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.100 +    by (rule power_add)
   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.202 -by (simp add: power_gt1_lemma)
   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.295 -apply (simp add: power_0_left)
   1.296 -apply (simp add: nonzero_power_inverse)
   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.301 -apply (simp add: divide_inverse)
   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.538 -    by (rule power_add)
   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.634 +apply (simp add: power_0_left)
   1.635 +apply (simp add: nonzero_power_inverse)
   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.645 +apply (simp add: power_0_left)
   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