src/HOL/Parity.thy
changeset 58679 33c90658448a
parent 58678 398e05aa84d4
child 58680 6b2fa479945f
     1.1 --- a/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Tue Oct 14 08:23:23 2014 +0200
     1.3 @@ -189,6 +189,15 @@
     1.4  
     1.5  end
     1.6  
     1.7 +context ring_parity
     1.8 +begin
     1.9 +
    1.10 +lemma even_minus [simp, presburger, algebra]:
    1.11 +  "even (- a) \<longleftrightarrow> even a"
    1.12 +  by (simp add: even_def)
    1.13 +
    1.14 +end
    1.15 +
    1.16  context semiring_div_parity
    1.17  begin
    1.18  
    1.19 @@ -196,38 +205,20 @@
    1.20    "even a \<longleftrightarrow> a mod 2 = 0"
    1.21    by (simp add: even_def dvd_eq_mod_eq_0)
    1.22  
    1.23 -lemma even_times_anything:
    1.24 -  "even a \<Longrightarrow> even (a * b)"
    1.25 -  by (simp add: even_def)
    1.26 -
    1.27 -lemma anything_times_even:
    1.28 -  "even a \<Longrightarrow> even (b * a)"
    1.29 -  by (simp add: even_def)
    1.30 -
    1.31 -lemma odd_times_odd:
    1.32 -  "odd a \<Longrightarrow> odd b \<Longrightarrow> odd (a * b)" 
    1.33 -  by (auto simp add: even_iff_mod_2_eq_zero mod_mult_left_eq)
    1.34 -
    1.35 -lemma even_product:
    1.36 -  "even (a * b) \<longleftrightarrow> even a \<or> even b"
    1.37 -  by (fact even_times_iff)
    1.38 -
    1.39  end
    1.40  
    1.41 -lemma even_nat_def [presburger]:
    1.42 -  "even x \<longleftrightarrow> even (int x)"
    1.43 -  by (auto simp add: even_iff_mod_2_eq_zero int_eq_iff int_mult nat_mult_distrib)
    1.44 -  
    1.45 -lemma transfer_int_nat_relations:
    1.46 -  "even (int x) \<longleftrightarrow> even x"
    1.47 -  by (simp add: even_nat_def)
    1.48 +lemma even_int_iff:
    1.49 +  "even (int n) \<longleftrightarrow> even n"
    1.50 +  by (simp add: even_def dvd_int_iff)
    1.51  
    1.52 -declare transfer_morphism_int_nat[transfer add return:
    1.53 -  transfer_int_nat_relations
    1.54 +declare transfer_morphism_int_nat [transfer add return:
    1.55 +  even_int_iff
    1.56  ]
    1.57  
    1.58 -declare even_iff_mod_2_eq_zero [of "- numeral v", simp] for v
    1.59 -
    1.60 +lemma [presburger]:
    1.61 +  "even n \<longleftrightarrow> even (int n)"
    1.62 +  using even_int_iff [of n] by simp
    1.63 +  
    1.64  
    1.65  subsection {* Behavior under integer arithmetic operations *}
    1.66  
    1.67 @@ -246,9 +237,6 @@
    1.68    "even ((x::int) + y) = ((even x & even y) | (odd x & odd y))"
    1.69  by presburger
    1.70  
    1.71 -lemma even_neg[simp,presburger,algebra]: "even (-(x::int)) = even x"
    1.72 -by presburger
    1.73 -
    1.74  lemma even_difference[simp]:
    1.75      "even ((x::int) - y) = ((even x & even y) | (odd x & odd y))" by presburger
    1.76  
    1.77 @@ -274,11 +262,7 @@
    1.78  subsection {* even and odd for nats *}
    1.79  
    1.80  lemma pos_int_even_equiv_nat_even: "0 \<le> x ==> even x = even (nat x)"
    1.81 -by (simp add: even_nat_def)
    1.82 -
    1.83 -lemma even_product_nat:
    1.84 -  "even((x::nat) * y) = (even x | even y)"
    1.85 -  by (fact even_times_iff)
    1.86 +by (simp add: even_int_iff [symmetric])
    1.87  
    1.88  lemma even_sum_nat[simp,presburger,algebra]:
    1.89    "even ((x::nat) + y) = ((even x & even y) | (odd x & odd y))"
    1.90 @@ -293,7 +277,7 @@
    1.91  
    1.92  lemma even_power_nat[simp,presburger,algebra]:
    1.93    "even ((x::nat)^y) = (even x & 0 < y)"
    1.94 -by (simp add: even_nat_def int_power)
    1.95 +by (simp add: even_int_iff [symmetric] int_power)
    1.96  
    1.97  
    1.98  subsection {* Equivalent definitions *}