src/HOL/Parity.thy
 changeset 67051 e7e54a0b9197 parent 66840 0d689d71dbdc child 67083 6b2c0681ef28
```     1.1 --- a/src/HOL/Parity.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Parity.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -318,6 +318,38 @@
1.4    using mult_div_mod_eq [of 2 a]
1.5    by (simp add: even_iff_mod_2_eq_zero)
1.6
1.7 +lemma coprime_left_2_iff_odd [simp]:
1.8 +  "coprime 2 a \<longleftrightarrow> odd a"
1.9 +proof
1.10 +  assume "odd a"
1.11 +  show "coprime 2 a"
1.12 +  proof (rule coprimeI)
1.13 +    fix b
1.14 +    assume "b dvd 2" "b dvd a"
1.15 +    then have "b dvd a mod 2"
1.16 +      by (auto intro: dvd_mod)
1.17 +    with \<open>odd a\<close> show "is_unit b"
1.18 +      by (simp add: mod_2_eq_odd)
1.19 +  qed
1.20 +next
1.21 +  assume "coprime 2 a"
1.22 +  show "odd a"
1.23 +  proof (rule notI)
1.24 +    assume "even a"
1.25 +    then obtain b where "a = 2 * b" ..
1.26 +    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
1.27 +      by simp
1.28 +    moreover have "\<not> coprime 2 (2 * b)"
1.29 +      by (rule not_coprimeI [of 2]) simp_all
1.30 +    ultimately show False
1.31 +      by blast
1.32 +  qed
1.33 +qed
1.34 +
1.35 +lemma coprime_right_2_iff_odd [simp]:
1.36 +  "coprime a 2 \<longleftrightarrow> odd a"
1.37 +  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
1.38 +
1.39  end
1.40
1.41  class ring_parity = ring + semiring_parity
```