src/HOL/Parity.thy
 changeset 58787 af9eb5e566dd parent 58778 e29cae8eab1f child 58889 5b7a9633cfa8
```     1.1 --- a/src/HOL/Parity.thy	Sat Oct 25 19:20:28 2014 +0200
1.2 +++ b/src/HOL/Parity.thy	Sun Oct 26 19:11:16 2014 +0100
1.3 @@ -3,148 +3,19 @@
1.4      Author:     Jacques D. Fleuriot
1.5  *)
1.6
1.7 -header {* Even and Odd for int and nat *}
1.8 +header {* Parity in rings and semirings *}
1.9
1.10  theory Parity
1.11  imports Nat_Transfer
1.12  begin
1.13
1.14 -subsection {* Preliminaries about divisibility on @{typ nat} and @{typ int} *}
1.15 -
1.16 -lemma two_dvd_Suc_Suc_iff [simp]:
1.17 -  "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
1.18 -  using dvd_add_triv_right_iff [of 2 n] by simp
1.19 -
1.20 -lemma two_dvd_Suc_iff:
1.21 -  "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
1.22 -  by (induct n) auto
1.23 -
1.24 -lemma two_dvd_diff_nat_iff:
1.25 -  fixes m n :: nat
1.26 -  shows "2 dvd m - n \<longleftrightarrow> m < n \<or> 2 dvd m + n"
1.27 -proof (cases "n \<le> m")
1.28 -  case True
1.29 -  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
1.30 -  moreover have "2 dvd m - n \<longleftrightarrow> 2 dvd m - n + n * 2" by simp
1.31 -  ultimately have "2 dvd m - n \<longleftrightarrow> 2 dvd m + n" by (simp only:)
1.32 -  then show ?thesis by auto
1.33 -next
1.34 -  case False
1.35 -  then show ?thesis by simp
1.36 -qed
1.37 -
1.38 -lemma two_dvd_diff_iff:
1.39 -  fixes k l :: int
1.40 -  shows "2 dvd k - l \<longleftrightarrow> 2 dvd k + l"
1.41 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
1.42 -
1.44 -  fixes k l :: int
1.45 -  shows "2 dvd \<bar>k\<bar> + l \<longleftrightarrow> 2 dvd k + l"
1.46 -  by (cases "k \<ge> 0") (simp_all add: two_dvd_diff_iff ac_simps)
1.47 -
1.49 -  fixes k l :: int
1.50 -  shows "2 dvd k + \<bar>l\<bar> \<longleftrightarrow> 2 dvd k + l"
1.52 -
1.53 -
1.54 -subsection {* Ring structures with parity *}
1.55 +subsection {* Ring structures with parity and @{text even}/@{text odd} predicates *}
1.56
1.57  class semiring_parity = semiring_dvd + semiring_numeral +
1.58 -  assumes two_not_dvd_one [simp]: "\<not> 2 dvd 1"
1.59 -  assumes not_dvd_not_dvd_dvd_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
1.60 -  assumes two_is_prime: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
1.61 -  assumes not_dvd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
1.62 -begin
1.63 -
1.64 -lemma two_dvd_plus_one_iff [simp]:
1.65 -  "2 dvd a + 1 \<longleftrightarrow> \<not> 2 dvd a"
1.67 -
1.68 -lemma not_two_dvdE [elim?]:
1.69 -  assumes "\<not> 2 dvd a"
1.70 -  obtains b where "a = 2 * b + 1"
1.71 -proof -
1.72 -  from assms obtain b where *: "a = b + 1"
1.73 -    by (blast dest: not_dvd_ex_decrement)
1.74 -  with assms have "2 dvd b + 2" by simp
1.75 -  then have "2 dvd b" by simp
1.76 -  then obtain c where "b = 2 * c" ..
1.77 -  with * have "a = 2 * c + 1" by simp
1.78 -  with that show thesis .
1.79 -qed
1.80 -
1.81 -end
1.82 -
1.83 -instance nat :: semiring_parity
1.84 -proof
1.85 -  show "\<not> (2 :: nat) dvd 1"
1.86 -    by (rule notI, erule dvdE) simp
1.87 -next
1.88 -  fix m n :: nat
1.89 -  assume "\<not> 2 dvd m"
1.90 -  moreover assume "\<not> 2 dvd n"
1.91 -  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
1.92 -    by (simp add: two_dvd_Suc_iff)
1.93 -  then have "2 dvd Suc m + Suc n"
1.94 -    by (blast intro: dvd_add)
1.95 -  also have "Suc m + Suc n = m + n + 2"
1.96 -    by simp
1.97 -  finally show "2 dvd m + n"
1.98 -    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
1.99 -next
1.100 -  fix m n :: nat
1.101 -  assume *: "2 dvd m * n"
1.102 -  show "2 dvd m \<or> 2 dvd n"
1.103 -  proof (rule disjCI)
1.104 -    assume "\<not> 2 dvd n"
1.105 -    then have "2 dvd Suc n" by (simp add: two_dvd_Suc_iff)
1.106 -    then obtain r where "Suc n = 2 * r" ..
1.107 -    moreover from * obtain s where "m * n = 2 * s" ..
1.108 -    then have "2 * s + m = m * Suc n" by simp
1.109 -    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
1.110 -    then have "m = 2 * (m * r - s)" by simp
1.111 -    then show "2 dvd m" ..
1.112 -  qed
1.113 -next
1.114 -  fix n :: nat
1.115 -  assume "\<not> 2 dvd n"
1.116 -  then show "\<exists>m. n = m + 1"
1.117 -    by (cases n) simp_all
1.118 -qed
1.119 -
1.120 -class ring_parity = comm_ring_1 + semiring_parity
1.121 -
1.122 -instance int :: ring_parity
1.123 -proof
1.124 -  show "\<not> (2 :: int) dvd 1" by (simp add: dvd_int_unfold_dvd_nat)
1.125 -  fix k l :: int
1.126 -  assume "\<not> 2 dvd k"
1.127 -  moreover assume "\<not> 2 dvd l"
1.128 -  ultimately have "2 dvd nat \<bar>k\<bar> + nat \<bar>l\<bar>"
1.130 -  then have "2 dvd \<bar>k\<bar> + \<bar>l\<bar>"
1.132 -  then show "2 dvd k + l"
1.134 -next
1.135 -  fix k l :: int
1.136 -  assume "2 dvd k * l"
1.137 -  then show "2 dvd k \<or> 2 dvd l"
1.138 -    by (simp add: dvd_int_unfold_dvd_nat two_is_prime nat_abs_mult_distrib)
1.139 -next
1.140 -  fix k :: int
1.141 -  have "k = (k - 1) + 1" by simp
1.142 -  then show "\<exists>l. k = l + 1" ..
1.143 -qed
1.144 -
1.145 -
1.146 -subsection {* Dedicated @{text even}/@{text odd} predicate *}
1.147 -
1.148 -subsubsection {* Properties *}
1.149 -
1.150 -context semiring_parity
1.151 +  assumes odd_one [simp]: "\<not> 2 dvd 1"
1.152 +  assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
1.153 +  assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
1.154 +  assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
1.155  begin
1.156
1.157  abbreviation even :: "'a \<Rightarrow> bool"
1.158 @@ -155,6 +26,14 @@
1.159  where
1.160    "odd a \<equiv> \<not> 2 dvd a"
1.161
1.162 +lemma even_zero [simp]:
1.163 +  "even 0"
1.164 +  by (fact dvd_0_right)
1.165 +
1.166 +lemma even_plus_one_iff [simp]:
1.167 +  "even (a + 1) \<longleftrightarrow> odd a"
1.169 +
1.170  lemma evenE [elim?]:
1.171    assumes "even a"
1.172    obtains b where "a = 2 * b"
1.173 @@ -163,19 +42,19 @@
1.174  lemma oddE [elim?]:
1.175    assumes "odd a"
1.176    obtains b where "a = 2 * b + 1"
1.177 -  using assms by (rule not_two_dvdE)
1.178 -
1.179 +proof -
1.180 +  from assms obtain b where *: "a = b + 1"
1.181 +    by (blast dest: odd_ex_decrement)
1.182 +  with assms have "even (b + 2)" by simp
1.183 +  then have "even b" by simp
1.184 +  then obtain c where "b = 2 * c" ..
1.185 +  with * have "a = 2 * c + 1" by simp
1.186 +  with that show thesis .
1.187 +qed
1.188 +
1.189  lemma even_times_iff [simp]:
1.190    "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.191 -  by (auto simp add: dest: two_is_prime)
1.192 -
1.193 -lemma even_zero [simp]:
1.194 -  "even 0"
1.195 -  by simp
1.196 -
1.197 -lemma odd_one [simp]:
1.198 -  "odd 1"
1.199 -  by simp
1.200 +  by (auto dest: even_multD)
1.201
1.202  lemma even_numeral [simp]:
1.203    "even (numeral (Num.Bit0 n))"
1.204 @@ -206,7 +85,7 @@
1.205
1.207    "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
1.210
1.212    "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
1.213 @@ -218,7 +97,7 @@
1.214
1.215  end
1.216
1.217 -context ring_parity
1.218 +class ring_parity = comm_ring_1 + semiring_parity
1.219  begin
1.220
1.221  lemma even_minus [simp]:
1.222 @@ -232,22 +111,110 @@
1.223  end
1.224
1.225
1.226 -subsubsection {* Particularities for @{typ nat} and @{typ int} *}
1.227 +subsection {* Instances for @{typ nat} and @{typ int} *}
1.228 +
1.229 +lemma even_Suc_Suc_iff [simp]:
1.230 +  "even (Suc (Suc n)) \<longleftrightarrow> even n"
1.231 +  using dvd_add_triv_right_iff [of 2 n] by simp
1.232
1.233  lemma even_Suc [simp]:
1.234 -  "even (Suc n) = odd n"
1.235 -  by (fact two_dvd_Suc_iff)
1.236 +  "even (Suc n) \<longleftrightarrow> odd n"
1.237 +  by (induct n) auto
1.238 +
1.239 +lemma even_diff_nat [simp]:
1.240 +  fixes m n :: nat
1.241 +  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
1.242 +proof (cases "n \<le> m")
1.243 +  case True
1.244 +  then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
1.245 +  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
1.246 +  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
1.247 +  then show ?thesis by auto
1.248 +next
1.249 +  case False
1.250 +  then show ?thesis by simp
1.251 +qed
1.252 +
1.253 +lemma even_diff_iff [simp]:
1.254 +  fixes k l :: int
1.255 +  shows "even (k - l) \<longleftrightarrow> even (k + l)"
1.256 +  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
1.257 +
1.259 +  fixes k l :: int
1.260 +  shows "even (\<bar>k\<bar> + l) \<longleftrightarrow> even (k + l)"
1.261 +  by (cases "k \<ge> 0") (simp_all add: ac_simps)
1.262 +
1.264 +  fixes k l :: int
1.265 +  shows "even (k + \<bar>l\<bar>) \<longleftrightarrow> even (k + l)"
1.267 +
1.268 +instance nat :: semiring_parity
1.269 +proof
1.270 +  show "odd (1 :: nat)"
1.271 +    by (rule notI, erule dvdE) simp
1.272 +next
1.273 +  fix m n :: nat
1.274 +  assume "odd m"
1.275 +  moreover assume "odd n"
1.276 +  ultimately have *: "even (Suc m) \<and> even (Suc n)"
1.277 +    by simp
1.278 +  then have "even (Suc m + Suc n)"
1.279 +    by (blast intro: dvd_add)
1.280 +  also have "Suc m + Suc n = m + n + 2"
1.281 +    by simp
1.282 +  finally show "even (m + n)"
1.283 +    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
1.284 +next
1.285 +  fix m n :: nat
1.286 +  assume *: "even (m * n)"
1.287 +  show "even m \<or> even n"
1.288 +  proof (rule disjCI)
1.289 +    assume "odd n"
1.290 +    then have "even (Suc n)" by simp
1.291 +    then obtain r where "Suc n = 2 * r" ..
1.292 +    moreover from * obtain s where "m * n = 2 * s" ..
1.293 +    then have "2 * s + m = m * Suc n" by simp
1.294 +    ultimately have " 2 * s + m = 2 * (m * r)" by (simp add: algebra_simps)
1.295 +    then have "m = 2 * (m * r - s)" by simp
1.296 +    then show "even m" ..
1.297 +  qed
1.298 +next
1.299 +  fix n :: nat
1.300 +  assume "odd n"
1.301 +  then show "\<exists>m. n = m + 1"
1.302 +    by (cases n) simp_all
1.303 +qed
1.304
1.305  lemma odd_pos:
1.306    "odd (n :: nat) \<Longrightarrow> 0 < n"
1.307    by (auto elim: oddE)
1.308
1.309 -lemma even_diff_nat [simp]:
1.310 -  fixes m n :: nat
1.311 -  shows "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)"
1.312 -  by (fact two_dvd_diff_nat_iff)
1.313 +instance int :: ring_parity
1.314 +proof
1.315 +  show "odd (1 :: int)" by (simp add: dvd_int_unfold_dvd_nat)
1.316 +  fix k l :: int
1.317 +  assume "odd k"
1.318 +  moreover assume "odd l"
1.319 +  ultimately have "even (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
1.321 +  then have "even (\<bar>k\<bar> + \<bar>l\<bar>)"
1.323 +  then show "even (k + l)"
1.324 +    by simp
1.325 +next
1.326 +  fix k l :: int
1.327 +  assume "even (k * l)"
1.328 +  then show "even k \<or> even l"
1.329 +    by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
1.330 +next
1.331 +  fix k :: int
1.332 +  have "k = (k - 1) + 1" by simp
1.333 +  then show "\<exists>l. k = l + 1" ..
1.334 +qed
1.335
1.336 -lemma even_int_iff:
1.337 +lemma even_int_iff [simp]:
1.338    "even (int n) \<longleftrightarrow> even n"
1.340
1.341 @@ -255,11 +222,8 @@
1.342    "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
1.343    by (simp add: even_int_iff [symmetric])
1.344
1.345 -lemma even_num_iff:
1.346 -  "0 < n \<Longrightarrow> even n = odd (n - 1 :: nat)"
1.347 -  by simp
1.348
1.349 -text {* Parity and powers *}
1.350 +subsection {* Parity and powers *}
1.351
1.352  context comm_ring_1
1.353  begin
1.354 @@ -272,10 +236,6 @@
1.355    "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
1.356    by (auto elim: oddE)
1.357
1.358 -lemma neg_power_if:
1.359 -  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
1.360 -  by simp
1.361 -
1.362  lemma neg_one_even_power [simp]:
1.363    "even n \<Longrightarrow> (- 1) ^ n = 1"
1.364    by simp
1.365 @@ -286,28 +246,9 @@
1.366
1.367  end
1.368
1.369 -lemma zero_less_power_nat_eq_numeral [simp]: -- \<open>FIXME move\<close>
1.370 -  "0 < (n :: nat) ^ numeral w \<longleftrightarrow> 0 < n \<or> numeral w = (0 :: nat)"
1.371 -  by (fact nat_zero_less_power_iff)
1.372 -
1.373  context linordered_idom
1.374  begin
1.375
1.376 -lemma power_eq_0_iff' [simp]: -- \<open>FIXME move\<close>
1.377 -  "a ^ n = 0 \<longleftrightarrow> a = 0 \<and> n > 0"
1.378 -  by (induct n) auto
1.379 -
1.380 -lemma power2_less_eq_zero_iff [simp]: -- \<open>FIXME move\<close>
1.381 -  "a\<^sup>2 \<le> 0 \<longleftrightarrow> a = 0"
1.382 -proof (cases "a = 0")
1.383 -  case True then show ?thesis by simp
1.384 -next
1.385 -  case False then have "a < 0 \<or> a > 0" by auto
1.386 -  then have "a\<^sup>2 > 0" by auto
1.387 -  then have "\<not> a\<^sup>2 \<le> 0" by (simp add: not_le)
1.388 -  with False show ?thesis by simp
1.389 -qed
1.390 -
1.391  lemma zero_le_even_power:
1.392    "even n \<Longrightarrow> 0 \<le> a ^ n"
1.393    by (auto elim: evenE)
1.394 @@ -316,35 +257,20 @@
1.395    "odd n \<Longrightarrow> 0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a"
1.396    by (auto simp add: power_even_eq zero_le_mult_iff elim: oddE)
1.397
1.398 -lemma zero_le_power_iff: -- \<open>FIXME cf. @{text zero_le_power_eq}\<close>
1.399 -  "0 \<le> a ^ n \<longleftrightarrow> 0 \<le> a \<or> even n"
1.400 -proof (cases "even n")
1.401 -  case True
1.402 -  then obtain k where "n = 2 * k" ..
1.403 -  then show ?thesis by simp
1.404 -next
1.405 -  case False
1.406 -  then obtain k where "n = 2 * k + 1" ..
1.407 -  moreover have "a ^ (2 * k) \<le> 0 \<Longrightarrow> a = 0"
1.408 -    by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
1.409 -  ultimately show ?thesis
1.410 -    by (auto simp add: zero_le_mult_iff zero_le_even_power)
1.411 -qed
1.412 -
1.413  lemma zero_le_power_eq:
1.414    "0 \<le> a ^ n \<longleftrightarrow> even n \<or> odd n \<and> 0 \<le> a"
1.415 -  using zero_le_power_iff [of a n] by auto
1.416 -
1.417 +  by (auto simp add: zero_le_even_power zero_le_odd_power)
1.418 +
1.419  lemma zero_less_power_eq:
1.420    "0 < a ^ n \<longleftrightarrow> n = 0 \<or> even n \<and> a \<noteq> 0 \<or> odd n \<and> 0 < a"
1.421  proof -
1.422    have [simp]: "0 = a ^ n \<longleftrightarrow> a = 0 \<and> n > 0"
1.423 -    unfolding power_eq_0_iff' [of a n, symmetric] by blast
1.424 +    unfolding power_eq_0_iff [of a n, symmetric] by blast
1.425    show ?thesis
1.426    unfolding less_le zero_le_power_eq by auto
1.427  qed
1.428
1.429 -lemma power_less_zero_eq:
1.430 +lemma power_less_zero_eq [simp]:
1.431    "a ^ n < 0 \<longleftrightarrow> odd n \<and> a < 0"
1.432    unfolding not_le [symmetric] zero_le_power_eq by auto
1.433
1.434 @@ -408,10 +334,6 @@
1.435    "a ^ numeral w < 0 \<longleftrightarrow> odd (numeral w :: nat) \<and> a < 0"
1.436    by (fact power_less_zero_eq)
1.437
1.438 -lemma power_eq_0_iff_numeral [simp]:
1.439 -  "a ^ numeral w = (0 :: nat) \<longleftrightarrow> a = 0 \<and> numeral w \<noteq> (0 :: nat)"
1.440 -  by (fact power_eq_0_iff)
1.441 -
1.442  lemma power_even_abs_numeral [simp]:
1.443    "even (numeral w :: nat) \<Longrightarrow> \<bar>a\<bar> ^ numeral w = a ^ numeral w"
1.444    by (fact power_even_abs)
```