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.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 -
```