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"