src/HOL/Parity.thy
 changeset 66815 93c6632ddf44 parent 66808 1907167b6038 child 66816 212a3334e7da
```     1.1 --- a/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
1.2 +++ b/src/HOL/Parity.thy	Sun Oct 08 22:28:22 2017 +0200
1.3 @@ -6,19 +6,73 @@
1.4  section \<open>Parity in rings and semirings\<close>
1.5
1.6  theory Parity
1.7 -  imports Nat_Transfer Euclidean_Division
1.8 +  imports Euclidean_Division
1.9  begin
1.10
1.11  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
1.12
1.13 -class semiring_parity = comm_semiring_1_cancel + numeral +
1.14 -  assumes odd_one [simp]: "\<not> 2 dvd 1"
1.15 -  assumes odd_even_add: "\<not> 2 dvd a \<Longrightarrow> \<not> 2 dvd b \<Longrightarrow> 2 dvd a + b"
1.16 -  assumes even_multD: "2 dvd a * b \<Longrightarrow> 2 dvd a \<or> 2 dvd b"
1.17 -  assumes odd_ex_decrement: "\<not> 2 dvd a \<Longrightarrow> \<exists>b. a = b + 1"
1.18 +class semiring_parity = linordered_semidom + unique_euclidean_semiring +
1.19 +  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
1.20 +    and odd_imp_mod_2_eq_1: "\<not> 2 dvd a \<Longrightarrow> a mod 2 = 1"
1.21 +
1.22 +context semiring_parity
1.23  begin
1.24
1.25 -subclass semiring_numeral ..
1.26 +lemma of_nat_dvd_iff:
1.27 +  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
1.28 +proof (cases "m = 0")
1.29 +  case True
1.30 +  then show ?thesis
1.31 +    by simp
1.32 +next
1.33 +  case False
1.34 +  show ?thesis
1.35 +  proof
1.36 +    assume ?Q
1.37 +    then show ?P
1.38 +      by (auto elim: dvd_class.dvdE)
1.39 +  next
1.40 +    assume ?P
1.41 +    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
1.42 +      by simp
1.43 +    then have "of_nat n = of_nat (n div m * m)"
1.44 +      by (simp add: of_nat_div)
1.45 +    then have "n = n div m * m"
1.46 +      by (simp only: of_nat_eq_iff)
1.47 +    then have "n = m * (n div m)"
1.48 +      by (simp add: ac_simps)
1.49 +    then show ?Q ..
1.50 +  qed
1.51 +qed
1.52 +
1.53 +lemma of_nat_mod:
1.54 +  "of_nat (m mod n) = of_nat m mod of_nat n"
1.55 +proof -
1.56 +  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
1.57 +    by (simp add: div_mult_mod_eq)
1.58 +  also have "of_nat m = of_nat (m div n * n + m mod n)"
1.59 +    by simp
1.60 +  finally show ?thesis
1.61 +    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
1.62 +qed
1.63 +
1.64 +lemma one_div_two_eq_zero [simp]:
1.65 +  "1 div 2 = 0"
1.66 +proof -
1.67 +  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
1.68 +    by (simp only:) simp
1.69 +  then show ?thesis
1.70 +    by simp
1.71 +qed
1.72 +
1.73 +lemma one_mod_two_eq_one [simp]:
1.74 +  "1 mod 2 = 1"
1.75 +proof -
1.76 +  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
1.77 +    by (simp only:) simp
1.78 +  then show ?thesis
1.79 +    by simp
1.80 +qed
1.81
1.82  abbreviation even :: "'a \<Rightarrow> bool"
1.83    where "even a \<equiv> 2 dvd a"
1.84 @@ -26,11 +80,27 @@
1.85  abbreviation odd :: "'a \<Rightarrow> bool"
1.86    where "odd a \<equiv> \<not> 2 dvd a"
1.87
1.88 -lemma even_zero [simp]: "even 0"
1.89 -  by (fact dvd_0_right)
1.90 +lemma even_iff_mod_2_eq_zero:
1.91 +  "even a \<longleftrightarrow> a mod 2 = 0"
1.92 +  by (fact dvd_eq_mod_eq_0)
1.93 +
1.94 +lemma odd_iff_mod_2_eq_one:
1.95 +  "odd a \<longleftrightarrow> a mod 2 = 1"
1.96 +  by (auto dest: odd_imp_mod_2_eq_1)
1.97
1.98 -lemma even_plus_one_iff [simp]: "even (a + 1) \<longleftrightarrow> odd a"
1.99 -  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
1.100 +lemma parity_cases [case_names even odd]:
1.101 +  assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
1.102 +  assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
1.103 +  shows P
1.104 +  using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
1.105 +
1.106 +lemma not_mod_2_eq_1_eq_0 [simp]:
1.107 +  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
1.108 +  by (cases a rule: parity_cases) simp_all
1.109 +
1.110 +lemma not_mod_2_eq_0_eq_1 [simp]:
1.111 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
1.112 +  by (cases a rule: parity_cases) simp_all
1.113
1.114  lemma evenE [elim?]:
1.115    assumes "even a"
1.116 @@ -41,22 +111,107 @@
1.117    assumes "odd a"
1.118    obtains b where "a = 2 * b + 1"
1.119  proof -
1.120 -  from assms obtain b where *: "a = b + 1"
1.121 -    by (blast dest: odd_ex_decrement)
1.122 -  with assms have "even (b + 2)" by simp
1.123 -  then have "even b" by simp
1.124 -  then obtain c where "b = 2 * c" ..
1.125 -  with * have "a = 2 * c + 1" by simp
1.126 -  with that show thesis .
1.127 +  have "a = 2 * (a div 2) + a mod 2"
1.128 +    by (simp add: mult_div_mod_eq)
1.129 +  with assms have "a = 2 * (a div 2) + 1"
1.130 +    by (simp add: odd_iff_mod_2_eq_one)
1.131 +  then show ?thesis ..
1.132 +qed
1.133 +
1.134 +lemma mod_2_eq_odd:
1.135 +  "a mod 2 = of_bool (odd a)"
1.136 +  by (auto elim: oddE)
1.137 +
1.138 +lemma one_mod_2_pow_eq [simp]:
1.139 +  "1 mod (2 ^ n) = of_bool (n > 0)"
1.140 +proof -
1.141 +  have "1 mod (2 ^ n) = (of_bool (n > 0) :: nat)"
1.142 +    by (induct n) (simp_all add: mod_mult2_eq)
1.143 +  then have "of_nat (1 mod (2 ^ n)) = of_bool (n > 0)"
1.144 +    by simp
1.145 +  then show ?thesis
1.146 +    by (simp add: of_nat_mod)
1.147 +qed
1.148 +
1.149 +lemma even_of_nat [simp]:
1.150 +  "even (of_nat a) \<longleftrightarrow> even a"
1.151 +proof -
1.152 +  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
1.153 +    by simp
1.154 +  also have "\<dots> \<longleftrightarrow> even a"
1.155 +    by (simp only: of_nat_dvd_iff)
1.156 +  finally show ?thesis .
1.157 +qed
1.158 +
1.159 +lemma even_zero [simp]:
1.160 +  "even 0"
1.161 +  by (fact dvd_0_right)
1.162 +
1.163 +lemma odd_one [simp]:
1.164 +  "odd 1"
1.165 +proof -
1.166 +  have "\<not> (2 :: nat) dvd 1"
1.167 +    by simp
1.168 +  then have "\<not> of_nat 2 dvd of_nat 1"
1.169 +    unfolding of_nat_dvd_iff by simp
1.170 +  then show ?thesis
1.171 +    by simp
1.172  qed
1.173
1.174 -lemma even_times_iff [simp]: "even (a * b) \<longleftrightarrow> even a \<or> even b"
1.175 -  by (auto dest: even_multD)
1.176 +lemma odd_even_add:
1.177 +  "even (a + b)" if "odd a" and "odd b"
1.178 +proof -
1.179 +  from that obtain c d where "a = 2 * c + 1" and "b = 2 * d + 1"
1.180 +    by (blast elim: oddE)
1.181 +  then have "a + b = 2 * c + 2 * d + (1 + 1)"
1.182 +    by (simp only: ac_simps)
1.183 +  also have "\<dots> = 2 * (c + d + 1)"
1.184 +    by (simp add: algebra_simps)
1.185 +  finally show ?thesis ..
1.186 +qed
1.187 +
1.188 +lemma even_add [simp]:
1.189 +  "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
1.190 +  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
1.191 +
1.192 +lemma odd_add [simp]:
1.193 +  "odd (a + b) \<longleftrightarrow> \<not> (odd a \<longleftrightarrow> odd b)"
1.194 +  by simp
1.195 +
1.196 +lemma even_plus_one_iff [simp]:
1.197 +  "even (a + 1) \<longleftrightarrow> odd a"
1.198 +  by (auto simp add: dvd_add_right_iff intro: odd_even_add)
1.199 +
1.200 +lemma even_mult_iff [simp]:
1.201 +  "even (a * b) \<longleftrightarrow> even a \<or> even b" (is "?P \<longleftrightarrow> ?Q")
1.202 +proof
1.203 +  assume ?Q
1.204 +  then show ?P
1.205 +    by auto
1.206 +next
1.207 +  assume ?P
1.208 +  show ?Q
1.209 +  proof (rule ccontr)
1.210 +    assume "\<not> (even a \<or> even b)"
1.211 +    then have "odd a" and "odd b"
1.212 +      by auto
1.213 +    then obtain r s where "a = 2 * r + 1" and "b = 2 * s + 1"
1.214 +      by (blast elim: oddE)
1.215 +    then have "a * b = (2 * r + 1) * (2 * s + 1)"
1.216 +      by simp
1.217 +    also have "\<dots> = 2 * (2 * r * s + r + s) + 1"
1.218 +      by (simp add: algebra_simps)
1.219 +    finally have "odd (a * b)"
1.220 +      by simp
1.221 +    with \<open>?P\<close> show False
1.222 +      by auto
1.223 +  qed
1.224 +qed
1.225
1.226  lemma even_numeral [simp]: "even (numeral (Num.Bit0 n))"
1.227  proof -
1.228    have "even (2 * numeral n)"
1.229 -    unfolding even_times_iff by simp
1.230 +    unfolding even_mult_iff by simp
1.231    then have "even (numeral n + numeral n)"
1.232      unfolding mult_2 .
1.233    then show ?thesis
1.234 @@ -77,15 +232,26 @@
1.235    then show False by simp
1.236  qed
1.237
1.238 -lemma even_add [simp]: "even (a + b) \<longleftrightarrow> (even a \<longleftrightarrow> even b)"
1.239 -  by (auto simp add: dvd_add_right_iff dvd_add_left_iff odd_even_add)
1.240 -
1.241 -lemma odd_add [simp]: "odd (a + b) \<longleftrightarrow> (\<not> (odd a \<longleftrightarrow> odd b))"
1.242 -  by simp
1.243 -
1.244  lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
1.245    by (induct n) auto
1.246
1.247 +lemma even_succ_div_two [simp]:
1.248 +  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
1.249 +  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
1.250 +
1.251 +lemma odd_succ_div_two [simp]:
1.252 +  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
1.253 +  by (auto elim!: oddE simp add: add.assoc)
1.254 +
1.255 +lemma even_two_times_div_two:
1.256 +  "even a \<Longrightarrow> 2 * (a div 2) = a"
1.257 +  by (fact dvd_mult_div_cancel)
1.258 +
1.259 +lemma odd_two_times_div_two_succ [simp]:
1.260 +  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
1.261 +  using mult_div_mod_eq [of 2 a]
1.262 +  by (simp add: even_iff_mod_2_eq_zero)
1.263 +
1.264  end
1.265
1.266  class ring_parity = ring + semiring_parity
1.267 @@ -93,166 +259,48 @@
1.268
1.269  subclass comm_ring_1 ..
1.270
1.271 -lemma even_minus [simp]: "even (- a) \<longleftrightarrow> even a"
1.272 +lemma even_minus [simp]:
1.273 +  "even (- a) \<longleftrightarrow> even a"
1.274    by (fact dvd_minus_iff)
1.275
1.276 -lemma even_diff [simp]: "even (a - b) \<longleftrightarrow> even (a + b)"
1.277 +lemma even_diff [simp]:
1.278 +  "even (a - b) \<longleftrightarrow> even (a + b)"
1.279    using even_add [of a "- b"] by simp
1.280
1.281  end
1.282
1.283 -class unique_euclidean_semiring_parity = unique_euclidean_semiring +
1.284 -  assumes parity: "a mod 2 = 0 \<or> a mod 2 = 1"
1.285 -  assumes one_mod_two_eq_one [simp]: "1 mod 2 = 1"
1.286 -  assumes zero_not_eq_two: "0 \<noteq> 2"
1.287 -begin
1.288
1.289 -lemma parity_cases [case_names even odd]:
1.290 -  assumes "a mod 2 = 0 \<Longrightarrow> P"
1.291 -  assumes "a mod 2 = 1 \<Longrightarrow> P"
1.292 -  shows P
1.293 -  using assms parity by blast
1.294 -
1.295 -lemma one_div_two_eq_zero [simp]:
1.296 -  "1 div 2 = 0"
1.297 -proof (cases "2 = 0")
1.298 -  case True then show ?thesis by simp
1.299 -next
1.300 -  case False
1.301 -  from div_mult_mod_eq have "1 div 2 * 2 + 1 mod 2 = 1" .
1.302 -  with one_mod_two_eq_one have "1 div 2 * 2 + 1 = 1" by simp
1.303 -  then have "1 div 2 * 2 = 0" by (simp add: ac_simps add_left_imp_eq del: mult_eq_0_iff)
1.304 -  then have "1 div 2 = 0 \<or> 2 = 0" by simp
1.305 -  with False show ?thesis by auto
1.306 -qed
1.307 -
1.308 -lemma not_mod_2_eq_0_eq_1 [simp]:
1.309 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
1.310 -  by (cases a rule: parity_cases) simp_all
1.311 -
1.312 -lemma not_mod_2_eq_1_eq_0 [simp]:
1.313 -  "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
1.314 -  by (cases a rule: parity_cases) simp_all
1.315 +subsection \<open>Instance for @{typ nat}\<close>
1.316
1.317 -subclass semiring_parity
1.318 -proof (unfold_locales, unfold dvd_eq_mod_eq_0 not_mod_2_eq_0_eq_1)
1.319 -  show "1 mod 2 = 1"
1.320 -    by (fact one_mod_two_eq_one)
1.321 -next
1.322 -  fix a b
1.323 -  assume "a mod 2 = 1"
1.324 -  moreover assume "b mod 2 = 1"
1.325 -  ultimately show "(a + b) mod 2 = 0"
1.326 -    using mod_add_eq [of a 2 b] by simp
1.327 -next
1.328 -  fix a b
1.329 -  assume "(a * b) mod 2 = 0"
1.330 -  then have "(a mod 2) * (b mod 2) mod 2 = 0"
1.331 -    by (simp add: mod_mult_eq)
1.332 -  then have "(a mod 2) * (b mod 2) = 0"
1.333 -    by (cases "a mod 2 = 0") simp_all
1.334 -  then show "a mod 2 = 0 \<or> b mod 2 = 0"
1.335 -    by (rule divisors_zero)
1.336 -next
1.337 -  fix a
1.338 -  assume "a mod 2 = 1"
1.339 -  then have "a = a div 2 * 2 + 1"
1.340 -    using div_mult_mod_eq [of a 2] by simp
1.341 -  then show "\<exists>b. a = b + 1" ..
1.342 -qed
1.343 +instance nat :: semiring_parity
1.344 +  by standard (simp_all add: dvd_eq_mod_eq_0)
1.345
1.346 -lemma even_iff_mod_2_eq_zero:
1.347 -  "even a \<longleftrightarrow> a mod 2 = 0"
1.348 -  by (fact dvd_eq_mod_eq_0)
1.349 -
1.350 -lemma odd_iff_mod_2_eq_one:
1.351 -  "odd a \<longleftrightarrow> a mod 2 = 1"
1.352 -  by (simp add: even_iff_mod_2_eq_zero)
1.353 -
1.354 -lemma even_succ_div_two [simp]:
1.355 -  "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
1.356 -  by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
1.357 -
1.358 -lemma odd_succ_div_two [simp]:
1.359 -  "odd a \<Longrightarrow> (a + 1) div 2 = a div 2 + 1"
1.360 -  by (auto elim!: oddE simp add: zero_not_eq_two [symmetric] add.assoc)
1.361 -
1.362 -lemma even_two_times_div_two:
1.363 -  "even a \<Longrightarrow> 2 * (a div 2) = a"
1.364 -  by (fact dvd_mult_div_cancel)
1.365 -
1.366 -lemma odd_two_times_div_two_succ [simp]:
1.367 -  "odd a \<Longrightarrow> 2 * (a div 2) + 1 = a"
1.368 -  using mult_div_mod_eq [of 2 a] by (simp add: even_iff_mod_2_eq_zero)
1.369 -
1.370 -end
1.371 -
1.372 -
1.373 -subsection \<open>Instances for @{typ nat} and @{typ int}\<close>
1.374 -
1.375 -lemma even_Suc_Suc_iff [simp]: "2 dvd Suc (Suc n) \<longleftrightarrow> 2 dvd n"
1.376 +lemma even_Suc_Suc_iff [simp]:
1.377 +  "even (Suc (Suc n)) \<longleftrightarrow> even n"
1.378    using dvd_add_triv_right_iff [of 2 n] by simp
1.379
1.380 -lemma even_Suc [simp]: "2 dvd Suc n \<longleftrightarrow> \<not> 2 dvd n"
1.381 -  by (induct n) auto
1.382 +lemma even_Suc [simp]: "even (Suc n) \<longleftrightarrow> odd n"
1.383 +  using even_plus_one_iff [of n] by simp
1.384
1.385 -lemma even_diff_nat [simp]: "2 dvd (m - n) \<longleftrightarrow> m < n \<or> 2 dvd (m + n)"
1.386 -  for m n :: nat
1.387 +lemma even_diff_nat [simp]:
1.388 +  "even (m - n) \<longleftrightarrow> m < n \<or> even (m + n)" for m n :: nat
1.389  proof (cases "n \<le> m")
1.390    case True
1.391    then have "m - n + n * 2 = m + n" by (simp add: mult_2_right)
1.392 -  moreover have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m - n + n * 2)" by simp
1.393 -  ultimately have "2 dvd (m - n) \<longleftrightarrow> 2 dvd (m + n)" by (simp only:)
1.394 +  moreover have "even (m - n) \<longleftrightarrow> even (m - n + n * 2)" by simp
1.395 +  ultimately have "even (m - n) \<longleftrightarrow> even (m + n)" by (simp only:)
1.396    then show ?thesis by auto
1.397  next
1.398    case False
1.399    then show ?thesis by simp
1.400  qed
1.401
1.402 -instance nat :: semiring_parity
1.403 -proof
1.404 -  show "\<not> 2 dvd (1 :: nat)"
1.405 -    by (rule notI, erule dvdE) simp
1.406 -next
1.407 -  fix m n :: nat
1.408 -  assume "\<not> 2 dvd m"
1.409 -  moreover assume "\<not> 2 dvd n"
1.410 -  ultimately have *: "2 dvd Suc m \<and> 2 dvd Suc n"
1.411 -    by simp
1.412 -  then have "2 dvd (Suc m + Suc n)"
1.413 -    by (blast intro: dvd_add)
1.414 -  also have "Suc m + Suc n = m + n + 2"
1.415 -    by simp
1.416 -  finally show "2 dvd (m + n)"
1.417 -    using dvd_add_triv_right_iff [of 2 "m + n"] by simp
1.418 -next
1.419 -  fix m n :: nat
1.420 -  assume *: "2 dvd (m * n)"
1.421 -  show "2 dvd m \<or> 2 dvd n"
1.422 -  proof (rule disjCI)
1.423 -    assume "\<not> 2 dvd n"
1.424 -    then have "2 dvd (Suc n)" by simp
1.425 -    then obtain r where "Suc n = 2 * r" ..
1.426 -    moreover from * obtain s where "m * n = 2 * s" ..
1.427 -    then have "2 * s + m = m * Suc n" by simp
1.428 -    ultimately have " 2 * s + m = 2 * (m * r)"
1.429 -      by (simp add: algebra_simps)
1.430 -    then have "m = 2 * (m * r - s)" by simp
1.431 -    then show "2 dvd m" ..
1.432 -  qed
1.433 -next
1.434 -  fix n :: nat
1.435 -  assume "\<not> 2 dvd n"
1.436 -  then show "\<exists>m. n = m + 1"
1.437 -    by (cases n) simp_all
1.438 -qed
1.439 -
1.440 -lemma odd_pos: "odd n \<Longrightarrow> 0 < n"
1.441 -  for n :: nat
1.442 +lemma odd_pos:
1.443 +  "odd n \<Longrightarrow> 0 < n" for n :: nat
1.444    by (auto elim: oddE)
1.445
1.446 -lemma Suc_double_not_eq_double: "Suc (2 * m) \<noteq> 2 * n"
1.447 -  for m n :: nat
1.448 +lemma Suc_double_not_eq_double:
1.449 +  "Suc (2 * m) \<noteq> 2 * n"
1.450  proof
1.451    assume "Suc (2 * m) = 2 * n"
1.452    moreover have "odd (Suc (2 * m))" and "even (2 * n)"
1.453 @@ -260,52 +308,58 @@
1.454    ultimately show False by simp
1.455  qed
1.456
1.457 -lemma double_not_eq_Suc_double: "2 * m \<noteq> Suc (2 * n)"
1.458 -  for m n :: nat
1.459 +lemma double_not_eq_Suc_double:
1.460 +  "2 * m \<noteq> Suc (2 * n)"
1.461    using Suc_double_not_eq_double [of n m] by simp
1.462
1.463 -lemma even_diff_iff [simp]: "2 dvd (k - l) \<longleftrightarrow> 2 dvd (k + l)"
1.464 -  for k l :: int
1.465 -  using dvd_add_times_triv_right_iff [of 2 "k - l" l] by (simp add: mult_2_right)
1.466 +lemma odd_Suc_minus_one [simp]: "odd n \<Longrightarrow> Suc (n - Suc 0) = n"
1.467 +  by (auto elim: oddE)
1.468
1.469 -lemma even_abs_add_iff [simp]: "2 dvd (\<bar>k\<bar> + l) \<longleftrightarrow> 2 dvd (k + l)"
1.470 -  for k l :: int
1.471 -  by (cases "k \<ge> 0") (simp_all add: ac_simps)
1.472 +lemma even_Suc_div_two [simp]:
1.473 +  "even n \<Longrightarrow> Suc n div 2 = n div 2"
1.474 +  using even_succ_div_two [of n] by simp
1.475
1.476 -lemma even_add_abs_iff [simp]: "2 dvd (k + \<bar>l\<bar>) \<longleftrightarrow> 2 dvd (k + l)"
1.477 -  for k l :: int
1.478 -  using even_abs_add_iff [of l k] by (simp add: ac_simps)
1.479 +lemma odd_Suc_div_two [simp]:
1.480 +  "odd n \<Longrightarrow> Suc n div 2 = Suc (n div 2)"
1.481 +  using odd_succ_div_two [of n] by simp
1.482
1.483 -instance int :: ring_parity
1.484 -proof
1.485 -  show "\<not> 2 dvd (1 :: int)"
1.486 -    by (simp add: dvd_int_unfold_dvd_nat)
1.487 -next
1.488 -  fix k l :: int
1.489 -  assume "\<not> 2 dvd k"
1.490 -  moreover assume "\<not> 2 dvd l"
1.491 -  ultimately have "2 dvd (nat \<bar>k\<bar> + nat \<bar>l\<bar>)"
1.492 -    by (auto simp add: dvd_int_unfold_dvd_nat intro: odd_even_add)
1.493 -  then have "2 dvd (\<bar>k\<bar> + \<bar>l\<bar>)"
1.494 -    by (simp add: dvd_int_unfold_dvd_nat nat_add_distrib)
1.495 -  then show "2 dvd (k + l)"
1.496 +lemma odd_two_times_div_two_nat [simp]:
1.497 +  assumes "odd n"
1.498 +  shows "2 * (n div 2) = n - (1 :: nat)"
1.499 +proof -
1.500 +  from assms have "2 * (n div 2) + 1 = n"
1.501 +    by (rule odd_two_times_div_two_succ)
1.502 +  then have "Suc (2 * (n div 2)) - 1 = n - 1"
1.503      by simp
1.504 -next
1.505 -  fix k l :: int
1.506 -  assume "2 dvd (k * l)"
1.507 -  then show "2 dvd k \<or> 2 dvd l"
1.508 -    by (simp add: dvd_int_unfold_dvd_nat even_multD nat_abs_mult_distrib)
1.509 -next
1.510 -  fix k :: int
1.511 -  have "k = (k - 1) + 1" by simp
1.512 -  then show "\<exists>l. k = l + 1" ..
1.513 +  then show ?thesis
1.514 +    by simp
1.515  qed
1.516
1.517 -lemma even_int_iff [simp]: "even (int n) \<longleftrightarrow> even n"
1.518 -  by (simp add: dvd_int_iff)
1.519 -
1.520 -lemma even_nat_iff: "0 \<le> k \<Longrightarrow> even (nat k) \<longleftrightarrow> even k"
1.521 -  by (simp add: even_int_iff [symmetric])
1.522 +lemma parity_induct [case_names zero even odd]:
1.523 +  assumes zero: "P 0"
1.524 +  assumes even: "\<And>n. P n \<Longrightarrow> P (2 * n)"
1.525 +  assumes odd: "\<And>n. P n \<Longrightarrow> P (Suc (2 * n))"
1.526 +  shows "P n"
1.527 +proof (induct n rule: less_induct)
1.528 +  case (less n)
1.529 +  show "P n"
1.530 +  proof (cases "n = 0")
1.531 +    case True with zero show ?thesis by simp
1.532 +  next
1.533 +    case False
1.534 +    with less have hyp: "P (n div 2)" by simp
1.535 +    show ?thesis
1.536 +    proof (cases "even n")
1.537 +      case True
1.538 +      with hyp even [of "n div 2"] show ?thesis
1.539 +        by simp
1.540 +    next
1.541 +      case False
1.542 +      with hyp odd [of "n div 2"] show ?thesis
1.543 +        by simp
1.544 +    qed
1.545 +  qed
1.546 +qed
1.547
1.548
1.549  subsection \<open>Parity and powers\<close>
1.550 @@ -319,6 +373,10 @@
1.551  lemma power_minus_odd [simp]: "odd n \<Longrightarrow> (- a) ^ n = - (a ^ n)"
1.552    by (auto elim: oddE)
1.553
1.554 +lemma uminus_power_if:
1.555 +  "(- a) ^ n = (if even n then a ^ n else - (a ^ n))"
1.556 +  by auto
1.557 +
1.558  lemma neg_one_even_power [simp]: "even n \<Longrightarrow> (- 1) ^ n = 1"
1.559    by simp
1.560
1.561 @@ -396,9 +454,6 @@
1.562    qed
1.563  qed
1.564
1.565 -lemma (in comm_ring_1) uminus_power_if: "(- x) ^ n = (if even n then x^n else - (x ^ n))"
1.566 -  by auto
1.567 -
1.568  text \<open>Simplify, when the exponent is a numeral\<close>
1.569
1.570  lemma zero_le_power_eq_numeral [simp]:
1.571 @@ -428,9 +483,4 @@
1.572
1.573  end
1.574
1.575 -
1.576 -subsubsection \<open>Tool setup\<close>
1.577 -
1.578 -declare transfer_morphism_int_nat [transfer add return: even_int_iff]
1.579 -
1.580  end
```