src/HOL/Parity.thy
 changeset 58770 ae5e9b4f8daf parent 58769 70fff47875cd child 58771 0997ea62e868
```     1.1 --- a/src/HOL/Parity.thy	Thu Oct 23 14:04:05 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Thu Oct 23 14:04:05 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 Main
1.8 +imports Presburger
1.9  begin
1.10
1.11  subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
1.12 @@ -24,7 +24,7 @@
1.13    shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
1.14  proof (cases "n \<le> m")
1.15    case True
1.16 -  then have "m - n + n * 2 = m + n" by simp
1.17 +  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
1.18    moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
1.19    ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
1.20    then show ?thesis by auto
1.21 @@ -103,7 +103,7 @@
1.22      then obtain r where "Suc n = 2 * r" ..
1.23      moreover from * obtain s where "m * n = 2 * s" ..
1.24      then have "2 * s + m = m * Suc n" by simp
1.25 -    ultimately have " 2 * s + m = 2 * (m * r)" by simp
1.26 +    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
1.27      then have "m = 2 * (m * r - s)" by simp
1.28      then show "2 dvd m" ..
1.29    qed
1.30 @@ -207,7 +207,7 @@
1.31    obtains b where "a = 2 * b + 1"
1.32    using assms by (rule not_two_dvdE)
1.33
1.34 -lemma even_times_iff [simp, presburger, algebra]:
1.35 +lemma even_times_iff [simp]:
1.36    "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.37    by (auto simp add: dest: two_is_prime)
1.38
1.39 @@ -254,7 +254,7 @@
1.40    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
1.41    by simp
1.42
1.43 -lemma even_power [simp, presburger]:
1.44 +lemma even_power [simp]:
1.45    "even (a ^ n) \<longleftrightarrow> even a \<and> n \<noteq> 0"
1.46    by (induct n) auto
1.47
1.48 @@ -263,7 +263,7 @@
1.49  context ring_parity
1.50  begin
1.51
1.52 -lemma even_minus [simp, presburger, algebra]:
1.53 +lemma even_minus [simp]:
1.54    "even (- a) \<longleftrightarrow> even a"
1.55    by (fact dvd_minus_iff)
1.56
1.57 @@ -317,7 +317,7 @@
1.58
1.59  subsubsection {* Particularities for @{typ nat} and @{typ int} *}
1.60
1.61 -lemma even_Suc [simp, presburger, algebra]:
1.62 +lemma even_Suc [simp]:
1.63    "even (Suc n) = odd n"
1.64    by (fact two_dvd_Suc_iff)
1.65
1.66 @@ -380,20 +380,6 @@
1.67    qed
1.68  qed
1.69
1.70 -text {* Nice facts about division by @{term 4} *}
1.71 -
1.72 -lemma even_even_mod_4_iff:
1.73 -  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
1.74 -  by presburger
1.75 -
1.76 -lemma odd_mod_4_div_2:
1.77 -  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
1.78 -  by presburger
1.79 -
1.80 -lemma even_mod_4_div_2:
1.81 -  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
1.82 -  by presburger
1.83 -
1.84  text {* Parity and powers *}
1.85
1.86  context comm_ring_1
1.87 @@ -451,7 +437,7 @@
1.88    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
1.89    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
1.90
1.91 -lemma zero_le_power_iff [presburger]: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
1.92 +lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
1.93    "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
1.94  proof (cases "even n")
1.95    case True
1.96 @@ -466,11 +452,11 @@
1.97      by (auto simp add: zero_le_mult_iff zero_le_even_power)
1.98  qed
1.99
1.100 -lemma zero_le_power_eq [presburger]:
1.101 +lemma zero_le_power_eq:
1.102    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
1.103    using zero_le_power_iff [of a n] by auto
1.104
1.105 -lemma zero_less_power_eq [presburger]:
1.106 +lemma zero_less_power_eq:
1.107    "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
1.108  proof -
1.109    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
1.110 @@ -479,11 +465,11 @@
1.111    unfolding less_le zero_le_power_eq by auto
1.112  qed
1.113
1.114 -lemma power_less_zero_eq [presburger]:
1.115 +lemma power_less_zero_eq:
1.116    "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
1.117    unfolding not_le [symmetric] zero_le_power_eq by auto
1.118
1.119 -lemma power_le_zero_eq [presburger]:
1.120 +lemma power_le_zero_eq:
1.121    "a ^ n \<le> 0 \<longleftrightarrow> n > 0 \<and> (odd n \<and> a \<le> 0 \<or> even n \<and> a = 0)"
1.122    unfolding not_less [symmetric] zero_less_power_eq by auto
1.123
1.124 @@ -560,14 +546,47 @@
1.125    even_int_iff
1.126  ]
1.127
1.128 +context semiring_parity
1.129 +begin
1.130 +
1.131 +declare even_times_iff [presburger, algebra]
1.132 +
1.133 +declare even_power [presburger]
1.134 +
1.135  lemma [presburger]:
1.136 -  "even n \<longleftrightarrow> even (int n)"
1.137 -  using even_int_iff [of n] by simp
1.138 -
1.139 -lemma (in semiring_parity) [presburger]:
1.140    "even (a + b) \<longleftrightarrow> even a \<and> even b \<or> odd a \<and> odd b"
1.141    by auto
1.142
1.143 +end
1.144 +
1.145 +context ring_parity
1.146 +begin
1.147 +
1.148 +declare even_minus [presburger, algebra]
1.149 +
1.150 +end
1.151 +
1.152 +context linordered_idom
1.153 +begin
1.154 +
1.155 +declare zero_le_power_iff [presburger]
1.156 +
1.157 +declare zero_le_power_eq [presburger]
1.158 +
1.159 +declare zero_less_power_eq [presburger]
1.160 +
1.161 +declare power_less_zero_eq [presburger]
1.162 +
1.163 +declare power_le_zero_eq [presburger]
1.164 +
1.165 +end
1.166 +
1.167 +declare even_Suc [presburger, algebra]
1.168 +
1.169 +lemma [presburger]:
1.170 +  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
1.171 +  by presburger
1.172 +
1.173  lemma [presburger, algebra]:
1.174    fixes m n :: nat
1.175    shows "even (m - n) \<longleftrightarrow> m < n \<or> even m \<and> even n \<or> odd m \<and> odd n"
1.176 @@ -587,10 +606,25 @@
1.177    fixes k :: int
1.178    shows "(k + 1) div 2 = k div 2 + 1 \<longleftrightarrow> odd k"
1.179    by presburger
1.180 -
1.181 +
1.182  lemma [presburger]:
1.183 -  "Suc n div Suc (Suc 0) = n div Suc (Suc 0) \<longleftrightarrow> even n"
1.184 +  "even n \<longleftrightarrow> even (int n)"
1.185 +  using even_int_iff [of n] by simp
1.186 +
1.187 +
1.188 +subsubsection {* Nice facts about division by @{term 4} *}
1.189 +
1.190 +lemma even_even_mod_4_iff:
1.191 +  "even (n::nat) \<longleftrightarrow> even (n mod 4)"
1.192    by presburger
1.193
1.194 +lemma odd_mod_4_div_2:
1.195 +  "n mod 4 = (3::nat) \<Longrightarrow> odd ((n - 1) div 2)"
1.196 +  by presburger
1.197 +
1.198 +lemma even_mod_4_div_2:
1.199 +  "n mod 4 = (1::nat) \<Longrightarrow> even ((n - 1) div 2)"
1.200 +  by presburger
1.201 +
1.202  end
1.203
```