src/HOL/GCD.thy
changeset 62344 759d684c0e60
parent 62343 24106dc44def
child 62345 e66d7841d5a2
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -668,14 +668,6 @@
     1.4  lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
     1.5    by (simp add: gcd_int_def)
     1.6  
     1.7 -lemma gcd_neg_numeral_1_int [simp]:
     1.8 -  "gcd (- numeral n :: int) x = gcd (numeral n) x"
     1.9 -  by (fact gcd_neg1_int)
    1.10 -
    1.11 -lemma gcd_neg_numeral_2_int [simp]:
    1.12 -  "gcd x (- numeral n :: int) = gcd x (numeral n)"
    1.13 -  by (fact gcd_neg2_int)
    1.14 -
    1.15  lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    1.16  by(simp add: gcd_int_def)
    1.17  
    1.18 @@ -822,27 +814,11 @@
    1.19  lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
    1.20    by (rule zdvd_imp_le, auto)
    1.21  
    1.22 -lemma gcd_greatest_iff_nat:
    1.23 -  "(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)"
    1.24 -  by (fact gcd_greatest_iff)
    1.25 -
    1.26 -lemma gcd_greatest_iff_int:
    1.27 -  "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
    1.28 -  by (fact gcd_greatest_iff)
    1.29 -
    1.30 -lemma gcd_zero_nat: 
    1.31 -  "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
    1.32 -  by (fact gcd_eq_0_iff)
    1.33 -
    1.34 -lemma gcd_zero_int [simp]:
    1.35 -  "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
    1.36 -  by (fact gcd_eq_0_iff)
    1.37 -
    1.38  lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
    1.39 -  by (insert gcd_zero_nat [of m n], arith)
    1.40 +  by (insert gcd_eq_0_iff [of m n], arith)
    1.41  
    1.42  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
    1.43 -  by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
    1.44 +  by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
    1.45  
    1.46  lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
    1.47      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    1.48 @@ -862,31 +838,14 @@
    1.49  done
    1.50  
    1.51  interpretation gcd_nat:
    1.52 -  semilattice_neutr_order gcd "0::nat" Rings.dvd "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
    1.53 -  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd.antisym dvd_trans)
    1.54 -
    1.55 -lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
    1.56 -lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
    1.57 -lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
    1.58 -lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
    1.59 -lemmas gcd_commute_int = gcd.commute [where ?'a = int]
    1.60 -lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
    1.61 -
    1.62 -lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    1.63 -
    1.64 -lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    1.65 -
    1.66 -lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
    1.67 -  by (fact gcd_nat.absorb1)
    1.68 -
    1.69 -lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
    1.70 -  by (fact gcd_nat.absorb2)
    1.71 +  semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
    1.72 +  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
    1.73  
    1.74  lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
    1.75    by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
    1.76  
    1.77  lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
    1.78 -  by (metis gcd_proj1_if_dvd_int gcd_commute_int)
    1.79 +  by (metis gcd_proj1_if_dvd_int gcd.commute)
    1.80  
    1.81  text \<open>
    1.82    \medskip Multiplication laws
    1.83 @@ -926,21 +885,10 @@
    1.84    ultimately show ?thesis by simp
    1.85  qed
    1.86  
    1.87 -end
    1.88 -
    1.89 -lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
    1.90 -lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
    1.91 -
    1.92 -lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
    1.93 -    (k dvd m * n) = (k dvd m)"
    1.94 -  by (auto intro: coprime_dvd_mult_nat)
    1.95 -
    1.96 -lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
    1.97 -    (k dvd m * n) = (k dvd m)"
    1.98 -  by (auto intro: coprime_dvd_mult_int)
    1.99 -
   1.100 -context semiring_gcd
   1.101 -begin
   1.102 +lemma coprime_dvd_mult_iff:
   1.103 +  assumes "coprime a c"
   1.104 +  shows "a dvd b * c \<longleftrightarrow> a dvd b"
   1.105 +  using assms by (auto intro: coprime_dvd_mult)
   1.106  
   1.107  lemma gcd_mult_cancel:
   1.108    "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   1.109 @@ -951,65 +899,79 @@
   1.110    apply (simp_all add: ac_simps)
   1.111    done
   1.112  
   1.113 -end  
   1.114 -
   1.115 -lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
   1.116 -lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
   1.117 -
   1.118 -lemma coprime_crossproduct_nat:
   1.119 -  fixes a b c d :: nat
   1.120 +lemma coprime_crossproduct:
   1.121 +  fixes a b c d
   1.122    assumes "coprime a d" and "coprime b c"
   1.123 -  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")
   1.124 +  shows "normalize a * normalize c = normalize b * normalize d
   1.125 +    \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
   1.126  proof
   1.127    assume ?rhs then show ?lhs by simp
   1.128  next
   1.129    assume ?lhs
   1.130 -  from \<open>?lhs\<close> have "a dvd b * d" by (auto intro: dvdI dest: sym)
   1.131 -  with \<open>coprime a d\<close> have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
   1.132 -  from \<open>?lhs\<close> have "b dvd a * c" by (auto intro: dvdI dest: sym)
   1.133 -  with \<open>coprime b c\<close> have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
   1.134 -  from \<open>?lhs\<close> have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.135 -  with \<open>coprime b c\<close> have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   1.136 -  from \<open>?lhs\<close> have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.137 -  with \<open>coprime a d\<close> have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   1.138 -  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "a = b" by (rule Nat.dvd.antisym)
   1.139 -  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "c = d" by (rule Nat.dvd.antisym)
   1.140 +  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   1.141 +    by (auto intro: dvdI dest: sym)
   1.142 +  with \<open>coprime a d\<close> have "a dvd b"
   1.143 +    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.144 +  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   1.145 +    by (auto intro: dvdI dest: sym)
   1.146 +  with \<open>coprime b c\<close> have "b dvd a"
   1.147 +    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   1.148 +  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   1.149 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.150 +  with \<open>coprime b c\<close> have "c dvd d"
   1.151 +    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.152 +  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   1.153 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   1.154 +  with \<open>coprime a d\<close> have "d dvd c"
   1.155 +    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   1.156 +  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   1.157 +    by (rule associatedI)
   1.158 +  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   1.159 +    by (rule associatedI)
   1.160    ultimately show ?rhs ..
   1.161  qed
   1.162  
   1.163 +end
   1.164 +
   1.165 +lemma coprime_crossproduct_nat:
   1.166 +  fixes a b c d :: nat
   1.167 +  assumes "coprime a d" and "coprime b c"
   1.168 +  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
   1.169 +  using assms coprime_crossproduct [of a d b c] by simp
   1.170 +
   1.171  lemma coprime_crossproduct_int:
   1.172    fixes a b c d :: int
   1.173    assumes "coprime a d" and "coprime b c"
   1.174    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.175 -  using assms by (intro coprime_crossproduct_nat [transferred]) auto
   1.176 +  using assms coprime_crossproduct [of a d b c] by simp
   1.177  
   1.178  text \<open>\medskip Addition laws\<close>
   1.179  
   1.180  lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   1.181    apply (case_tac "n = 0")
   1.182    apply (simp_all add: gcd_non_0_nat)
   1.183 -done
   1.184 +  done
   1.185  
   1.186  lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   1.187 -  apply (subst (1 2) gcd_commute_nat)
   1.188 +  apply (subst (1 2) gcd.commute)
   1.189    apply (subst add.commute)
   1.190    apply simp
   1.191 -done
   1.192 +  done
   1.193  
   1.194  (* to do: add the other variations? *)
   1.195  
   1.196  lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   1.197 -  by (subst gcd_add1_nat [symmetric], auto)
   1.198 +  by (subst gcd_add1_nat [symmetric]) auto
   1.199  
   1.200  lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   1.201 -  apply (subst gcd_commute_nat)
   1.202 +  apply (subst gcd.commute)
   1.203    apply (subst gcd_diff1_nat [symmetric])
   1.204    apply auto
   1.205 -  apply (subst gcd_commute_nat)
   1.206 +  apply (subst gcd.commute)
   1.207    apply (subst gcd_diff1_nat)
   1.208    apply assumption
   1.209 -  apply (rule gcd_commute_nat)
   1.210 -done
   1.211 +  apply (rule gcd.commute)
   1.212 +  done
   1.213  
   1.214  lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   1.215    apply (frule_tac b = y and a = x in pos_mod_sign)
   1.216 @@ -1017,10 +979,10 @@
   1.217    apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   1.218      zmod_zminus1_eq_if)
   1.219    apply (frule_tac a = x in pos_mod_bound)
   1.220 -  apply (subst (1 2) gcd_commute_nat)
   1.221 +  apply (subst (1 2) gcd.commute)
   1.222    apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   1.223      nat_le_eq_zle)
   1.224 -done
   1.225 +  done
   1.226  
   1.227  lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   1.228    apply (case_tac "y = 0")
   1.229 @@ -1035,13 +997,13 @@
   1.230  by (metis gcd_red_int mod_add_self1 add.commute)
   1.231  
   1.232  lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   1.233 -by (metis gcd_add1_int gcd_commute_int add.commute)
   1.234 +by (metis gcd_add1_int gcd.commute add.commute)
   1.235  
   1.236  lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   1.237 -by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   1.238 +by (metis mod_mult_self3 gcd.commute gcd_red_nat)
   1.239  
   1.240  lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   1.241 -by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute)
   1.242 +by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute)
   1.243  
   1.244  
   1.245  (* to do: differences, and all variations of addition rules
   1.246 @@ -1087,7 +1049,7 @@
   1.247  apply(rule Max_eqI[THEN sym])
   1.248    apply (metis finite_Collect_conjI finite_divisors_nat)
   1.249   apply simp
   1.250 - apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   1.251 + apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
   1.252  apply simp
   1.253  done
   1.254  
   1.255 @@ -1096,7 +1058,7 @@
   1.256  apply(rule Max_eqI[THEN sym])
   1.257    apply (metis finite_Collect_conjI finite_divisors_int)
   1.258   apply simp
   1.259 - apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   1.260 + apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
   1.261  apply simp
   1.262  done
   1.263  
   1.264 @@ -1136,9 +1098,6 @@
   1.265  
   1.266  end
   1.267  
   1.268 -lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
   1.269 -lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
   1.270 -
   1.271  lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   1.272    using gcd_unique_nat[of 1 a b, simplified] by auto
   1.273  
   1.274 @@ -1165,7 +1124,7 @@
   1.275    apply (erule ssubst)
   1.276    apply (subgoal_tac "b' = b div gcd a b")
   1.277    apply (erule ssubst)
   1.278 -  apply (rule div_gcd_coprime_nat)
   1.279 +  apply (rule div_gcd_coprime)
   1.280    using z apply force
   1.281    apply (subst (1) b)
   1.282    using z apply force
   1.283 @@ -1182,7 +1141,7 @@
   1.284    apply (erule ssubst)
   1.285    apply (subgoal_tac "b' = b div gcd a b")
   1.286    apply (erule ssubst)
   1.287 -  apply (rule div_gcd_coprime_int)
   1.288 +  apply (rule div_gcd_coprime)
   1.289    using z apply force
   1.290    apply (subst (1) b)
   1.291    using z apply force
   1.292 @@ -1204,9 +1163,6 @@
   1.293  
   1.294  end
   1.295  
   1.296 -lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
   1.297 -lemmas coprime_mult_int = coprime_mult [where ?'a = int]
   1.298 -  
   1.299  lemma coprime_lmult_nat:
   1.300    assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   1.301  proof -
   1.302 @@ -1246,13 +1202,13 @@
   1.303  lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   1.304      coprime d a \<and>  coprime d b"
   1.305    using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   1.306 -    coprime_mult_nat[of d a b]
   1.307 +    coprime_mult [of d a b]
   1.308    by blast
   1.309  
   1.310  lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   1.311      coprime d a \<and>  coprime d b"
   1.312    using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   1.313 -    coprime_mult_int[of d a b]
   1.314 +    coprime_mult [of d a b]
   1.315    by blast
   1.316  
   1.317  lemma coprime_power_int:
   1.318 @@ -1268,7 +1224,7 @@
   1.319      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.320    apply (rule_tac x = "a div gcd a b" in exI)
   1.321    apply (rule_tac x = "b div gcd a b" in exI)
   1.322 -  using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   1.323 +  using nz apply (auto simp add: div_gcd_coprime dvd_div_mult)
   1.324  done
   1.325  
   1.326  lemma gcd_coprime_exists_int:
   1.327 @@ -1276,14 +1232,14 @@
   1.328      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   1.329    apply (rule_tac x = "a div gcd a b" in exI)
   1.330    apply (rule_tac x = "b div gcd a b" in exI)
   1.331 -  using nz apply (auto simp add: div_gcd_coprime_int)
   1.332 +  using nz apply (auto simp add: div_gcd_coprime)
   1.333  done
   1.334  
   1.335  lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   1.336 -  by (induct n) (simp_all add: coprime_mult_nat)
   1.337 +  by (induct n) (simp_all add: coprime_mult)
   1.338  
   1.339  lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   1.340 -  by (induct n) (simp_all add: coprime_mult_int)
   1.341 +  by (induct n) (simp_all add: coprime_mult)
   1.342  
   1.343  context semiring_gcd
   1.344  begin
   1.345 @@ -1303,12 +1259,6 @@
   1.346  
   1.347  end
   1.348  
   1.349 -lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.350 -  by (fact coprime_exp2)
   1.351 -
   1.352 -lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.353 -  by (fact coprime_exp2)
   1.354 -
   1.355  lemma gcd_exp_nat:
   1.356    "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
   1.357  proof (cases "a = 0 \<and> b = 0")
   1.358 @@ -1352,7 +1302,7 @@
   1.359      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   1.360      hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
   1.361      with z have th_1: "a' dvd b' * c" by auto
   1.362 -    from coprime_dvd_mult_nat[OF ab'(3)] th_1
   1.363 +    from coprime_dvd_mult [OF ab'(3)] th_1
   1.364      have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   1.365      from ab' have "a = ?g*a'" by algebra
   1.366      with thb thc have ?thesis by blast }
   1.367 @@ -1376,7 +1326,7 @@
   1.368      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   1.369      hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
   1.370      with z have th_1: "a' dvd b' * c" by auto
   1.371 -    from coprime_dvd_mult_int[OF ab'(3)] th_1
   1.372 +    from coprime_dvd_mult [OF ab'(3)] th_1
   1.373      have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   1.374      from ab' have "a = ?g*a'" by algebra
   1.375      with thb thc have ?thesis by blast }
   1.376 @@ -1405,7 +1355,7 @@
   1.377      have "a' dvd a'^n" by (simp add: m)
   1.378      with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   1.379      hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   1.380 -    from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   1.381 +    from coprime_dvd_mult [OF coprime_exp_nat [OF ab'(3), of m]] th1
   1.382      have "a' dvd b'" by (subst (asm) mult.commute, blast)
   1.383      hence "a'*?g dvd b'*?g" by simp
   1.384      with ab'(1,2)  have ?thesis by simp }
   1.385 @@ -1434,7 +1384,7 @@
   1.386      with th0 have "a' dvd b'^n"
   1.387        using dvd_trans[of a' "a'^n" "b'^n"] by simp
   1.388      hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   1.389 -    from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   1.390 +    from coprime_dvd_mult [OF coprime_exp_int [OF ab'(3), of m]] th1
   1.391      have "a' dvd b'" by (subst (asm) mult.commute, blast)
   1.392      hence "a'*?g dvd b'*?g" by simp
   1.393      with ab'(1,2)  have ?thesis by simp }
   1.394 @@ -1454,7 +1404,7 @@
   1.395    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.396      unfolding dvd_def by blast
   1.397    from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   1.398 -  hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   1.399 +  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   1.400    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.401    from n' k show ?thesis unfolding dvd_def by auto
   1.402  qed
   1.403 @@ -1466,7 +1416,7 @@
   1.404    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.405      unfolding dvd_def by blast
   1.406    from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   1.407 -  hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   1.408 +  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   1.409    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.410    from n' k show ?thesis unfolding dvd_def by auto
   1.411  qed
   1.412 @@ -1482,29 +1432,27 @@
   1.413  
   1.414  lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   1.415    using coprime_plus_one_nat [of "n - 1"]
   1.416 -    gcd_commute_nat [of "n - 1" n] by auto
   1.417 +    gcd.commute [of "n - 1" n] by auto
   1.418  
   1.419  lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   1.420    using coprime_plus_one_int [of "n - 1"]
   1.421 -    gcd_commute_int [of "n - 1" n] by auto
   1.422 +    gcd.commute [of "n - 1" n] by auto
   1.423  
   1.424 -lemma setprod_coprime_nat [rule_format]:
   1.425 -    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
   1.426 -  apply (case_tac "finite A")
   1.427 -  apply (induct set: finite)
   1.428 -  apply (auto simp add: gcd_mult_cancel_nat)
   1.429 -done
   1.430 +lemma setprod_coprime_nat:
   1.431 +  fixes x :: nat
   1.432 +  shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
   1.433 +  by (induct A rule: infinite_finite_induct)
   1.434 +    (auto simp add: gcd_mult_cancel One_nat_def [symmetric] simp del: One_nat_def)
   1.435  
   1.436 -lemma setprod_coprime_int [rule_format]:
   1.437 -    "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
   1.438 -  apply (case_tac "finite A")
   1.439 -  apply (induct set: finite)
   1.440 -  apply (auto simp add: gcd_mult_cancel_int)
   1.441 -done
   1.442 +lemma setprod_coprime_int:
   1.443 +  fixes x :: int
   1.444 +  shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
   1.445 +  by (induct A rule: infinite_finite_induct)
   1.446 +    (auto simp add: gcd_mult_cancel)
   1.447  
   1.448  lemma coprime_common_divisor_nat: 
   1.449    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   1.450 -  by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
   1.451 +  by (metis gcd_greatest_iff nat_dvd_1_iff_1)
   1.452  
   1.453  lemma coprime_common_divisor_int:
   1.454    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   1.455 @@ -1515,10 +1463,10 @@
   1.456    by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   1.457  
   1.458  lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
   1.459 -by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   1.460 +by (metis coprime_lmult_nat gcd_1_nat gcd.commute gcd_red_nat)
   1.461  
   1.462  lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
   1.463 -by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   1.464 +by (metis coprime_lmult_int gcd_1_int gcd.commute gcd_red_int)
   1.465  
   1.466  
   1.467  subsection \<open>Bezout's theorem\<close>
   1.468 @@ -1764,8 +1712,7 @@
   1.469  subsection \<open>LCM properties\<close>
   1.470  
   1.471  lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   1.472 -  by (simp add: lcm_int_def lcm_nat_def zdiv_int
   1.473 -    of_nat_mult gcd_int_def)
   1.474 +  by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
   1.475  
   1.476  lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
   1.477    unfolding lcm_nat_def
   1.478 @@ -1800,70 +1747,21 @@
   1.479    apply (subst lcm_abs_int)
   1.480    apply (rule lcm_pos_nat [transferred])
   1.481    apply auto
   1.482 -done
   1.483 +  done
   1.484  
   1.485  lemma dvd_pos_nat:
   1.486    fixes n m :: nat
   1.487    assumes "n > 0" and "m dvd n"
   1.488    shows "m > 0"
   1.489 -using assms by (cases m) auto
   1.490 -
   1.491 -lemma lcm_least_nat:
   1.492 -  assumes "(m::nat) dvd k" and "n dvd k"
   1.493 -  shows "lcm m n dvd k"
   1.494 -  using assms by (rule lcm_least)
   1.495 -
   1.496 -lemma lcm_least_int:
   1.497 -  "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
   1.498 -  by (rule lcm_least)
   1.499 -
   1.500 -lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
   1.501 -  by (fact dvd_lcm1)
   1.502 -
   1.503 -lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
   1.504 -  by (fact dvd_lcm1)
   1.505 -
   1.506 -lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
   1.507 -  by (fact dvd_lcm2)
   1.508 -
   1.509 -lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
   1.510 -  by (fact dvd_lcm2)
   1.511 -
   1.512 -lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
   1.513 -by(metis lcm_dvd1_nat dvd_trans)
   1.514 -
   1.515 -lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
   1.516 -by(metis lcm_dvd2_nat dvd_trans)
   1.517 -
   1.518 -lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   1.519 -by(metis lcm_dvd1_int dvd_trans)
   1.520 -
   1.521 -lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   1.522 -by(metis lcm_dvd2_int dvd_trans)
   1.523 +  using assms by (cases m) auto
   1.524  
   1.525  lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
   1.526      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   1.527 -  by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
   1.528 +  by (auto intro: dvd_antisym lcm_least)
   1.529  
   1.530  lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
   1.531      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   1.532 -  using lcm_least_int zdvd_antisym_nonneg by auto
   1.533 -
   1.534 -interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   1.535 -  + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
   1.536 -  by standard (simp_all del: One_nat_def)
   1.537 -
   1.538 -interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
   1.539 -
   1.540 -lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
   1.541 -lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
   1.542 -lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
   1.543 -lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
   1.544 -lemmas lcm_commute_int = lcm.commute [where ?'a = int]
   1.545 -lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
   1.546 -
   1.547 -lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   1.548 -lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   1.549 +  using lcm_least zdvd_antisym_nonneg by auto
   1.550  
   1.551  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   1.552    apply (rule sym)
   1.553 @@ -1878,10 +1776,10 @@
   1.554  done
   1.555  
   1.556  lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
   1.557 -by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
   1.558 +by (subst lcm.commute, erule lcm_proj2_if_dvd_nat)
   1.559  
   1.560  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
   1.561 -by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
   1.562 +by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
   1.563  
   1.564  lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   1.565  by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
   1.566 @@ -1903,24 +1801,6 @@
   1.567    "comp_fun_idem lcm"
   1.568    by standard (simp_all add: fun_eq_iff ac_simps)
   1.569  
   1.570 -lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.571 -  by (fact comp_fun_idem_gcd)
   1.572 -
   1.573 -lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   1.574 -  by (fact comp_fun_idem_gcd)
   1.575 -
   1.576 -lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.577 -  by (fact comp_fun_idem_lcm)
   1.578 -
   1.579 -lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   1.580 -  by (fact comp_fun_idem_lcm)
   1.581 -
   1.582 -lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
   1.583 -  by (fact lcm_eq_0_iff)
   1.584 -
   1.585 -lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
   1.586 -  by (fact lcm_eq_0_iff)
   1.587 -
   1.588  lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
   1.589    by (simp only: lcm_eq_1_iff) simp
   1.590    
   1.591 @@ -1930,14 +1810,6 @@
   1.592  
   1.593  subsection \<open>The complete divisibility lattice\<close>
   1.594  
   1.595 -interpretation gcd_semilattice_nat: semilattice_inf gcd Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
   1.596 -  by standard simp_all
   1.597 -
   1.598 -interpretation lcm_semilattice_nat: semilattice_sup lcm Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
   1.599 -  by standard simp_all
   1.600 -
   1.601 -interpretation gcd_lcm_lattice_nat: lattice gcd Rings.dvd "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
   1.602 -
   1.603  text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
   1.604  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
   1.605  \<close>
   1.606 @@ -1945,7 +1817,8 @@
   1.607  instantiation nat :: Gcd
   1.608  begin
   1.609  
   1.610 -interpretation semilattice_neutr_set lcm "1::nat" ..
   1.611 +interpretation semilattice_neutr_set lcm "1::nat"
   1.612 +  by standard simp_all
   1.613  
   1.614  definition
   1.615    "Lcm (M::nat set) = (if finite M then F M else 0)"
   1.616 @@ -1990,8 +1863,6 @@
   1.617  definition
   1.618    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
   1.619  
   1.620 -interpretation bla: semilattice_neutr_set gcd "0::nat" ..
   1.621 -
   1.622  instance ..
   1.623  
   1.624  end
   1.625 @@ -2012,18 +1883,6 @@
   1.626      by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
   1.627  qed
   1.628  
   1.629 -interpretation gcd_lcm_complete_lattice_nat:
   1.630 -  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
   1.631 -  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   1.632 -
   1.633 -lemma Lcm_empty_nat:
   1.634 -  "Lcm {} = (1::nat)"
   1.635 -  by (fact Lcm_empty)
   1.636 -
   1.637 -lemma Lcm_insert_nat [simp]:
   1.638 -  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   1.639 -  by (fact Lcm_insert)
   1.640 -
   1.641  lemma Lcm_eq_0 [simp]:
   1.642    "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
   1.643    by (rule Lcm_eq_0_I)
   1.644 @@ -2080,14 +1939,6 @@
   1.645  apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
   1.646  done
   1.647  
   1.648 -lemma Lcm_set_nat [code, code_unfold]:
   1.649 -  "Lcm (set ns) = fold lcm ns (1::nat)"
   1.650 -  by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
   1.651 -
   1.652 -lemma Gcd_set_nat [code]:
   1.653 -  "Gcd (set ns) = fold gcd ns (0::nat)"
   1.654 -  by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
   1.655 -
   1.656  lemma mult_inj_if_coprime_nat:
   1.657    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
   1.658     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
   1.659 @@ -2142,58 +1993,14 @@
   1.660        by auto
   1.661    qed
   1.662    then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
   1.663 -    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd)
   1.664 +    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd image_image)
   1.665  qed
   1.666  
   1.667 -lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
   1.668 -  by (fact Lcm_empty)
   1.669 -
   1.670 -lemma Lcm_insert_int [simp]:
   1.671 -  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   1.672 -  by (fact Lcm_insert)
   1.673 -
   1.674 -lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   1.675 -  by (fact dvd_int_unfold_dvd_nat)
   1.676 -
   1.677 -lemma dvd_Lcm_int [simp]:
   1.678 -  fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   1.679 -  using assms by (fact dvd_Lcm)
   1.680 -
   1.681  lemma Lcm_dvd_int [simp]:
   1.682    fixes M :: "int set"
   1.683    assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   1.684 -  using assms by (simp add: Lcm_int_def dvd_int_iff)
   1.685 -
   1.686 -lemma Lcm_set_int [code, code_unfold]:
   1.687 -  "Lcm (set xs) = fold lcm xs (1::int)"
   1.688 -  by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
   1.689 -
   1.690 -lemma Gcd_set_int [code]:
   1.691 -  "Gcd (set xs) = fold gcd xs (0::int)"
   1.692 -  by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
   1.693 -
   1.694 -
   1.695 -text \<open>Fact aliasses\<close>
   1.696 +  using assms by (auto intro: Lcm_least)
   1.697  
   1.698 -lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
   1.699 -  and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
   1.700 -  and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
   1.701 -
   1.702 -lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
   1.703 -  and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
   1.704 -  and gcd_greatest_int = gcd_greatest [where ?'a = int]
   1.705 -
   1.706 -lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
   1.707 -  and dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
   1.708 -
   1.709 -lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
   1.710 -  and dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
   1.711 -
   1.712 -lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
   1.713 -  and Gcd_insert_nat = Gcd_insert [where ?'a = nat]
   1.714 -
   1.715 -lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
   1.716 -  and Gcd_insert_int = Gcd_insert [where ?'a = int]
   1.717  
   1.718  subsection \<open>gcd and lcm instances for @{typ integer}\<close>
   1.719  
   1.720 @@ -2224,4 +2031,177 @@
   1.721    and (Scala) "_.gcd'((_)')"
   1.722    \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
   1.723  
   1.724 +text \<open>Some code equations\<close>
   1.725 +
   1.726 +lemma Lcm_set_nat [code, code_unfold]:
   1.727 +  "Lcm (set ns) = fold lcm ns (1::nat)"
   1.728 +  using Lcm_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   1.729 +
   1.730 +lemma Gcd_set_nat [code]:
   1.731 +  "Gcd (set ns) = fold gcd ns (0::nat)"
   1.732 +  using Gcd_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   1.733 +
   1.734 +lemma Lcm_set_int [code, code_unfold]:
   1.735 +  "Lcm (set xs) = fold lcm xs (1::int)"
   1.736 +  using Lcm_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   1.737 +
   1.738 +lemma Gcd_set_int [code]:
   1.739 +  "Gcd (set xs) = fold gcd xs (0::int)"
   1.740 +  using Gcd_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   1.741 +
   1.742 +text \<open>Fact aliasses\<close>
   1.743 +
   1.744 +lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   1.745 +  by (fact dvd_int_unfold_dvd_nat)
   1.746 +
   1.747 +lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
   1.748 +lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
   1.749 +lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
   1.750 +lemmas gcd_commute_int = gcd.commute [where ?'a = int]
   1.751 +lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
   1.752 +lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
   1.753 +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   1.754 +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   1.755 +lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
   1.756 +lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
   1.757 +lemmas gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
   1.758 +lemmas gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
   1.759 +lemmas gcd_greatest_nat = gcd_greatest [where ?'a = nat]
   1.760 +lemmas gcd_greatest_int = gcd_greatest [where ?'a = int]
   1.761 +lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
   1.762 +lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
   1.763 +lemmas gcd_greatest_iff_nat = gcd_greatest_iff [where ?'a = nat]
   1.764 +lemmas gcd_greatest_iff_int = gcd_greatest_iff [where ?'a = int]
   1.765 +lemmas gcd_zero_nat = gcd_eq_0_iff [where ?'a = nat]
   1.766 +lemmas gcd_zero_int = gcd_eq_0_iff [where ?'a = int]
   1.767 +
   1.768 +lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
   1.769 +lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
   1.770 +lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
   1.771 +lemmas lcm_commute_int = lcm.commute [where ?'a = int]
   1.772 +lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
   1.773 +lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
   1.774 +lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   1.775 +lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   1.776 +lemmas lcm_dvd1_nat = dvd_lcm1 [where ?'a = nat]
   1.777 +lemmas lcm_dvd1_int = dvd_lcm1 [where ?'a = int]
   1.778 +lemmas lcm_dvd2_nat = dvd_lcm2 [where ?'a = nat]
   1.779 +lemmas lcm_dvd2_int = dvd_lcm2 [where ?'a = int]
   1.780 +lemmas lcm_least_nat = lcm_least [where ?'a = nat]
   1.781 +lemmas lcm_least_int = lcm_least [where ?'a = int]
   1.782 +
   1.783 +lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
   1.784 +  by (fact lcm_eq_0_iff)
   1.785 +
   1.786 +lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   1.787 +  by (fact lcm_eq_0_iff)
   1.788 +
   1.789 +lemma dvd_lcm_I1_nat [simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
   1.790 +  by (fact dvd_lcmI1)
   1.791 +
   1.792 +lemma dvd_lcm_I2_nat [simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
   1.793 +  by (fact dvd_lcmI2)
   1.794 +
   1.795 +lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   1.796 +  by (fact dvd_lcmI1)
   1.797 +
   1.798 +lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   1.799 +  by (fact dvd_lcmI2)
   1.800 +
   1.801 +lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
   1.802 +lemmas coprime_mult_int = coprime_mult [where ?'a = int]
   1.803 +lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
   1.804 +lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
   1.805 +lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
   1.806 +lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
   1.807 +
   1.808 +lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   1.809 +    (k dvd m * n) = (k dvd m)"
   1.810 +  by (fact coprime_dvd_mult_iff)
   1.811 +
   1.812 +lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   1.813 +    (k dvd m * n) = (k dvd m)"
   1.814 +  by (fact coprime_dvd_mult_iff)
   1.815 +
   1.816 +lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.817 +  by (fact coprime_exp2)
   1.818 +
   1.819 +lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.820 +  by (fact coprime_exp2)
   1.821 +
   1.822 +lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
   1.823 +lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
   1.824 +lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
   1.825 +lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
   1.826 +lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
   1.827 +lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
   1.828 +lemmas Gcd_insert_nat = Gcd_insert [where ?'a = nat]
   1.829 +lemmas Gcd_insert_int = Gcd_insert [where ?'a = int]
   1.830 +
   1.831 +lemma dvd_Lcm_int [simp]:
   1.832 +  fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   1.833 +  using assms by (fact dvd_Lcm)
   1.834 +
   1.835 +lemma Lcm_empty_nat:
   1.836 +  "Lcm {} = (1::nat)"
   1.837 +  by (fact Lcm_empty)
   1.838 +
   1.839 +lemma Lcm_empty_int:
   1.840 +  "Lcm {} = (1::int)"
   1.841 +  by (fact Lcm_empty)
   1.842 +
   1.843 +lemma Lcm_insert_nat:
   1.844 +  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   1.845 +  by (fact Lcm_insert)
   1.846 +
   1.847 +lemma Lcm_insert_int:
   1.848 +  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   1.849 +  by (fact Lcm_insert)
   1.850 +
   1.851 +lemma gcd_neg_numeral_1_int [simp]:
   1.852 +  "gcd (- numeral n :: int) x = gcd (numeral n) x"
   1.853 +  by (fact gcd_neg1_int)
   1.854 +
   1.855 +lemma gcd_neg_numeral_2_int [simp]:
   1.856 +  "gcd x (- numeral n :: int) = gcd x (numeral n)"
   1.857 +  by (fact gcd_neg2_int)
   1.858 +
   1.859 +lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   1.860 +  by (fact gcd_nat.absorb1)
   1.861 +
   1.862 +lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   1.863 +  by (fact gcd_nat.absorb2)
   1.864 +
   1.865 +lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.866 +  by (fact comp_fun_idem_gcd)
   1.867 +
   1.868 +lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   1.869 +  by (fact comp_fun_idem_gcd)
   1.870 +
   1.871 +lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.872 +  by (fact comp_fun_idem_lcm)
   1.873 +
   1.874 +lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   1.875 +  by (fact comp_fun_idem_lcm)
   1.876 +
   1.877 +interpretation dvd:
   1.878 +  order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
   1.879 +  by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
   1.880 +
   1.881 +interpretation gcd_semilattice_nat:
   1.882 +  semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
   1.883 +  by standard (auto dest: dvd_antisym dvd_trans)
   1.884 +
   1.885 +interpretation lcm_semilattice_nat:
   1.886 +  semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
   1.887 +  by standard simp_all
   1.888 +
   1.889 +interpretation gcd_lcm_lattice_nat:
   1.890 +  lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
   1.891 +  ..
   1.892 +
   1.893 +interpretation gcd_lcm_complete_lattice_nat:
   1.894 +  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
   1.895 +  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   1.896 +
   1.897  end