src/HOL/Parity.thy
changeset 58777 6ba2f1fa243b
parent 58771 0997ea62e868
child 58778 e29cae8eab1f
     1.1 --- a/src/HOL/Parity.thy	Fri Oct 24 15:07:51 2014 +0200
     1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 19:40:39 2014 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Even and Odd for int and nat *}
     1.5  
     1.6  theory Parity
     1.7 -imports Presburger
     1.8 +imports Divides
     1.9  begin
    1.10  
    1.11  subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
    1.12 @@ -36,7 +36,7 @@
    1.13  lemma two_dvd_diff_iff:
    1.14    fixes k l :: int
    1.15    shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
    1.16 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: ac_simps)
    1.17 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
    1.18  
    1.19  lemma two_dvd_abs_add_iff:
    1.20    fixes k l :: int
    1.21 @@ -546,77 +546,5 @@
    1.22    even_int_iff
    1.23  ]
    1.24  
    1.25 -context semiring_parity
    1.26 -begin
    1.27 -
    1.28 -declare even_times_iff [presburger, algebra]
    1.29 -
    1.30 -declare even_power [presburger, algebra]
    1.31 -
    1.32 -lemma [presburger]:
    1.33 -  "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
    1.34 -  by auto
    1.35 -
    1.36 -end
    1.37 -
    1.38 -context ring_parity
    1.39 -begin
    1.40 -
    1.41 -declare even_minus [presburger, algebra]
    1.42 -
    1.43 -end
    1.44 -
    1.45 -context linordered_idom
    1.46 -begin
    1.47 -
    1.48 -declare zero_le_power_iff [presburger]
    1.49 -
    1.50 -declare zero_le_power_eq [presburger]
    1.51 -
    1.52 -declare zero_less_power_eq [presburger]
    1.53 -
    1.54 -declare power_less_zero_eq [presburger]
    1.55 -  
    1.56 -declare power_le_zero_eq [presburger]
    1.57 -
    1.58  end
    1.59  
    1.60 -declare even_Suc [presburger, algebra]
    1.61 -
    1.62 -lemma [presburger]:
    1.63 -  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
    1.64 -  by presburger
    1.65 -
    1.66 -declare even_diff_nat [presburger, algebra]
    1.67 -
    1.68 -lemma [presburger]:
    1.69 -  fixes k :: int
    1.70 -  shows "(k + 1) div 2 = k div 2 \<longleftrightarrow> even k"
    1.71 -  by presburger
    1.72 -
    1.73 -lemma [presburger]:
    1.74 -  fixes k :: int
    1.75 -  shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
    1.76 -  by presburger
    1.77 -
    1.78 -lemma [presburger]:
    1.79 -  "even n \<longleftrightarrow> even (int n)"
    1.80 -  using even_int_iff [of n] by simp
    1.81 -  
    1.82 -
    1.83 -subsubsection {* Nice facts about division by @{term 4} *}  
    1.84 -
    1.85 -lemma even_even_mod_4_iff:
    1.86 -  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
    1.87 -  by presburger
    1.88 -
    1.89 -lemma odd_mod_4_div_2:
    1.90 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
    1.91 -  by presburger
    1.92 -
    1.93 -lemma even_mod_4_div_2:
    1.94 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
    1.95 -  by presburger
    1.96 -  
    1.97 -end
    1.98 -