equal
deleted
inserted
replaced
1 (* Title: Parity.thy |
1 (* Title: Parity.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Jeremy Avigad |
3 Author: Jeremy Avigad |
4 *) |
4 *) |
5 |
5 |
6 header {* Parity: Even and Odd for ints and nats*} |
6 header {* Even and Odd for ints and nats*} |
7 |
7 |
8 theory Parity |
8 theory Parity |
9 imports Divides IntDiv NatSimprocs |
9 imports Divides IntDiv NatSimprocs |
10 begin |
10 begin |
11 |
11 |
395 |
395 |
396 lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] |
396 lemmas power_even_abs_number_of = power_even_abs [of "number_of w" _, standard] |
397 declare power_even_abs_number_of [simp] |
397 declare power_even_abs_number_of [simp] |
398 |
398 |
399 |
399 |
400 subsection {* An Equivalence for @{term "0 \<le> a^n"} *} |
400 subsection {* An Equivalence for @{term [source] "0 \<le> a^n"} *} |
401 |
401 |
402 lemma even_power_le_0_imp_0: |
402 lemma even_power_le_0_imp_0: |
403 "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0" |
403 "a ^ (2*k) \<le> (0::'a::{ordered_idom,recpower}) ==> a=0" |
404 apply (induct k) |
404 apply (induct k) |
405 apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |
405 apply (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc) |