src/HOL/Parity.thy
 changeset 54489 03ff4d1e6784 parent 54228 229282d53781 child 58645 94bef115c08f
```     1.1 --- a/src/HOL/Parity.thy	Tue Nov 19 01:30:14 2013 +0100
1.2 +++ b/src/HOL/Parity.thy	Tue Nov 19 10:05:53 2013 +0100
1.3 @@ -78,7 +78,7 @@
1.4    unfolding even_def by simp
1.5
1.6  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
1.7 -declare even_def [of "neg_numeral v", simp] for v
1.8 +declare even_def [of "- numeral v", simp] for v
1.9
1.10  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
1.11    unfolding even_nat_def by simp
1.12 @@ -190,14 +190,9 @@
1.13    by (induct n) simp_all
1.14
1.15  lemma (in comm_ring_1)
1.16 -  shows minus_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
1.17 -  and minus_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
1.18 -  by (simp_all add: neg_power_if del: minus_one)
1.19 -
1.20 -lemma (in comm_ring_1)
1.21 -  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (-1) ^ n = 1"
1.22 -  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (-1) ^ n = - 1"
1.23 -  by (simp_all add: minus_one [symmetric] del: minus_one)
1.24 +  shows neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
1.25 +  and neg_one_odd_power [simp]: "odd n \<Longrightarrow> (- 1) ^ n = - 1"
1.26 +  by (simp_all add: neg_power_if)
1.27
1.28  lemma zero_le_even_power: "even n ==>
1.29      0 <= (x::'a::{linordered_ring,monoid_mult}) ^ n"
```