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