247 lemma neg_one_odd_power [simp]: |
247 lemma neg_one_odd_power [simp]: |
248 "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1" |
248 "odd x ==> (-1::'a::{number_ring,ringpower})^x = -1" |
249 by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) |
249 by (rule neg_one_even_odd_power [THEN conjunct2, THEN mp], assumption) |
250 |
250 |
251 lemma neg_power_if: |
251 lemma neg_power_if: |
252 "(-x::'a::{ring,ringpower}) ^ n = |
252 "(-x::'a::{comm_ring_1,ringpower}) ^ n = |
253 (if even n then (x ^ n) else -(x ^ n))" |
253 (if even n then (x ^ n) else -(x ^ n))" |
254 by (induct n, simp_all split: split_if_asm add: power_Suc) |
254 by (induct n, simp_all split: split_if_asm add: power_Suc) |
255 |
255 |
256 |
256 |
257 subsection {* An Equivalence for @{term "0 \<le> a^n"} *} |
257 subsection {* An Equivalence for @{term "0 \<le> a^n"} *} |
258 |
258 |
259 lemma even_power_le_0_imp_0: |
259 lemma even_power_le_0_imp_0: |
260 "a ^ (2*k) \<le> (0::'a::{ordered_ring,ringpower}) ==> a=0" |
260 "a ^ (2*k) \<le> (0::'a::{ordered_idom,ringpower}) ==> a=0" |
261 apply (induct k) |
261 apply (induct k) |
262 apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |
262 apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |
263 done |
263 done |
264 |
264 |
265 lemma zero_le_power_iff: |
265 lemma zero_le_power_iff: |
266 "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_ring,ringpower}) | even n)" |
266 "(0 \<le> a^n) = (0 \<le> (a::'a::{ordered_idom,ringpower}) | even n)" |
267 (is "?P n") |
267 (is "?P n") |
268 proof cases |
268 proof cases |
269 assume even: "even n" |
269 assume even: "even n" |
270 then obtain k where "n = 2*k" |
270 then obtain k where "n = 2*k" |
271 by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) |
271 by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) |