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