crossproduct coprimality lemmas
authorhaftmann
Wed Feb 24 14:19:53 2010 +0100 (2010-02-24)
changeset 3536819b340c3f1ff
parent 35367 45a193f0ed0c
child 35369 e4a7947e02b8
crossproduct coprimality lemmas
src/HOL/GCD.thy
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 24 14:19:53 2010 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 24 14:19:53 2010 +0100
     1.3 @@ -412,6 +412,33 @@
     1.4  apply (rule gcd_mult_cancel_nat [transferred], auto)
     1.5  done
     1.6  
     1.7 +lemma coprime_crossproduct_nat:
     1.8 +  fixes a b c d :: nat
     1.9 +  assumes "coprime a d" and "coprime b c"
    1.10 +  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")
    1.11 +proof
    1.12 +  assume ?rhs then show ?lhs by simp
    1.13 +next
    1.14 +  assume ?lhs
    1.15 +  from `?lhs` have "a dvd b * d" by (auto intro: dvdI dest: sym)
    1.16 +  with `coprime a d` have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
    1.17 +  from `?lhs` have "b dvd a * c" by (auto intro: dvdI dest: sym)
    1.18 +  with `coprime b c` have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
    1.19 +  from `?lhs` have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult_commute)
    1.20 +  with `coprime b c` have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
    1.21 +  from `?lhs` have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult_commute)
    1.22 +  with `coprime a d` have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
    1.23 +  from `a dvd b` `b dvd a` have "a = b" by (rule Nat.dvd.antisym)
    1.24 +  moreover from `c dvd d` `d dvd c` have "c = d" by (rule Nat.dvd.antisym)
    1.25 +  ultimately show ?rhs ..
    1.26 +qed
    1.27 +
    1.28 +lemma coprime_crossproduct_int:
    1.29 +  fixes a b c d :: int
    1.30 +  assumes "coprime a d" and "coprime b c"
    1.31 +  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
    1.32 +  using assms by (intro coprime_crossproduct_nat [transferred]) auto
    1.33 +
    1.34  text {* \medskip Addition laws *}
    1.35  
    1.36  lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"