# HG changeset patch
# User haftmann
# Date 1414065845 -7200
# Node ID 0997ea62e868f9b2d84a53381928efa6b102c357
# Parent  ae5e9b4f8daffb0e2a4c5d932212fb459a2965a5
slight generalization and unification of simp rules for algebraic procedures

diff -r ae5e9b4f8daf -r 0997ea62e868 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
+++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
@@ -255,7 +255,7 @@
   by simp
 
 lemma even_power [simp]:
-  "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
+  "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   by (induct n) auto
 
 end
@@ -551,7 +551,7 @@
 
 declare even_times_iff [presburger, algebra]
 
-declare even_power [presburger]
+declare even_power [presburger, algebra]
 
 lemma [presburger]:
   "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
@@ -587,15 +587,7 @@
   "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
   by presburger
 
-lemma [presburger, algebra]:
-  fixes m n :: nat
-  shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
-  by auto
-
-lemma [presburger, algebra]:
-  fixes m n :: nat
-  shows "even (m ^ n) \<longleftrightarrow> even m \<and> 0 < n"
-  by simp
+declare even_diff_nat [presburger, algebra]
 
 lemma [presburger]:
   fixes k :: int