216 apply (induct n) |
216 apply (induct n) |
217 apply (simp_all split: split_if_asm add: power_Suc) |
217 apply (simp_all split: split_if_asm add: power_Suc) |
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::{ordered_ring_strict,monoid_mult}) ^ n" |
221 0 <= (x::'a::{linlinordered_ring_strict,monoid_mult}) ^ n" |
222 apply (simp add: even_nat_equiv_def2) |
222 apply (simp add: even_nat_equiv_def2) |
223 apply (erule exE) |
223 apply (erule exE) |
224 apply (erule ssubst) |
224 apply (erule ssubst) |
225 apply (subst power_add) |
225 apply (subst power_add) |
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::{ordered_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_Suc 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::{ordered_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))" |
237 apply auto |
237 apply auto |
238 apply (subst zero_le_odd_power [symmetric]) |
238 apply (subst zero_le_odd_power [symmetric]) |
239 apply assumption+ |
239 apply assumption+ |
240 apply (erule zero_le_even_power) |
240 apply (erule zero_le_even_power) |
241 done |
241 done |
242 |
242 |
243 lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{ordered_idom}) ^ n) = |
243 lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{linordered_idom}) ^ n) = |
244 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" |
244 (n = 0 | (even n & x ~= 0) | (odd n & 0 < x))" |
245 |
245 |
246 unfolding order_less_le zero_le_power_eq by auto |
246 unfolding order_less_le zero_le_power_eq by auto |
247 |
247 |
248 lemma power_less_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n < 0) = |
248 lemma power_less_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n < 0) = |
249 (odd n & x < 0)" |
249 (odd n & x < 0)" |
250 apply (subst linorder_not_le [symmetric])+ |
250 apply (subst linorder_not_le [symmetric])+ |
251 apply (subst zero_le_power_eq) |
251 apply (subst zero_le_power_eq) |
252 apply auto |
252 apply auto |
253 done |
253 done |
254 |
254 |
255 lemma power_le_zero_eq[presburger]: "((x::'a::{ordered_idom}) ^ n <= 0) = |
255 lemma power_le_zero_eq[presburger]: "((x::'a::{linordered_idom}) ^ n <= 0) = |
256 (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" |
256 (n ~= 0 & ((odd n & x <= 0) | (even n & x = 0)))" |
257 apply (subst linorder_not_less [symmetric])+ |
257 apply (subst linorder_not_less [symmetric])+ |
258 apply (subst zero_less_power_eq) |
258 apply (subst zero_less_power_eq) |
259 apply auto |
259 apply auto |
260 done |
260 done |
261 |
261 |
262 lemma power_even_abs: "even n ==> |
262 lemma power_even_abs: "even n ==> |
263 (abs (x::'a::{ordered_idom}))^n = x^n" |
263 (abs (x::'a::{linordered_idom}))^n = x^n" |
264 apply (subst power_abs [symmetric]) |
264 apply (subst power_abs [symmetric]) |
265 apply (simp add: zero_le_even_power) |
265 apply (simp add: zero_le_even_power) |
266 done |
266 done |
267 |
267 |
268 lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" |
268 lemma zero_less_power_nat_eq[presburger]: "(0 < (x::nat) ^ n) = (n = 0 | 0 < x)" |
278 (- x)^n = - (x^n::'a::{comm_ring_1})" |
278 (- x)^n = - (x^n::'a::{comm_ring_1})" |
279 apply (subst power_minus) |
279 apply (subst power_minus) |
280 apply simp |
280 apply simp |
281 done |
281 done |
282 |
282 |
283 lemma power_mono_even: fixes x y :: "'a :: {ordered_idom}" |
283 lemma power_mono_even: fixes x y :: "'a :: {linordered_idom}" |
284 assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>" |
284 assumes "even n" and "\<bar>x\<bar> \<le> \<bar>y\<bar>" |
285 shows "x^n \<le> y^n" |
285 shows "x^n \<le> y^n" |
286 proof - |
286 proof - |
287 have "0 \<le> \<bar>x\<bar>" by auto |
287 have "0 \<le> \<bar>x\<bar>" by auto |
288 with `\<bar>x\<bar> \<le> \<bar>y\<bar>` |
288 with `\<bar>x\<bar> \<le> \<bar>y\<bar>` |
290 thus ?thesis unfolding power_even_abs[OF `even n`] . |
290 thus ?thesis unfolding power_even_abs[OF `even n`] . |
291 qed |
291 qed |
292 |
292 |
293 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger |
293 lemma odd_pos: "odd (n::nat) \<Longrightarrow> 0 < n" by presburger |
294 |
294 |
295 lemma power_mono_odd: fixes x y :: "'a :: {ordered_idom}" |
295 lemma power_mono_odd: fixes x y :: "'a :: {linordered_idom}" |
296 assumes "odd n" and "x \<le> y" |
296 assumes "odd n" and "x \<le> y" |
297 shows "x^n \<le> y^n" |
297 shows "x^n \<le> y^n" |
298 proof (cases "y < 0") |
298 proof (cases "y < 0") |
299 case True with `x \<le> y` have "-y \<le> -x" and "0 \<le> -y" by auto |
299 case True with `x \<le> y` have "-y \<le> -x" and "0 \<le> -y" by auto |
300 hence "(-y)^n \<le> (-x)^n" by (rule power_mono) |
300 hence "(-y)^n \<le> (-x)^n" by (rule power_mono) |
370 |
370 |
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::{ordered_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 power_Suc) |
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::{ordered_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" |
382 then obtain k where "n = 2*k" |
382 then obtain k where "n = 2*k" |
383 by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) |
383 by (auto simp add: even_nat_equiv_def2 numeral_2_eq_2) |
384 thus ?thesis by (simp add: zero_le_even_power even) |
384 thus ?thesis by (simp add: zero_le_even_power even) |