9 |
9 |
10 theory Power = Divides: |
10 theory Power = Divides: |
11 |
11 |
12 subsection{*Powers for Arbitrary (Semi)Rings*} |
12 subsection{*Powers for Arbitrary (Semi)Rings*} |
13 |
13 |
14 axclass ringpower \<subseteq> semiring, power |
14 axclass ringpower \<subseteq> comm_semiring_1_cancel, power |
15 power_0 [simp]: "a ^ 0 = 1" |
15 power_0 [simp]: "a ^ 0 = 1" |
16 power_Suc: "a ^ (Suc n) = a * (a ^ n)" |
16 power_Suc: "a ^ (Suc n) = a * (a ^ n)" |
17 |
17 |
18 lemma power_0_Suc [simp]: "(0::'a::ringpower) ^ (Suc n) = 0" |
18 lemma power_0_Suc [simp]: "(0::'a::ringpower) ^ (Suc n) = 0" |
19 by (simp add: power_Suc) |
19 by (simp add: power_Suc) |
44 apply (induct_tac "n") |
44 apply (induct_tac "n") |
45 apply (auto simp add: power_Suc mult_ac) |
45 apply (auto simp add: power_Suc mult_ac) |
46 done |
46 done |
47 |
47 |
48 lemma zero_less_power: |
48 lemma zero_less_power: |
49 "0 < (a::'a::{ordered_semiring,ringpower}) ==> 0 < a^n" |
49 "0 < (a::'a::{ordered_semidom,ringpower}) ==> 0 < a^n" |
50 apply (induct_tac "n") |
50 apply (induct_tac "n") |
51 apply (simp_all add: power_Suc zero_less_one mult_pos) |
51 apply (simp_all add: power_Suc zero_less_one mult_pos) |
52 done |
52 done |
53 |
53 |
54 lemma zero_le_power: |
54 lemma zero_le_power: |
55 "0 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 0 \<le> a^n" |
55 "0 \<le> (a::'a::{ordered_semidom,ringpower}) ==> 0 \<le> a^n" |
56 apply (simp add: order_le_less) |
56 apply (simp add: order_le_less) |
57 apply (erule disjE) |
57 apply (erule disjE) |
58 apply (simp_all add: zero_less_power zero_less_one power_0_left) |
58 apply (simp_all add: zero_less_power zero_less_one power_0_left) |
59 done |
59 done |
60 |
60 |
61 lemma one_le_power: |
61 lemma one_le_power: |
62 "1 \<le> (a::'a::{ordered_semiring,ringpower}) ==> 1 \<le> a^n" |
62 "1 \<le> (a::'a::{ordered_semidom,ringpower}) ==> 1 \<le> a^n" |
63 apply (induct_tac "n") |
63 apply (induct_tac "n") |
64 apply (simp_all add: power_Suc) |
64 apply (simp_all add: power_Suc) |
65 apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) |
65 apply (rule order_trans [OF _ mult_mono [of 1 _ 1]]) |
66 apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) |
66 apply (simp_all add: zero_le_one order_trans [OF zero_le_one]) |
67 done |
67 done |
68 |
68 |
69 lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semiring)" |
69 lemma gt1_imp_ge0: "1 < a ==> 0 \<le> (a::'a::ordered_semidom)" |
70 by (simp add: order_trans [OF zero_le_one order_less_imp_le]) |
70 by (simp add: order_trans [OF zero_le_one order_less_imp_le]) |
71 |
71 |
72 lemma power_gt1_lemma: |
72 lemma power_gt1_lemma: |
73 assumes gt1: "1 < (a::'a::{ordered_semiring,ringpower})" |
73 assumes gt1: "1 < (a::'a::{ordered_semidom,ringpower})" |
74 shows "1 < a * a^n" |
74 shows "1 < a * a^n" |
75 proof - |
75 proof - |
76 have "1*1 < a*1" using gt1 by simp |
76 have "1*1 < a*1" using gt1 by simp |
77 also have "\<dots> \<le> a * a^n" using gt1 |
77 also have "\<dots> \<le> a * a^n" using gt1 |
78 by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le |
78 by (simp only: mult_mono gt1_imp_ge0 one_le_power order_less_imp_le |
79 zero_le_one order_refl) |
79 zero_le_one order_refl) |
80 finally show ?thesis by simp |
80 finally show ?thesis by simp |
81 qed |
81 qed |
82 |
82 |
83 lemma power_gt1: |
83 lemma power_gt1: |
84 "1 < (a::'a::{ordered_semiring,ringpower}) ==> 1 < a ^ (Suc n)" |
84 "1 < (a::'a::{ordered_semidom,ringpower}) ==> 1 < a ^ (Suc n)" |
85 by (simp add: power_gt1_lemma power_Suc) |
85 by (simp add: power_gt1_lemma power_Suc) |
86 |
86 |
87 lemma power_le_imp_le_exp: |
87 lemma power_le_imp_le_exp: |
88 assumes gt1: "(1::'a::{ringpower,ordered_semiring}) < a" |
88 assumes gt1: "(1::'a::{ringpower,ordered_semidom}) < a" |
89 shows "!!n. a^m \<le> a^n ==> m \<le> n" |
89 shows "!!n. a^m \<le> a^n ==> m \<le> n" |
90 proof (induct m) |
90 proof (induct m) |
91 case 0 |
91 case 0 |
92 show ?case by simp |
92 show ?case by simp |
93 next |
93 next |
107 qed |
107 qed |
108 qed |
108 qed |
109 |
109 |
110 text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*} |
110 text{*Surely we can strengthen this? It holds for @{text "0<a<1"} too.*} |
111 lemma power_inject_exp [simp]: |
111 lemma power_inject_exp [simp]: |
112 "1 < (a::'a::{ordered_semiring,ringpower}) ==> (a^m = a^n) = (m=n)" |
112 "1 < (a::'a::{ordered_semidom,ringpower}) ==> (a^m = a^n) = (m=n)" |
113 by (force simp add: order_antisym power_le_imp_le_exp) |
113 by (force simp add: order_antisym power_le_imp_le_exp) |
114 |
114 |
115 text{*Can relax the first premise to @{term "0<a"} in the case of the |
115 text{*Can relax the first premise to @{term "0<a"} in the case of the |
116 natural numbers.*} |
116 natural numbers.*} |
117 lemma power_less_imp_less_exp: |
117 lemma power_less_imp_less_exp: |
118 "[| (1::'a::{ringpower,ordered_semiring}) < a; a^m < a^n |] ==> m < n" |
118 "[| (1::'a::{ringpower,ordered_semidom}) < a; a^m < a^n |] ==> m < n" |
119 by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] |
119 by (simp add: order_less_le [of m n] order_less_le [of "a^m" "a^n"] |
120 power_le_imp_le_exp) |
120 power_le_imp_le_exp) |
121 |
121 |
122 |
122 |
123 lemma power_mono: |
123 lemma power_mono: |
124 "[|a \<le> b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] ==> a^n \<le> b^n" |
124 "[|a \<le> b; (0::'a::{ringpower,ordered_semidom}) \<le> a|] ==> a^n \<le> b^n" |
125 apply (induct_tac "n") |
125 apply (induct_tac "n") |
126 apply (simp_all add: power_Suc) |
126 apply (simp_all add: power_Suc) |
127 apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b]) |
127 apply (auto intro: mult_mono zero_le_power order_trans [of 0 a b]) |
128 done |
128 done |
129 |
129 |
130 lemma power_strict_mono [rule_format]: |
130 lemma power_strict_mono [rule_format]: |
131 "[|a < b; (0::'a::{ringpower,ordered_semiring}) \<le> a|] |
131 "[|a < b; (0::'a::{ringpower,ordered_semidom}) \<le> a|] |
132 ==> 0 < n --> a^n < b^n" |
132 ==> 0 < n --> a^n < b^n" |
133 apply (induct_tac "n") |
133 apply (induct_tac "n") |
134 apply (auto simp add: mult_strict_mono zero_le_power power_Suc |
134 apply (auto simp add: mult_strict_mono zero_le_power power_Suc |
135 order_le_less_trans [of 0 a b]) |
135 order_le_less_trans [of 0 a b]) |
136 done |
136 done |
137 |
137 |
138 lemma power_eq_0_iff [simp]: |
138 lemma power_eq_0_iff [simp]: |
139 "(a^n = 0) = (a = (0::'a::{ordered_ring,ringpower}) & 0<n)" |
139 "(a^n = 0) = (a = (0::'a::{ordered_idom,ringpower}) & 0<n)" |
140 apply (induct_tac "n") |
140 apply (induct_tac "n") |
141 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym]) |
141 apply (auto simp add: power_Suc zero_neq_one [THEN not_sym]) |
142 done |
142 done |
143 |
143 |
144 lemma field_power_eq_0_iff [simp]: |
144 lemma field_power_eq_0_iff [simp]: |
172 apply (case_tac "b=0", simp add: power_0_left) |
172 apply (case_tac "b=0", simp add: power_0_left) |
173 apply (rule nonzero_power_divide) |
173 apply (rule nonzero_power_divide) |
174 apply assumption |
174 apply assumption |
175 done |
175 done |
176 |
176 |
177 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_ring,ringpower}) ^ n" |
177 lemma power_abs: "abs(a ^ n) = abs(a::'a::{ordered_idom,ringpower}) ^ n" |
178 apply (induct_tac "n") |
178 apply (induct_tac "n") |
179 apply (auto simp add: power_Suc abs_mult) |
179 apply (auto simp add: power_Suc abs_mult) |
180 done |
180 done |
181 |
181 |
182 lemma zero_less_power_abs_iff [simp]: |
182 lemma zero_less_power_abs_iff [simp]: |
183 "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_ring,ringpower}) | n=0)" |
183 "(0 < (abs a)^n) = (a \<noteq> (0::'a::{ordered_idom,ringpower}) | n=0)" |
184 proof (induct "n") |
184 proof (induct "n") |
185 case 0 |
185 case 0 |
186 show ?case by (simp add: zero_less_one) |
186 show ?case by (simp add: zero_less_one) |
187 next |
187 next |
188 case (Suc n) |
188 case (Suc n) |
189 show ?case by (force simp add: prems power_Suc zero_less_mult_iff) |
189 show ?case by (force simp add: prems power_Suc zero_less_mult_iff) |
190 qed |
190 qed |
191 |
191 |
192 lemma zero_le_power_abs [simp]: |
192 lemma zero_le_power_abs [simp]: |
193 "(0::'a::{ordered_ring,ringpower}) \<le> (abs a)^n" |
193 "(0::'a::{ordered_idom,ringpower}) \<le> (abs a)^n" |
194 apply (induct_tac "n") |
194 apply (induct_tac "n") |
195 apply (auto simp add: zero_le_one zero_le_power) |
195 apply (auto simp add: zero_le_one zero_le_power) |
196 done |
196 done |
197 |
197 |
198 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{ring,ringpower}) ^ n" |
198 lemma power_minus: "(-a) ^ n = (- 1)^n * (a::'a::{comm_ring_1,ringpower}) ^ n" |
199 proof - |
199 proof - |
200 have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) |
200 have "-a = (- 1) * a" by (simp add: minus_mult_left [symmetric]) |
201 thus ?thesis by (simp only: power_mult_distrib) |
201 thus ?thesis by (simp only: power_mult_distrib) |
202 qed |
202 qed |
203 |
203 |
204 text{*Lemma for @{text power_strict_decreasing}*} |
204 text{*Lemma for @{text power_strict_decreasing}*} |
205 lemma power_Suc_less: |
205 lemma power_Suc_less: |
206 "[|(0::'a::{ordered_semiring,ringpower}) < a; a < 1|] |
206 "[|(0::'a::{ordered_semidom,ringpower}) < a; a < 1|] |
207 ==> a * a^n < a^n" |
207 ==> a * a^n < a^n" |
208 apply (induct_tac n) |
208 apply (induct_tac n) |
209 apply (auto simp add: power_Suc mult_strict_left_mono) |
209 apply (auto simp add: power_Suc mult_strict_left_mono) |
210 done |
210 done |
211 |
211 |
212 lemma power_strict_decreasing: |
212 lemma power_strict_decreasing: |
213 "[|n < N; 0 < a; a < (1::'a::{ordered_semiring,ringpower})|] |
213 "[|n < N; 0 < a; a < (1::'a::{ordered_semidom,ringpower})|] |
214 ==> a^N < a^n" |
214 ==> a^N < a^n" |
215 apply (erule rev_mp) |
215 apply (erule rev_mp) |
216 apply (induct_tac "N") |
216 apply (induct_tac "N") |
217 apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) |
217 apply (auto simp add: power_Suc power_Suc_less less_Suc_eq) |
218 apply (rename_tac m) |
218 apply (rename_tac m) |
221 apply (auto simp add: zero_le_power zero_less_one order_less_imp_le) |
221 apply (auto simp add: zero_le_power zero_less_one order_less_imp_le) |
222 done |
222 done |
223 |
223 |
224 text{*Proof resembles that of @{text power_strict_decreasing}*} |
224 text{*Proof resembles that of @{text power_strict_decreasing}*} |
225 lemma power_decreasing: |
225 lemma power_decreasing: |
226 "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semiring,ringpower})|] |
226 "[|n \<le> N; 0 \<le> a; a \<le> (1::'a::{ordered_semidom,ringpower})|] |
227 ==> a^N \<le> a^n" |
227 ==> a^N \<le> a^n" |
228 apply (erule rev_mp) |
228 apply (erule rev_mp) |
229 apply (induct_tac "N") |
229 apply (induct_tac "N") |
230 apply (auto simp add: power_Suc le_Suc_eq) |
230 apply (auto simp add: power_Suc le_Suc_eq) |
231 apply (rename_tac m) |
231 apply (rename_tac m) |
233 apply (rule mult_mono) |
233 apply (rule mult_mono) |
234 apply (auto simp add: zero_le_power zero_le_one) |
234 apply (auto simp add: zero_le_power zero_le_one) |
235 done |
235 done |
236 |
236 |
237 lemma power_Suc_less_one: |
237 lemma power_Suc_less_one: |
238 "[| 0 < a; a < (1::'a::{ordered_semiring,ringpower}) |] ==> a ^ Suc n < 1" |
238 "[| 0 < a; a < (1::'a::{ordered_semidom,ringpower}) |] ==> a ^ Suc n < 1" |
239 apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) |
239 apply (insert power_strict_decreasing [of 0 "Suc n" a], simp) |
240 done |
240 done |
241 |
241 |
242 text{*Proof again resembles that of @{text power_strict_decreasing}*} |
242 text{*Proof again resembles that of @{text power_strict_decreasing}*} |
243 lemma power_increasing: |
243 lemma power_increasing: |
244 "[|n \<le> N; (1::'a::{ordered_semiring,ringpower}) \<le> a|] ==> a^n \<le> a^N" |
244 "[|n \<le> N; (1::'a::{ordered_semidom,ringpower}) \<le> a|] ==> a^n \<le> a^N" |
245 apply (erule rev_mp) |
245 apply (erule rev_mp) |
246 apply (induct_tac "N") |
246 apply (induct_tac "N") |
247 apply (auto simp add: power_Suc le_Suc_eq) |
247 apply (auto simp add: power_Suc le_Suc_eq) |
248 apply (rename_tac m) |
248 apply (rename_tac m) |
249 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp) |
249 apply (subgoal_tac "1 * a^n \<le> a * a^m", simp) |
251 apply (auto simp add: order_trans [OF zero_le_one] zero_le_power) |
251 apply (auto simp add: order_trans [OF zero_le_one] zero_le_power) |
252 done |
252 done |
253 |
253 |
254 text{*Lemma for @{text power_strict_increasing}*} |
254 text{*Lemma for @{text power_strict_increasing}*} |
255 lemma power_less_power_Suc: |
255 lemma power_less_power_Suc: |
256 "(1::'a::{ordered_semiring,ringpower}) < a ==> a^n < a * a^n" |
256 "(1::'a::{ordered_semidom,ringpower}) < a ==> a^n < a * a^n" |
257 apply (induct_tac n) |
257 apply (induct_tac n) |
258 apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) |
258 apply (auto simp add: power_Suc mult_strict_left_mono order_less_trans [OF zero_less_one]) |
259 done |
259 done |
260 |
260 |
261 lemma power_strict_increasing: |
261 lemma power_strict_increasing: |
262 "[|n < N; (1::'a::{ordered_semiring,ringpower}) < a|] ==> a^n < a^N" |
262 "[|n < N; (1::'a::{ordered_semidom,ringpower}) < a|] ==> a^n < a^N" |
263 apply (erule rev_mp) |
263 apply (erule rev_mp) |
264 apply (induct_tac "N") |
264 apply (induct_tac "N") |
265 apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) |
265 apply (auto simp add: power_less_power_Suc power_Suc less_Suc_eq) |
266 apply (rename_tac m) |
266 apply (rename_tac m) |
267 apply (subgoal_tac "1 * a^n < a * a^m", simp) |
267 apply (subgoal_tac "1 * a^n < a * a^m", simp) |
284 by (simp add: linorder_not_less [symmetric]) |
284 by (simp add: linorder_not_less [symmetric]) |
285 qed |
285 qed |
286 |
286 |
287 lemma power_inject_base: |
287 lemma power_inject_base: |
288 "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |] |
288 "[| a ^ Suc n = b ^ Suc n; 0 \<le> a; 0 \<le> b |] |
289 ==> a = (b::'a::{ordered_semiring,ringpower})" |
289 ==> a = (b::'a::{ordered_semidom,ringpower})" |
290 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) |
290 by (blast intro: power_le_imp_le_base order_antisym order_eq_refl sym) |
291 |
291 |
292 |
292 |
293 subsection{*Exponentiation for the Natural Numbers*} |
293 subsection{*Exponentiation for the Natural Numbers*} |
294 |
294 |