# HG changeset patch
# User huffman
# Date 1333113864 -7200
# Node ID 773fe2754b8c7fc54cfcafae6f764c2cbb9c0744
# Parent  4fc34c62847440519ccebc59e188de36596fa789
add simp rules for eve/odd on numerals

diff -r 4fc34c628474 -r 773fe2754b8c src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Fri Mar 30 14:27:29 2012 +0200
+++ b/src/HOL/Parity.thy	Fri Mar 30 15:24:24 2012 +0200
@@ -45,11 +45,20 @@
 
 lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
 
+lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
+  unfolding even_def by simp
+
+lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
+  unfolding even_def by simp
+
 (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
-declare even_def[of "numeral v", simp] for v
 declare even_def[of "neg_numeral v", simp] for v
 
-declare even_nat_def[of "numeral v", simp] for v
+lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
+  unfolding even_nat_def by simp
+
+lemma odd_numeral_nat [simp]: "odd (numeral (Num.Bit1 k) :: nat)"
+  unfolding even_nat_def by simp
 
 subsection {* Even and odd are mutually exclusive *}