author haftmann Thu Oct 23 14:04:05 2014 +0200 (2014-10-23) changeset 58771 0997ea62e868 parent 58770 ae5e9b4f8daf child 58772 1df01f0c0589
slight generalization and unification of simp rules for algebraic procedures
 src/HOL/Parity.thy file | annotate | diff | revisions
```     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
```