43 |
43 |
44 lemma even_zero_nat[simp]: "even (0::nat)" by presburger |
44 lemma even_zero_nat[simp]: "even (0::nat)" by presburger |
45 |
45 |
46 lemma odd_1_nat [simp]: "odd (1::nat)" by presburger |
46 lemma odd_1_nat [simp]: "odd (1::nat)" by presburger |
47 |
47 |
48 declare even_def[of "number_of v", simp] for v |
48 (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *) |
49 |
49 declare even_def[of "numeral v", simp] for v |
50 declare even_nat_def[of "number_of v", simp] for v |
50 declare even_def[of "neg_numeral v", simp] for v |
|
51 |
|
52 declare even_nat_def[of "numeral v", simp] for v |
51 |
53 |
52 subsection {* Even and odd are mutually exclusive *} |
54 subsection {* Even and odd are mutually exclusive *} |
53 |
55 |
54 lemma int_pos_lt_two_imp_zero_or_one: |
56 lemma int_pos_lt_two_imp_zero_or_one: |
55 "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1" |
57 "0 <= x ==> (x::int) < 2 ==> x = 0 | x = 1" |
195 lemma minus_one_odd_power [simp]: |
197 lemma minus_one_odd_power [simp]: |
196 "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1" |
198 "odd x ==> (- 1::'a::{comm_ring_1})^x = - 1" |
197 using minus_one_even_odd_power by blast |
199 using minus_one_even_odd_power by blast |
198 |
200 |
199 lemma neg_one_even_odd_power: |
201 lemma neg_one_even_odd_power: |
200 "(even x --> (-1::'a::{number_ring})^x = 1) & |
202 "(even x --> (-1::'a::{comm_ring_1})^x = 1) & |
201 (odd x --> (-1::'a)^x = -1)" |
203 (odd x --> (-1::'a)^x = -1)" |
202 apply (induct x) |
204 apply (induct x) |
203 apply (simp, simp) |
205 apply (simp, simp) |
204 done |
206 done |
205 |
207 |
206 lemma neg_one_even_power [simp]: |
208 lemma neg_one_even_power [simp]: |
207 "even x ==> (-1::'a::{number_ring})^x = 1" |
209 "even x ==> (-1::'a::{comm_ring_1})^x = 1" |
208 using neg_one_even_odd_power by blast |
210 using neg_one_even_odd_power by blast |
209 |
211 |
210 lemma neg_one_odd_power [simp]: |
212 lemma neg_one_odd_power [simp]: |
211 "odd x ==> (-1::'a::{number_ring})^x = -1" |
213 "odd x ==> (-1::'a::{comm_ring_1})^x = -1" |
212 using neg_one_even_odd_power by blast |
214 using neg_one_even_odd_power by blast |
213 |
215 |
214 lemma neg_power_if: |
216 lemma neg_power_if: |
215 "(-x::'a::{comm_ring_1}) ^ n = |
217 "(-x::'a::{comm_ring_1}) ^ n = |
216 (if even n then (x ^ n) else -(x ^ n))" |
218 (if even n then (x ^ n) else -(x ^ n))" |
345 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
347 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)" |
346 by presburger |
348 by presburger |
347 |
349 |
348 text {* Simplify, when the exponent is a numeral *} |
350 text {* Simplify, when the exponent is a numeral *} |
349 |
351 |
350 lemmas power_0_left_number_of = power_0_left [of "number_of w"] for w |
352 lemma power_0_left_numeral [simp]: |
351 declare power_0_left_number_of [simp] |
353 "0 ^ numeral w = (0::'a::{power,semiring_0})" |
352 |
354 by (simp add: power_0_left) |
353 lemmas zero_le_power_eq_number_of [simp] = |
355 |
354 zero_le_power_eq [of _ "number_of w"] for w |
356 lemmas zero_le_power_eq_numeral [simp] = |
355 |
357 zero_le_power_eq [of _ "numeral w"] for w |
356 lemmas zero_less_power_eq_number_of [simp] = |
358 |
357 zero_less_power_eq [of _ "number_of w"] for w |
359 lemmas zero_less_power_eq_numeral [simp] = |
358 |
360 zero_less_power_eq [of _ "numeral w"] for w |
359 lemmas power_le_zero_eq_number_of [simp] = |
361 |
360 power_le_zero_eq [of _ "number_of w"] for w |
362 lemmas power_le_zero_eq_numeral [simp] = |
361 |
363 power_le_zero_eq [of _ "numeral w"] for w |
362 lemmas power_less_zero_eq_number_of [simp] = |
364 |
363 power_less_zero_eq [of _ "number_of w"] for w |
365 lemmas power_less_zero_eq_numeral [simp] = |
364 |
366 power_less_zero_eq [of _ "numeral w"] for w |
365 lemmas zero_less_power_nat_eq_number_of [simp] = |
367 |
366 zero_less_power_nat_eq [of _ "number_of w"] for w |
368 lemmas zero_less_power_nat_eq_numeral [simp] = |
367 |
369 zero_less_power_nat_eq [of _ "numeral w"] for w |
368 lemmas power_eq_0_iff_number_of [simp] = power_eq_0_iff [of _ "number_of w"] for w |
370 |
369 |
371 lemmas power_eq_0_iff_numeral [simp] = power_eq_0_iff [of _ "numeral w"] for w |
370 lemmas power_even_abs_number_of [simp] = power_even_abs [of "number_of w" _] for w |
372 |
|
373 lemmas power_even_abs_numeral [simp] = power_even_abs [of "numeral w" _] for w |
371 |
374 |
372 |
375 |
373 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
376 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
374 |
377 |
375 lemma even_power_le_0_imp_0: |
378 lemma even_power_le_0_imp_0: |