equal
deleted
inserted
replaced
182 (odd x --> (- 1::'a)^x = - 1)" |
182 (odd x --> (- 1::'a)^x = - 1)" |
183 apply (induct x) |
183 apply (induct x) |
184 apply (rule conjI) |
184 apply (rule conjI) |
185 apply simp |
185 apply simp |
186 apply (insert even_zero_nat, blast) |
186 apply (insert even_zero_nat, blast) |
187 apply (simp add: power_Suc) |
187 apply simp |
188 done |
188 done |
189 |
189 |
190 lemma minus_one_even_power [simp]: |
190 lemma minus_one_even_power [simp]: |
191 "even x ==> (- 1::'a::{comm_ring_1})^x = 1" |
191 "even x ==> (- 1::'a::{comm_ring_1})^x = 1" |
192 using minus_one_even_odd_power by blast |
192 using minus_one_even_odd_power by blast |
197 |
197 |
198 lemma neg_one_even_odd_power: |
198 lemma neg_one_even_odd_power: |
199 "(even x --> (-1::'a::{number_ring})^x = 1) & |
199 "(even x --> (-1::'a::{number_ring})^x = 1) & |
200 (odd x --> (-1::'a)^x = -1)" |
200 (odd x --> (-1::'a)^x = -1)" |
201 apply (induct x) |
201 apply (induct x) |
202 apply (simp, simp add: power_Suc) |
202 apply (simp, simp) |
203 done |
203 done |
204 |
204 |
205 lemma neg_one_even_power [simp]: |
205 lemma neg_one_even_power [simp]: |
206 "even x ==> (-1::'a::{number_ring})^x = 1" |
206 "even x ==> (-1::'a::{number_ring})^x = 1" |
207 using neg_one_even_odd_power by blast |
207 using neg_one_even_odd_power by blast |
212 |
212 |
213 lemma neg_power_if: |
213 lemma neg_power_if: |
214 "(-x::'a::{comm_ring_1}) ^ n = |
214 "(-x::'a::{comm_ring_1}) ^ n = |
215 (if even n then (x ^ n) else -(x ^ n))" |
215 (if even n then (x ^ n) else -(x ^ n))" |
216 apply (induct n) |
216 apply (induct n) |
217 apply (simp_all split: split_if_asm add: power_Suc) |
217 apply simp_all |
218 done |
218 done |
219 |
219 |
220 lemma zero_le_even_power: "even n ==> |
220 lemma zero_le_even_power: "even n ==> |
221 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n" |
221 0 <= (x::'a::{linordered_ring_strict,monoid_mult}) ^ n" |
222 apply (simp add: even_nat_equiv_def2) |
222 apply (simp add: even_nat_equiv_def2) |
226 apply (rule zero_le_square) |
226 apply (rule zero_le_square) |
227 done |
227 done |
228 |
228 |
229 lemma zero_le_odd_power: "odd n ==> |
229 lemma zero_le_odd_power: "odd n ==> |
230 (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" |
230 (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)" |
231 apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff) |
231 apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff) |
232 apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) |
232 apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square) |
233 done |
233 done |
234 |
234 |
235 lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = |
235 lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{linordered_idom}) ^ n) = |
236 (even n | (odd n & 0 <= x))" |
236 (even n | (odd n & 0 <= x))" |
371 |
371 |
372 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
372 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
373 |
373 |
374 lemma even_power_le_0_imp_0: |
374 lemma even_power_le_0_imp_0: |
375 "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0" |
375 "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0" |
376 by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |
376 by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff) |
377 |
377 |
378 lemma zero_le_power_iff[presburger]: |
378 lemma zero_le_power_iff[presburger]: |
379 "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)" |
379 "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)" |
380 proof cases |
380 proof cases |
381 assume even: "even n" |
381 assume even: "even n" |
385 next |
385 next |
386 assume odd: "odd n" |
386 assume odd: "odd n" |
387 then obtain k where "n = Suc(2*k)" |
387 then obtain k where "n = Suc(2*k)" |
388 by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
388 by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2) |
389 thus ?thesis |
389 thus ?thesis |
390 by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power |
390 by (auto simp add: zero_le_mult_iff zero_le_even_power |
391 dest!: even_power_le_0_imp_0) |
391 dest!: even_power_le_0_imp_0) |
392 qed |
392 qed |
393 |
393 |
394 |
394 |
395 subsection {* Miscellaneous *} |
395 subsection {* Miscellaneous *} |