src/HOL/Parity.thy
 changeset 58645 94bef115c08f parent 54489 03ff4d1e6784 child 58678 398e05aa84d4
```     1.1 --- a/src/HOL/Parity.thy	Fri Oct 10 18:23:59 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 09 22:43:48 2014 +0200
1.3 @@ -14,15 +14,17 @@
1.4
1.5  definition even :: "'a \<Rightarrow> bool"
1.6  where
1.7 -  even_def [presburger]: "even a \<longleftrightarrow> a mod 2 = 0"
1.8 +  [algebra]: "even a \<longleftrightarrow> 2 dvd a"
1.9
1.10 -lemma even_iff_2_dvd [algebra]:
1.11 -  "even a \<longleftrightarrow> 2 dvd a"
1.12 +lemmas even_iff_2_dvd = even_def
1.13 +
1.14 +lemma even_iff_mod_2_eq_zero [presburger]:
1.15 +  "even a \<longleftrightarrow> a mod 2 = 0"
1.16    by (simp add: even_def dvd_eq_mod_eq_0)
1.17
1.18  lemma even_zero [simp]:
1.19    "even 0"
1.20 -  by (simp add: even_def)
1.21 +  by (simp add: even_iff_mod_2_eq_zero)
1.22
1.23  lemma even_times_anything:
1.24    "even a \<Longrightarrow> even (a * b)"
1.25 @@ -38,7 +40,7 @@
1.26
1.27  lemma odd_times_odd:
1.28    "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)"
1.29 -  by (auto simp add: even_def mod_mult_left_eq)
1.30 +  by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)
1.31
1.32  lemma even_product [simp, presburger]:
1.33    "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.34 @@ -53,7 +55,7 @@
1.35
1.36  lemma even_nat_def [presburger]:
1.37    "even x \<longleftrightarrow> even (int x)"
1.38 -  by (auto simp add: even_def int_eq_iff int_mult nat_mult_distrib)
1.39 +  by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)
1.40
1.41  lemma transfer_int_nat_relations:
1.42    "even (int x) \<longleftrightarrow> even x"
1.43 @@ -72,13 +74,13 @@
1.44    by presburger
1.45
1.46  lemma even_numeral_int [simp]: "even (numeral (Num.Bit0 k) :: int)"
1.47 -  unfolding even_def by simp
1.48 +  unfolding even_iff_mod_2_eq_zero by simp
1.49
1.50  lemma odd_numeral_int [simp]: "odd (numeral (Num.Bit1 k) :: int)"
1.51 -  unfolding even_def by simp
1.52 +  unfolding even_iff_mod_2_eq_zero by simp
1.53
1.54  (* TODO: proper simp rules for Num.Bit0, Num.Bit1 *)
1.55 -declare even_def [of "- numeral v", simp] for v
1.56 +declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v
1.57
1.58  lemma even_numeral_nat [simp]: "even (numeral (Num.Bit0 k) :: nat)"
1.59    unfolding even_nat_def by simp
```