src/HOL/Parity.thy
changeset 58771 0997ea62e868
parent 58770 ae5e9b4f8daf
child 58777 6ba2f1fa243b
     1.1 --- a/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
     1.3 @@ -255,7 +255,7 @@
     1.4    by simp
     1.5  
     1.6  lemma even_power [simp]:
     1.7 -  "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
     1.8 +  "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
     1.9    by (induct n) auto
    1.10  
    1.11  end
    1.12 @@ -551,7 +551,7 @@
    1.13  
    1.14  declare even_times_iff [presburger, algebra]
    1.15  
    1.16 -declare even_power [presburger]
    1.17 +declare even_power [presburger, algebra]
    1.18  
    1.19  lemma [presburger]:
    1.20    "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
    1.21 @@ -587,15 +587,7 @@
    1.22    "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
    1.23    by presburger
    1.24  
    1.25 -lemma [presburger, algebra]:
    1.26 -  fixes m n :: nat
    1.27 -  shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
    1.28 -  by auto
    1.29 -
    1.30 -lemma [presburger, algebra]:
    1.31 -  fixes m n :: nat
    1.32 -  shows "even (m ^ n) \<longleftrightarrow> even m \<and> 0 < n"
    1.33 -  by simp
    1.34 +declare even_diff_nat [presburger, algebra]
    1.35  
    1.36  lemma [presburger]:
    1.37    fixes k :: int