further generalization and polishing
authorhaftmann
Wed Feb 17 21:51:56 2016 +0100 (2016-02-17)
changeset 62345e66d7841d5a2
parent 62344 759d684c0e60
child 62346 97f2ed240431
further generalization and polishing
NEWS
src/HOL/GCD.thy
     1.1 --- a/NEWS	Wed Feb 17 21:51:56 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 17 21:51:56 2016 +0100
     1.3 @@ -35,6 +35,8 @@
     1.4  * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
     1.8 +
     1.9  
    1.10  New in Isabelle2016 (February 2016)
    1.11  -----------------------------------
     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 @@ -31,7 +31,7 @@
     2.4  imports Main
     2.5  begin
     2.6  
     2.7 -subsection \<open>GCD and LCM definitions\<close>
     2.8 +subsection \<open>Abstract GCD and LCM\<close>
     2.9  
    2.10  class gcd = zero + one + dvd +
    2.11    fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    2.12 @@ -67,6 +67,14 @@
    2.13    "b dvd c \<Longrightarrow> gcd a b dvd c"
    2.14    by (rule dvd_trans) (rule gcd_dvd2)
    2.15  
    2.16 +lemma dvd_gcdD1:
    2.17 +  "a dvd gcd b c \<Longrightarrow> a dvd b"
    2.18 +  using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
    2.19 +
    2.20 +lemma dvd_gcdD2:
    2.21 +  "a dvd gcd b c \<Longrightarrow> a dvd c"
    2.22 +  using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
    2.23 +
    2.24  lemma gcd_0_left [simp]:
    2.25    "gcd 0 a = normalize a"
    2.26    by (rule associated_eqI) simp_all
    2.27 @@ -203,6 +211,14 @@
    2.28    "a dvd c \<Longrightarrow> a dvd lcm b c"
    2.29    by (rule dvd_trans) (assumption, blast)
    2.30  
    2.31 +lemma lcm_dvdD1:
    2.32 +  "lcm a b dvd c \<Longrightarrow> a dvd c"
    2.33 +  using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
    2.34 +
    2.35 +lemma lcm_dvdD2:
    2.36 +  "lcm a b dvd c \<Longrightarrow> b dvd c"
    2.37 +  using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
    2.38 +
    2.39  lemma lcm_least:
    2.40    assumes "a dvd c" and "b dvd c"
    2.41    shows "lcm a b dvd c"
    2.42 @@ -350,16 +366,79 @@
    2.43    
    2.44  end
    2.45  
    2.46 +class ring_gcd = comm_ring_1 + semiring_gcd
    2.47 +
    2.48  class semiring_Gcd = semiring_gcd + Gcd +
    2.49    assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
    2.50      and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
    2.51      and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
    2.52 +  assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
    2.53 +    and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
    2.54 +    and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
    2.55  begin
    2.56  
    2.57 +lemma Lcm_Gcd:
    2.58 +  "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
    2.59 +  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
    2.60 +
    2.61 +lemma Gcd_Lcm:
    2.62 +  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
    2.63 +  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
    2.64 +
    2.65  lemma Gcd_empty [simp]:
    2.66    "Gcd {} = 0"
    2.67    by (rule dvd_0_left, rule Gcd_greatest) simp
    2.68  
    2.69 +lemma Lcm_empty [simp]:
    2.70 +  "Lcm {} = 1"
    2.71 +  by (auto intro: associated_eqI Lcm_least)
    2.72 +
    2.73 +lemma Gcd_insert [simp]:
    2.74 +  "Gcd (insert a A) = gcd a (Gcd A)"
    2.75 +proof -
    2.76 +  have "Gcd (insert a A) dvd gcd a (Gcd A)"
    2.77 +    by (auto intro: Gcd_dvd Gcd_greatest)
    2.78 +  moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
    2.79 +  proof (rule Gcd_greatest)
    2.80 +    fix b
    2.81 +    assume "b \<in> insert a A"
    2.82 +    then show "gcd a (Gcd A) dvd b"
    2.83 +    proof
    2.84 +      assume "b = a" then show ?thesis by simp
    2.85 +    next
    2.86 +      assume "b \<in> A"
    2.87 +      then have "Gcd A dvd b" by (rule Gcd_dvd)
    2.88 +      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
    2.89 +      ultimately show ?thesis by (blast intro: dvd_trans)
    2.90 +    qed
    2.91 +  qed
    2.92 +  ultimately show ?thesis
    2.93 +    by (auto intro: associated_eqI)
    2.94 +qed
    2.95 +
    2.96 +lemma Lcm_insert [simp]:
    2.97 +  "Lcm (insert a A) = lcm a (Lcm A)"
    2.98 +proof (rule sym)
    2.99 +  have "lcm a (Lcm A) dvd Lcm (insert a A)"
   2.100 +    by (auto intro: dvd_Lcm Lcm_least)
   2.101 +  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
   2.102 +  proof (rule Lcm_least)
   2.103 +    fix b
   2.104 +    assume "b \<in> insert a A"
   2.105 +    then show "b dvd lcm a (Lcm A)"
   2.106 +    proof
   2.107 +      assume "b = a" then show ?thesis by simp
   2.108 +    next
   2.109 +      assume "b \<in> A"
   2.110 +      then have "b dvd Lcm A" by (rule dvd_Lcm)
   2.111 +      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
   2.112 +      ultimately show ?thesis by (blast intro: dvd_trans)
   2.113 +    qed
   2.114 +  qed
   2.115 +  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   2.116 +    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   2.117 +qed
   2.118 +
   2.119  lemma Gcd_0_iff [simp]:
   2.120    "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
   2.121  proof
   2.122 @@ -384,147 +463,6 @@
   2.123    then show ?P by simp
   2.124  qed
   2.125  
   2.126 -lemma unit_factor_Gcd:
   2.127 -  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
   2.128 -proof (cases "Gcd A = 0")
   2.129 -  case True then show ?thesis by auto
   2.130 -next
   2.131 -  case False
   2.132 -  from unit_factor_mult_normalize
   2.133 -  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
   2.134 -  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
   2.135 -  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
   2.136 -  with False have "unit_factor (Gcd A) = 1" by simp
   2.137 -  with False show ?thesis by auto
   2.138 -qed
   2.139 -
   2.140 -lemma Gcd_UNIV [simp]:
   2.141 -  "Gcd UNIV = 1"
   2.142 -  by (rule associated_eqI) (auto intro: Gcd_dvd simp add: unit_factor_Gcd)
   2.143 -
   2.144 -lemma Gcd_eq_1_I:
   2.145 -  assumes "is_unit a" and "a \<in> A"
   2.146 -  shows "Gcd A = 1"
   2.147 -proof -
   2.148 -  from assms have "is_unit (Gcd A)"
   2.149 -    by (blast intro: Gcd_dvd dvd_unit_imp_unit)
   2.150 -  then have "normalize (Gcd A) = 1"
   2.151 -    by (rule is_unit_normalize)
   2.152 -  then show ?thesis
   2.153 -    by simp
   2.154 -qed
   2.155 -
   2.156 -lemma Gcd_insert [simp]:
   2.157 -  "Gcd (insert a A) = gcd a (Gcd A)"
   2.158 -proof -
   2.159 -  have "Gcd (insert a A) dvd gcd a (Gcd A)"
   2.160 -    by (auto intro: Gcd_dvd Gcd_greatest)
   2.161 -  moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
   2.162 -  proof (rule Gcd_greatest)
   2.163 -    fix b
   2.164 -    assume "b \<in> insert a A"
   2.165 -    then show "gcd a (Gcd A) dvd b"
   2.166 -    proof
   2.167 -      assume "b = a" then show ?thesis by simp
   2.168 -    next
   2.169 -      assume "b \<in> A"
   2.170 -      then have "Gcd A dvd b" by (rule Gcd_dvd)
   2.171 -      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
   2.172 -      ultimately show ?thesis by (blast intro: dvd_trans)
   2.173 -    qed
   2.174 -  qed
   2.175 -  ultimately show ?thesis
   2.176 -    by (auto intro: associated_eqI)
   2.177 -qed
   2.178 -
   2.179 -lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
   2.180 -  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
   2.181 -  by (blast intro: Gcd_greatest)
   2.182 -
   2.183 -lemma Gcd_set [code_unfold]:
   2.184 -  "Gcd (set as) = foldr gcd as 0"
   2.185 -  by (induct as) simp_all
   2.186 -
   2.187 -lemma Gcd_image_normalize [simp]:
   2.188 -  "Gcd (normalize ` A) = Gcd A"
   2.189 -proof -
   2.190 -  have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   2.191 -  proof -
   2.192 -    from that obtain B where "A = insert a B" by blast
   2.193 -    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
   2.194 -      by (rule gcd_dvd1)
   2.195 -    ultimately show "Gcd (normalize ` A) dvd a"
   2.196 -      by simp
   2.197 -  qed
   2.198 -  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
   2.199 -    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   2.200 -  then show ?thesis
   2.201 -    by (auto intro: associated_eqI)
   2.202 -qed
   2.203 -
   2.204 -end  
   2.205 -
   2.206 -class semiring_Lcm = semiring_Gcd +
   2.207 -  assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
   2.208 -begin
   2.209 -
   2.210 -lemma dvd_Lcm:
   2.211 -  assumes "a \<in> A"
   2.212 -  shows "a dvd Lcm A"
   2.213 -  using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
   2.214 -
   2.215 -lemma Lcm_least:
   2.216 -  assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
   2.217 -  shows "Lcm A dvd a"
   2.218 -  using assms by (auto intro: Gcd_dvd simp add: Lcm_Gcd)
   2.219 -
   2.220 -lemma normalize_Lcm [simp]:
   2.221 -  "normalize (Lcm A) = Lcm A"
   2.222 -  by (simp add: Lcm_Gcd)
   2.223 -
   2.224 -lemma unit_factor_Lcm:
   2.225 -  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   2.226 -proof (cases "Lcm A = 0")
   2.227 -  case True then show ?thesis by simp
   2.228 -next
   2.229 -  case False
   2.230 -  with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
   2.231 -    by blast
   2.232 -  with False show ?thesis
   2.233 -    by simp
   2.234 -qed
   2.235 -
   2.236 -lemma Gcd_Lcm:
   2.237 -  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   2.238 -  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   2.239 - 
   2.240 -lemma Lcm_empty [simp]:
   2.241 -  "Lcm {} = 1"
   2.242 -  by (simp add: Lcm_Gcd)
   2.243 -
   2.244 -lemma Lcm_insert [simp]:
   2.245 -  "Lcm (insert a A) = lcm a (Lcm A)"
   2.246 -proof (rule sym)
   2.247 -  have "lcm a (Lcm A) dvd Lcm (insert a A)"
   2.248 -    by (auto intro: dvd_Lcm Lcm_least)
   2.249 -  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
   2.250 -  proof (rule Lcm_least)
   2.251 -    fix b
   2.252 -    assume "b \<in> insert a A"
   2.253 -    then show "b dvd lcm a (Lcm A)"
   2.254 -    proof
   2.255 -      assume "b = a" then show ?thesis by simp
   2.256 -    next
   2.257 -      assume "b \<in> A"
   2.258 -      then have "b dvd Lcm A" by (rule dvd_Lcm)
   2.259 -      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
   2.260 -      ultimately show ?thesis by (blast intro: dvd_trans)
   2.261 -    qed
   2.262 -  qed
   2.263 -  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   2.264 -    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   2.265 -qed
   2.266 -
   2.267  lemma Lcm_1_iff [simp]:
   2.268    "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
   2.269  proof
   2.270 @@ -548,6 +486,44 @@
   2.271      by simp
   2.272  qed
   2.273  
   2.274 +lemma unit_factor_Gcd:
   2.275 +  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
   2.276 +proof (cases "Gcd A = 0")
   2.277 +  case True then show ?thesis by auto
   2.278 +next
   2.279 +  case False
   2.280 +  from unit_factor_mult_normalize
   2.281 +  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
   2.282 +  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
   2.283 +  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
   2.284 +  with False have "unit_factor (Gcd A) = 1" by simp
   2.285 +  with False show ?thesis by auto
   2.286 +qed
   2.287 +
   2.288 +lemma unit_factor_Lcm:
   2.289 +  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   2.290 +proof (cases "Lcm A = 0")
   2.291 +  case True then show ?thesis by simp
   2.292 +next
   2.293 +  case False
   2.294 +  with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
   2.295 +    by blast
   2.296 +  with False show ?thesis
   2.297 +    by simp
   2.298 +qed
   2.299 +
   2.300 +lemma Gcd_eq_1_I:
   2.301 +  assumes "is_unit a" and "a \<in> A"
   2.302 +  shows "Gcd A = 1"
   2.303 +proof -
   2.304 +  from assms have "is_unit (Gcd A)"
   2.305 +    by (blast intro: Gcd_dvd dvd_unit_imp_unit)
   2.306 +  then have "normalize (Gcd A) = 1"
   2.307 +    by (rule is_unit_normalize)
   2.308 +  then show ?thesis
   2.309 +    by simp
   2.310 +qed
   2.311 +
   2.312  lemma Lcm_eq_0_I:
   2.313    assumes "0 \<in> A"
   2.314    shows "Lcm A = 0"
   2.315 @@ -558,6 +534,10 @@
   2.316      by simp
   2.317  qed
   2.318  
   2.319 +lemma Gcd_UNIV [simp]:
   2.320 +  "Gcd UNIV = 1"
   2.321 +  using dvd_refl by (rule Gcd_eq_1_I) simp
   2.322 +
   2.323  lemma Lcm_UNIV [simp]:
   2.324    "Lcm UNIV = 0"
   2.325    by (rule Lcm_eq_0_I) simp
   2.326 @@ -573,25 +553,48 @@
   2.327        (auto simp add: lcm_eq_0_iff)
   2.328  qed
   2.329  
   2.330 +lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
   2.331 +  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
   2.332 +  by (blast intro: Gcd_greatest)
   2.333 +
   2.334 +lemma Gcd_set [code_unfold]:
   2.335 +  "Gcd (set as) = foldr gcd as 0"
   2.336 +  by (induct as) simp_all
   2.337 +
   2.338  lemma Lcm_set [code_unfold]:
   2.339    "Lcm (set as) = foldr lcm as 1"
   2.340    by (induct as) simp_all
   2.341 -  
   2.342 -end
   2.343  
   2.344 -class ring_gcd = comm_ring_1 + semiring_gcd
   2.345 +lemma Gcd_image_normalize [simp]:
   2.346 +  "Gcd (normalize ` A) = Gcd A"
   2.347 +proof -
   2.348 +  have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   2.349 +  proof -
   2.350 +    from that obtain B where "A = insert a B" by blast
   2.351 +    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
   2.352 +      by (rule gcd_dvd1)
   2.353 +    ultimately show "Gcd (normalize ` A) dvd a"
   2.354 +      by simp
   2.355 +  qed
   2.356 +  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
   2.357 +    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   2.358 +  then show ?thesis
   2.359 +    by (auto intro: associated_eqI)
   2.360 +qed
   2.361 +
   2.362 +end  
   2.363 +
   2.364 +
   2.365 +subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
   2.366  
   2.367  instantiation nat :: gcd
   2.368  begin
   2.369  
   2.370 -fun
   2.371 -  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.372 -where
   2.373 -  "gcd_nat x y =
   2.374 -   (if y = 0 then x else gcd y (x mod y))"
   2.375 +fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.376 +where "gcd_nat x y =
   2.377 +  (if y = 0 then x else gcd y (x mod y))"
   2.378  
   2.379 -definition
   2.380 -  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.381 +definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   2.382  where
   2.383    "lcm_nat x y = x * y div (gcd x y)"
   2.384  
   2.385 @@ -602,22 +605,17 @@
   2.386  instantiation int :: gcd
   2.387  begin
   2.388  
   2.389 -definition
   2.390 -  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   2.391 -where
   2.392 -  "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   2.393 +definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   2.394 +  where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   2.395  
   2.396 -definition
   2.397 -  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   2.398 -where
   2.399 -  "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   2.400 +definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   2.401 +  where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   2.402  
   2.403  instance ..
   2.404  
   2.405  end
   2.406  
   2.407 -
   2.408 -subsection \<open>Transfer setup\<close>
   2.409 +text \<open>Transfer setup\<close>
   2.410  
   2.411  lemma transfer_nat_int_gcd:
   2.412    "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   2.413 @@ -646,10 +644,6 @@
   2.414  declare transfer_morphism_int_nat[transfer add return:
   2.415      transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   2.416  
   2.417 -
   2.418 -subsection \<open>GCD properties\<close>
   2.419 -
   2.420 -(* was gcd_induct *)
   2.421  lemma gcd_nat_induct:
   2.422    fixes m n :: nat
   2.423    assumes "\<And>m. P m 0"
   2.424 @@ -722,11 +716,9 @@
   2.425  lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   2.426    by (simp add: lcm_int_def)
   2.427  
   2.428 -(* was gcd_0, etc. *)
   2.429  lemma gcd_0_nat: "gcd (x::nat) 0 = x"
   2.430    by simp
   2.431  
   2.432 -(* was igcd_0, etc. *)
   2.433  lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
   2.434    by (unfold gcd_int_def, auto)
   2.435  
   2.436 @@ -741,7 +733,7 @@
   2.437  
   2.438  (* weaker, but useful for the simplifier *)
   2.439  
   2.440 -lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   2.441 +lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   2.442    by simp
   2.443  
   2.444  lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   2.445 @@ -790,18 +782,6 @@
   2.446    by standard
   2.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)
   2.448  
   2.449 -lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   2.450 -  by (metis gcd_dvd1 dvd_trans)
   2.451 -
   2.452 -lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   2.453 -  by (metis gcd_dvd2 dvd_trans)
   2.454 -
   2.455 -lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   2.456 -  by (metis gcd_dvd1 dvd_trans)
   2.457 -
   2.458 -lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   2.459 -  by (metis gcd_dvd2 dvd_trans)
   2.460 -
   2.461  lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   2.462    by (rule dvd_imp_le, auto)
   2.463  
   2.464 @@ -1096,17 +1076,32 @@
   2.465    ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
   2.466  qed
   2.467  
   2.468 +lemma coprime:
   2.469 +  "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
   2.470 +proof
   2.471 +  assume ?P then show ?Q by auto
   2.472 +next
   2.473 +  assume ?Q
   2.474 +  then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b"
   2.475 +    by blast
   2.476 +  then have "is_unit (gcd a b)"
   2.477 +    by simp
   2.478 +  then show ?P
   2.479 +    by simp
   2.480 +qed
   2.481 +
   2.482  end
   2.483  
   2.484 -lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   2.485 -  using gcd_unique_nat[of 1 a b, simplified] by auto
   2.486 +lemma coprime_nat:
   2.487 +  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   2.488 +  using coprime [of a b] by simp
   2.489  
   2.490  lemma coprime_Suc_0_nat:
   2.491 -    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   2.492 +  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   2.493    using coprime_nat by simp
   2.494  
   2.495 -lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
   2.496 -    (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   2.497 +lemma coprime_int:
   2.498 +  "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   2.499    using gcd_unique_int [of 1 a b]
   2.500    apply clarsimp
   2.501    apply (erule subst)
   2.502 @@ -1136,7 +1131,6 @@
   2.503    assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
   2.504      b: "b = b' * gcd a b"
   2.505    shows    "coprime a' b'"
   2.506 -
   2.507    apply (subgoal_tac "a' = a div gcd a b")
   2.508    apply (erule ssubst)
   2.509    apply (subgoal_tac "b' = b div gcd a b")
   2.510 @@ -1709,7 +1703,7 @@
   2.511  qed
   2.512  
   2.513  
   2.514 -subsection \<open>LCM properties\<close>
   2.515 +subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
   2.516  
   2.517  lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   2.518    by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
   2.519 @@ -1808,13 +1802,13 @@
   2.520    by auto
   2.521  
   2.522  
   2.523 -subsection \<open>The complete divisibility lattice\<close>
   2.524 +subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
   2.525  
   2.526  text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
   2.527  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
   2.528  \<close>
   2.529  
   2.530 -instantiation nat :: Gcd
   2.531 +instantiation nat :: semiring_Gcd
   2.532  begin
   2.533  
   2.534  interpretation semilattice_neutr_set lcm "1::nat"
   2.535 @@ -1863,35 +1857,22 @@
   2.536  definition
   2.537    "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
   2.538  
   2.539 -instance ..
   2.540 -
   2.541 -end
   2.542 -
   2.543 -instance nat :: semiring_Gcd
   2.544 -proof
   2.545 +instance proof
   2.546    show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
   2.547    using that by (induct N rule: infinite_finite_induct)
   2.548      (auto simp add: Gcd_nat_def)
   2.549    show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
   2.550    using that by (induct N rule: infinite_finite_induct)
   2.551      (auto simp add: Gcd_nat_def)
   2.552 -qed simp
   2.553 -
   2.554 -instance nat :: semiring_Lcm
   2.555 -proof
   2.556 -  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
   2.557 -    by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
   2.558 -qed
   2.559 +  show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
   2.560 +  using that by (induct N rule: infinite_finite_induct)
   2.561 +    auto
   2.562 +  show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
   2.563 +  using that by (induct N rule: infinite_finite_induct)
   2.564 +    auto
   2.565 +qed simp_all
   2.566  
   2.567 -lemma Lcm_eq_0 [simp]:
   2.568 -  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
   2.569 -  by (rule Lcm_eq_0_I)
   2.570 -
   2.571 -lemma Lcm0_iff [simp]:
   2.572 -  fixes M :: "nat set"
   2.573 -  assumes "finite M" and "M \<noteq> {}"
   2.574 -  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
   2.575 -  using assms by (simp add: Lcm_0_iff)
   2.576 +end
   2.577  
   2.578  text\<open>Alternative characterizations of Gcd:\<close>
   2.579  
   2.580 @@ -1935,8 +1916,7 @@
   2.581  apply(rule antisym)
   2.582   apply(rule Max_ge, assumption)
   2.583   apply(erule (2) Lcm_in_lcm_closed_set_nat)
   2.584 -apply clarsimp
   2.585 -apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
   2.586 +apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
   2.587  done
   2.588  
   2.589  lemma mult_inj_if_coprime_nat:
   2.590 @@ -1956,7 +1936,7 @@
   2.591  
   2.592  subsubsection \<open>Setwise gcd and lcm for integers\<close>
   2.593  
   2.594 -instantiation int :: Gcd
   2.595 +instantiation int :: semiring_Gcd
   2.596  begin
   2.597  
   2.598  definition
   2.599 @@ -1965,63 +1945,45 @@
   2.600  definition
   2.601    "Gcd M = int (Gcd (nat ` abs ` M))"
   2.602  
   2.603 +instance by standard
   2.604 +  (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def
   2.605 +    Lcm_int_def int_dvd_iff dvd_int_iff dvd_int_unfold_dvd_nat [symmetric])
   2.606 +
   2.607 +end
   2.608 +
   2.609 +
   2.610 +subsection \<open>GCD and LCM on @{typ integer}\<close>
   2.611 +
   2.612 +instantiation integer :: gcd
   2.613 +begin
   2.614 +
   2.615 +context
   2.616 +  includes integer.lifting
   2.617 +begin
   2.618 +
   2.619 +lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   2.620 +  is gcd .
   2.621 +lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   2.622 +  is lcm .
   2.623 +
   2.624 +end
   2.625  instance ..
   2.626  
   2.627  end
   2.628  
   2.629 -instance int :: semiring_Gcd
   2.630 -  by standard (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def Lcm_int_def int_dvd_iff dvd_int_iff
   2.631 -    dvd_int_unfold_dvd_nat [symmetric])
   2.632 -
   2.633 -instance int :: semiring_Lcm
   2.634 -proof
   2.635 -  fix K :: "int set"
   2.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})"
   2.637 -  proof (rule set_eqI)
   2.638 -    fix n
   2.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")
   2.640 -    proof
   2.641 -      assume ?P
   2.642 -      then have "(\<forall>k\<in>K. k dvd int n) \<and> n = nat \<bar>int n\<bar>"
   2.643 -        by (auto simp add: dvd_int_unfold_dvd_nat)
   2.644 -      then show ?Q by blast
   2.645 -    next
   2.646 -      assume ?Q then show ?P
   2.647 -        by (auto simp add: dvd_int_unfold_dvd_nat)
   2.648 -    qed
   2.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}"
   2.650 -      by auto
   2.651 -  qed
   2.652 -  then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
   2.653 -    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd image_image)
   2.654 -qed
   2.655 -
   2.656 -lemma Lcm_dvd_int [simp]:
   2.657 -  fixes M :: "int set"
   2.658 -  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   2.659 -  using assms by (auto intro: Lcm_least)
   2.660 -
   2.661 -
   2.662 -subsection \<open>gcd and lcm instances for @{typ integer}\<close>
   2.663 -
   2.664 -instantiation integer :: gcd begin
   2.665 -context includes integer.lifting begin
   2.666 -lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
   2.667 -lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
   2.668 -end
   2.669 -instance ..
   2.670 -end
   2.671  lifting_update integer.lifting
   2.672  lifting_forget integer.lifting
   2.673  
   2.674 -context includes integer.lifting begin
   2.675 +context
   2.676 +  includes integer.lifting
   2.677 +begin
   2.678  
   2.679  lemma gcd_code_integer [code]:
   2.680    "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   2.681 -by transfer(fact gcd_code_int)
   2.682 +  by transfer (fact gcd_code_int)
   2.683  
   2.684  lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   2.685 -by transfer(fact lcm_altdef_int)
   2.686 +  by transfer (fact lcm_altdef_int)
   2.687  
   2.688  end
   2.689  
   2.690 @@ -2184,6 +2146,33 @@
   2.691  lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   2.692    by (fact comp_fun_idem_lcm)
   2.693  
   2.694 +lemma Lcm_eq_0 [simp]:
   2.695 +  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
   2.696 +  by (rule Lcm_eq_0_I)
   2.697 +
   2.698 +lemma Lcm0_iff [simp]:
   2.699 +  fixes M :: "nat set"
   2.700 +  assumes "finite M" and "M \<noteq> {}"
   2.701 +  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
   2.702 +  using assms by (simp add: Lcm_0_iff)
   2.703 +
   2.704 +lemma Lcm_dvd_int [simp]:
   2.705 +  fixes M :: "int set"
   2.706 +  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   2.707 +  using assms by (auto intro: Lcm_least)
   2.708 +
   2.709 +lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   2.710 +  by (fact dvd_gcdD1)
   2.711 +
   2.712 +lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   2.713 +  by (fact dvd_gcdD2)
   2.714 +
   2.715 +lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   2.716 +  by (fact dvd_gcdD1)
   2.717 +
   2.718 +lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   2.719 +  by (fact dvd_gcdD2)
   2.720 +
   2.721  interpretation dvd:
   2.722    order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
   2.723    by standard (auto intro: dvd_refl dvd_trans dvd_antisym)