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