src/HOL/Euclidean_Division.thy
changeset 67051 e7e54a0b9197
parent 66886 960509bfd47e
child 67083 6b2c0681ef28
     1.1 --- a/src/HOL/Euclidean_Division.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Euclidean_Division.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -125,6 +125,15 @@
     1.4    "a mod b = 0" if "is_unit b"
     1.5    using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
     1.6  
     1.7 +lemma coprime_mod_left_iff [simp]:
     1.8 +  "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
     1.9 +  by (rule; rule coprimeI)
    1.10 +    (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
    1.11 +
    1.12 +lemma coprime_mod_right_iff [simp]:
    1.13 +  "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0"
    1.14 +  using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)
    1.15 +
    1.16  end
    1.17  
    1.18  class euclidean_ring = idom_modulo + euclidean_semiring
    1.19 @@ -533,6 +542,10 @@
    1.20    with that show thesis .
    1.21  qed
    1.22  
    1.23 +lemma invertible_coprime:
    1.24 +  "coprime a c" if "a * b mod c = 1"
    1.25 +  by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)
    1.26 +
    1.27  end
    1.28  
    1.29    
    1.30 @@ -772,6 +785,18 @@
    1.31  
    1.32  end
    1.33  
    1.34 +lemma coprime_Suc_0_left [simp]:
    1.35 +  "coprime (Suc 0) n"
    1.36 +  using coprime_1_left [of n] by simp
    1.37 +
    1.38 +lemma coprime_Suc_0_right [simp]:
    1.39 +  "coprime n (Suc 0)"
    1.40 +  using coprime_1_right [of n] by simp
    1.41 +
    1.42 +lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
    1.43 +  for a b :: nat
    1.44 +  by (drule coprime_common_divisor [of _ _ x]) simp_all
    1.45 +
    1.46  instantiation nat :: unique_euclidean_semiring
    1.47  begin
    1.48  
    1.49 @@ -1422,6 +1447,64 @@
    1.50  
    1.51  end
    1.52  
    1.53 +lemma coprime_int_iff [simp]:
    1.54 +  "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
    1.55 +proof
    1.56 +  assume ?P
    1.57 +  show ?Q
    1.58 +  proof (rule coprimeI)
    1.59 +    fix q
    1.60 +    assume "q dvd m" "q dvd n"
    1.61 +    then have "int q dvd int m" "int q dvd int n"
    1.62 +      by (simp_all add: zdvd_int)
    1.63 +    with \<open>?P\<close> have "is_unit (int q)"
    1.64 +      by (rule coprime_common_divisor)
    1.65 +    then show "is_unit q"
    1.66 +      by simp
    1.67 +  qed
    1.68 +next
    1.69 +  assume ?Q
    1.70 +  show ?P
    1.71 +  proof (rule coprimeI)
    1.72 +    fix k
    1.73 +    assume "k dvd int m" "k dvd int n"
    1.74 +    then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
    1.75 +      by (simp_all add: zdvd_int)
    1.76 +    with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
    1.77 +      by (rule coprime_common_divisor)
    1.78 +    then show "is_unit k"
    1.79 +      by simp
    1.80 +  qed
    1.81 +qed
    1.82 +
    1.83 +lemma coprime_abs_left_iff [simp]:
    1.84 +  "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int
    1.85 +  using coprime_normalize_left_iff [of k l] by simp
    1.86 +
    1.87 +lemma coprime_abs_right_iff [simp]:
    1.88 +  "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int
    1.89 +  using coprime_abs_left_iff [of l k] by (simp add: ac_simps)
    1.90 +
    1.91 +lemma coprime_nat_abs_left_iff [simp]:
    1.92 +  "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)"
    1.93 +proof -
    1.94 +  define m where "m = nat \<bar>k\<bar>"
    1.95 +  then have "\<bar>k\<bar> = int m"
    1.96 +    by simp
    1.97 +  moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)"
    1.98 +    by simp
    1.99 +  ultimately show ?thesis
   1.100 +    by simp
   1.101 +qed
   1.102 +
   1.103 +lemma coprime_nat_abs_right_iff [simp]:
   1.104 +  "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k"
   1.105 +  using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)
   1.106 +
   1.107 +lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   1.108 +  for a b :: int
   1.109 +  by (drule coprime_common_divisor [of _ _ x]) simp_all
   1.110 +
   1.111  instantiation int :: idom_modulo
   1.112  begin
   1.113