src/HOL/Rings.thy
changeset 67051 e7e54a0b9197
parent 66937 a1a4a5e2933a
child 67084 e138d96ed083
     1.1 --- a/src/HOL/Rings.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Rings.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -1161,6 +1161,108 @@
     1.4    "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
     1.5    by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
     1.6  
     1.7 +
     1.8 +text \<open>Coprimality\<close>
     1.9 +
    1.10 +definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    1.11 +  where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)"
    1.12 +
    1.13 +lemma coprimeI:
    1.14 +  assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c"
    1.15 +  shows "coprime a b"
    1.16 +  using assms by (auto simp: coprime_def)
    1.17 +
    1.18 +lemma not_coprimeI:
    1.19 +  assumes "c dvd a" and "c dvd b" and "\<not> is_unit c"
    1.20 +  shows "\<not> coprime a b"
    1.21 +  using assms by (auto simp: coprime_def)
    1.22 +
    1.23 +lemma coprime_common_divisor:
    1.24 +  "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
    1.25 +  using that by (auto simp: coprime_def)
    1.26 +
    1.27 +lemma not_coprimeE:
    1.28 +  assumes "\<not> coprime a b"
    1.29 +  obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c"
    1.30 +  using assms by (auto simp: coprime_def)
    1.31 +
    1.32 +lemma coprime_imp_coprime:
    1.33 +  "coprime a b" if "coprime c d"
    1.34 +    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c"
    1.35 +    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d"
    1.36 +proof (rule coprimeI)
    1.37 +  fix e
    1.38 +  assume "e dvd a" and "e dvd b"
    1.39 +  with that have "e dvd c" and "e dvd d"
    1.40 +    by (auto intro: dvd_trans)
    1.41 +  with \<open>coprime c d\<close> show "is_unit e"
    1.42 +    by (rule coprime_common_divisor)
    1.43 +qed
    1.44 +
    1.45 +lemma coprime_divisors:
    1.46 +  "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
    1.47 +using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
    1.48 +  fix e
    1.49 +  assume "e dvd a" then show "e dvd c"
    1.50 +    using \<open>a dvd c\<close> by (rule dvd_trans)
    1.51 +  assume "e dvd b" then show "e dvd d"
    1.52 +    using \<open>b dvd d\<close> by (rule dvd_trans)
    1.53 +qed
    1.54 +
    1.55 +lemma coprime_self [simp]:
    1.56 +  "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
    1.57 +proof
    1.58 +  assume ?P
    1.59 +  then show ?Q
    1.60 +    by (rule coprime_common_divisor) simp_all
    1.61 +next
    1.62 +  assume ?Q
    1.63 +  show ?P
    1.64 +    by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
    1.65 +qed
    1.66 +
    1.67 +lemma coprime_commute [ac_simps]:
    1.68 +  "coprime b a \<longleftrightarrow> coprime a b"
    1.69 +  unfolding coprime_def by auto
    1.70 +
    1.71 +lemma is_unit_left_imp_coprime:
    1.72 +  "coprime a b" if "is_unit a"
    1.73 +proof (rule coprimeI)
    1.74 +  fix c
    1.75 +  assume "c dvd a"
    1.76 +  with that show "is_unit c"
    1.77 +    by (auto intro: dvd_unit_imp_unit)
    1.78 +qed
    1.79 +
    1.80 +lemma is_unit_right_imp_coprime:
    1.81 +  "coprime a b" if "is_unit b"
    1.82 +  using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)
    1.83 +
    1.84 +lemma coprime_1_left [simp]:
    1.85 +  "coprime 1 a"
    1.86 +  by (rule coprimeI)
    1.87 +
    1.88 +lemma coprime_1_right [simp]:
    1.89 +  "coprime a 1"
    1.90 +  by (rule coprimeI)
    1.91 +
    1.92 +lemma coprime_0_left_iff [simp]:
    1.93 +  "coprime 0 a \<longleftrightarrow> is_unit a"
    1.94 +  by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])
    1.95 +
    1.96 +lemma coprime_0_right_iff [simp]:
    1.97 +  "coprime a 0 \<longleftrightarrow> is_unit a"
    1.98 +  using coprime_0_left_iff [of a] by (simp add: ac_simps)
    1.99 +
   1.100 +lemma coprime_mult_self_left_iff [simp]:
   1.101 +  "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b"
   1.102 +  by (auto intro: coprime_common_divisor)
   1.103 +    (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+
   1.104 +
   1.105 +lemma coprime_mult_self_right_iff [simp]:
   1.106 +  "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
   1.107 +  using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
   1.108 +
   1.109  end
   1.110  
   1.111  class unit_factor =
   1.112 @@ -1430,6 +1532,14 @@
   1.113    shows "is_unit a \<longleftrightarrow> a = 1"
   1.114    using assms by (cases "a = 0") (auto dest: is_unit_normalize)
   1.115  
   1.116 +lemma coprime_normalize_left_iff [simp]:
   1.117 +  "coprime (normalize a) b \<longleftrightarrow> coprime a b"
   1.118 +  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
   1.119 +
   1.120 +lemma coprime_normalize_right_iff [simp]:
   1.121 +  "coprime a (normalize b) \<longleftrightarrow> coprime a b"
   1.122 +  using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)
   1.123 +
   1.124  text \<open>
   1.125    We avoid an explicit definition of associated elements but prefer explicit
   1.126    normalisation instead. In theory we could define an abbreviation like @{prop
   1.127 @@ -2435,8 +2545,8 @@
   1.128  subclass ordered_ring_abs
   1.129    by standard (auto simp: abs_if not_less mult_less_0_iff)
   1.130  
   1.131 -lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   1.132 -  by (simp add: abs_if)
   1.133 +lemma abs_mult_self: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
   1.134 +  by (fact abs_mult_self_eq)
   1.135  
   1.136  lemma abs_mult_less:
   1.137    assumes ac: "\<bar>a\<bar> < c"