generalized type classes for parity to cover word types also, which contain zero divisors
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago)
changeset 70341972c0c744e7c
parent 70340 7383930fc946
child 70342 e4d626692640
generalized type classes for parity to cover word types also, which contain zero divisors
src/HOL/Groebner_Basis.thy
src/HOL/Parity.thy
src/HOL/Presburger.thy
     1.1 --- a/src/HOL/Groebner_Basis.thy	Fri Jun 14 08:34:27 2019 +0000
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -75,7 +75,7 @@
     1.4  declare mod_eq_dvd_iff[algebra]
     1.5  declare nat_mod_eq_iff[algebra]
     1.6  
     1.7 -context unique_euclidean_semiring_with_nat
     1.8 +context semiring_parity
     1.9  begin
    1.10  
    1.11  declare even_mult_iff [algebra]
    1.12 @@ -83,7 +83,7 @@
    1.13  
    1.14  end
    1.15  
    1.16 -context unique_euclidean_ring_with_nat
    1.17 +context ring_parity
    1.18  begin
    1.19  
    1.20  declare even_minus [algebra]
     2.1 --- a/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
     2.2 +++ b/src/HOL/Parity.thy	Fri Jun 14 08:34:27 2019 +0000
     2.3 @@ -11,165 +11,35 @@
     2.4  
     2.5  subsection \<open>Ring structures with parity and \<open>even\<close>/\<open>odd\<close> predicates\<close>
     2.6  
     2.7 -class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
     2.8 -  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
     2.9 -    and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
    2.10 -    and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
    2.11 +class semiring_parity = comm_semiring_1 + semiring_modulo +
    2.12 +  assumes even_iff_mod_2_eq_zero: "2 dvd a \<longleftrightarrow> a mod 2 = 0"
    2.13 +    and odd_iff_mod_2_eq_one: "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1"
    2.14 +    and odd_one [simp]: "\<not> 2 dvd 1"
    2.15  begin
    2.16  
    2.17 -lemma division_segment_eq_iff:
    2.18 -  "a = b" if "division_segment a = division_segment b"
    2.19 -    and "euclidean_size a = euclidean_size b"
    2.20 -  using that division_segment_euclidean_size [of a] by simp
    2.21 -
    2.22 -lemma euclidean_size_of_nat [simp]:
    2.23 -  "euclidean_size (of_nat n) = n"
    2.24 -proof -
    2.25 -  have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
    2.26 -    by (fact division_segment_euclidean_size)
    2.27 -  then show ?thesis by simp
    2.28 -qed
    2.29 -
    2.30 -lemma of_nat_euclidean_size:
    2.31 -  "of_nat (euclidean_size a) = a div division_segment a"
    2.32 -proof -
    2.33 -  have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
    2.34 -    by (subst nonzero_mult_div_cancel_left) simp_all
    2.35 -  also have "\<dots> = a div division_segment a"
    2.36 -    by simp
    2.37 -  finally show ?thesis .
    2.38 -qed
    2.39 -
    2.40 -lemma division_segment_1 [simp]:
    2.41 -  "division_segment 1 = 1"
    2.42 -  using division_segment_of_nat [of 1] by simp
    2.43 -
    2.44 -lemma division_segment_numeral [simp]:
    2.45 -  "division_segment (numeral k) = 1"
    2.46 -  using division_segment_of_nat [of "numeral k"] by simp
    2.47 -
    2.48 -lemma euclidean_size_1 [simp]:
    2.49 -  "euclidean_size 1 = 1"
    2.50 -  using euclidean_size_of_nat [of 1] by simp
    2.51 -
    2.52 -lemma euclidean_size_numeral [simp]:
    2.53 -  "euclidean_size (numeral k) = numeral k"
    2.54 -  using euclidean_size_of_nat [of "numeral k"] by simp
    2.55 -
    2.56 -lemma of_nat_dvd_iff:
    2.57 -  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
    2.58 -proof (cases "m = 0")
    2.59 -  case True
    2.60 -  then show ?thesis
    2.61 -    by simp
    2.62 -next
    2.63 -  case False
    2.64 -  show ?thesis
    2.65 -  proof
    2.66 -    assume ?Q
    2.67 -    then show ?P
    2.68 -      by (auto elim: dvd_class.dvdE)
    2.69 -  next
    2.70 -    assume ?P
    2.71 -    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
    2.72 -      by simp
    2.73 -    then have "of_nat n = of_nat (n div m * m)"
    2.74 -      by (simp add: of_nat_div)
    2.75 -    then have "n = n div m * m"
    2.76 -      by (simp only: of_nat_eq_iff)
    2.77 -    then have "n = m * (n div m)"
    2.78 -      by (simp add: ac_simps)
    2.79 -    then show ?Q ..
    2.80 -  qed
    2.81 -qed
    2.82 -
    2.83 -lemma of_nat_mod:
    2.84 -  "of_nat (m mod n) = of_nat m mod of_nat n"
    2.85 -proof -
    2.86 -  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
    2.87 -    by (simp add: div_mult_mod_eq)
    2.88 -  also have "of_nat m = of_nat (m div n * n + m mod n)"
    2.89 -    by simp
    2.90 -  finally show ?thesis
    2.91 -    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
    2.92 -qed
    2.93 -
    2.94 -lemma one_div_two_eq_zero [simp]:
    2.95 -  "1 div 2 = 0"
    2.96 -proof -
    2.97 -  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
    2.98 -    by (simp only:) simp
    2.99 -  then show ?thesis
   2.100 -    by simp
   2.101 -qed
   2.102 -
   2.103 -lemma one_mod_two_eq_one [simp]:
   2.104 -  "1 mod 2 = 1"
   2.105 -proof -
   2.106 -  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
   2.107 -    by (simp only:) simp
   2.108 -  then show ?thesis
   2.109 -    by simp
   2.110 -qed
   2.111 -
   2.112  abbreviation even :: "'a \<Rightarrow> bool"
   2.113    where "even a \<equiv> 2 dvd a"
   2.114  
   2.115  abbreviation odd :: "'a \<Rightarrow> bool"
   2.116    where "odd a \<equiv> \<not> 2 dvd a"
   2.117  
   2.118 -lemma even_iff_mod_2_eq_zero:
   2.119 -  "even a \<longleftrightarrow> a mod 2 = 0"
   2.120 -  by (fact dvd_eq_mod_eq_0)
   2.121 -
   2.122 -lemma odd_iff_mod_2_eq_one:
   2.123 -  "odd a \<longleftrightarrow> a mod 2 = 1"
   2.124 -proof
   2.125 -  assume "a mod 2 = 1"
   2.126 -  then show "odd a"
   2.127 -    by auto
   2.128 -next
   2.129 -  assume "odd a"
   2.130 -  have eucl: "euclidean_size (a mod 2) = 1"
   2.131 -  proof (rule order_antisym)
   2.132 -    show "euclidean_size (a mod 2) \<le> 1"
   2.133 -      using mod_size_less [of 2 a] by simp
   2.134 -    show "1 \<le> euclidean_size (a mod 2)"
   2.135 -      using \<open>odd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
   2.136 -  qed 
   2.137 -  from \<open>odd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
   2.138 -    by simp
   2.139 -  then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
   2.140 -    by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
   2.141 -  then have "\<not> 2 dvd euclidean_size a"
   2.142 -    using of_nat_dvd_iff [of 2] by simp
   2.143 -  then have "euclidean_size a mod 2 = 1"
   2.144 -    by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
   2.145 -  then have "of_nat (euclidean_size a mod 2) = of_nat 1"
   2.146 -    by simp
   2.147 -  then have "of_nat (euclidean_size a) mod 2 = 1"
   2.148 -    by (simp add: of_nat_mod)
   2.149 -  from \<open>odd a\<close> eucl
   2.150 -  show "a mod 2 = 1"
   2.151 -    by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
   2.152 -qed
   2.153 -
   2.154 -lemma mod2_eq_if: "x mod 2 = (if even x then 0 else 1)"
   2.155 -by (simp add: odd_iff_mod_2_eq_one)
   2.156 -
   2.157  lemma parity_cases [case_names even odd]:
   2.158    assumes "even a \<Longrightarrow> a mod 2 = 0 \<Longrightarrow> P"
   2.159    assumes "odd a \<Longrightarrow> a mod 2 = 1 \<Longrightarrow> P"
   2.160    shows P
   2.161 -  using assms by (cases "even a") (simp_all add: odd_iff_mod_2_eq_one)
   2.162 +  using assms by (cases "even a")
   2.163 +    (simp_all add: even_iff_mod_2_eq_zero [symmetric] odd_iff_mod_2_eq_one [symmetric])
   2.164 +
   2.165 +lemma not_mod_2_eq_0_eq_1 [simp]:
   2.166 +  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   2.167 +  by (cases a rule: parity_cases) simp_all
   2.168  
   2.169  lemma not_mod_2_eq_1_eq_0 [simp]:
   2.170    "a mod 2 \<noteq> 1 \<longleftrightarrow> a mod 2 = 0"
   2.171    by (cases a rule: parity_cases) simp_all
   2.172  
   2.173 -lemma not_mod_2_eq_0_eq_1 [simp]:
   2.174 -  "a mod 2 \<noteq> 0 \<longleftrightarrow> a mod 2 = 1"
   2.175 -  by (cases a rule: parity_cases) simp_all
   2.176 +lemma mod2_eq_if: "a mod 2 = (if 2 dvd a then 0 else 1)"
   2.177 +  by (simp add: even_iff_mod_2_eq_zero odd_iff_mod_2_eq_one)
   2.178  
   2.179  lemma evenE [elim?]:
   2.180    assumes "even a"
   2.181 @@ -189,51 +59,16 @@
   2.182  
   2.183  lemma mod_2_eq_odd:
   2.184    "a mod 2 = of_bool (odd a)"
   2.185 -  by (auto elim: oddE)
   2.186 +  by (auto elim: oddE simp add: even_iff_mod_2_eq_zero)
   2.187  
   2.188  lemma of_bool_odd_eq_mod_2:
   2.189    "of_bool (odd a) = a mod 2"
   2.190    by (simp add: mod_2_eq_odd)
   2.191  
   2.192 -lemma one_mod_2_pow_eq [simp]:
   2.193 -  "1 mod (2 ^ n) = of_bool (n > 0)"
   2.194 -proof -
   2.195 -  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
   2.196 -    using of_nat_mod [of 1 "2 ^ n"] by simp
   2.197 -  also have "\<dots> = of_bool (n > 0)"
   2.198 -    by simp
   2.199 -  finally show ?thesis .
   2.200 -qed
   2.201 -
   2.202 -lemma one_div_2_pow_eq [simp]:
   2.203 -  "1 div (2 ^ n) = of_bool (n = 0)"
   2.204 -  using div_mult_mod_eq [of 1 "2 ^ n"] by auto
   2.205 -
   2.206 -lemma even_of_nat [simp]:
   2.207 -  "even (of_nat a) \<longleftrightarrow> even a"
   2.208 -proof -
   2.209 -  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
   2.210 -    by simp
   2.211 -  also have "\<dots> \<longleftrightarrow> even a"
   2.212 -    by (simp only: of_nat_dvd_iff)
   2.213 -  finally show ?thesis .
   2.214 -qed
   2.215 -
   2.216  lemma even_zero [simp]:
   2.217    "even 0"
   2.218    by (fact dvd_0_right)
   2.219  
   2.220 -lemma odd_one [simp]:
   2.221 -  "odd 1"
   2.222 -proof -
   2.223 -  have "\<not> (2 :: nat) dvd 1"
   2.224 -    by simp
   2.225 -  then have "\<not> of_nat 2 dvd of_nat 1"
   2.226 -    unfolding of_nat_dvd_iff by simp
   2.227 -  then show ?thesis
   2.228 -    by simp
   2.229 -qed
   2.230 -
   2.231  lemma odd_even_add:
   2.232    "even (a + b)" if "odd a" and "odd b"
   2.233  proof -
   2.234 @@ -311,6 +146,197 @@
   2.235  lemma even_power [simp]: "even (a ^ n) \<longleftrightarrow> even a \<and> n > 0"
   2.236    by (induct n) auto
   2.237  
   2.238 +end
   2.239 +
   2.240 +class ring_parity = ring + semiring_parity
   2.241 +begin
   2.242 +
   2.243 +subclass comm_ring_1 ..
   2.244 +
   2.245 +lemma even_minus:
   2.246 +  "even (- a) \<longleftrightarrow> even a"
   2.247 +  by (fact dvd_minus_iff)
   2.248 +
   2.249 +lemma even_diff [simp]:
   2.250 +  "even (a - b) \<longleftrightarrow> even (a + b)"
   2.251 +  using even_add [of a "- b"] by simp
   2.252 +
   2.253 +end
   2.254 +
   2.255 +
   2.256 +subsection \<open>Special case: euclidean rings containing the natural numbers\<close>
   2.257 +
   2.258 +class unique_euclidean_semiring_with_nat = semidom + semiring_char_0 + unique_euclidean_semiring +
   2.259 +  assumes of_nat_div: "of_nat (m div n) = of_nat m div of_nat n"
   2.260 +    and division_segment_of_nat [simp]: "division_segment (of_nat n) = 1"
   2.261 +    and division_segment_euclidean_size [simp]: "division_segment a * of_nat (euclidean_size a) = a"
   2.262 +begin
   2.263 +
   2.264 +lemma division_segment_eq_iff:
   2.265 +  "a = b" if "division_segment a = division_segment b"
   2.266 +    and "euclidean_size a = euclidean_size b"
   2.267 +  using that division_segment_euclidean_size [of a] by simp
   2.268 +
   2.269 +lemma euclidean_size_of_nat [simp]:
   2.270 +  "euclidean_size (of_nat n) = n"
   2.271 +proof -
   2.272 +  have "division_segment (of_nat n) * of_nat (euclidean_size (of_nat n)) = of_nat n"
   2.273 +    by (fact division_segment_euclidean_size)
   2.274 +  then show ?thesis by simp
   2.275 +qed
   2.276 +
   2.277 +lemma of_nat_euclidean_size:
   2.278 +  "of_nat (euclidean_size a) = a div division_segment a"
   2.279 +proof -
   2.280 +  have "of_nat (euclidean_size a) = division_segment a * of_nat (euclidean_size a) div division_segment a"
   2.281 +    by (subst nonzero_mult_div_cancel_left) simp_all
   2.282 +  also have "\<dots> = a div division_segment a"
   2.283 +    by simp
   2.284 +  finally show ?thesis .
   2.285 +qed
   2.286 +
   2.287 +lemma division_segment_1 [simp]:
   2.288 +  "division_segment 1 = 1"
   2.289 +  using division_segment_of_nat [of 1] by simp
   2.290 +
   2.291 +lemma division_segment_numeral [simp]:
   2.292 +  "division_segment (numeral k) = 1"
   2.293 +  using division_segment_of_nat [of "numeral k"] by simp
   2.294 +
   2.295 +lemma euclidean_size_1 [simp]:
   2.296 +  "euclidean_size 1 = 1"
   2.297 +  using euclidean_size_of_nat [of 1] by simp
   2.298 +
   2.299 +lemma euclidean_size_numeral [simp]:
   2.300 +  "euclidean_size (numeral k) = numeral k"
   2.301 +  using euclidean_size_of_nat [of "numeral k"] by simp
   2.302 +
   2.303 +lemma of_nat_dvd_iff:
   2.304 +  "of_nat m dvd of_nat n \<longleftrightarrow> m dvd n" (is "?P \<longleftrightarrow> ?Q")
   2.305 +proof (cases "m = 0")
   2.306 +  case True
   2.307 +  then show ?thesis
   2.308 +    by simp
   2.309 +next
   2.310 +  case False
   2.311 +  show ?thesis
   2.312 +  proof
   2.313 +    assume ?Q
   2.314 +    then show ?P
   2.315 +      by auto
   2.316 +  next
   2.317 +    assume ?P
   2.318 +    with False have "of_nat n = of_nat n div of_nat m * of_nat m"
   2.319 +      by simp
   2.320 +    then have "of_nat n = of_nat (n div m * m)"
   2.321 +      by (simp add: of_nat_div)
   2.322 +    then have "n = n div m * m"
   2.323 +      by (simp only: of_nat_eq_iff)
   2.324 +    then have "n = m * (n div m)"
   2.325 +      by (simp add: ac_simps)
   2.326 +    then show ?Q ..
   2.327 +  qed
   2.328 +qed
   2.329 +
   2.330 +lemma of_nat_mod:
   2.331 +  "of_nat (m mod n) = of_nat m mod of_nat n"
   2.332 +proof -
   2.333 +  have "of_nat m div of_nat n * of_nat n + of_nat m mod of_nat n = of_nat m"
   2.334 +    by (simp add: div_mult_mod_eq)
   2.335 +  also have "of_nat m = of_nat (m div n * n + m mod n)"
   2.336 +    by simp
   2.337 +  finally show ?thesis
   2.338 +    by (simp only: of_nat_div of_nat_mult of_nat_add) simp
   2.339 +qed
   2.340 +
   2.341 +lemma one_div_two_eq_zero [simp]:
   2.342 +  "1 div 2 = 0"
   2.343 +proof -
   2.344 +  from of_nat_div [symmetric] have "of_nat 1 div of_nat 2 = of_nat 0"
   2.345 +    by (simp only:) simp
   2.346 +  then show ?thesis
   2.347 +    by simp
   2.348 +qed
   2.349 +
   2.350 +lemma one_mod_two_eq_one [simp]:
   2.351 +  "1 mod 2 = 1"
   2.352 +proof -
   2.353 +  from of_nat_mod [symmetric] have "of_nat 1 mod of_nat 2 = of_nat 1"
   2.354 +    by (simp only:) simp
   2.355 +  then show ?thesis
   2.356 +    by simp
   2.357 +qed
   2.358 +
   2.359 +subclass semiring_parity
   2.360 +proof
   2.361 +  show "2 dvd a \<longleftrightarrow> a mod 2 = 0" for a
   2.362 +    by (fact dvd_eq_mod_eq_0)
   2.363 +  show "\<not> 2 dvd a \<longleftrightarrow> a mod 2 = 1" for a
   2.364 +  proof
   2.365 +    assume "a mod 2 = 1"
   2.366 +    then show "\<not> 2 dvd a"
   2.367 +      by auto
   2.368 +  next
   2.369 +    assume "\<not> 2 dvd a"
   2.370 +    have eucl: "euclidean_size (a mod 2) = 1"
   2.371 +    proof (rule order_antisym)
   2.372 +      show "euclidean_size (a mod 2) \<le> 1"
   2.373 +        using mod_size_less [of 2 a] by simp
   2.374 +      show "1 \<le> euclidean_size (a mod 2)"
   2.375 +        using \<open>\<not> 2 dvd a\<close> by (simp add: Suc_le_eq dvd_eq_mod_eq_0)
   2.376 +    qed 
   2.377 +    from \<open>\<not> 2 dvd a\<close> have "\<not> of_nat 2 dvd division_segment a * of_nat (euclidean_size a)"
   2.378 +      by simp
   2.379 +    then have "\<not> of_nat 2 dvd of_nat (euclidean_size a)"
   2.380 +      by (auto simp only: dvd_mult_unit_iff' is_unit_division_segment)
   2.381 +    then have "\<not> 2 dvd euclidean_size a"
   2.382 +      using of_nat_dvd_iff [of 2] by simp
   2.383 +    then have "euclidean_size a mod 2 = 1"
   2.384 +      by (simp add: semidom_modulo_class.dvd_eq_mod_eq_0)
   2.385 +    then have "of_nat (euclidean_size a mod 2) = of_nat 1"
   2.386 +      by simp
   2.387 +    then have "of_nat (euclidean_size a) mod 2 = 1"
   2.388 +      by (simp add: of_nat_mod)
   2.389 +    from \<open>\<not> 2 dvd a\<close> eucl
   2.390 +    show "a mod 2 = 1"
   2.391 +      by (auto intro: division_segment_eq_iff simp add: division_segment_mod)
   2.392 +  qed
   2.393 +  show "\<not> is_unit 2"
   2.394 +  proof (rule notI)
   2.395 +    assume "is_unit 2"
   2.396 +    then have "of_nat 2 dvd of_nat 1"
   2.397 +      by simp
   2.398 +    then have "is_unit (2::nat)"
   2.399 +      by (simp only: of_nat_dvd_iff)
   2.400 +    then show False
   2.401 +      by simp
   2.402 +  qed
   2.403 +qed
   2.404 +
   2.405 +lemma even_of_nat [simp]:
   2.406 +  "even (of_nat a) \<longleftrightarrow> even a"
   2.407 +proof -
   2.408 +  have "even (of_nat a) \<longleftrightarrow> of_nat 2 dvd of_nat a"
   2.409 +    by simp
   2.410 +  also have "\<dots> \<longleftrightarrow> even a"
   2.411 +    by (simp only: of_nat_dvd_iff)
   2.412 +  finally show ?thesis .
   2.413 +qed
   2.414 +
   2.415 +lemma one_mod_2_pow_eq [simp]:
   2.416 +  "1 mod (2 ^ n) = of_bool (n > 0)"
   2.417 +proof -
   2.418 +  have "1 mod (2 ^ n) = of_nat (1 mod (2 ^ n))"
   2.419 +    using of_nat_mod [of 1 "2 ^ n"] by simp
   2.420 +  also have "\<dots> = of_bool (n > 0)"
   2.421 +    by simp
   2.422 +  finally show ?thesis .
   2.423 +qed
   2.424 +
   2.425 +lemma one_div_2_pow_eq [simp]:
   2.426 +  "1 div (2 ^ n) = of_bool (n = 0)"
   2.427 +  using div_mult_mod_eq [of 1 "2 ^ n"] by auto
   2.428 +
   2.429  lemma even_succ_div_two [simp]:
   2.430    "even a \<Longrightarrow> (a + 1) div 2 = a div 2"
   2.431    by (cases "a = 0") (auto elim!: evenE dest: mult_not_zero)
   2.432 @@ -427,15 +453,7 @@
   2.433  class unique_euclidean_ring_with_nat = ring + unique_euclidean_semiring_with_nat
   2.434  begin
   2.435  
   2.436 -subclass comm_ring_1 ..
   2.437 -
   2.438 -lemma even_minus:
   2.439 -  "even (- a) \<longleftrightarrow> even a"
   2.440 -  by (fact dvd_minus_iff)
   2.441 -
   2.442 -lemma even_diff [simp]:
   2.443 -  "even (a - b) \<longleftrightarrow> even (a + b)"
   2.444 -  using even_add [of a "- b"] by simp
   2.445 +subclass ring_parity ..
   2.446  
   2.447  lemma minus_1_mod_2_eq [simp]:
   2.448    "- 1 mod 2 = 1"
   2.449 @@ -446,7 +464,7 @@
   2.450  proof -
   2.451    from div_mult_mod_eq [of "- 1" 2]
   2.452    have "- 1 div 2 * 2 = - 1 * 2"
   2.453 -    using local.add_implies_diff by fastforce
   2.454 +    using add_implies_diff by fastforce
   2.455    then show ?thesis
   2.456      using mult_right_cancel [of 2 "- 1 div 2" "- 1"] by simp
   2.457  qed
   2.458 @@ -519,6 +537,10 @@
   2.459      by simp
   2.460  qed
   2.461  
   2.462 +lemma not_mod2_eq_Suc_0_eq_0 [simp]:
   2.463 +  "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
   2.464 +  using not_mod_2_eq_1_eq_0 [of n] by simp
   2.465 +
   2.466  lemma nat_parity_induct [case_names zero even odd]:
   2.467    "P n" if zero: "P 0"
   2.468      and even: "\<And>n. P n \<Longrightarrow> n > 0 \<Longrightarrow> P (2 * n)"
   2.469 @@ -548,10 +570,6 @@
   2.470    qed
   2.471  qed
   2.472  
   2.473 -lemma not_mod2_eq_Suc_0_eq_0 [simp]:
   2.474 -  "n mod 2 \<noteq> Suc 0 \<longleftrightarrow> n mod 2 = 0"
   2.475 -  using not_mod_2_eq_1_eq_0 [of n] by simp
   2.476 -
   2.477  lemma odd_card_imp_not_empty:
   2.478    \<open>A \<noteq> {}\<close> if \<open>odd (card A)\<close>
   2.479    using that by auto
   2.480 @@ -762,7 +780,7 @@
   2.481  
   2.482  subsection \<open>Abstract bit operations\<close>
   2.483  
   2.484 -context unique_euclidean_semiring_with_nat
   2.485 +context semiring_parity
   2.486  begin
   2.487  
   2.488  text \<open>The primary purpose of the following operations is
   2.489 @@ -777,6 +795,11 @@
   2.490  definition drop_bit :: "nat \<Rightarrow> 'a \<Rightarrow> 'a"
   2.491    where drop_bit_eq_div: "drop_bit n a = a div 2 ^ n"
   2.492  
   2.493 +end
   2.494 +
   2.495 +context unique_euclidean_semiring_with_nat
   2.496 +begin
   2.497 +
   2.498  lemma bit_ident:
   2.499    "push_bit n (drop_bit n a) + take_bit n a = a"
   2.500    using div_mult_mod_eq by (simp add: push_bit_eq_mult take_bit_eq_mod drop_bit_eq_div)
     3.1 --- a/src/HOL/Presburger.thy	Fri Jun 14 08:34:27 2019 +0000
     3.2 +++ b/src/HOL/Presburger.thy	Fri Jun 14 08:34:27 2019 +0000
     3.3 @@ -432,7 +432,7 @@
     3.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     3.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     3.6  
     3.7 -context unique_euclidean_semiring_with_nat
     3.8 +context semiring_parity
     3.9  begin
    3.10  
    3.11  declare even_mult_iff [presburger]
    3.12 @@ -445,7 +445,7 @@
    3.13  
    3.14  end
    3.15  
    3.16 -context unique_euclidean_ring_with_nat
    3.17 +context ring_parity
    3.18  begin
    3.19  
    3.20  declare even_minus [presburger]