pulled out legacy aliasses and infamous dvd interpretations into theory appendix
authorhaftmann
Wed Feb 17 21:51:56 2016 +0100 (2016-02-17)
changeset 62344759d684c0e60
parent 62343 24106dc44def
child 62345 e66d7841d5a2
pulled out legacy aliasses and infamous dvd interpretations into theory appendix
src/HOL/Binomial.thy
src/HOL/GCD.thy
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Binomial.thy	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/src/HOL/Binomial.thy	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -1323,7 +1323,7 @@
     1.4    also have "... = (fact (m+r+k) * fact (m+r)) div (fact r * (fact k * fact m) * fact (m+r))"
     1.5      apply (subst div_mult_div_if_dvd [symmetric])
     1.6      apply (auto simp add: algebra_simps)
     1.7 -    apply (metis fact_fact_dvd_fact dvd.order.trans nat_mult_dvd_cancel_disj)
     1.8 +    apply (metis fact_fact_dvd_fact dvd_trans nat_mult_dvd_cancel_disj)
     1.9      done
    1.10    also have "... = (fact (m+r+k) div (fact k * fact (m+r)) * (fact (m+r) div (fact r * fact m)))"
    1.11      apply (subst div_mult_div_if_dvd)
     2.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     2.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
     2.3 @@ -668,14 +668,6 @@
     2.4  lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
     2.5    by (simp add: gcd_int_def)
     2.6  
     2.7 -lemma gcd_neg_numeral_1_int [simp]:
     2.8 -  "gcd (- numeral n :: int) x = gcd (numeral n) x"
     2.9 -  by (fact gcd_neg1_int)
    2.10 -
    2.11 -lemma gcd_neg_numeral_2_int [simp]:
    2.12 -  "gcd x (- numeral n :: int) = gcd x (numeral n)"
    2.13 -  by (fact gcd_neg2_int)
    2.14 -
    2.15  lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    2.16  by(simp add: gcd_int_def)
    2.17  
    2.18 @@ -822,27 +814,11 @@
    2.19  lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
    2.20    by (rule zdvd_imp_le, auto)
    2.21  
    2.22 -lemma gcd_greatest_iff_nat:
    2.23 -  "(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)"
    2.24 -  by (fact gcd_greatest_iff)
    2.25 -
    2.26 -lemma gcd_greatest_iff_int:
    2.27 -  "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
    2.28 -  by (fact gcd_greatest_iff)
    2.29 -
    2.30 -lemma gcd_zero_nat: 
    2.31 -  "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
    2.32 -  by (fact gcd_eq_0_iff)
    2.33 -
    2.34 -lemma gcd_zero_int [simp]:
    2.35 -  "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
    2.36 -  by (fact gcd_eq_0_iff)
    2.37 -
    2.38  lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
    2.39 -  by (insert gcd_zero_nat [of m n], arith)
    2.40 +  by (insert gcd_eq_0_iff [of m n], arith)
    2.41  
    2.42  lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
    2.43 -  by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
    2.44 +  by (insert gcd_eq_0_iff [of m n], insert gcd_ge_0_int [of m n], arith)
    2.45  
    2.46  lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
    2.47      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    2.48 @@ -862,31 +838,14 @@
    2.49  done
    2.50  
    2.51  interpretation gcd_nat:
    2.52 -  semilattice_neutr_order gcd "0::nat" Rings.dvd "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
    2.53 -  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd.antisym dvd_trans)
    2.54 -
    2.55 -lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
    2.56 -lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
    2.57 -lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
    2.58 -lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
    2.59 -lemmas gcd_commute_int = gcd.commute [where ?'a = int]
    2.60 -lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
    2.61 -
    2.62 -lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
    2.63 -
    2.64 -lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
    2.65 -
    2.66 -lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
    2.67 -  by (fact gcd_nat.absorb1)
    2.68 -
    2.69 -lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
    2.70 -  by (fact gcd_nat.absorb2)
    2.71 +  semilattice_neutr_order gcd "0::nat" Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n"
    2.72 +  by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd_antisym dvd_trans)
    2.73  
    2.74  lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
    2.75    by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
    2.76  
    2.77  lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
    2.78 -  by (metis gcd_proj1_if_dvd_int gcd_commute_int)
    2.79 +  by (metis gcd_proj1_if_dvd_int gcd.commute)
    2.80  
    2.81  text \<open>
    2.82    \medskip Multiplication laws
    2.83 @@ -926,21 +885,10 @@
    2.84    ultimately show ?thesis by simp
    2.85  qed
    2.86  
    2.87 -end
    2.88 -
    2.89 -lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
    2.90 -lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
    2.91 -
    2.92 -lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
    2.93 -    (k dvd m * n) = (k dvd m)"
    2.94 -  by (auto intro: coprime_dvd_mult_nat)
    2.95 -
    2.96 -lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
    2.97 -    (k dvd m * n) = (k dvd m)"
    2.98 -  by (auto intro: coprime_dvd_mult_int)
    2.99 -
   2.100 -context semiring_gcd
   2.101 -begin
   2.102 +lemma coprime_dvd_mult_iff:
   2.103 +  assumes "coprime a c"
   2.104 +  shows "a dvd b * c \<longleftrightarrow> a dvd b"
   2.105 +  using assms by (auto intro: coprime_dvd_mult)
   2.106  
   2.107  lemma gcd_mult_cancel:
   2.108    "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   2.109 @@ -951,65 +899,79 @@
   2.110    apply (simp_all add: ac_simps)
   2.111    done
   2.112  
   2.113 -end  
   2.114 -
   2.115 -lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
   2.116 -lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
   2.117 -
   2.118 -lemma coprime_crossproduct_nat:
   2.119 -  fixes a b c d :: nat
   2.120 +lemma coprime_crossproduct:
   2.121 +  fixes a b c d
   2.122    assumes "coprime a d" and "coprime b c"
   2.123 -  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")
   2.124 +  shows "normalize a * normalize c = normalize b * normalize d
   2.125 +    \<longleftrightarrow> normalize a = normalize b \<and> normalize c = normalize d" (is "?lhs \<longleftrightarrow> ?rhs")
   2.126  proof
   2.127    assume ?rhs then show ?lhs by simp
   2.128  next
   2.129    assume ?lhs
   2.130 -  from \<open>?lhs\<close> have "a dvd b * d" by (auto intro: dvdI dest: sym)
   2.131 -  with \<open>coprime a d\<close> have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
   2.132 -  from \<open>?lhs\<close> have "b dvd a * c" by (auto intro: dvdI dest: sym)
   2.133 -  with \<open>coprime b c\<close> have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
   2.134 -  from \<open>?lhs\<close> have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
   2.135 -  with \<open>coprime b c\<close> have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   2.136 -  from \<open>?lhs\<close> have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
   2.137 -  with \<open>coprime a d\<close> have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   2.138 -  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "a = b" by (rule Nat.dvd.antisym)
   2.139 -  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "c = d" by (rule Nat.dvd.antisym)
   2.140 +  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
   2.141 +    by (auto intro: dvdI dest: sym)
   2.142 +  with \<open>coprime a d\<close> have "a dvd b"
   2.143 +    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   2.144 +  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
   2.145 +    by (auto intro: dvdI dest: sym)
   2.146 +  with \<open>coprime b c\<close> have "b dvd a"
   2.147 +    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
   2.148 +  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
   2.149 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   2.150 +  with \<open>coprime b c\<close> have "c dvd d"
   2.151 +    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   2.152 +  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
   2.153 +    by (auto intro: dvdI dest: sym simp add: mult.commute)
   2.154 +  with \<open>coprime a d\<close> have "d dvd c"
   2.155 +    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
   2.156 +  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
   2.157 +    by (rule associatedI)
   2.158 +  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
   2.159 +    by (rule associatedI)
   2.160    ultimately show ?rhs ..
   2.161  qed
   2.162  
   2.163 +end
   2.164 +
   2.165 +lemma coprime_crossproduct_nat:
   2.166 +  fixes a b c d :: nat
   2.167 +  assumes "coprime a d" and "coprime b c"
   2.168 +  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
   2.169 +  using assms coprime_crossproduct [of a d b c] by simp
   2.170 +
   2.171  lemma coprime_crossproduct_int:
   2.172    fixes a b c d :: int
   2.173    assumes "coprime a d" and "coprime b c"
   2.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>"
   2.175 -  using assms by (intro coprime_crossproduct_nat [transferred]) auto
   2.176 +  using assms coprime_crossproduct [of a d b c] by simp
   2.177  
   2.178  text \<open>\medskip Addition laws\<close>
   2.179  
   2.180  lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   2.181    apply (case_tac "n = 0")
   2.182    apply (simp_all add: gcd_non_0_nat)
   2.183 -done
   2.184 +  done
   2.185  
   2.186  lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   2.187 -  apply (subst (1 2) gcd_commute_nat)
   2.188 +  apply (subst (1 2) gcd.commute)
   2.189    apply (subst add.commute)
   2.190    apply simp
   2.191 -done
   2.192 +  done
   2.193  
   2.194  (* to do: add the other variations? *)
   2.195  
   2.196  lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
   2.197 -  by (subst gcd_add1_nat [symmetric], auto)
   2.198 +  by (subst gcd_add1_nat [symmetric]) auto
   2.199  
   2.200  lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
   2.201 -  apply (subst gcd_commute_nat)
   2.202 +  apply (subst gcd.commute)
   2.203    apply (subst gcd_diff1_nat [symmetric])
   2.204    apply auto
   2.205 -  apply (subst gcd_commute_nat)
   2.206 +  apply (subst gcd.commute)
   2.207    apply (subst gcd_diff1_nat)
   2.208    apply assumption
   2.209 -  apply (rule gcd_commute_nat)
   2.210 -done
   2.211 +  apply (rule gcd.commute)
   2.212 +  done
   2.213  
   2.214  lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
   2.215    apply (frule_tac b = y and a = x in pos_mod_sign)
   2.216 @@ -1017,10 +979,10 @@
   2.217    apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
   2.218      zmod_zminus1_eq_if)
   2.219    apply (frule_tac a = x in pos_mod_bound)
   2.220 -  apply (subst (1 2) gcd_commute_nat)
   2.221 +  apply (subst (1 2) gcd.commute)
   2.222    apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
   2.223      nat_le_eq_zle)
   2.224 -done
   2.225 +  done
   2.226  
   2.227  lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
   2.228    apply (case_tac "y = 0")
   2.229 @@ -1035,13 +997,13 @@
   2.230  by (metis gcd_red_int mod_add_self1 add.commute)
   2.231  
   2.232  lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
   2.233 -by (metis gcd_add1_int gcd_commute_int add.commute)
   2.234 +by (metis gcd_add1_int gcd.commute add.commute)
   2.235  
   2.236  lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
   2.237 -by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
   2.238 +by (metis mod_mult_self3 gcd.commute gcd_red_nat)
   2.239  
   2.240  lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
   2.241 -by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute)
   2.242 +by (metis gcd.commute gcd_red_int mod_mult_self1 add.commute)
   2.243  
   2.244  
   2.245  (* to do: differences, and all variations of addition rules
   2.246 @@ -1087,7 +1049,7 @@
   2.247  apply(rule Max_eqI[THEN sym])
   2.248    apply (metis finite_Collect_conjI finite_divisors_nat)
   2.249   apply simp
   2.250 - apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
   2.251 + apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff gcd_pos_nat)
   2.252  apply simp
   2.253  done
   2.254  
   2.255 @@ -1096,7 +1058,7 @@
   2.256  apply(rule Max_eqI[THEN sym])
   2.257    apply (metis finite_Collect_conjI finite_divisors_int)
   2.258   apply simp
   2.259 - apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
   2.260 + apply (metis gcd_greatest_iff gcd_pos_int zdvd_imp_le)
   2.261  apply simp
   2.262  done
   2.263  
   2.264 @@ -1136,9 +1098,6 @@
   2.265  
   2.266  end
   2.267  
   2.268 -lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
   2.269 -lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
   2.270 -
   2.271  lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   2.272    using gcd_unique_nat[of 1 a b, simplified] by auto
   2.273  
   2.274 @@ -1165,7 +1124,7 @@
   2.275    apply (erule ssubst)
   2.276    apply (subgoal_tac "b' = b div gcd a b")
   2.277    apply (erule ssubst)
   2.278 -  apply (rule div_gcd_coprime_nat)
   2.279 +  apply (rule div_gcd_coprime)
   2.280    using z apply force
   2.281    apply (subst (1) b)
   2.282    using z apply force
   2.283 @@ -1182,7 +1141,7 @@
   2.284    apply (erule ssubst)
   2.285    apply (subgoal_tac "b' = b div gcd a b")
   2.286    apply (erule ssubst)
   2.287 -  apply (rule div_gcd_coprime_int)
   2.288 +  apply (rule div_gcd_coprime)
   2.289    using z apply force
   2.290    apply (subst (1) b)
   2.291    using z apply force
   2.292 @@ -1204,9 +1163,6 @@
   2.293  
   2.294  end
   2.295  
   2.296 -lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
   2.297 -lemmas coprime_mult_int = coprime_mult [where ?'a = int]
   2.298 -  
   2.299  lemma coprime_lmult_nat:
   2.300    assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
   2.301  proof -
   2.302 @@ -1246,13 +1202,13 @@
   2.303  lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
   2.304      coprime d a \<and>  coprime d b"
   2.305    using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
   2.306 -    coprime_mult_nat[of d a b]
   2.307 +    coprime_mult [of d a b]
   2.308    by blast
   2.309  
   2.310  lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
   2.311      coprime d a \<and>  coprime d b"
   2.312    using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
   2.313 -    coprime_mult_int[of d a b]
   2.314 +    coprime_mult [of d a b]
   2.315    by blast
   2.316  
   2.317  lemma coprime_power_int:
   2.318 @@ -1268,7 +1224,7 @@
   2.319      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   2.320    apply (rule_tac x = "a div gcd a b" in exI)
   2.321    apply (rule_tac x = "b div gcd a b" in exI)
   2.322 -  using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
   2.323 +  using nz apply (auto simp add: div_gcd_coprime dvd_div_mult)
   2.324  done
   2.325  
   2.326  lemma gcd_coprime_exists_int:
   2.327 @@ -1276,14 +1232,14 @@
   2.328      shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
   2.329    apply (rule_tac x = "a div gcd a b" in exI)
   2.330    apply (rule_tac x = "b div gcd a b" in exI)
   2.331 -  using nz apply (auto simp add: div_gcd_coprime_int)
   2.332 +  using nz apply (auto simp add: div_gcd_coprime)
   2.333  done
   2.334  
   2.335  lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
   2.336 -  by (induct n) (simp_all add: coprime_mult_nat)
   2.337 +  by (induct n) (simp_all add: coprime_mult)
   2.338  
   2.339  lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   2.340 -  by (induct n) (simp_all add: coprime_mult_int)
   2.341 +  by (induct n) (simp_all add: coprime_mult)
   2.342  
   2.343  context semiring_gcd
   2.344  begin
   2.345 @@ -1303,12 +1259,6 @@
   2.346  
   2.347  end
   2.348  
   2.349 -lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   2.350 -  by (fact coprime_exp2)
   2.351 -
   2.352 -lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   2.353 -  by (fact coprime_exp2)
   2.354 -
   2.355  lemma gcd_exp_nat:
   2.356    "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
   2.357  proof (cases "a = 0 \<and> b = 0")
   2.358 @@ -1352,7 +1302,7 @@
   2.359      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   2.360      hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
   2.361      with z have th_1: "a' dvd b' * c" by auto
   2.362 -    from coprime_dvd_mult_nat[OF ab'(3)] th_1
   2.363 +    from coprime_dvd_mult [OF ab'(3)] th_1
   2.364      have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   2.365      from ab' have "a = ?g*a'" by algebra
   2.366      with thb thc have ?thesis by blast }
   2.367 @@ -1376,7 +1326,7 @@
   2.368      from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
   2.369      hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
   2.370      with z have th_1: "a' dvd b' * c" by auto
   2.371 -    from coprime_dvd_mult_int[OF ab'(3)] th_1
   2.372 +    from coprime_dvd_mult [OF ab'(3)] th_1
   2.373      have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
   2.374      from ab' have "a = ?g*a'" by algebra
   2.375      with thb thc have ?thesis by blast }
   2.376 @@ -1405,7 +1355,7 @@
   2.377      have "a' dvd a'^n" by (simp add: m)
   2.378      with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
   2.379      hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   2.380 -    from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
   2.381 +    from coprime_dvd_mult [OF coprime_exp_nat [OF ab'(3), of m]] th1
   2.382      have "a' dvd b'" by (subst (asm) mult.commute, blast)
   2.383      hence "a'*?g dvd b'*?g" by simp
   2.384      with ab'(1,2)  have ?thesis by simp }
   2.385 @@ -1434,7 +1384,7 @@
   2.386      with th0 have "a' dvd b'^n"
   2.387        using dvd_trans[of a' "a'^n" "b'^n"] by simp
   2.388      hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
   2.389 -    from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
   2.390 +    from coprime_dvd_mult [OF coprime_exp_int [OF ab'(3), of m]] th1
   2.391      have "a' dvd b'" by (subst (asm) mult.commute, blast)
   2.392      hence "a'*?g dvd b'*?g" by simp
   2.393      with ab'(1,2)  have ?thesis by simp }
   2.394 @@ -1454,7 +1404,7 @@
   2.395    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   2.396      unfolding dvd_def by blast
   2.397    from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   2.398 -  hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
   2.399 +  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   2.400    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   2.401    from n' k show ?thesis unfolding dvd_def by auto
   2.402  qed
   2.403 @@ -1466,7 +1416,7 @@
   2.404    from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   2.405      unfolding dvd_def by blast
   2.406    from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   2.407 -  hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
   2.408 +  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   2.409    then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   2.410    from n' k show ?thesis unfolding dvd_def by auto
   2.411  qed
   2.412 @@ -1482,29 +1432,27 @@
   2.413  
   2.414  lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   2.415    using coprime_plus_one_nat [of "n - 1"]
   2.416 -    gcd_commute_nat [of "n - 1" n] by auto
   2.417 +    gcd.commute [of "n - 1" n] by auto
   2.418  
   2.419  lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
   2.420    using coprime_plus_one_int [of "n - 1"]
   2.421 -    gcd_commute_int [of "n - 1" n] by auto
   2.422 +    gcd.commute [of "n - 1" n] by auto
   2.423  
   2.424 -lemma setprod_coprime_nat [rule_format]:
   2.425 -    "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
   2.426 -  apply (case_tac "finite A")
   2.427 -  apply (induct set: finite)
   2.428 -  apply (auto simp add: gcd_mult_cancel_nat)
   2.429 -done
   2.430 +lemma setprod_coprime_nat:
   2.431 +  fixes x :: nat
   2.432 +  shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
   2.433 +  by (induct A rule: infinite_finite_induct)
   2.434 +    (auto simp add: gcd_mult_cancel One_nat_def [symmetric] simp del: One_nat_def)
   2.435  
   2.436 -lemma setprod_coprime_int [rule_format]:
   2.437 -    "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
   2.438 -  apply (case_tac "finite A")
   2.439 -  apply (induct set: finite)
   2.440 -  apply (auto simp add: gcd_mult_cancel_int)
   2.441 -done
   2.442 +lemma setprod_coprime_int:
   2.443 +  fixes x :: int
   2.444 +  shows "(\<And>i. i \<in> A \<Longrightarrow> coprime (f i) x) \<Longrightarrow> coprime (\<Prod>i\<in>A. f i) x"
   2.445 +  by (induct A rule: infinite_finite_induct)
   2.446 +    (auto simp add: gcd_mult_cancel)
   2.447  
   2.448  lemma coprime_common_divisor_nat: 
   2.449    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   2.450 -  by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
   2.451 +  by (metis gcd_greatest_iff nat_dvd_1_iff_1)
   2.452  
   2.453  lemma coprime_common_divisor_int:
   2.454    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
   2.455 @@ -1515,10 +1463,10 @@
   2.456    by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
   2.457  
   2.458  lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
   2.459 -by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
   2.460 +by (metis coprime_lmult_nat gcd_1_nat gcd.commute gcd_red_nat)
   2.461  
   2.462  lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
   2.463 -by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
   2.464 +by (metis coprime_lmult_int gcd_1_int gcd.commute gcd_red_int)
   2.465  
   2.466  
   2.467  subsection \<open>Bezout's theorem\<close>
   2.468 @@ -1764,8 +1712,7 @@
   2.469  subsection \<open>LCM properties\<close>
   2.470  
   2.471  lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   2.472 -  by (simp add: lcm_int_def lcm_nat_def zdiv_int
   2.473 -    of_nat_mult gcd_int_def)
   2.474 +  by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
   2.475  
   2.476  lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
   2.477    unfolding lcm_nat_def
   2.478 @@ -1800,70 +1747,21 @@
   2.479    apply (subst lcm_abs_int)
   2.480    apply (rule lcm_pos_nat [transferred])
   2.481    apply auto
   2.482 -done
   2.483 +  done
   2.484  
   2.485  lemma dvd_pos_nat:
   2.486    fixes n m :: nat
   2.487    assumes "n > 0" and "m dvd n"
   2.488    shows "m > 0"
   2.489 -using assms by (cases m) auto
   2.490 -
   2.491 -lemma lcm_least_nat:
   2.492 -  assumes "(m::nat) dvd k" and "n dvd k"
   2.493 -  shows "lcm m n dvd k"
   2.494 -  using assms by (rule lcm_least)
   2.495 -
   2.496 -lemma lcm_least_int:
   2.497 -  "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
   2.498 -  by (rule lcm_least)
   2.499 -
   2.500 -lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
   2.501 -  by (fact dvd_lcm1)
   2.502 -
   2.503 -lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
   2.504 -  by (fact dvd_lcm1)
   2.505 -
   2.506 -lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
   2.507 -  by (fact dvd_lcm2)
   2.508 -
   2.509 -lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
   2.510 -  by (fact dvd_lcm2)
   2.511 -
   2.512 -lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
   2.513 -by(metis lcm_dvd1_nat dvd_trans)
   2.514 -
   2.515 -lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
   2.516 -by(metis lcm_dvd2_nat dvd_trans)
   2.517 -
   2.518 -lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   2.519 -by(metis lcm_dvd1_int dvd_trans)
   2.520 -
   2.521 -lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   2.522 -by(metis lcm_dvd2_int dvd_trans)
   2.523 +  using assms by (cases m) auto
   2.524  
   2.525  lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
   2.526      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   2.527 -  by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
   2.528 +  by (auto intro: dvd_antisym lcm_least)
   2.529  
   2.530  lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
   2.531      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   2.532 -  using lcm_least_int zdvd_antisym_nonneg by auto
   2.533 -
   2.534 -interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   2.535 -  + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
   2.536 -  by standard (simp_all del: One_nat_def)
   2.537 -
   2.538 -interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
   2.539 -
   2.540 -lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
   2.541 -lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
   2.542 -lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
   2.543 -lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
   2.544 -lemmas lcm_commute_int = lcm.commute [where ?'a = int]
   2.545 -lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
   2.546 -
   2.547 -lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   2.548 -lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   2.549 +  using lcm_least zdvd_antisym_nonneg by auto
   2.550  
   2.551  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   2.552    apply (rule sym)
   2.553 @@ -1878,10 +1776,10 @@
   2.554  done
   2.555  
   2.556  lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
   2.557 -by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
   2.558 +by (subst lcm.commute, erule lcm_proj2_if_dvd_nat)
   2.559  
   2.560  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
   2.561 -by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
   2.562 +by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
   2.563  
   2.564  lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   2.565  by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
   2.566 @@ -1903,24 +1801,6 @@
   2.567    "comp_fun_idem lcm"
   2.568    by standard (simp_all add: fun_eq_iff ac_simps)
   2.569  
   2.570 -lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.571 -  by (fact comp_fun_idem_gcd)
   2.572 -
   2.573 -lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   2.574 -  by (fact comp_fun_idem_gcd)
   2.575 -
   2.576 -lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.577 -  by (fact comp_fun_idem_lcm)
   2.578 -
   2.579 -lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   2.580 -  by (fact comp_fun_idem_lcm)
   2.581 -
   2.582 -lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
   2.583 -  by (fact lcm_eq_0_iff)
   2.584 -
   2.585 -lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
   2.586 -  by (fact lcm_eq_0_iff)
   2.587 -
   2.588  lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
   2.589    by (simp only: lcm_eq_1_iff) simp
   2.590    
   2.591 @@ -1930,14 +1810,6 @@
   2.592  
   2.593  subsection \<open>The complete divisibility lattice\<close>
   2.594  
   2.595 -interpretation gcd_semilattice_nat: semilattice_inf gcd Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
   2.596 -  by standard simp_all
   2.597 -
   2.598 -interpretation lcm_semilattice_nat: semilattice_sup lcm Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
   2.599 -  by standard simp_all
   2.600 -
   2.601 -interpretation gcd_lcm_lattice_nat: lattice gcd Rings.dvd "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
   2.602 -
   2.603  text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
   2.604  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
   2.605  \<close>
   2.606 @@ -1945,7 +1817,8 @@
   2.607  instantiation nat :: Gcd
   2.608  begin
   2.609  
   2.610 -interpretation semilattice_neutr_set lcm "1::nat" ..
   2.611 +interpretation semilattice_neutr_set lcm "1::nat"
   2.612 +  by standard simp_all
   2.613  
   2.614  definition
   2.615    "Lcm (M::nat set) = (if finite M then F M else 0)"
   2.616 @@ -1990,8 +1863,6 @@
   2.617  definition
   2.618    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
   2.619  
   2.620 -interpretation bla: semilattice_neutr_set gcd "0::nat" ..
   2.621 -
   2.622  instance ..
   2.623  
   2.624  end
   2.625 @@ -2012,18 +1883,6 @@
   2.626      by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
   2.627  qed
   2.628  
   2.629 -interpretation gcd_lcm_complete_lattice_nat:
   2.630 -  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
   2.631 -  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   2.632 -
   2.633 -lemma Lcm_empty_nat:
   2.634 -  "Lcm {} = (1::nat)"
   2.635 -  by (fact Lcm_empty)
   2.636 -
   2.637 -lemma Lcm_insert_nat [simp]:
   2.638 -  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   2.639 -  by (fact Lcm_insert)
   2.640 -
   2.641  lemma Lcm_eq_0 [simp]:
   2.642    "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
   2.643    by (rule Lcm_eq_0_I)
   2.644 @@ -2080,14 +1939,6 @@
   2.645  apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
   2.646  done
   2.647  
   2.648 -lemma Lcm_set_nat [code, code_unfold]:
   2.649 -  "Lcm (set ns) = fold lcm ns (1::nat)"
   2.650 -  by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
   2.651 -
   2.652 -lemma Gcd_set_nat [code]:
   2.653 -  "Gcd (set ns) = fold gcd ns (0::nat)"
   2.654 -  by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
   2.655 -
   2.656  lemma mult_inj_if_coprime_nat:
   2.657    "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
   2.658     \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
   2.659 @@ -2142,58 +1993,14 @@
   2.660        by auto
   2.661    qed
   2.662    then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
   2.663 -    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd)
   2.664 +    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd image_image)
   2.665  qed
   2.666  
   2.667 -lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
   2.668 -  by (fact Lcm_empty)
   2.669 -
   2.670 -lemma Lcm_insert_int [simp]:
   2.671 -  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   2.672 -  by (fact Lcm_insert)
   2.673 -
   2.674 -lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   2.675 -  by (fact dvd_int_unfold_dvd_nat)
   2.676 -
   2.677 -lemma dvd_Lcm_int [simp]:
   2.678 -  fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   2.679 -  using assms by (fact dvd_Lcm)
   2.680 -
   2.681  lemma Lcm_dvd_int [simp]:
   2.682    fixes M :: "int set"
   2.683    assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   2.684 -  using assms by (simp add: Lcm_int_def dvd_int_iff)
   2.685 -
   2.686 -lemma Lcm_set_int [code, code_unfold]:
   2.687 -  "Lcm (set xs) = fold lcm xs (1::int)"
   2.688 -  by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
   2.689 -
   2.690 -lemma Gcd_set_int [code]:
   2.691 -  "Gcd (set xs) = fold gcd xs (0::int)"
   2.692 -  by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
   2.693 -
   2.694 -
   2.695 -text \<open>Fact aliasses\<close>
   2.696 +  using assms by (auto intro: Lcm_least)
   2.697  
   2.698 -lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
   2.699 -  and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
   2.700 -  and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
   2.701 -
   2.702 -lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
   2.703 -  and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
   2.704 -  and gcd_greatest_int = gcd_greatest [where ?'a = int]
   2.705 -
   2.706 -lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
   2.707 -  and dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
   2.708 -
   2.709 -lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
   2.710 -  and dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
   2.711 -
   2.712 -lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
   2.713 -  and Gcd_insert_nat = Gcd_insert [where ?'a = nat]
   2.714 -
   2.715 -lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
   2.716 -  and Gcd_insert_int = Gcd_insert [where ?'a = int]
   2.717  
   2.718  subsection \<open>gcd and lcm instances for @{typ integer}\<close>
   2.719  
   2.720 @@ -2224,4 +2031,177 @@
   2.721    and (Scala) "_.gcd'((_)')"
   2.722    \<comment> \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
   2.723  
   2.724 +text \<open>Some code equations\<close>
   2.725 +
   2.726 +lemma Lcm_set_nat [code, code_unfold]:
   2.727 +  "Lcm (set ns) = fold lcm ns (1::nat)"
   2.728 +  using Lcm_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   2.729 +
   2.730 +lemma Gcd_set_nat [code]:
   2.731 +  "Gcd (set ns) = fold gcd ns (0::nat)"
   2.732 +  using Gcd_set [of ns] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   2.733 +
   2.734 +lemma Lcm_set_int [code, code_unfold]:
   2.735 +  "Lcm (set xs) = fold lcm xs (1::int)"
   2.736 +  using Lcm_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   2.737 +
   2.738 +lemma Gcd_set_int [code]:
   2.739 +  "Gcd (set xs) = fold gcd xs (0::int)"
   2.740 +  using Gcd_set [of xs] by (simp_all add: fun_eq_iff ac_simps foldr_fold [symmetric])
   2.741 +
   2.742 +text \<open>Fact aliasses\<close>
   2.743 +
   2.744 +lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
   2.745 +  by (fact dvd_int_unfold_dvd_nat)
   2.746 +
   2.747 +lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
   2.748 +lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
   2.749 +lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
   2.750 +lemmas gcd_commute_int = gcd.commute [where ?'a = int]
   2.751 +lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
   2.752 +lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
   2.753 +lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   2.754 +lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   2.755 +lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
   2.756 +lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
   2.757 +lemmas gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
   2.758 +lemmas gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
   2.759 +lemmas gcd_greatest_nat = gcd_greatest [where ?'a = nat]
   2.760 +lemmas gcd_greatest_int = gcd_greatest [where ?'a = int]
   2.761 +lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
   2.762 +lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
   2.763 +lemmas gcd_greatest_iff_nat = gcd_greatest_iff [where ?'a = nat]
   2.764 +lemmas gcd_greatest_iff_int = gcd_greatest_iff [where ?'a = int]
   2.765 +lemmas gcd_zero_nat = gcd_eq_0_iff [where ?'a = nat]
   2.766 +lemmas gcd_zero_int = gcd_eq_0_iff [where ?'a = int]
   2.767 +
   2.768 +lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
   2.769 +lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
   2.770 +lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
   2.771 +lemmas lcm_commute_int = lcm.commute [where ?'a = int]
   2.772 +lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
   2.773 +lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
   2.774 +lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
   2.775 +lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
   2.776 +lemmas lcm_dvd1_nat = dvd_lcm1 [where ?'a = nat]
   2.777 +lemmas lcm_dvd1_int = dvd_lcm1 [where ?'a = int]
   2.778 +lemmas lcm_dvd2_nat = dvd_lcm2 [where ?'a = nat]
   2.779 +lemmas lcm_dvd2_int = dvd_lcm2 [where ?'a = int]
   2.780 +lemmas lcm_least_nat = lcm_least [where ?'a = nat]
   2.781 +lemmas lcm_least_int = lcm_least [where ?'a = int]
   2.782 +
   2.783 +lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
   2.784 +  by (fact lcm_eq_0_iff)
   2.785 +
   2.786 +lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   2.787 +  by (fact lcm_eq_0_iff)
   2.788 +
   2.789 +lemma dvd_lcm_I1_nat [simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
   2.790 +  by (fact dvd_lcmI1)
   2.791 +
   2.792 +lemma dvd_lcm_I2_nat [simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
   2.793 +  by (fact dvd_lcmI2)
   2.794 +
   2.795 +lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   2.796 +  by (fact dvd_lcmI1)
   2.797 +
   2.798 +lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   2.799 +  by (fact dvd_lcmI2)
   2.800 +
   2.801 +lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
   2.802 +lemmas coprime_mult_int = coprime_mult [where ?'a = int]
   2.803 +lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
   2.804 +lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
   2.805 +lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
   2.806 +lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
   2.807 +
   2.808 +lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   2.809 +    (k dvd m * n) = (k dvd m)"
   2.810 +  by (fact coprime_dvd_mult_iff)
   2.811 +
   2.812 +lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   2.813 +    (k dvd m * n) = (k dvd m)"
   2.814 +  by (fact coprime_dvd_mult_iff)
   2.815 +
   2.816 +lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   2.817 +  by (fact coprime_exp2)
   2.818 +
   2.819 +lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
   2.820 +  by (fact coprime_exp2)
   2.821 +
   2.822 +lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
   2.823 +lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
   2.824 +lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
   2.825 +lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
   2.826 +lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
   2.827 +lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
   2.828 +lemmas Gcd_insert_nat = Gcd_insert [where ?'a = nat]
   2.829 +lemmas Gcd_insert_int = Gcd_insert [where ?'a = int]
   2.830 +
   2.831 +lemma dvd_Lcm_int [simp]:
   2.832 +  fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   2.833 +  using assms by (fact dvd_Lcm)
   2.834 +
   2.835 +lemma Lcm_empty_nat:
   2.836 +  "Lcm {} = (1::nat)"
   2.837 +  by (fact Lcm_empty)
   2.838 +
   2.839 +lemma Lcm_empty_int:
   2.840 +  "Lcm {} = (1::int)"
   2.841 +  by (fact Lcm_empty)
   2.842 +
   2.843 +lemma Lcm_insert_nat:
   2.844 +  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   2.845 +  by (fact Lcm_insert)
   2.846 +
   2.847 +lemma Lcm_insert_int:
   2.848 +  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   2.849 +  by (fact Lcm_insert)
   2.850 +
   2.851 +lemma gcd_neg_numeral_1_int [simp]:
   2.852 +  "gcd (- numeral n :: int) x = gcd (numeral n) x"
   2.853 +  by (fact gcd_neg1_int)
   2.854 +
   2.855 +lemma gcd_neg_numeral_2_int [simp]:
   2.856 +  "gcd x (- numeral n :: int) = gcd x (numeral n)"
   2.857 +  by (fact gcd_neg2_int)
   2.858 +
   2.859 +lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   2.860 +  by (fact gcd_nat.absorb1)
   2.861 +
   2.862 +lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   2.863 +  by (fact gcd_nat.absorb2)
   2.864 +
   2.865 +lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.866 +  by (fact comp_fun_idem_gcd)
   2.867 +
   2.868 +lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   2.869 +  by (fact comp_fun_idem_gcd)
   2.870 +
   2.871 +lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.872 +  by (fact comp_fun_idem_lcm)
   2.873 +
   2.874 +lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   2.875 +  by (fact comp_fun_idem_lcm)
   2.876 +
   2.877 +interpretation dvd:
   2.878 +  order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
   2.879 +  by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
   2.880 +
   2.881 +interpretation gcd_semilattice_nat:
   2.882 +  semilattice_inf gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
   2.883 +  by standard (auto dest: dvd_antisym dvd_trans)
   2.884 +
   2.885 +interpretation lcm_semilattice_nat:
   2.886 +  semilattice_sup lcm Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n"
   2.887 +  by standard simp_all
   2.888 +
   2.889 +interpretation gcd_lcm_lattice_nat:
   2.890 +  lattice gcd Rings.dvd "\<lambda>m n::nat. m dvd n \<and> m \<noteq> n" lcm
   2.891 +  ..
   2.892 +
   2.893 +interpretation gcd_lcm_complete_lattice_nat:
   2.894 +  complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> m \<noteq> n" lcm 1 "0::nat"
   2.895 +  by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   2.896 +
   2.897  end
     3.1 --- a/src/HOL/Nat.thy	Wed Feb 17 21:51:56 2016 +0100
     3.2 +++ b/src/HOL/Nat.thy	Wed Feb 17 21:51:56 2016 +0100
     3.3 @@ -1934,11 +1934,6 @@
     3.4    unfolding dvd_def
     3.5    by (force dest: mult_eq_self_implies_10 simp add: mult.assoc)
     3.6  
     3.7 -text \<open>@{term "op dvd"} is a partial order\<close>
     3.8 -
     3.9 -interpretation dvd: order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> \<not> m dvd n"
    3.10 -  proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)
    3.11 -
    3.12  lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
    3.13  unfolding dvd_def
    3.14  by (blast intro: diff_mult_distrib2 [symmetric])