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.327        (auto simp add: lcm_eq_0_iff)
   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.414  declare transfer_morphism_int_nat[transfer add return:
   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.426    by (simp add: lcm_int_def)
   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.548      (auto simp add: Gcd_nat_def)
   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.551      (auto simp add: Gcd_nat_def)
   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)