16 |
16 |
17 subsection{*Powers for Arbitrary Monoids*} |
17 subsection{*Powers for Arbitrary Monoids*} |
18 |
18 |
19 class recpower = monoid_mult + power + |
19 class recpower = monoid_mult + power + |
20 assumes power_0 [simp]: "a ^ 0 = 1" |
20 assumes power_0 [simp]: "a ^ 0 = 1" |
21 assumes power_Suc: "a ^ Suc n = a * (a ^ n)" |
21 assumes power_Suc [simp]: "a ^ Suc n = a * (a ^ n)" |
22 |
22 |
23 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0" |
23 lemma power_0_Suc [simp]: "(0::'a::{recpower,semiring_0}) ^ (Suc n) = 0" |
24 by (simp add: power_Suc) |
24 by simp |
25 |
25 |
26 text{*It looks plausible as a simprule, but its effect can be strange.*} |
26 text{*It looks plausible as a simprule, but its effect can be strange.*} |
27 lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))" |
27 lemma power_0_left: "0^n = (if n=0 then 1 else (0::'a::{recpower,semiring_0}))" |
28 by (induct n) simp_all |
28 by (induct n) simp_all |
29 |
29 |
30 lemma power_one [simp]: "1^n = (1::'a::recpower)" |
30 lemma power_one [simp]: "1^n = (1::'a::recpower)" |
31 by (induct n) (simp_all add: power_Suc) |
31 by (induct n) simp_all |
32 |
32 |
33 lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a" |
33 lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a" |
34 unfolding One_nat_def by (simp add: power_Suc) |
34 unfolding One_nat_def by simp |
35 |
35 |
36 lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n" |
36 lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n" |
37 by (induct n) (simp_all add: power_Suc mult_assoc) |
37 by (induct n) (simp_all add: mult_assoc) |
38 |
38 |
39 lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a" |
39 lemma power_Suc2: "(a::'a::recpower) ^ Suc n = a ^ n * a" |
40 by (simp add: power_Suc power_commutes) |
40 by (simp add: power_commutes) |
41 |
41 |
42 lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)" |
42 lemma power_add: "(a::'a::recpower) ^ (m+n) = (a^m) * (a^n)" |
43 by (induct m) (simp_all add: power_Suc mult_ac) |
43 by (induct m) (simp_all add: mult_ac) |
44 |
44 |
45 lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n" |
45 lemma power_mult: "(a::'a::recpower) ^ (m*n) = (a^m) ^ n" |
46 by (induct n) (simp_all add: power_Suc power_add) |
46 by (induct n) (simp_all add: power_add) |
47 |
47 |
48 lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)" |
48 lemma power_mult_distrib: "((a::'a::{recpower,comm_monoid_mult}) * b) ^ n = (a^n) * (b^n)" |
49 by (induct n) (simp_all add: power_Suc mult_ac) |
49 by (induct n) (simp_all add: mult_ac) |
50 |
50 |
51 lemma zero_less_power[simp]: |
51 lemma zero_less_power[simp]: |
52 "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n" |
52 "0 < (a::'a::{ordered_semidom,recpower}) ==> 0 < a^n" |
53 apply (induct "n") |
53 by (induct n) (simp_all add: mult_pos_pos) |
54 apply (simp_all add: power_Suc zero_less_one mult_pos_pos) |
|
55 done |
|
56 |
54 |
57 lemma zero_le_power[simp]: |
55 lemma zero_le_power[simp]: |
58 "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n" |
56 "0 \<le> (a::'a::{ordered_semidom,recpower}) ==> 0 \<le> a^n" |
59 apply (simp add: order_le_less) |
57 by (induct n) (simp_all add: mult_nonneg_nonneg) |
60 apply (erule disjE) |
|
61 apply (simp_all add: zero_less_one power_0_left) |
|
62 done |
|
63 |
58 |
64 lemma one_le_power[simp]: |
59 lemma one_le_power[simp]: |
65 "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n" |
60 "1 \<le> (a::'a::{ordered_semidom,recpower}) ==> 1 \<le> a^n" |
66 apply (induct "n") |
61 apply (induct "n") |
67 apply (simp_all add: power_Suc) |
62 apply simp_all |
68 apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) |
63 apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) |
69 apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) |
64 apply (simp_all add: order_trans [OF zero_le_one]) |
70 done |
65 done |
71 |
66 |
72 lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semidom)" |
67 lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semidom)" |
73 by (simp add: order_trans [OF zero_le_one order_less_imp_le]) |
68 by (simp add: order_trans [OF zero_le_one order_less_imp_le]) |
74 |
69 |
83 finally show ?thesis by simp |
78 finally show ?thesis by simp |
84 qed |
79 qed |
85 |
80 |
86 lemma one_less_power[simp]: |
81 lemma one_less_power[simp]: |
87 "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n" |
82 "\<lbrakk>1 < (a::'a::{ordered_semidom,recpower}); 0 < n\<rbrakk> \<Longrightarrow> 1 < a ^ n" |
88 by (cases n, simp_all add: power_gt1_lemma power_Suc) |
83 by (cases n, simp_all add: power_gt1_lemma) |
89 |
84 |
90 lemma power_gt1: |
85 lemma power_gt1: |
91 "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)" |
86 "1 < (a::'a::{ordered_semidom,recpower}) ==> 1 < a ^ (Suc n)" |
92 by (simp add: power_gt1_lemma power_Suc) |
87 by (simp add: power_gt1_lemma) |
93 |
88 |
94 lemma power_le_imp_le_exp: |
89 lemma power_le_imp_le_exp: |
95 assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a" |
90 assumes gt1: "(1::'a::{recpower,ordered_semidom}) < a" |
96 shows "!!n. a^m \<le> a^n ==> m \<le> n" |
91 shows "!!n. a^m \<le> a^n ==> m \<le> n" |
97 proof (induct m) |
92 proof (induct m) |
100 next |
95 next |
101 case (Suc m) |
96 case (Suc m) |
102 show ?case |
97 show ?case |
103 proof (cases n) |
98 proof (cases n) |
104 case 0 |
99 case 0 |
105 from prems have "a * a^m \<le> 1" by (simp add: power_Suc) |
100 from prems have "a * a^m \<le> 1" by simp |
106 with gt1 show ?thesis |
101 with gt1 show ?thesis |
107 by (force simp only: power_gt1_lemma |
102 by (force simp only: power_gt1_lemma |
108 linorder_not_less [symmetric]) |
103 linorder_not_less [symmetric]) |
109 next |
104 next |
110 case (Suc n) |
105 case (Suc n) |
111 from prems show ?thesis |
106 from prems show ?thesis |
112 by (force dest: mult_left_le_imp_le |
107 by (force dest: mult_left_le_imp_le |
113 simp add: power_Suc order_less_trans [OF zero_less_one gt1]) |
108 simp add: order_less_trans [OF zero_less_one gt1]) |
114 qed |
109 qed |
115 qed |
110 qed |
116 |
111 |
117 text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*} |
112 text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*} |
118 lemma power_inject_exp [simp]: |
113 lemma power_inject_exp [simp]: |
128 |
123 |
129 |
124 |
130 lemma power_mono: |
125 lemma power_mono: |
131 "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n" |
126 "[|a \<le> b; (0::'a::{recpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n" |
132 apply (induct "n") |
127 apply (induct "n") |
133 apply (simp_all add: power_Suc) |
128 apply simp_all |
134 apply (auto intro: mult_mono order_trans [of 0 a b]) |
129 apply (auto intro: mult_mono order_trans [of 0 a b]) |
135 done |
130 done |
136 |
131 |
137 lemma power_strict_mono [rule_format]: |
132 lemma power_strict_mono [rule_format]: |
138 "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|] |
133 "[|a < b; (0::'a::{recpower,ordered_semidom}) \<le> a|] |
139 ==> 0 < n --> a^n < b^n" |
134 ==> 0 < n --> a^n < b^n" |
140 apply (induct "n") |
135 apply (induct "n") |
141 apply (auto simp add: mult_strict_mono power_Suc |
136 apply (auto simp add: mult_strict_mono order_le_less_trans [of 0 a b]) |
142 order_le_less_trans [of 0 a b]) |
|
143 done |
137 done |
144 |
138 |
145 lemma power_eq_0_iff [simp]: |
139 lemma power_eq_0_iff [simp]: |
146 "(a^n = 0) \<longleftrightarrow> |
140 "(a^n = 0) \<longleftrightarrow> |
147 (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)" |
141 (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)" |
148 apply (induct "n") |
142 apply (induct "n") |
149 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors) |
143 apply (auto simp add: no_zero_divisors) |
150 done |
144 done |
151 |
145 |
152 |
146 |
153 lemma field_power_not_zero: |
147 lemma field_power_not_zero: |
154 "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0" |
148 "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0" |
156 |
150 |
157 lemma nonzero_power_inverse: |
151 lemma nonzero_power_inverse: |
158 fixes a :: "'a::{division_ring,recpower}" |
152 fixes a :: "'a::{division_ring,recpower}" |
159 shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n" |
153 shows "a \<noteq> 0 ==> inverse (a ^ n) = (inverse a) ^ n" |
160 apply (induct "n") |
154 apply (induct "n") |
161 apply (auto simp add: power_Suc nonzero_inverse_mult_distrib power_commutes) |
155 apply (auto simp add: nonzero_inverse_mult_distrib power_commutes) |
162 done (* TODO: reorient or rename to nonzero_inverse_power *) |
156 done (* TODO: reorient or rename to nonzero_inverse_power *) |
163 |
157 |
164 text{*Perhaps these should be simprules.*} |
158 text{*Perhaps these should be simprules.*} |
165 lemma power_inverse: |
159 lemma power_inverse: |
166 fixes a :: "'a::{division_ring,division_by_zero,recpower}" |
160 fixes a :: "'a::{division_ring,division_by_zero,recpower}" |
187 apply assumption |
181 apply assumption |
188 done |
182 done |
189 |
183 |
190 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n" |
184 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,recpower}) ^ n" |
191 apply (induct "n") |
185 apply (induct "n") |
192 apply (auto simp add: power_Suc abs_mult) |
186 apply (auto simp add: abs_mult) |
193 done |
187 done |
194 |
188 |
195 lemma zero_less_power_abs_iff [simp,noatp]: |
189 lemma zero_less_power_abs_iff [simp,noatp]: |
196 "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)" |
190 "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,recpower}) | n=0)" |
197 proof (induct "n") |
191 proof (induct "n") |
198 case 0 |
192 case 0 |
199 show ?case by (simp add: zero_less_one) |
193 show ?case by simp |
200 next |
194 next |
201 case (Suc n) |
195 case (Suc n) |
202 show ?case by (auto simp add: prems power_Suc zero_less_mult_iff |
196 show ?case by (auto simp add: prems zero_less_mult_iff) |
203 abs_zero) |
|
204 qed |
197 qed |
205 |
198 |
206 lemma zero_le_power_abs [simp]: |
199 lemma zero_le_power_abs [simp]: |
207 "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" |
200 "(0::'a::{ordered_idom,recpower}) \<le> (abs a)^n" |
208 by (rule zero_le_power [OF abs_ge_zero]) |
201 by (rule zero_le_power [OF abs_ge_zero]) |
210 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring_1,recpower}) ^ n" |
203 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring_1,recpower}) ^ n" |
211 proof (induct n) |
204 proof (induct n) |
212 case 0 show ?case by simp |
205 case 0 show ?case by simp |
213 next |
206 next |
214 case (Suc n) then show ?case |
207 case (Suc n) then show ?case |
215 by (simp add: power_Suc2 mult_assoc) |
208 by (simp del: power_Suc add: power_Suc2 mult_assoc) |
216 qed |
209 qed |
217 |
210 |
218 text{*Lemma for @{text power_strict_decreasing}*} |
211 text{*Lemma for @{text power_strict_decreasing}*} |
219 lemma power_Suc_less: |
212 lemma power_Suc_less: |
220 "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|] |
213 "[|(0::'a::{ordered_semidom,recpower}) < a; a < 1|] |
221 ==> a * a^n < a^n" |
214 ==> a * a^n < a^n" |
222 apply (induct n) |
215 apply (induct n) |
223 apply (auto simp add: power_Suc mult_strict_left_mono) |
216 apply (auto simp add: mult_strict_left_mono) |
224 done |
217 done |
225 |
218 |
226 lemma power_strict_decreasing: |
219 lemma power_strict_decreasing: |
227 "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|] |
220 "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,recpower})|] |
228 ==> a^N < a^n" |
221 ==> a^N < a^n" |
229 apply (erule rev_mp) |
222 apply (erule rev_mp) |
230 apply (induct "N") |
223 apply (induct "N") |
231 apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) |
224 apply (auto simp add: power_Suc_less less_Suc_eq) |
232 apply (rename_tac m) |
225 apply (rename_tac m) |
233 apply (subgoal_tac "a * a^m < 1 * a^n", simp) |
226 apply (subgoal_tac "a * a^m < 1 * a^n", simp) |
234 apply (rule mult_strict_mono) |
227 apply (rule mult_strict_mono) |
235 apply (auto simp add: zero_less_one order_less_imp_le) |
228 apply (auto simp add: order_less_imp_le) |
236 done |
229 done |
237 |
230 |
238 text{*Proof resembles that of @{text power_strict_decreasing}*} |
231 text{*Proof resembles that of @{text power_strict_decreasing}*} |
239 lemma power_decreasing: |
232 lemma power_decreasing: |
240 "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|] |
233 "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,recpower})|] |
241 ==> a^N \<le> a^n" |
234 ==> a^N \<le> a^n" |
242 apply (erule rev_mp) |
235 apply (erule rev_mp) |
243 apply (induct "N") |
236 apply (induct "N") |
244 apply (auto simp add: power_Suc le_Suc_eq) |
237 apply (auto simp add: le_Suc_eq) |
245 apply (rename_tac m) |
238 apply (rename_tac m) |
246 apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp) |
239 apply (subgoal_tac "a * a^m \<le> 1 * a^n", simp) |
247 apply (rule mult_mono) |
240 apply (rule mult_mono) |
248 apply (auto simp add: zero_le_one) |
241 apply auto |
249 done |
242 done |
250 |
243 |
251 lemma power_Suc_less_one: |
244 lemma power_Suc_less_one: |
252 "[| 0 < a; a < (1::'a::{ordered_semidom,recpower}) |] ==> a ^ Suc n < 1" |
245 "[| 0 < a; a < (1::'a::{ordered_semidom,recpower}) |] ==> a ^ Suc n < 1" |
253 apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) |
246 apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) |
256 text{*Proof again resembles that of @{text power_strict_decreasing}*} |
249 text{*Proof again resembles that of @{text power_strict_decreasing}*} |
257 lemma power_increasing: |
250 lemma power_increasing: |
258 "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N" |
251 "[|n \<le> N; (1::'a::{ordered_semidom,recpower}) \<le> a|] ==> a^n \<le> a^N" |
259 apply (erule rev_mp) |
252 apply (erule rev_mp) |
260 apply (induct "N") |
253 apply (induct "N") |
261 apply (auto simp add: power_Suc le_Suc_eq) |
254 apply (auto simp add: le_Suc_eq) |
262 apply (rename_tac m) |
255 apply (rename_tac m) |
263 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp) |
256 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp) |
264 apply (rule mult_mono) |
257 apply (rule mult_mono) |
265 apply (auto simp add: order_trans [OF zero_le_one]) |
258 apply (auto simp add: order_trans [OF zero_le_one]) |
266 done |
259 done |
267 |
260 |
268 text{*Lemma for @{text power_strict_increasing}*} |
261 text{*Lemma for @{text power_strict_increasing}*} |
269 lemma power_less_power_Suc: |
262 lemma power_less_power_Suc: |
270 "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n" |
263 "(1::'a::{ordered_semidom,recpower}) < a ==> a^n < a * a^n" |
271 apply (induct n) |
264 apply (induct n) |
272 apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) |
265 apply (auto simp add: mult_strict_left_mono order_less_trans [OF zero_less_one]) |
273 done |
266 done |
274 |
267 |
275 lemma power_strict_increasing: |
268 lemma power_strict_increasing: |
276 "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N" |
269 "[|n < N; (1::'a::{ordered_semidom,recpower}) < a|] ==> a^n < a^N" |
277 apply (erule rev_mp) |
270 apply (erule rev_mp) |
278 apply (induct "N") |
271 apply (induct "N") |
279 apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) |
272 apply (auto simp add: power_less_power_Suc less_Suc_eq) |
280 apply (rename_tac m) |
273 apply (rename_tac m) |
281 apply (subgoal_tac "1 * a^n < a * a^m", simp) |
274 apply (subgoal_tac "1 * a^n < a * a^m", simp) |
282 apply (rule mult_strict_mono) |
275 apply (rule mult_strict_mono) |
283 apply (auto simp add: order_less_trans [OF zero_less_one] order_less_imp_le) |
276 apply (auto simp add: order_less_trans [OF zero_less_one] order_less_imp_le) |
284 done |
277 done |
322 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) |
315 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) |
323 |
316 |
324 lemma power_eq_imp_eq_base: |
317 lemma power_eq_imp_eq_base: |
325 fixes a b :: "'a::{ordered_semidom,recpower}" |
318 fixes a b :: "'a::{ordered_semidom,recpower}" |
326 shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b" |
319 shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b" |
327 by (cases n, simp_all, rule power_inject_base) |
320 by (cases n, simp_all del: power_Suc, rule power_inject_base) |
328 |
321 |
329 text {* The divides relation *} |
322 text {* The divides relation *} |
330 |
323 |
331 lemma le_imp_power_dvd: |
324 lemma le_imp_power_dvd: |
332 fixes a :: "'a::{comm_semiring_1,recpower}" |
325 fixes a :: "'a::{comm_semiring_1,recpower}" |
358 fix z n :: nat |
351 fix z n :: nat |
359 show "z^0 = 1" by simp |
352 show "z^0 = 1" by simp |
360 show "z^(Suc n) = z * (z^n)" by simp |
353 show "z^(Suc n) = z * (z^n)" by simp |
361 qed |
354 qed |
362 |
355 |
|
356 declare power_nat.simps [simp del] |
|
357 |
363 end |
358 end |
364 |
359 |
365 lemma of_nat_power: |
360 lemma of_nat_power: |
366 "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n" |
361 "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n" |
367 by (induct n, simp_all add: power_Suc of_nat_mult) |
362 by (induct n, simp_all add: of_nat_mult) |
368 |
363 |
369 lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n" |
364 lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n" |
370 by (rule one_le_power [of i n, unfolded One_nat_def]) |
365 by (rule one_le_power [of i n, unfolded One_nat_def]) |
371 |
366 |
372 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)" |
367 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)" |