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