src/HOL/GCD.thy
 changeset 62345 e66d7841d5a2 parent 62344 759d684c0e60 child 62346 97f2ed240431
```     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 @@ -31,7 +31,7 @@
1.4  imports Main
1.5  begin
1.6
1.7 -subsection \<open>GCD and LCM definitions\<close>
1.8 +subsection \<open>Abstract GCD and LCM\<close>
1.9
1.10  class gcd = zero + one + dvd +
1.11    fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.12 @@ -67,6 +67,14 @@
1.13    "b dvd c \<Longrightarrow> gcd a b dvd c"
1.14    by (rule dvd_trans) (rule gcd_dvd2)
1.15
1.16 +lemma dvd_gcdD1:
1.17 +  "a dvd gcd b c \<Longrightarrow> a dvd b"
1.18 +  using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
1.19 +
1.20 +lemma dvd_gcdD2:
1.21 +  "a dvd gcd b c \<Longrightarrow> a dvd c"
1.22 +  using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
1.23 +
1.24  lemma gcd_0_left [simp]:
1.25    "gcd 0 a = normalize a"
1.26    by (rule associated_eqI) simp_all
1.27 @@ -203,6 +211,14 @@
1.28    "a dvd c \<Longrightarrow> a dvd lcm b c"
1.29    by (rule dvd_trans) (assumption, blast)
1.30
1.31 +lemma lcm_dvdD1:
1.32 +  "lcm a b dvd c \<Longrightarrow> a dvd c"
1.33 +  using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
1.34 +
1.35 +lemma lcm_dvdD2:
1.36 +  "lcm a b dvd c \<Longrightarrow> b dvd c"
1.37 +  using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
1.38 +
1.39  lemma lcm_least:
1.40    assumes "a dvd c" and "b dvd c"
1.41    shows "lcm a b dvd c"
1.42 @@ -350,16 +366,79 @@
1.43
1.44  end
1.45
1.46 +class ring_gcd = comm_ring_1 + semiring_gcd
1.47 +
1.48  class semiring_Gcd = semiring_gcd + Gcd +
1.49    assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
1.50      and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
1.51      and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
1.52 +  assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
1.53 +    and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
1.54 +    and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
1.55  begin
1.56
1.57 +lemma Lcm_Gcd:
1.58 +  "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
1.59 +  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
1.60 +
1.61 +lemma Gcd_Lcm:
1.62 +  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
1.63 +  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
1.64 +
1.65  lemma Gcd_empty [simp]:
1.66    "Gcd {} = 0"
1.67    by (rule dvd_0_left, rule Gcd_greatest) simp
1.68
1.69 +lemma Lcm_empty [simp]:
1.70 +  "Lcm {} = 1"
1.71 +  by (auto intro: associated_eqI Lcm_least)
1.72 +
1.73 +lemma Gcd_insert [simp]:
1.74 +  "Gcd (insert a A) = gcd a (Gcd A)"
1.75 +proof -
1.76 +  have "Gcd (insert a A) dvd gcd a (Gcd A)"
1.77 +    by (auto intro: Gcd_dvd Gcd_greatest)
1.78 +  moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
1.79 +  proof (rule Gcd_greatest)
1.80 +    fix b
1.81 +    assume "b \<in> insert a A"
1.82 +    then show "gcd a (Gcd A) dvd b"
1.83 +    proof
1.84 +      assume "b = a" then show ?thesis by simp
1.85 +    next
1.86 +      assume "b \<in> A"
1.87 +      then have "Gcd A dvd b" by (rule Gcd_dvd)
1.88 +      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
1.89 +      ultimately show ?thesis by (blast intro: dvd_trans)
1.90 +    qed
1.91 +  qed
1.92 +  ultimately show ?thesis
1.93 +    by (auto intro: associated_eqI)
1.94 +qed
1.95 +
1.96 +lemma Lcm_insert [simp]:
1.97 +  "Lcm (insert a A) = lcm a (Lcm A)"
1.98 +proof (rule sym)
1.99 +  have "lcm a (Lcm A) dvd Lcm (insert a A)"
1.100 +    by (auto intro: dvd_Lcm Lcm_least)
1.101 +  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
1.102 +  proof (rule Lcm_least)
1.103 +    fix b
1.104 +    assume "b \<in> insert a A"
1.105 +    then show "b dvd lcm a (Lcm A)"
1.106 +    proof
1.107 +      assume "b = a" then show ?thesis by simp
1.108 +    next
1.109 +      assume "b \<in> A"
1.110 +      then have "b dvd Lcm A" by (rule dvd_Lcm)
1.111 +      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
1.112 +      ultimately show ?thesis by (blast intro: dvd_trans)
1.113 +    qed
1.114 +  qed
1.115 +  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
1.116 +    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
1.117 +qed
1.118 +
1.119  lemma Gcd_0_iff [simp]:
1.120    "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
1.121  proof
1.122 @@ -384,147 +463,6 @@
1.123    then show ?P by simp
1.124  qed
1.125
1.126 -lemma unit_factor_Gcd:
1.127 -  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
1.128 -proof (cases "Gcd A = 0")
1.129 -  case True then show ?thesis by auto
1.130 -next
1.131 -  case False
1.132 -  from unit_factor_mult_normalize
1.133 -  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
1.134 -  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
1.135 -  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
1.136 -  with False have "unit_factor (Gcd A) = 1" by simp
1.137 -  with False show ?thesis by auto
1.138 -qed
1.139 -
1.140 -lemma Gcd_UNIV [simp]:
1.141 -  "Gcd UNIV = 1"
1.142 -  by (rule associated_eqI) (auto intro: Gcd_dvd simp add: unit_factor_Gcd)
1.143 -
1.144 -lemma Gcd_eq_1_I:
1.145 -  assumes "is_unit a" and "a \<in> A"
1.146 -  shows "Gcd A = 1"
1.147 -proof -
1.148 -  from assms have "is_unit (Gcd A)"
1.149 -    by (blast intro: Gcd_dvd dvd_unit_imp_unit)
1.150 -  then have "normalize (Gcd A) = 1"
1.151 -    by (rule is_unit_normalize)
1.152 -  then show ?thesis
1.153 -    by simp
1.154 -qed
1.155 -
1.156 -lemma Gcd_insert [simp]:
1.157 -  "Gcd (insert a A) = gcd a (Gcd A)"
1.158 -proof -
1.159 -  have "Gcd (insert a A) dvd gcd a (Gcd A)"
1.160 -    by (auto intro: Gcd_dvd Gcd_greatest)
1.161 -  moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
1.162 -  proof (rule Gcd_greatest)
1.163 -    fix b
1.164 -    assume "b \<in> insert a A"
1.165 -    then show "gcd a (Gcd A) dvd b"
1.166 -    proof
1.167 -      assume "b = a" then show ?thesis by simp
1.168 -    next
1.169 -      assume "b \<in> A"
1.170 -      then have "Gcd A dvd b" by (rule Gcd_dvd)
1.171 -      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
1.172 -      ultimately show ?thesis by (blast intro: dvd_trans)
1.173 -    qed
1.174 -  qed
1.175 -  ultimately show ?thesis
1.176 -    by (auto intro: associated_eqI)
1.177 -qed
1.178 -
1.179 -lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
1.180 -  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
1.181 -  by (blast intro: Gcd_greatest)
1.182 -
1.183 -lemma Gcd_set [code_unfold]:
1.184 -  "Gcd (set as) = foldr gcd as 0"
1.185 -  by (induct as) simp_all
1.186 -
1.187 -lemma Gcd_image_normalize [simp]:
1.188 -  "Gcd (normalize ` A) = Gcd A"
1.189 -proof -
1.190 -  have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
1.191 -  proof -
1.192 -    from that obtain B where "A = insert a B" by blast
1.193 -    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
1.194 -      by (rule gcd_dvd1)
1.195 -    ultimately show "Gcd (normalize ` A) dvd a"
1.196 -      by simp
1.197 -  qed
1.198 -  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
1.199 -    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
1.200 -  then show ?thesis
1.201 -    by (auto intro: associated_eqI)
1.202 -qed
1.203 -
1.204 -end
1.205 -
1.206 -class semiring_Lcm = semiring_Gcd +
1.207 -  assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
1.208 -begin
1.209 -
1.210 -lemma dvd_Lcm:
1.211 -  assumes "a \<in> A"
1.212 -  shows "a dvd Lcm A"
1.213 -  using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
1.214 -
1.215 -lemma Lcm_least:
1.216 -  assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
1.217 -  shows "Lcm A dvd a"
1.218 -  using assms by (auto intro: Gcd_dvd simp add: Lcm_Gcd)
1.219 -
1.220 -lemma normalize_Lcm [simp]:
1.221 -  "normalize (Lcm A) = Lcm A"
1.222 -  by (simp add: Lcm_Gcd)
1.223 -
1.224 -lemma unit_factor_Lcm:
1.225 -  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
1.226 -proof (cases "Lcm A = 0")
1.227 -  case True then show ?thesis by simp
1.228 -next
1.229 -  case False
1.230 -  with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
1.231 -    by blast
1.232 -  with False show ?thesis
1.233 -    by simp
1.234 -qed
1.235 -
1.236 -lemma Gcd_Lcm:
1.237 -  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
1.238 -  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
1.239 -
1.240 -lemma Lcm_empty [simp]:
1.241 -  "Lcm {} = 1"
1.242 -  by (simp add: Lcm_Gcd)
1.243 -
1.244 -lemma Lcm_insert [simp]:
1.245 -  "Lcm (insert a A) = lcm a (Lcm A)"
1.246 -proof (rule sym)
1.247 -  have "lcm a (Lcm A) dvd Lcm (insert a A)"
1.248 -    by (auto intro: dvd_Lcm Lcm_least)
1.249 -  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
1.250 -  proof (rule Lcm_least)
1.251 -    fix b
1.252 -    assume "b \<in> insert a A"
1.253 -    then show "b dvd lcm a (Lcm A)"
1.254 -    proof
1.255 -      assume "b = a" then show ?thesis by simp
1.256 -    next
1.257 -      assume "b \<in> A"
1.258 -      then have "b dvd Lcm A" by (rule dvd_Lcm)
1.259 -      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
1.260 -      ultimately show ?thesis by (blast intro: dvd_trans)
1.261 -    qed
1.262 -  qed
1.263 -  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
1.264 -    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
1.265 -qed
1.266 -
1.267  lemma Lcm_1_iff [simp]:
1.268    "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
1.269  proof
1.270 @@ -548,6 +486,44 @@
1.271      by simp
1.272  qed
1.273
1.274 +lemma unit_factor_Gcd:
1.275 +  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
1.276 +proof (cases "Gcd A = 0")
1.277 +  case True then show ?thesis by auto
1.278 +next
1.279 +  case False
1.280 +  from unit_factor_mult_normalize
1.281 +  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
1.282 +  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
1.283 +  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
1.284 +  with False have "unit_factor (Gcd A) = 1" by simp
1.285 +  with False show ?thesis by auto
1.286 +qed
1.287 +
1.288 +lemma unit_factor_Lcm:
1.289 +  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
1.290 +proof (cases "Lcm A = 0")
1.291 +  case True then show ?thesis by simp
1.292 +next
1.293 +  case False
1.294 +  with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
1.295 +    by blast
1.296 +  with False show ?thesis
1.297 +    by simp
1.298 +qed
1.299 +
1.300 +lemma Gcd_eq_1_I:
1.301 +  assumes "is_unit a" and "a \<in> A"
1.302 +  shows "Gcd A = 1"
1.303 +proof -
1.304 +  from assms have "is_unit (Gcd A)"
1.305 +    by (blast intro: Gcd_dvd dvd_unit_imp_unit)
1.306 +  then have "normalize (Gcd A) = 1"
1.307 +    by (rule is_unit_normalize)
1.308 +  then show ?thesis
1.309 +    by simp
1.310 +qed
1.311 +
1.312  lemma Lcm_eq_0_I:
1.313    assumes "0 \<in> A"
1.314    shows "Lcm A = 0"
1.315 @@ -558,6 +534,10 @@
1.316      by simp
1.317  qed
1.318
1.319 +lemma Gcd_UNIV [simp]:
1.320 +  "Gcd UNIV = 1"
1.321 +  using dvd_refl by (rule Gcd_eq_1_I) simp
1.322 +
1.323  lemma Lcm_UNIV [simp]:
1.324    "Lcm UNIV = 0"
1.325    by (rule Lcm_eq_0_I) simp
1.326 @@ -573,25 +553,48 @@
1.328  qed
1.329
1.330 +lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
1.331 +  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
1.332 +  by (blast intro: Gcd_greatest)
1.333 +
1.334 +lemma Gcd_set [code_unfold]:
1.335 +  "Gcd (set as) = foldr gcd as 0"
1.336 +  by (induct as) simp_all
1.337 +
1.338  lemma Lcm_set [code_unfold]:
1.339    "Lcm (set as) = foldr lcm as 1"
1.340    by (induct as) simp_all
1.341 -
1.342 -end
1.343
1.344 -class ring_gcd = comm_ring_1 + semiring_gcd
1.345 +lemma Gcd_image_normalize [simp]:
1.346 +  "Gcd (normalize ` A) = Gcd A"
1.347 +proof -
1.348 +  have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
1.349 +  proof -
1.350 +    from that obtain B where "A = insert a B" by blast
1.351 +    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
1.352 +      by (rule gcd_dvd1)
1.353 +    ultimately show "Gcd (normalize ` A) dvd a"
1.354 +      by simp
1.355 +  qed
1.356 +  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
1.357 +    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
1.358 +  then show ?thesis
1.359 +    by (auto intro: associated_eqI)
1.360 +qed
1.361 +
1.362 +end
1.363 +
1.364 +
1.365 +subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
1.366
1.367  instantiation nat :: gcd
1.368  begin
1.369
1.370 -fun
1.371 -  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.372 -where
1.373 -  "gcd_nat x y =
1.374 -   (if y = 0 then x else gcd y (x mod y))"
1.375 +fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.376 +where "gcd_nat x y =
1.377 +  (if y = 0 then x else gcd y (x mod y))"
1.378
1.379 -definition
1.380 -  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.381 +definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
1.382  where
1.383    "lcm_nat x y = x * y div (gcd x y)"
1.384
1.385 @@ -602,22 +605,17 @@
1.386  instantiation int :: gcd
1.387  begin
1.388
1.389 -definition
1.390 -  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
1.391 -where
1.392 -  "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1.393 +definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
1.394 +  where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1.395
1.396 -definition
1.397 -  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
1.398 -where
1.399 -  "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1.400 +definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
1.401 +  where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
1.402
1.403  instance ..
1.404
1.405  end
1.406
1.407 -
1.408 -subsection \<open>Transfer setup\<close>
1.409 +text \<open>Transfer setup\<close>
1.410
1.411  lemma transfer_nat_int_gcd:
1.412    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
1.413 @@ -646,10 +644,6 @@
1.415      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
1.416
1.417 -
1.418 -subsection \<open>GCD properties\<close>
1.419 -
1.420 -(* was gcd_induct *)
1.421  lemma gcd_nat_induct:
1.422    fixes m n :: nat
1.423    assumes "\<And>m. P m 0"
1.424 @@ -722,11 +716,9 @@
1.425  lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
1.427
1.428 -(* was gcd_0, etc. *)
1.429  lemma gcd_0_nat: "gcd (x::nat) 0 = x"
1.430    by simp
1.431
1.432 -(* was igcd_0, etc. *)
1.433  lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
1.434    by (unfold gcd_int_def, auto)
1.435
1.436 @@ -741,7 +733,7 @@
1.437
1.438  (* weaker, but useful for the simplifier *)
1.439
1.440 -lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
1.441 +lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
1.442    by simp
1.443
1.444  lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
1.445 @@ -790,18 +782,6 @@
1.446    by standard
1.447      (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
1.448
1.449 -lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
1.450 -  by (metis gcd_dvd1 dvd_trans)
1.451 -
1.452 -lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
1.453 -  by (metis gcd_dvd2 dvd_trans)
1.454 -
1.455 -lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
1.456 -  by (metis gcd_dvd1 dvd_trans)
1.457 -
1.458 -lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
1.459 -  by (metis gcd_dvd2 dvd_trans)
1.460 -
1.461  lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
1.462    by (rule dvd_imp_le, auto)
1.463
1.464 @@ -1096,17 +1076,32 @@
1.465    ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
1.466  qed
1.467
1.468 +lemma coprime:
1.469 +  "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
1.470 +proof
1.471 +  assume ?P then show ?Q by auto
1.472 +next
1.473 +  assume ?Q
1.474 +  then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b"
1.475 +    by blast
1.476 +  then have "is_unit (gcd a b)"
1.477 +    by simp
1.478 +  then show ?P
1.479 +    by simp
1.480 +qed
1.481 +
1.482  end
1.483
1.484 -lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.485 -  using gcd_unique_nat[of 1 a b, simplified] by auto
1.486 +lemma coprime_nat:
1.487 +  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.488 +  using coprime [of a b] by simp
1.489
1.490  lemma coprime_Suc_0_nat:
1.491 -    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
1.492 +  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
1.493    using coprime_nat by simp
1.494
1.495 -lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
1.496 -    (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.497 +lemma coprime_int:
1.498 +  "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
1.499    using gcd_unique_int [of 1 a b]
1.500    apply clarsimp
1.501    apply (erule subst)
1.502 @@ -1136,7 +1131,6 @@
1.503    assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
1.504      b: "b = b' * gcd a b"
1.505    shows    "coprime a' b'"
1.506 -
1.507    apply (subgoal_tac "a' = a div gcd a b")
1.508    apply (erule ssubst)
1.509    apply (subgoal_tac "b' = b div gcd a b")
1.510 @@ -1709,7 +1703,7 @@
1.511  qed
1.512
1.513
1.514 -subsection \<open>LCM properties\<close>
1.515 +subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
1.516
1.517  lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
1.518    by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
1.519 @@ -1808,13 +1802,13 @@
1.520    by auto
1.521
1.522
1.523 -subsection \<open>The complete divisibility lattice\<close>
1.524 +subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
1.525
1.526  text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
1.527  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
1.528  \<close>
1.529
1.530 -instantiation nat :: Gcd
1.531 +instantiation nat :: semiring_Gcd
1.532  begin
1.533
1.534  interpretation semilattice_neutr_set lcm "1::nat"
1.535 @@ -1863,35 +1857,22 @@
1.536  definition
1.537    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
1.538
1.539 -instance ..
1.540 -
1.541 -end
1.542 -
1.543 -instance nat :: semiring_Gcd
1.544 -proof
1.545 +instance proof
1.546    show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
1.547    using that by (induct N rule: infinite_finite_induct)
1.549    show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
1.550    using that by (induct N rule: infinite_finite_induct)
1.552 -qed simp
1.553 -
1.554 -instance nat :: semiring_Lcm
1.555 -proof
1.556 -  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
1.557 -    by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
1.558 -qed
1.559 +  show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
1.560 +  using that by (induct N rule: infinite_finite_induct)
1.561 +    auto
1.562 +  show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
1.563 +  using that by (induct N rule: infinite_finite_induct)
1.564 +    auto
1.565 +qed simp_all
1.566
1.567 -lemma Lcm_eq_0 [simp]:
1.568 -  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
1.569 -  by (rule Lcm_eq_0_I)
1.570 -
1.571 -lemma Lcm0_iff [simp]:
1.572 -  fixes M :: "nat set"
1.573 -  assumes "finite M" and "M \<noteq> {}"
1.574 -  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
1.575 -  using assms by (simp add: Lcm_0_iff)
1.576 +end
1.577
1.578  text\<open>Alternative characterizations of Gcd:\<close>
1.579
1.580 @@ -1935,8 +1916,7 @@
1.581  apply(rule antisym)
1.582   apply(rule Max_ge, assumption)
1.583   apply(erule (2) Lcm_in_lcm_closed_set_nat)
1.584 -apply clarsimp
1.585 -apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
1.586 +apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
1.587  done
1.588
1.589  lemma mult_inj_if_coprime_nat:
1.590 @@ -1956,7 +1936,7 @@
1.591
1.592  subsubsection \<open>Setwise gcd and lcm for integers\<close>
1.593
1.594 -instantiation int :: Gcd
1.595 +instantiation int :: semiring_Gcd
1.596  begin
1.597
1.598  definition
1.599 @@ -1965,63 +1945,45 @@
1.600  definition
1.601    "Gcd M = int (Gcd (nat ` abs ` M))"
1.602
1.603 +instance by standard
1.604 +  (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
1.605 +    Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
1.606 +
1.607 +end
1.608 +
1.609 +
1.610 +subsection \<open>GCD and LCM on @{typ integer}\<close>
1.611 +
1.612 +instantiation integer :: gcd
1.613 +begin
1.614 +
1.615 +context
1.616 +  includes integer.lifting
1.617 +begin
1.618 +
1.619 +lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
1.620 +  is gcd .
1.621 +lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
1.622 +  is lcm .
1.623 +
1.624 +end
1.625  instance ..
1.626
1.627  end
1.628
1.629 -instance int :: semiring_Gcd
1.630 -  by standard (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def Lcm_int_def int_dvd_iff dvd_int_iff
1.631 -    dvd_int_unfold_dvd_nat [symmetric])
1.632 -
1.633 -instance int :: semiring_Lcm
1.634 -proof
1.635 -  fix K :: "int set"
1.636 -  have "{n. \<forall>k\<in>K. nat \<bar>k\<bar> dvd n} = ((\<lambda>k. nat \<bar>k\<bar>) ` {l. \<forall>k\<in>K. k dvd l})"
1.637 -  proof (rule set_eqI)
1.638 -    fix n
1.639 -    have "(\<forall>k\<in>K. nat \<bar>k\<bar> dvd n) \<longleftrightarrow> (\<exists>l. (\<forall>k\<in>K. k dvd l) \<and> n = nat \<bar>l\<bar>)" (is "?P \<longleftrightarrow> ?Q")
1.640 -    proof
1.641 -      assume ?P
1.642 -      then have "(\<forall>k\<in>K. k dvd int n) \<and> n = nat \<bar>int n\<bar>"
1.643 -        by (auto simp add: dvd_int_unfold_dvd_nat)
1.644 -      then show ?Q by blast
1.645 -    next
1.646 -      assume ?Q then show ?P
1.647 -        by (auto simp add: dvd_int_unfold_dvd_nat)
1.648 -    qed
1.649 -    then show "n \<in> {n. \<forall>k\<in>K. nat \<bar>k\<bar> dvd n} \<longleftrightarrow> n \<in> (\<lambda>k. nat \<bar>k\<bar>) ` {l. \<forall>k\<in>K. k dvd l}"
1.650 -      by auto
1.651 -  qed
1.652 -  then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
1.653 -    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd image_image)
1.654 -qed
1.655 -
1.656 -lemma Lcm_dvd_int [simp]:
1.657 -  fixes M :: "int set"
1.658 -  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
1.659 -  using assms by (auto intro: Lcm_least)
1.660 -
1.661 -
1.662 -subsection \<open>gcd and lcm instances for @{typ integer}\<close>
1.663 -
1.664 -instantiation integer :: gcd begin
1.665 -context includes integer.lifting begin
1.666 -lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
1.667 -lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
1.668 -end
1.669 -instance ..
1.670 -end
1.671  lifting_update integer.lifting
1.672  lifting_forget integer.lifting
1.673
1.674 -context includes integer.lifting begin
1.675 +context
1.676 +  includes integer.lifting
1.677 +begin
1.678
1.679  lemma gcd_code_integer [code]:
1.680    "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
1.681 -by transfer(fact gcd_code_int)
1.682 +  by transfer (fact gcd_code_int)
1.683
1.684  lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
1.685 -by transfer(fact lcm_altdef_int)
1.686 +  by transfer (fact lcm_altdef_int)
1.687
1.688  end
1.689
1.690 @@ -2184,6 +2146,33 @@
1.691  lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
1.692    by (fact comp_fun_idem_lcm)
1.693
1.694 +lemma Lcm_eq_0 [simp]:
1.695 +  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
1.696 +  by (rule Lcm_eq_0_I)
1.697 +
1.698 +lemma Lcm0_iff [simp]:
1.699 +  fixes M :: "nat set"
1.700 +  assumes "finite M" and "M \<noteq> {}"
1.701 +  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
1.702 +  using assms by (simp add: Lcm_0_iff)
1.703 +
1.704 +lemma Lcm_dvd_int [simp]:
1.705 +  fixes M :: "int set"
1.706 +  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
1.707 +  using assms by (auto intro: Lcm_least)
1.708 +
1.709 +lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
1.710 +  by (fact dvd_gcdD1)
1.711 +
1.712 +lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
1.713 +  by (fact dvd_gcdD2)
1.714 +
1.715 +lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
1.716 +  by (fact dvd_gcdD1)
1.717 +
1.718 +lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
1.719 +  by (fact dvd_gcdD2)
1.720 +
1.721  interpretation dvd:
1.722    order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
1.723    by standard (auto intro: dvd_refl dvd_trans dvd_antisym)
```