1.1 --- a/src/HOL/Parity.thy	Fri Mar 30 14:27:29 2012 +0200
     1.2 +++ b/src/HOL/Parity.thy	Fri Mar 30 15:24:24 2012 +0200
     1.3 @@ -45,11 +45,20 @@
     1.4  
     1.5  lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
     1.6  
     1.7 +lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
     1.8 +  unfolding even_def by simp
     1.9 +
    1.10 +lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
    1.11 +  unfolding even_def by simp
    1.12 +
    1.13  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
    1.14 -declare even_def[of "numeral v", simp] for v
    1.15  declare even_def[of "neg_numeral v", simp] for v
    1.16  
    1.17 -declare even_nat_def[of "numeral v", simp] for v
    1.18 +lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
    1.19 +  unfolding even_nat_def by simp
    1.20 +
    1.21 +lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
    1.22 +  unfolding even_nat_def by simp
    1.23  
    1.24  subsection {* Even and odd are mutually exclusive *}
    1.25