src/HOL/GCD.thy
author wenzelm
Mon Dec 28 19:23:15 2015 +0100 (2015-12-28)
changeset 61954 1d43f86f48be
parent 61944 5d06ecfdb472
child 61975 b4b11391c676
permissions -rw-r--r--
more symbols;
     1 (*  Authors:    Christophe Tabacznyj, Lawrence C. Paulson, Amine Chaieb,
     2                 Thomas M. Rasmussen, Jeremy Avigad, Tobias Nipkow
     3 
     4 
     5 This file deals with the functions gcd and lcm.  Definitions and
     6 lemmas are proved uniformly for the natural numbers and integers.
     7 
     8 This file combines and revises a number of prior developments.
     9 
    10 The original theories "GCD" and "Primes" were by Christophe Tabacznyj
    11 and Lawrence C. Paulson, based on @{cite davenport92}. They introduced
    12 gcd, lcm, and prime for the natural numbers.
    13 
    14 The original theory "IntPrimes" was by Thomas M. Rasmussen, and
    15 extended gcd, lcm, primes to the integers. Amine Chaieb provided
    16 another extension of the notions to the integers, and added a number
    17 of results to "Primes" and "GCD". IntPrimes also defined and developed
    18 the congruence relations on the integers. The notion was extended to
    19 the natural numbers by Chaieb.
    20 
    21 Jeremy Avigad combined all of these, made everything uniform for the
    22 natural numbers and the integers, and added a number of new theorems.
    23 
    24 Tobias Nipkow cleaned up a lot.
    25 *)
    26 
    27 
    28 section \<open>Greatest common divisor and least common multiple\<close>
    29 
    30 theory GCD
    31 imports Main
    32 begin
    33 
    34 subsection \<open>GCD and LCM definitions\<close>
    35 
    36 class gcd = zero + one + dvd +
    37   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    38     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    39 begin
    40 
    41 abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    42   where "coprime x y \<equiv> gcd x y = 1"
    43 
    44 end
    45 
    46 class Gcd = gcd +
    47   fixes Gcd :: "'a set \<Rightarrow> 'a"
    48     and Lcm :: "'a set \<Rightarrow> 'a"
    49 
    50 class semiring_gcd = normalization_semidom + gcd +
    51   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
    52     and gcd_dvd2 [iff]: "gcd a b dvd b"
    53     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
    54     and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
    55     and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
    56 begin    
    57 
    58 lemma gcd_greatest_iff [simp]:
    59   "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
    60   by (blast intro!: gcd_greatest intro: dvd_trans)
    61 
    62 lemma gcd_dvdI1:
    63   "a dvd c \<Longrightarrow> gcd a b dvd c"
    64   by (rule dvd_trans) (rule gcd_dvd1)
    65 
    66 lemma gcd_dvdI2:
    67   "b dvd c \<Longrightarrow> gcd a b dvd c"
    68   by (rule dvd_trans) (rule gcd_dvd2)
    69 
    70 lemma gcd_0_left [simp]:
    71   "gcd 0 a = normalize a"
    72   by (rule associated_eqI) simp_all
    73 
    74 lemma gcd_0_right [simp]:
    75   "gcd a 0 = normalize a"
    76   by (rule associated_eqI) simp_all
    77   
    78 lemma gcd_eq_0_iff [simp]:
    79   "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
    80 proof
    81   assume ?P then have "0 dvd gcd a b" by simp
    82   then have "0 dvd a" and "0 dvd b" by (blast intro: dvd_trans)+
    83   then show ?Q by simp
    84 next
    85   assume ?Q then show ?P by simp
    86 qed
    87 
    88 lemma unit_factor_gcd:
    89   "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
    90 proof (cases "gcd a b = 0")
    91   case True then show ?thesis by simp
    92 next
    93   case False
    94   have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
    95     by (rule unit_factor_mult_normalize)
    96   then have "unit_factor (gcd a b) * gcd a b = gcd a b"
    97     by simp
    98   then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
    99     by simp
   100   with False show ?thesis by simp
   101 qed
   102 
   103 lemma is_unit_gcd [simp]:
   104   "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
   105   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
   106 
   107 sublocale gcd: abel_semigroup gcd
   108 proof
   109   fix a b c
   110   show "gcd a b = gcd b a"
   111     by (rule associated_eqI) simp_all
   112   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
   113     by (rule dvd_trans) simp
   114   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
   115     by (rule dvd_trans) simp
   116   ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
   117     by (auto intro!: gcd_greatest)
   118   from gcd_dvd2 have "gcd a (gcd b c) dvd b"
   119     by (rule dvd_trans) simp
   120   moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
   121     by (rule dvd_trans) simp
   122   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
   123     by (auto intro!: gcd_greatest)
   124   from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
   125     by (rule associated_eqI) simp_all
   126 qed
   127 
   128 lemma gcd_self [simp]:
   129   "gcd a a = normalize a"
   130 proof -
   131   have "a dvd gcd a a"
   132     by (rule gcd_greatest) simp_all
   133   then show ?thesis
   134     by (auto intro: associated_eqI)
   135 qed
   136 
   137 lemma gcd_left_idem [simp]:
   138   "gcd a (gcd a b) = gcd a b"
   139   by (auto intro: associated_eqI)
   140 
   141 lemma gcd_right_idem [simp]:
   142   "gcd (gcd a b) b = gcd a b"
   143   unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
   144 
   145 lemma coprime_1_left [simp]:
   146   "coprime 1 a"
   147   by (rule associated_eqI) simp_all
   148 
   149 lemma coprime_1_right [simp]:
   150   "coprime a 1"
   151   using coprime_1_left [of a] by (simp add: ac_simps)
   152 
   153 lemma gcd_mult_left:
   154   "gcd (c * a) (c * b) = normalize c * gcd a b"
   155 proof (cases "c = 0")
   156   case True then show ?thesis by simp
   157 next
   158   case False
   159   then have "c * gcd a b dvd gcd (c * a) (c * b)"
   160     by (auto intro: gcd_greatest)
   161   moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
   162     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   163   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
   164     by (auto intro: associated_eqI)
   165   then show ?thesis by (simp add: normalize_mult)
   166 qed
   167 
   168 lemma gcd_mult_right:
   169   "gcd (a * c) (b * c) = gcd b a * normalize c"
   170   using gcd_mult_left [of c a b] by (simp add: ac_simps)
   171 
   172 lemma mult_gcd_left:
   173   "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
   174   by (simp add: gcd_mult_left mult.assoc [symmetric])
   175 
   176 lemma mult_gcd_right:
   177   "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
   178   using mult_gcd_left [of c a b] by (simp add: ac_simps)
   179 
   180 lemma dvd_lcm1 [iff]:
   181   "a dvd lcm a b"
   182 proof -
   183   have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
   184     by (simp add: lcm_gcd normalize_mult div_mult_swap)
   185   then show ?thesis
   186     by (simp add: lcm_gcd)
   187 qed
   188   
   189 lemma dvd_lcm2 [iff]:
   190   "b dvd lcm a b"
   191 proof -
   192   have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
   193     by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
   194   then show ?thesis
   195     by (simp add: lcm_gcd)
   196 qed
   197 
   198 lemma dvd_lcmI1:
   199   "a dvd b \<Longrightarrow> a dvd lcm b c"
   200   by (rule dvd_trans) (assumption, blast) 
   201 
   202 lemma dvd_lcmI2:
   203   "a dvd c \<Longrightarrow> a dvd lcm b c"
   204   by (rule dvd_trans) (assumption, blast)
   205 
   206 lemma lcm_least:
   207   assumes "a dvd c" and "b dvd c"
   208   shows "lcm a b dvd c"
   209 proof (cases "c = 0")
   210   case True then show ?thesis by simp
   211 next
   212   case False then have U: "is_unit (unit_factor c)" by simp
   213   show ?thesis
   214   proof (cases "gcd a b = 0")
   215     case True with assms show ?thesis by simp
   216   next
   217     case False then have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
   218     with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
   219       by (simp_all add: mult_dvd_mono)
   220     then have "normalize (a * b) dvd gcd (a * c) (b * c)"
   221       by (auto intro: gcd_greatest simp add: ac_simps)
   222     then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
   223       using U by (simp add: dvd_mult_unit_iff)
   224     then have "normalize (a * b) dvd gcd a b * c"
   225       by (simp add: mult_gcd_right [of a b c])
   226     then have "normalize (a * b) div gcd a b dvd c"
   227       using False by (simp add: div_dvd_iff_mult ac_simps)
   228     then show ?thesis by (simp add: lcm_gcd)
   229   qed
   230 qed
   231 
   232 lemma lcm_least_iff [simp]:
   233   "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
   234   by (blast intro!: lcm_least intro: dvd_trans)
   235 
   236 lemma normalize_lcm [simp]:
   237   "normalize (lcm a b) = lcm a b"
   238   by (simp add: lcm_gcd dvd_normalize_div)
   239 
   240 lemma lcm_0_left [simp]:
   241   "lcm 0 a = 0"
   242   by (simp add: lcm_gcd)
   243   
   244 lemma lcm_0_right [simp]:
   245   "lcm a 0 = 0"
   246   by (simp add: lcm_gcd)
   247 
   248 lemma lcm_eq_0_iff:
   249   "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" (is "?P \<longleftrightarrow> ?Q")
   250 proof
   251   assume ?P then have "0 dvd lcm a b" by simp
   252   then have "0 dvd normalize (a * b) div gcd a b"
   253     by (simp add: lcm_gcd)
   254   then have "0 * gcd a b dvd normalize (a * b)"
   255     using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
   256   then have "normalize (a * b) = 0"
   257     by simp
   258   then show ?Q by simp
   259 next
   260   assume ?Q then show ?P by auto
   261 qed
   262 
   263 lemma lcm_eq_1_iff [simp]:
   264   "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
   265   by (auto intro: associated_eqI)
   266 
   267 lemma unit_factor_lcm :
   268   "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
   269   by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
   270 
   271 sublocale lcm: abel_semigroup lcm
   272 proof
   273   fix a b c
   274   show "lcm a b = lcm b a"
   275     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
   276   have "lcm (lcm a b) c dvd lcm a (lcm b c)"
   277     and "lcm a (lcm b c) dvd lcm (lcm a b) c"
   278     by (auto intro: lcm_least
   279       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
   280       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
   281       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
   282       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   283   then show "lcm (lcm a b) c = lcm a (lcm b c)"
   284     by (rule associated_eqI) simp_all
   285 qed
   286 
   287 lemma lcm_self [simp]:
   288   "lcm a a = normalize a"
   289 proof -
   290   have "lcm a a dvd a"
   291     by (rule lcm_least) simp_all
   292   then show ?thesis
   293     by (auto intro: associated_eqI)
   294 qed
   295 
   296 lemma lcm_left_idem [simp]:
   297   "lcm a (lcm a b) = lcm a b"
   298   by (auto intro: associated_eqI)
   299 
   300 lemma lcm_right_idem [simp]:
   301   "lcm (lcm a b) b = lcm a b"
   302   unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
   303 
   304 lemma gcd_mult_lcm [simp]:
   305   "gcd a b * lcm a b = normalize a * normalize b"
   306   by (simp add: lcm_gcd normalize_mult)
   307 
   308 lemma lcm_mult_gcd [simp]:
   309   "lcm a b * gcd a b = normalize a * normalize b"
   310   using gcd_mult_lcm [of a b] by (simp add: ac_simps) 
   311 
   312 lemma gcd_lcm:
   313   assumes "a \<noteq> 0" and "b \<noteq> 0"
   314   shows "gcd a b = normalize (a * b) div lcm a b"
   315 proof -
   316   from assms have "lcm a b \<noteq> 0"
   317     by (simp add: lcm_eq_0_iff)
   318   have "gcd a b * lcm a b = normalize a * normalize b" by simp
   319   then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
   320     by (simp_all add: normalize_mult)
   321   with \<open>lcm a b \<noteq> 0\<close> show ?thesis
   322     using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
   323 qed
   324 
   325 lemma lcm_1_left [simp]:
   326   "lcm 1 a = normalize a"
   327   by (simp add: lcm_gcd)
   328 
   329 lemma lcm_1_right [simp]:
   330   "lcm a 1 = normalize a"
   331   by (simp add: lcm_gcd)
   332   
   333 lemma lcm_mult_left:
   334   "lcm (c * a) (c * b) = normalize c * lcm a b"
   335   by (cases "c = 0")
   336     (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
   337       simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
   338 
   339 lemma lcm_mult_right:
   340   "lcm (a * c) (b * c) = lcm b a * normalize c"
   341   using lcm_mult_left [of c a b] by (simp add: ac_simps)
   342 
   343 lemma mult_lcm_left:
   344   "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
   345   by (simp add: lcm_mult_left mult.assoc [symmetric])
   346 
   347 lemma mult_lcm_right:
   348   "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
   349   using mult_lcm_left [of c a b] by (simp add: ac_simps)
   350   
   351 end
   352 
   353 class semiring_Gcd = semiring_gcd + Gcd +
   354   assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
   355     and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
   356     and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
   357 begin
   358 
   359 lemma Gcd_empty [simp]:
   360   "Gcd {} = 0"
   361   by (rule dvd_0_left, rule Gcd_greatest) simp
   362 
   363 lemma Gcd_0_iff [simp]:
   364   "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
   365 proof
   366   assume ?P
   367   show ?Q
   368   proof
   369     fix a
   370     assume "a \<in> A"
   371     then have "Gcd A dvd a" by (rule Gcd_dvd)
   372     with \<open>?P\<close> have "a = 0" by simp
   373     then show "a \<in> {0}" by simp
   374   qed
   375 next
   376   assume ?Q
   377   have "0 dvd Gcd A"
   378   proof (rule Gcd_greatest)
   379     fix a
   380     assume "a \<in> A"
   381     with \<open>?Q\<close> have "a = 0" by auto
   382     then show "0 dvd a" by simp
   383   qed
   384   then show ?P by simp
   385 qed
   386 
   387 lemma unit_factor_Gcd:
   388   "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
   389 proof (cases "Gcd A = 0")
   390   case True then show ?thesis by auto
   391 next
   392   case False
   393   from unit_factor_mult_normalize
   394   have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
   395   then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
   396   then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
   397   with False have "unit_factor (Gcd A) = 1" by simp
   398   with False show ?thesis by auto
   399 qed
   400 
   401 lemma Gcd_UNIV [simp]:
   402   "Gcd UNIV = 1"
   403   by (rule associated_eqI) (auto intro: Gcd_dvd simp add: unit_factor_Gcd)
   404 
   405 lemma Gcd_eq_1_I:
   406   assumes "is_unit a" and "a \<in> A"
   407   shows "Gcd A = 1"
   408 proof -
   409   from assms have "is_unit (Gcd A)"
   410     by (blast intro: Gcd_dvd dvd_unit_imp_unit)
   411   then have "normalize (Gcd A) = 1"
   412     by (rule is_unit_normalize)
   413   then show ?thesis
   414     by simp
   415 qed
   416 
   417 lemma Gcd_insert [simp]:
   418   "Gcd (insert a A) = gcd a (Gcd A)"
   419 proof -
   420   have "Gcd (insert a A) dvd gcd a (Gcd A)"
   421     by (auto intro: Gcd_dvd Gcd_greatest)
   422   moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
   423   proof (rule Gcd_greatest)
   424     fix b
   425     assume "b \<in> insert a A"
   426     then show "gcd a (Gcd A) dvd b"
   427     proof
   428       assume "b = a" then show ?thesis by simp
   429     next
   430       assume "b \<in> A"
   431       then have "Gcd A dvd b" by (rule Gcd_dvd)
   432       moreover have "gcd a (Gcd A) dvd Gcd A" by simp
   433       ultimately show ?thesis by (blast intro: dvd_trans)
   434     qed
   435   qed
   436   ultimately show ?thesis
   437     by (auto intro: associated_eqI)
   438 qed
   439 
   440 lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
   441   "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
   442   by (blast intro: Gcd_greatest)
   443 
   444 lemma Gcd_set [code_unfold]:
   445   "Gcd (set as) = foldr gcd as 0"
   446   by (induct as) simp_all
   447 
   448 lemma Gcd_image_normalize [simp]:
   449   "Gcd (normalize ` A) = Gcd A"
   450 proof -
   451   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   452   proof -
   453     from that obtain B where "A = insert a B" by blast
   454     moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
   455       by (rule gcd_dvd1)
   456     ultimately show "Gcd (normalize ` A) dvd a"
   457       by simp
   458   qed
   459   then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
   460     by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   461   then show ?thesis
   462     by (auto intro: associated_eqI)
   463 qed
   464 
   465 end  
   466 
   467 class semiring_Lcm = semiring_Gcd +
   468   assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
   469 begin
   470 
   471 lemma dvd_Lcm:
   472   assumes "a \<in> A"
   473   shows "a dvd Lcm A"
   474   using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
   475 
   476 lemma Lcm_least:
   477   assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
   478   shows "Lcm A dvd a"
   479   using assms by (auto intro: Gcd_dvd simp add: Lcm_Gcd)
   480 
   481 lemma normalize_Lcm [simp]:
   482   "normalize (Lcm A) = Lcm A"
   483   by (simp add: Lcm_Gcd)
   484 
   485 lemma unit_factor_Lcm:
   486   "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
   487 proof (cases "Lcm A = 0")
   488   case True then show ?thesis by simp
   489 next
   490   case False
   491   with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
   492     by blast
   493   with False show ?thesis
   494     by simp
   495 qed
   496 
   497 lemma Gcd_Lcm:
   498   "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
   499   by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
   500  
   501 lemma Lcm_empty [simp]:
   502   "Lcm {} = 1"
   503   by (simp add: Lcm_Gcd)
   504 
   505 lemma Lcm_insert [simp]:
   506   "Lcm (insert a A) = lcm a (Lcm A)"
   507 proof (rule sym)
   508   have "lcm a (Lcm A) dvd Lcm (insert a A)"
   509     by (auto intro: dvd_Lcm Lcm_least)
   510   moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
   511   proof (rule Lcm_least)
   512     fix b
   513     assume "b \<in> insert a A"
   514     then show "b dvd lcm a (Lcm A)"
   515     proof
   516       assume "b = a" then show ?thesis by simp
   517     next
   518       assume "b \<in> A"
   519       then have "b dvd Lcm A" by (rule dvd_Lcm)
   520       moreover have "Lcm A dvd lcm a (Lcm A)" by simp
   521       ultimately show ?thesis by (blast intro: dvd_trans)
   522     qed
   523   qed
   524   ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
   525     by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
   526 qed
   527 
   528 lemma Lcm_1_iff [simp]:
   529   "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
   530 proof
   531   assume ?P
   532   show ?Q
   533   proof
   534     fix a
   535     assume "a \<in> A"
   536     then have "a dvd Lcm A"
   537       by (rule dvd_Lcm)
   538     with \<open>?P\<close> show "is_unit a"
   539       by simp
   540   qed
   541 next
   542   assume ?Q
   543   then have "is_unit (Lcm A)"
   544     by (blast intro: Lcm_least)
   545   then have "normalize (Lcm A) = 1"
   546     by (rule is_unit_normalize)
   547   then show ?P
   548     by simp
   549 qed
   550 
   551 lemma Lcm_eq_0_I:
   552   assumes "0 \<in> A"
   553   shows "Lcm A = 0"
   554 proof -
   555   from assms have "0 dvd Lcm A"
   556     by (rule dvd_Lcm)
   557   then show ?thesis
   558     by simp
   559 qed
   560 
   561 lemma Lcm_UNIV [simp]:
   562   "Lcm UNIV = 0"
   563   by (rule Lcm_eq_0_I) simp
   564 
   565 lemma Lcm_0_iff:
   566   assumes "finite A"
   567   shows "Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
   568 proof (cases "A = {}")
   569   case True then show ?thesis by simp
   570 next
   571   case False with assms show ?thesis
   572     by (induct A rule: finite_ne_induct)
   573       (auto simp add: lcm_eq_0_iff)
   574 qed
   575 
   576 lemma Lcm_set [code_unfold]:
   577   "Lcm (set as) = foldr lcm as 1"
   578   by (induct as) simp_all
   579   
   580 end
   581 
   582 class ring_gcd = comm_ring_1 + semiring_gcd
   583 
   584 instantiation nat :: gcd
   585 begin
   586 
   587 fun
   588   gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   589 where
   590   "gcd_nat x y =
   591    (if y = 0 then x else gcd y (x mod y))"
   592 
   593 definition
   594   lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
   595 where
   596   "lcm_nat x y = x * y div (gcd x y)"
   597 
   598 instance proof qed
   599 
   600 end
   601 
   602 instantiation int :: gcd
   603 begin
   604 
   605 definition
   606   gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
   607 where
   608   "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   609 
   610 definition
   611   lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
   612 where
   613   "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
   614 
   615 instance ..
   616 
   617 end
   618 
   619 
   620 subsection \<open>Transfer setup\<close>
   621 
   622 lemma transfer_nat_int_gcd:
   623   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
   624   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> lcm (nat x) (nat y) = nat (lcm x y)"
   625   unfolding gcd_int_def lcm_int_def
   626   by auto
   627 
   628 lemma transfer_nat_int_gcd_closures:
   629   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> gcd x y >= 0"
   630   "x >= (0::int) \<Longrightarrow> y >= 0 \<Longrightarrow> lcm x y >= 0"
   631   by (auto simp add: gcd_int_def lcm_int_def)
   632 
   633 declare transfer_morphism_nat_int[transfer add return:
   634     transfer_nat_int_gcd transfer_nat_int_gcd_closures]
   635 
   636 lemma transfer_int_nat_gcd:
   637   "gcd (int x) (int y) = int (gcd x y)"
   638   "lcm (int x) (int y) = int (lcm x y)"
   639   by (unfold gcd_int_def lcm_int_def, auto)
   640 
   641 lemma transfer_int_nat_gcd_closures:
   642   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> gcd x y >= 0"
   643   "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> lcm x y >= 0"
   644   by (auto simp add: gcd_int_def lcm_int_def)
   645 
   646 declare transfer_morphism_int_nat[transfer add return:
   647     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
   648 
   649 
   650 subsection \<open>GCD properties\<close>
   651 
   652 (* was gcd_induct *)
   653 lemma gcd_nat_induct:
   654   fixes m n :: nat
   655   assumes "\<And>m. P m 0"
   656     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
   657   shows "P m n"
   658   apply (rule gcd_nat.induct)
   659   apply (case_tac "y = 0")
   660   using assms apply simp_all
   661 done
   662 
   663 (* specific to int *)
   664 
   665 lemma gcd_neg1_int [simp]: "gcd (-x::int) y = gcd x y"
   666   by (simp add: gcd_int_def)
   667 
   668 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   669   by (simp add: gcd_int_def)
   670 
   671 lemma gcd_neg_numeral_1_int [simp]:
   672   "gcd (- numeral n :: int) x = gcd (numeral n) x"
   673   by (fact gcd_neg1_int)
   674 
   675 lemma gcd_neg_numeral_2_int [simp]:
   676   "gcd x (- numeral n :: int) = gcd x (numeral n)"
   677   by (fact gcd_neg2_int)
   678 
   679 lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
   680 by(simp add: gcd_int_def)
   681 
   682 lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
   683 by (simp add: gcd_int_def)
   684 
   685 lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
   686 by (metis abs_idempotent gcd_abs_int)
   687 
   688 lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
   689 by (metis abs_idempotent gcd_abs_int)
   690 
   691 lemma gcd_cases_int:
   692   fixes x :: int and y
   693   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd x y)"
   694       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd x (-y))"
   695       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (gcd (-x) y)"
   696       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (gcd (-x) (-y))"
   697   shows "P (gcd x y)"
   698   by (insert assms, auto, arith)
   699 
   700 lemma gcd_ge_0_int [simp]: "gcd (x::int) y >= 0"
   701   by (simp add: gcd_int_def)
   702 
   703 lemma lcm_neg1_int: "lcm (-x::int) y = lcm x y"
   704   by (simp add: lcm_int_def)
   705 
   706 lemma lcm_neg2_int: "lcm (x::int) (-y) = lcm x y"
   707   by (simp add: lcm_int_def)
   708 
   709 lemma lcm_abs_int: "lcm (x::int) y = lcm \<bar>x\<bar> \<bar>y\<bar>"
   710   by (simp add: lcm_int_def)
   711 
   712 lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
   713   by (simp add:lcm_int_def)
   714 
   715 lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
   716   by (metis abs_idempotent lcm_int_def)
   717 
   718 lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
   719   by (metis abs_idempotent lcm_int_def)
   720 
   721 lemma lcm_cases_int:
   722   fixes x :: int and y
   723   assumes "x >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm x y)"
   724       and "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm x (-y))"
   725       and "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> P (lcm (-x) y)"
   726       and "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> P (lcm (-x) (-y))"
   727   shows "P (lcm x y)"
   728   using assms by (auto simp add: lcm_neg1_int lcm_neg2_int) arith
   729 
   730 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   731   by (simp add: lcm_int_def)
   732 
   733 (* was gcd_0, etc. *)
   734 lemma gcd_0_nat: "gcd (x::nat) 0 = x"
   735   by simp
   736 
   737 (* was igcd_0, etc. *)
   738 lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
   739   by (unfold gcd_int_def, auto)
   740 
   741 lemma gcd_0_left_nat: "gcd 0 (x::nat) = x"
   742   by simp
   743 
   744 lemma gcd_0_left_int [simp]: "gcd 0 (x::int) = \<bar>x\<bar>"
   745   by (unfold gcd_int_def, auto)
   746 
   747 lemma gcd_red_nat: "gcd (x::nat) y = gcd y (x mod y)"
   748   by (case_tac "y = 0", auto)
   749 
   750 (* weaker, but useful for the simplifier *)
   751 
   752 lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   753   by simp
   754 
   755 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
   756   by simp
   757 
   758 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
   759   by simp
   760 
   761 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   762   by (simp add: gcd_int_def)
   763 
   764 lemma gcd_idem_nat: "gcd (x::nat) x = x"
   765 by simp
   766 
   767 lemma gcd_idem_int: "gcd (x::int) x = \<bar>x\<bar>"
   768 by (auto simp add: gcd_int_def)
   769 
   770 declare gcd_nat.simps [simp del]
   771 
   772 text \<open>
   773   \medskip @{term "gcd m n"} divides \<open>m\<close> and \<open>n\<close>.  The
   774   conjunctions don't seem provable separately.
   775 \<close>
   776 
   777 instance nat :: semiring_gcd
   778 proof
   779   fix m n :: nat
   780   show "gcd m n dvd m" and "gcd m n dvd n"
   781   proof (induct m n rule: gcd_nat_induct)
   782     fix m n :: nat
   783     assume "gcd n (m mod n) dvd m mod n" and "gcd n (m mod n) dvd n"
   784     then have "gcd n (m mod n) dvd m"
   785       by (rule dvd_mod_imp_dvd)
   786     moreover assume "0 < n"
   787     ultimately show "gcd m n dvd m"
   788       by (simp add: gcd_non_0_nat)
   789   qed (simp_all add: gcd_0_nat gcd_non_0_nat)
   790 next
   791   fix m n k :: nat
   792   assume "k dvd m" and "k dvd n"
   793   then show "k dvd gcd m n"
   794     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
   795 qed (simp_all add: lcm_nat_def)
   796 
   797 instance int :: ring_gcd
   798   by standard
   799     (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)
   800 
   801 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   802   by (metis gcd_dvd1 dvd_trans)
   803 
   804 lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   805   by (metis gcd_dvd2 dvd_trans)
   806 
   807 lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   808   by (metis gcd_dvd1 dvd_trans)
   809 
   810 lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   811   by (metis gcd_dvd2 dvd_trans)
   812 
   813 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   814   by (rule dvd_imp_le, auto)
   815 
   816 lemma gcd_le2_nat [simp]: "b \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> b"
   817   by (rule dvd_imp_le, auto)
   818 
   819 lemma gcd_le1_int [simp]: "a > 0 \<Longrightarrow> gcd (a::int) b \<le> a"
   820   by (rule zdvd_imp_le, auto)
   821 
   822 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   823   by (rule zdvd_imp_le, auto)
   824 
   825 lemma gcd_greatest_iff_nat:
   826   "(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)"
   827   by (fact gcd_greatest_iff)
   828 
   829 lemma gcd_greatest_iff_int:
   830   "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
   831   by (fact gcd_greatest_iff)
   832 
   833 lemma gcd_zero_nat: 
   834   "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
   835   by (fact gcd_eq_0_iff)
   836 
   837 lemma gcd_zero_int [simp]:
   838   "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
   839   by (fact gcd_eq_0_iff)
   840 
   841 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   842   by (insert gcd_zero_nat [of m n], arith)
   843 
   844 lemma gcd_pos_int [simp]: "(gcd (m::int) n > 0) = (m ~= 0 | n ~= 0)"
   845   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
   846 
   847 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
   848     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   849   apply auto
   850   apply (rule dvd_antisym)
   851   apply (erule (1) gcd_greatest)
   852   apply auto
   853 done
   854 
   855 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
   856     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   857 apply (case_tac "d = 0")
   858  apply simp
   859 apply (rule iffI)
   860  apply (rule zdvd_antisym_nonneg)
   861  apply (auto intro: gcd_greatest)
   862 done
   863 
   864 interpretation gcd_nat:
   865   semilattice_neutr_order gcd "0::nat" Rings.dvd "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
   866   by standard (auto simp add: gcd_unique_nat [symmetric] intro: dvd.antisym dvd_trans)
   867 
   868 lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
   869 lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
   870 lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
   871 lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
   872 lemmas gcd_commute_int = gcd.commute [where ?'a = int]
   873 lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
   874 
   875 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
   876 
   877 lemmas gcd_ac_int = gcd_assoc_int gcd_commute_int gcd_left_commute_int
   878 
   879 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
   880   by (fact gcd_nat.absorb1)
   881 
   882 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   883   by (fact gcd_nat.absorb2)
   884 
   885 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd (x::int) y = \<bar>x\<bar>"
   886   by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
   887 
   888 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd (x::int) y = \<bar>y\<bar>"
   889   by (metis gcd_proj1_if_dvd_int gcd_commute_int)
   890 
   891 text \<open>
   892   \medskip Multiplication laws
   893 \<close>
   894 
   895 lemma gcd_mult_distrib_nat: "(k::nat) * gcd m n = gcd (k * m) (k * n)"
   896     \<comment> \<open>@{cite \<open>page 27\<close> davenport92}\<close>
   897   apply (induct m n rule: gcd_nat_induct)
   898   apply simp
   899   apply (case_tac "k = 0")
   900   apply (simp_all add: gcd_non_0_nat)
   901 done
   902 
   903 lemma gcd_mult_distrib_int: "\<bar>k::int\<bar> * gcd m n = gcd (k * m) (k * n)"
   904   apply (subst (1 2) gcd_abs_int)
   905   apply (subst (1 2) abs_mult)
   906   apply (rule gcd_mult_distrib_nat [transferred])
   907   apply auto
   908 done
   909 
   910 context semiring_gcd
   911 begin
   912 
   913 lemma coprime_dvd_mult:
   914   assumes "coprime a b" and "a dvd c * b"
   915   shows "a dvd c"
   916 proof (cases "c = 0")
   917   case True then show ?thesis by simp
   918 next
   919   case False
   920   then have unit: "is_unit (unit_factor c)" by simp
   921   from \<open>coprime a b\<close> mult_gcd_left [of c a b]
   922   have "gcd (c * a) (c * b) * unit_factor c = c"
   923     by (simp add: ac_simps)
   924   moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
   925     by (simp add: dvd_mult_unit_iff unit)
   926   ultimately show ?thesis by simp
   927 qed
   928 
   929 end
   930 
   931 lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
   932 lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
   933 
   934 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   935     (k dvd m * n) = (k dvd m)"
   936   by (auto intro: coprime_dvd_mult_nat)
   937 
   938 lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   939     (k dvd m * n) = (k dvd m)"
   940   by (auto intro: coprime_dvd_mult_int)
   941 
   942 context semiring_gcd
   943 begin
   944 
   945 lemma gcd_mult_cancel:
   946   "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
   947   apply (rule associated_eqI)
   948   apply (rule gcd_greatest)
   949   apply (rule_tac b = c in coprime_dvd_mult)
   950   apply (simp add: gcd.assoc)
   951   apply (simp_all add: ac_simps)
   952   done
   953 
   954 end  
   955 
   956 lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
   957 lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
   958 
   959 lemma coprime_crossproduct_nat:
   960   fixes a b c d :: nat
   961   assumes "coprime a d" and "coprime b c"
   962   shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d" (is "?lhs \<longleftrightarrow> ?rhs")
   963 proof
   964   assume ?rhs then show ?lhs by simp
   965 next
   966   assume ?lhs
   967   from \<open>?lhs\<close> have "a dvd b * d" by (auto intro: dvdI dest: sym)
   968   with \<open>coprime a d\<close> have "a dvd b" by (simp add: coprime_dvd_mult_iff_nat)
   969   from \<open>?lhs\<close> have "b dvd a * c" by (auto intro: dvdI dest: sym)
   970   with \<open>coprime b c\<close> have "b dvd a" by (simp add: coprime_dvd_mult_iff_nat)
   971   from \<open>?lhs\<close> have "c dvd d * b" by (auto intro: dvdI dest: sym simp add: mult.commute)
   972   with \<open>coprime b c\<close> have "c dvd d" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   973   from \<open>?lhs\<close> have "d dvd c * a" by (auto intro: dvdI dest: sym simp add: mult.commute)
   974   with \<open>coprime a d\<close> have "d dvd c" by (simp add: coprime_dvd_mult_iff_nat gcd_commute_nat)
   975   from \<open>a dvd b\<close> \<open>b dvd a\<close> have "a = b" by (rule Nat.dvd.antisym)
   976   moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "c = d" by (rule Nat.dvd.antisym)
   977   ultimately show ?rhs ..
   978 qed
   979 
   980 lemma coprime_crossproduct_int:
   981   fixes a b c d :: int
   982   assumes "coprime a d" and "coprime b c"
   983   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>"
   984   using assms by (intro coprime_crossproduct_nat [transferred]) auto
   985 
   986 text \<open>\medskip Addition laws\<close>
   987 
   988 lemma gcd_add1_nat [simp]: "gcd ((m::nat) + n) n = gcd m n"
   989   apply (case_tac "n = 0")
   990   apply (simp_all add: gcd_non_0_nat)
   991 done
   992 
   993 lemma gcd_add2_nat [simp]: "gcd (m::nat) (m + n) = gcd m n"
   994   apply (subst (1 2) gcd_commute_nat)
   995   apply (subst add.commute)
   996   apply simp
   997 done
   998 
   999 (* to do: add the other variations? *)
  1000 
  1001 lemma gcd_diff1_nat: "(m::nat) >= n \<Longrightarrow> gcd (m - n) n = gcd m n"
  1002   by (subst gcd_add1_nat [symmetric], auto)
  1003 
  1004 lemma gcd_diff2_nat: "(n::nat) >= m \<Longrightarrow> gcd (n - m) n = gcd m n"
  1005   apply (subst gcd_commute_nat)
  1006   apply (subst gcd_diff1_nat [symmetric])
  1007   apply auto
  1008   apply (subst gcd_commute_nat)
  1009   apply (subst gcd_diff1_nat)
  1010   apply assumption
  1011   apply (rule gcd_commute_nat)
  1012 done
  1013 
  1014 lemma gcd_non_0_int: "(y::int) > 0 \<Longrightarrow> gcd x y = gcd y (x mod y)"
  1015   apply (frule_tac b = y and a = x in pos_mod_sign)
  1016   apply (simp del: pos_mod_sign add: gcd_int_def abs_if nat_mod_distrib)
  1017   apply (auto simp add: gcd_non_0_nat nat_mod_distrib [symmetric]
  1018     zmod_zminus1_eq_if)
  1019   apply (frule_tac a = x in pos_mod_bound)
  1020   apply (subst (1 2) gcd_commute_nat)
  1021   apply (simp del: pos_mod_bound add: nat_diff_distrib gcd_diff2_nat
  1022     nat_le_eq_zle)
  1023 done
  1024 
  1025 lemma gcd_red_int: "gcd (x::int) y = gcd y (x mod y)"
  1026   apply (case_tac "y = 0")
  1027   apply force
  1028   apply (case_tac "y > 0")
  1029   apply (subst gcd_non_0_int, auto)
  1030   apply (insert gcd_non_0_int [of "-y" "-x"])
  1031   apply auto
  1032 done
  1033 
  1034 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
  1035 by (metis gcd_red_int mod_add_self1 add.commute)
  1036 
  1037 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
  1038 by (metis gcd_add1_int gcd_commute_int add.commute)
  1039 
  1040 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
  1041 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
  1042 
  1043 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
  1044 by (metis gcd_commute_int gcd_red_int mod_mult_self1 add.commute)
  1045 
  1046 
  1047 (* to do: differences, and all variations of addition rules
  1048     as simplification rules for nat and int *)
  1049 
  1050 lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n"
  1051   using mult_dvd_mono [of 1] by auto
  1052 
  1053 (* to do: add the three variations of these, and for ints? *)
  1054 
  1055 lemma finite_divisors_nat[simp]:
  1056   assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
  1057 proof-
  1058   have "finite{d. d <= m}"
  1059     by (blast intro: bounded_nat_set_is_finite)
  1060   from finite_subset[OF _ this] show ?thesis using assms
  1061     by (metis Collect_mono dvd_imp_le neq0_conv)
  1062 qed
  1063 
  1064 lemma finite_divisors_int[simp]:
  1065   assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
  1066 proof-
  1067   have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
  1068   hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
  1069   from finite_subset[OF _ this] show ?thesis using assms
  1070     by (simp add: dvd_imp_le_int subset_iff)
  1071 qed
  1072 
  1073 lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
  1074 apply(rule antisym)
  1075  apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
  1076 apply simp
  1077 done
  1078 
  1079 lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
  1080 apply(rule antisym)
  1081  apply(rule Max_le_iff [THEN iffD2])
  1082   apply (auto intro: abs_le_D1 dvd_imp_le_int)
  1083 done
  1084 
  1085 lemma gcd_is_Max_divisors_nat:
  1086   "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
  1087 apply(rule Max_eqI[THEN sym])
  1088   apply (metis finite_Collect_conjI finite_divisors_nat)
  1089  apply simp
  1090  apply(metis Suc_diff_1 Suc_neq_Zero dvd_imp_le gcd_greatest_iff_nat gcd_pos_nat)
  1091 apply simp
  1092 done
  1093 
  1094 lemma gcd_is_Max_divisors_int:
  1095   "m ~= 0 ==> n ~= 0 ==> gcd (m::int) n = (Max {d. d dvd m & d dvd n})"
  1096 apply(rule Max_eqI[THEN sym])
  1097   apply (metis finite_Collect_conjI finite_divisors_int)
  1098  apply simp
  1099  apply (metis gcd_greatest_iff_int gcd_pos_int zdvd_imp_le)
  1100 apply simp
  1101 done
  1102 
  1103 lemma gcd_code_int [code]:
  1104   "gcd k l = \<bar>if l = (0::int) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  1105   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
  1106 
  1107 
  1108 subsection \<open>Coprimality\<close>
  1109 
  1110 context semiring_gcd
  1111 begin
  1112 
  1113 lemma div_gcd_coprime:
  1114   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
  1115   shows "coprime (a div gcd a b) (b div gcd a b)"
  1116 proof -
  1117   let ?g = "gcd a b"
  1118   let ?a' = "a div ?g"
  1119   let ?b' = "b div ?g"
  1120   let ?g' = "gcd ?a' ?b'"
  1121   have dvdg: "?g dvd a" "?g dvd b" by simp_all
  1122   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
  1123   from dvdg dvdg' obtain ka kb ka' kb' where
  1124       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
  1125     unfolding dvd_def by blast
  1126   from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
  1127     by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
  1128   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
  1129     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
  1130       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
  1131   have "?g \<noteq> 0" using nz by simp
  1132   moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
  1133   thm dvd_mult_cancel_left
  1134   ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
  1135 qed
  1136 
  1137 end
  1138 
  1139 lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
  1140 lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
  1141 
  1142 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1143   using gcd_unique_nat[of 1 a b, simplified] by auto
  1144 
  1145 lemma coprime_Suc_0_nat:
  1146     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
  1147   using coprime_nat by simp
  1148 
  1149 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
  1150     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
  1151   using gcd_unique_int [of 1 a b]
  1152   apply clarsimp
  1153   apply (erule subst)
  1154   apply (rule iffI)
  1155   apply force
  1156   using abs_dvd_iff abs_ge_zero apply blast
  1157   done
  1158 
  1159 lemma gcd_coprime_nat:
  1160   assumes z: "gcd (a::nat) b \<noteq> 0" and a: "a = a' * gcd a b" and
  1161     b: "b = b' * gcd a b"
  1162   shows    "coprime a' b'"
  1163 
  1164   apply (subgoal_tac "a' = a div gcd a b")
  1165   apply (erule ssubst)
  1166   apply (subgoal_tac "b' = b div gcd a b")
  1167   apply (erule ssubst)
  1168   apply (rule div_gcd_coprime_nat)
  1169   using z apply force
  1170   apply (subst (1) b)
  1171   using z apply force
  1172   apply (subst (1) a)
  1173   using z apply force
  1174   done
  1175 
  1176 lemma gcd_coprime_int:
  1177   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
  1178     b: "b = b' * gcd a b"
  1179   shows    "coprime a' b'"
  1180 
  1181   apply (subgoal_tac "a' = a div gcd a b")
  1182   apply (erule ssubst)
  1183   apply (subgoal_tac "b' = b div gcd a b")
  1184   apply (erule ssubst)
  1185   apply (rule div_gcd_coprime_int)
  1186   using z apply force
  1187   apply (subst (1) b)
  1188   using z apply force
  1189   apply (subst (1) a)
  1190   using z apply force
  1191   done
  1192 
  1193 context semiring_gcd
  1194 begin
  1195 
  1196 lemma coprime_mult:
  1197   assumes da: "coprime d a" and db: "coprime d b"
  1198   shows "coprime d (a * b)"
  1199   apply (subst gcd.commute)
  1200   using da apply (subst gcd_mult_cancel)
  1201   apply (subst gcd.commute, assumption)
  1202   apply (subst gcd.commute, rule db)
  1203   done
  1204 
  1205 end
  1206 
  1207 lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
  1208 lemmas coprime_mult_int = coprime_mult [where ?'a = int]
  1209   
  1210 lemma coprime_lmult_nat:
  1211   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
  1212 proof -
  1213   have "gcd d a dvd gcd d (a * b)"
  1214     by (rule gcd_greatest, auto)
  1215   with dab show ?thesis
  1216     by auto
  1217 qed
  1218 
  1219 lemma coprime_lmult_int:
  1220   assumes "coprime (d::int) (a * b)" shows "coprime d a"
  1221 proof -
  1222   have "gcd d a dvd gcd d (a * b)"
  1223     by (rule gcd_greatest, auto)
  1224   with assms show ?thesis
  1225     by auto
  1226 qed
  1227 
  1228 lemma coprime_rmult_nat:
  1229   assumes "coprime (d::nat) (a * b)" shows "coprime d b"
  1230 proof -
  1231   have "gcd d b dvd gcd d (a * b)"
  1232     by (rule gcd_greatest, auto intro: dvd_mult)
  1233   with assms show ?thesis
  1234     by auto
  1235 qed
  1236 
  1237 lemma coprime_rmult_int:
  1238   assumes dab: "coprime (d::int) (a * b)" shows "coprime d b"
  1239 proof -
  1240   have "gcd d b dvd gcd d (a * b)"
  1241     by (rule gcd_greatest, auto intro: dvd_mult)
  1242   with dab show ?thesis
  1243     by auto
  1244 qed
  1245 
  1246 lemma coprime_mul_eq_nat: "coprime (d::nat) (a * b) \<longleftrightarrow>
  1247     coprime d a \<and>  coprime d b"
  1248   using coprime_rmult_nat[of d a b] coprime_lmult_nat[of d a b]
  1249     coprime_mult_nat[of d a b]
  1250   by blast
  1251 
  1252 lemma coprime_mul_eq_int: "coprime (d::int) (a * b) \<longleftrightarrow>
  1253     coprime d a \<and>  coprime d b"
  1254   using coprime_rmult_int[of d a b] coprime_lmult_int[of d a b]
  1255     coprime_mult_int[of d a b]
  1256   by blast
  1257 
  1258 lemma coprime_power_int:
  1259   assumes "0 < n" shows "coprime (a :: int) (b ^ n) \<longleftrightarrow> coprime a b"
  1260   using assms
  1261 proof (induct n)
  1262   case (Suc n) then show ?case
  1263     by (cases n) (simp_all add: coprime_mul_eq_int)
  1264 qed simp
  1265 
  1266 lemma gcd_coprime_exists_nat:
  1267     assumes nz: "gcd (a::nat) b \<noteq> 0"
  1268     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1269   apply (rule_tac x = "a div gcd a b" in exI)
  1270   apply (rule_tac x = "b div gcd a b" in exI)
  1271   using nz apply (auto simp add: div_gcd_coprime_nat dvd_div_mult)
  1272 done
  1273 
  1274 lemma gcd_coprime_exists_int:
  1275     assumes nz: "gcd (a::int) b \<noteq> 0"
  1276     shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
  1277   apply (rule_tac x = "a div gcd a b" in exI)
  1278   apply (rule_tac x = "b div gcd a b" in exI)
  1279   using nz apply (auto simp add: div_gcd_coprime_int)
  1280 done
  1281 
  1282 lemma coprime_exp_nat: "coprime (d::nat) a \<Longrightarrow> coprime d (a^n)"
  1283   by (induct n) (simp_all add: coprime_mult_nat)
  1284 
  1285 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
  1286   by (induct n) (simp_all add: coprime_mult_int)
  1287 
  1288 context semiring_gcd
  1289 begin
  1290 
  1291 lemma coprime_exp_left:
  1292   assumes "coprime a b"
  1293   shows "coprime (a ^ n) b"
  1294   using assms by (induct n) (simp_all add: gcd_mult_cancel)
  1295 
  1296 lemma coprime_exp2:
  1297   assumes "coprime a b"
  1298   shows "coprime (a ^ n) (b ^ m)"
  1299 proof (rule coprime_exp_left)
  1300   from assms show "coprime a (b ^ m)"
  1301     by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
  1302 qed
  1303 
  1304 end
  1305 
  1306 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
  1307   by (fact coprime_exp2)
  1308 
  1309 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
  1310   by (fact coprime_exp2)
  1311 
  1312 lemma gcd_exp_nat:
  1313   "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
  1314 proof (cases "a = 0 \<and> b = 0")
  1315   case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
  1316 next
  1317   case False
  1318   then have "coprime (a div gcd a b) (b div gcd a b)"
  1319     by (auto simp: div_gcd_coprime)
  1320   then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
  1321     by (simp add: coprime_exp2)
  1322   then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
  1323       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
  1324     by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
  1325   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
  1326     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1327   also have "(b div gcd a b)^n * (gcd a b)^n = b^n"
  1328     by (metis dvd_div_mult_self gcd_unique_nat power_mult_distrib)
  1329   finally show ?thesis .
  1330 qed
  1331 
  1332 lemma gcd_exp_int: "gcd ((a::int)^n) (b^n) = (gcd a b)^n"
  1333   apply (subst (1 2) gcd_abs_int)
  1334   apply (subst (1 2) power_abs)
  1335   apply (rule gcd_exp_nat [where n = n, transferred])
  1336   apply auto
  1337 done
  1338 
  1339 lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
  1340   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1341 proof-
  1342   let ?g = "gcd a b"
  1343   {assume "?g = 0" with dc have ?thesis by auto}
  1344   moreover
  1345   {assume z: "?g \<noteq> 0"
  1346     from gcd_coprime_exists_nat[OF z]
  1347     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1348       by blast
  1349     have thb: "?g dvd b" by auto
  1350     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1351     with dc have th0: "a' dvd b*c" using dvd_trans[of a' a "b*c"] by simp
  1352     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1353     hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
  1354     with z have th_1: "a' dvd b' * c" by auto
  1355     from coprime_dvd_mult_nat[OF ab'(3)] th_1
  1356     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1357     from ab' have "a = ?g*a'" by algebra
  1358     with thb thc have ?thesis by blast }
  1359   ultimately show ?thesis by blast
  1360 qed
  1361 
  1362 lemma division_decomp_int: assumes dc: "(a::int) dvd b * c"
  1363   shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
  1364 proof-
  1365   let ?g = "gcd a b"
  1366   {assume "?g = 0" with dc have ?thesis by auto}
  1367   moreover
  1368   {assume z: "?g \<noteq> 0"
  1369     from gcd_coprime_exists_int[OF z]
  1370     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1371       by blast
  1372     have thb: "?g dvd b" by auto
  1373     from ab'(1) have "a' dvd a"  unfolding dvd_def by blast
  1374     with dc have th0: "a' dvd b*c"
  1375       using dvd_trans[of a' a "b*c"] by simp
  1376     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
  1377     hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
  1378     with z have th_1: "a' dvd b' * c" by auto
  1379     from coprime_dvd_mult_int[OF ab'(3)] th_1
  1380     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
  1381     from ab' have "a = ?g*a'" by algebra
  1382     with thb thc have ?thesis by blast }
  1383   ultimately show ?thesis by blast
  1384 qed
  1385 
  1386 lemma pow_divides_pow_nat:
  1387   assumes ab: "(a::nat) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1388   shows "a dvd b"
  1389 proof-
  1390   let ?g = "gcd a b"
  1391   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1392   {assume "?g = 0" with ab n have ?thesis by auto }
  1393   moreover
  1394   {assume z: "?g \<noteq> 0"
  1395     hence zn: "?g ^ n \<noteq> 0" using n by simp
  1396     from gcd_coprime_exists_nat[OF z]
  1397     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1398       by blast
  1399     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1400       by (simp add: ab'(1,2)[symmetric])
  1401     hence "?g^n*a'^n dvd ?g^n *b'^n"
  1402       by (simp only: power_mult_distrib mult.commute)
  1403     then have th0: "a'^n dvd b'^n"
  1404       using zn by auto
  1405     have "a' dvd a'^n" by (simp add: m)
  1406     with th0 have "a' dvd b'^n" using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1407     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1408     from coprime_dvd_mult_nat[OF coprime_exp_nat [OF ab'(3), of m]] th1
  1409     have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1410     hence "a'*?g dvd b'*?g" by simp
  1411     with ab'(1,2)  have ?thesis by simp }
  1412   ultimately show ?thesis by blast
  1413 qed
  1414 
  1415 lemma pow_divides_pow_int:
  1416   assumes ab: "(a::int) ^ n dvd b ^n" and n:"n \<noteq> 0"
  1417   shows "a dvd b"
  1418 proof-
  1419   let ?g = "gcd a b"
  1420   from n obtain m where m: "n = Suc m" by (cases n, simp_all)
  1421   {assume "?g = 0" with ab n have ?thesis by auto }
  1422   moreover
  1423   {assume z: "?g \<noteq> 0"
  1424     hence zn: "?g ^ n \<noteq> 0" using n by simp
  1425     from gcd_coprime_exists_int[OF z]
  1426     obtain a' b' where ab': "a = a' * ?g" "b = b' * ?g" "coprime a' b'"
  1427       by blast
  1428     from ab have "(a' * ?g) ^ n dvd (b' * ?g)^n"
  1429       by (simp add: ab'(1,2)[symmetric])
  1430     hence "?g^n*a'^n dvd ?g^n *b'^n"
  1431       by (simp only: power_mult_distrib mult.commute)
  1432     with zn z n have th0:"a'^n dvd b'^n" by auto
  1433     have "a' dvd a'^n" by (simp add: m)
  1434     with th0 have "a' dvd b'^n"
  1435       using dvd_trans[of a' "a'^n" "b'^n"] by simp
  1436     hence th1: "a' dvd b'^m * b'" by (simp add: m mult.commute)
  1437     from coprime_dvd_mult_int[OF coprime_exp_int [OF ab'(3), of m]] th1
  1438     have "a' dvd b'" by (subst (asm) mult.commute, blast)
  1439     hence "a'*?g dvd b'*?g" by simp
  1440     with ab'(1,2)  have ?thesis by simp }
  1441   ultimately show ?thesis by blast
  1442 qed
  1443 
  1444 lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
  1445   by (auto intro: pow_divides_pow_nat dvd_power_same)
  1446 
  1447 lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
  1448   by (auto intro: pow_divides_pow_int dvd_power_same)
  1449 
  1450 lemma divides_mult_nat:
  1451   assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1452   shows "m * n dvd r"
  1453 proof-
  1454   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1455     unfolding dvd_def by blast
  1456   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
  1457   hence "m dvd n'" using coprime_dvd_mult_iff_nat[OF mn] by simp
  1458   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1459   from n' k show ?thesis unfolding dvd_def by auto
  1460 qed
  1461 
  1462 lemma divides_mult_int:
  1463   assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
  1464   shows "m * n dvd r"
  1465 proof-
  1466   from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
  1467     unfolding dvd_def by blast
  1468   from mr n' have "m dvd n'*n" by (simp add: mult.commute)
  1469   hence "m dvd n'" using coprime_dvd_mult_iff_int[OF mn] by simp
  1470   then obtain k where k: "n' = m*k" unfolding dvd_def by blast
  1471   from n' k show ?thesis unfolding dvd_def by auto
  1472 qed
  1473 
  1474 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
  1475   by (simp add: gcd.commute del: One_nat_def)
  1476 
  1477 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
  1478   using coprime_plus_one_nat by simp
  1479 
  1480 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
  1481   by (simp add: gcd.commute)
  1482 
  1483 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
  1484   using coprime_plus_one_nat [of "n - 1"]
  1485     gcd_commute_nat [of "n - 1" n] by auto
  1486 
  1487 lemma coprime_minus_one_int: "coprime ((n::int) - 1) n"
  1488   using coprime_plus_one_int [of "n - 1"]
  1489     gcd_commute_int [of "n - 1" n] by auto
  1490 
  1491 lemma setprod_coprime_nat [rule_format]:
  1492     "(ALL i: A. coprime (f i) (x::nat)) --> coprime (\<Prod>i\<in>A. f i) x"
  1493   apply (case_tac "finite A")
  1494   apply (induct set: finite)
  1495   apply (auto simp add: gcd_mult_cancel_nat)
  1496 done
  1497 
  1498 lemma setprod_coprime_int [rule_format]:
  1499     "(ALL i: A. coprime (f i) (x::int)) --> coprime (\<Prod>i\<in>A. f i) x"
  1500   apply (case_tac "finite A")
  1501   apply (induct set: finite)
  1502   apply (auto simp add: gcd_mult_cancel_int)
  1503 done
  1504 
  1505 lemma coprime_common_divisor_nat: 
  1506   "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
  1507   by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
  1508 
  1509 lemma coprime_common_divisor_int:
  1510   "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
  1511   using gcd_greatest_iff [of x a b] by auto
  1512 
  1513 lemma coprime_divisors_nat:
  1514     "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
  1515   by (meson coprime_int dvd_trans gcd_dvd1 gcd_dvd2 gcd_ge_0_int)
  1516 
  1517 lemma invertible_coprime_nat: "(x::nat) * y mod m = 1 \<Longrightarrow> coprime x m"
  1518 by (metis coprime_lmult_nat gcd_1_nat gcd_commute_nat gcd_red_nat)
  1519 
  1520 lemma invertible_coprime_int: "(x::int) * y mod m = 1 \<Longrightarrow> coprime x m"
  1521 by (metis coprime_lmult_int gcd_1_int gcd_commute_int gcd_red_int)
  1522 
  1523 
  1524 subsection \<open>Bezout's theorem\<close>
  1525 
  1526 (* Function bezw returns a pair of witnesses to Bezout's theorem --
  1527    see the theorems that follow the definition. *)
  1528 fun
  1529   bezw  :: "nat \<Rightarrow> nat \<Rightarrow> int * int"
  1530 where
  1531   "bezw x y =
  1532   (if y = 0 then (1, 0) else
  1533       (snd (bezw y (x mod y)),
  1534        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y)))"
  1535 
  1536 lemma bezw_0 [simp]: "bezw x 0 = (1, 0)" by simp
  1537 
  1538 lemma bezw_non_0: "y > 0 \<Longrightarrow> bezw x y = (snd (bezw y (x mod y)),
  1539        fst (bezw y (x mod y)) - snd (bezw y (x mod y)) * int(x div y))"
  1540   by simp
  1541 
  1542 declare bezw.simps [simp del]
  1543 
  1544 lemma bezw_aux [rule_format]:
  1545     "fst (bezw x y) * int x + snd (bezw x y) * int y = int (gcd x y)"
  1546 proof (induct x y rule: gcd_nat_induct)
  1547   fix m :: nat
  1548   show "fst (bezw m 0) * int m + snd (bezw m 0) * int 0 = int (gcd m 0)"
  1549     by auto
  1550   next fix m :: nat and n
  1551     assume ngt0: "n > 0" and
  1552       ih: "fst (bezw n (m mod n)) * int n +
  1553         snd (bezw n (m mod n)) * int (m mod n) =
  1554         int (gcd n (m mod n))"
  1555     thus "fst (bezw m n) * int m + snd (bezw m n) * int n = int (gcd m n)"
  1556       apply (simp add: bezw_non_0 gcd_non_0_nat)
  1557       apply (erule subst)
  1558       apply (simp add: field_simps)
  1559       apply (subst mod_div_equality [of m n, symmetric])
  1560       (* applying simp here undoes the last substitution!
  1561          what is procedure cancel_div_mod? *)
  1562       apply (simp only: NO_MATCH_def field_simps of_nat_add of_nat_mult)
  1563       done
  1564 qed
  1565 
  1566 lemma bezout_int:
  1567   fixes x y
  1568   shows "EX u v. u * (x::int) + v * y = gcd x y"
  1569 proof -
  1570   have bezout_aux: "!!x y. x \<ge> (0::int) \<Longrightarrow> y \<ge> 0 \<Longrightarrow>
  1571       EX u v. u * x + v * y = gcd x y"
  1572     apply (rule_tac x = "fst (bezw (nat x) (nat y))" in exI)
  1573     apply (rule_tac x = "snd (bezw (nat x) (nat y))" in exI)
  1574     apply (unfold gcd_int_def)
  1575     apply simp
  1576     apply (subst bezw_aux [symmetric])
  1577     apply auto
  1578     done
  1579   have "(x \<ge> 0 \<and> y \<ge> 0) | (x \<ge> 0 \<and> y \<le> 0) | (x \<le> 0 \<and> y \<ge> 0) |
  1580       (x \<le> 0 \<and> y \<le> 0)"
  1581     by auto
  1582   moreover have "x \<ge> 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> ?thesis"
  1583     by (erule (1) bezout_aux)
  1584   moreover have "x >= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1585     apply (insert bezout_aux [of x "-y"])
  1586     apply auto
  1587     apply (rule_tac x = u in exI)
  1588     apply (rule_tac x = "-v" in exI)
  1589     apply (subst gcd_neg2_int [symmetric])
  1590     apply auto
  1591     done
  1592   moreover have "x <= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> ?thesis"
  1593     apply (insert bezout_aux [of "-x" y])
  1594     apply auto
  1595     apply (rule_tac x = "-u" in exI)
  1596     apply (rule_tac x = v in exI)
  1597     apply (subst gcd_neg1_int [symmetric])
  1598     apply auto
  1599     done
  1600   moreover have "x <= 0 \<Longrightarrow> y <= 0 \<Longrightarrow> ?thesis"
  1601     apply (insert bezout_aux [of "-x" "-y"])
  1602     apply auto
  1603     apply (rule_tac x = "-u" in exI)
  1604     apply (rule_tac x = "-v" in exI)
  1605     apply (subst gcd_neg1_int [symmetric])
  1606     apply (subst gcd_neg2_int [symmetric])
  1607     apply auto
  1608     done
  1609   ultimately show ?thesis by blast
  1610 qed
  1611 
  1612 text \<open>versions of Bezout for nat, by Amine Chaieb\<close>
  1613 
  1614 lemma ind_euclid:
  1615   assumes c: " \<forall>a b. P (a::nat) b \<longleftrightarrow> P b a" and z: "\<forall>a. P a 0"
  1616   and add: "\<forall>a b. P a b \<longrightarrow> P a (a + b)"
  1617   shows "P a b"
  1618 proof(induct "a + b" arbitrary: a b rule: less_induct)
  1619   case less
  1620   have "a = b \<or> a < b \<or> b < a" by arith
  1621   moreover {assume eq: "a= b"
  1622     from add[rule_format, OF z[rule_format, of a]] have "P a b" using eq
  1623     by simp}
  1624   moreover
  1625   {assume lt: "a < b"
  1626     hence "a + b - a < a + b \<or> a = 0" by arith
  1627     moreover
  1628     {assume "a =0" with z c have "P a b" by blast }
  1629     moreover
  1630     {assume "a + b - a < a + b"
  1631       also have th0: "a + b - a = a + (b - a)" using lt by arith
  1632       finally have "a + (b - a) < a + b" .
  1633       then have "P a (a + (b - a))" by (rule add[rule_format, OF less])
  1634       then have "P a b" by (simp add: th0[symmetric])}
  1635     ultimately have "P a b" by blast}
  1636   moreover
  1637   {assume lt: "a > b"
  1638     hence "b + a - b < a + b \<or> b = 0" by arith
  1639     moreover
  1640     {assume "b =0" with z c have "P a b" by blast }
  1641     moreover
  1642     {assume "b + a - b < a + b"
  1643       also have th0: "b + a - b = b + (a - b)" using lt by arith
  1644       finally have "b + (a - b) < a + b" .
  1645       then have "P b (b + (a - b))" by (rule add[rule_format, OF less])
  1646       then have "P b a" by (simp add: th0[symmetric])
  1647       hence "P a b" using c by blast }
  1648     ultimately have "P a b" by blast}
  1649 ultimately  show "P a b" by blast
  1650 qed
  1651 
  1652 lemma bezout_lemma_nat:
  1653   assumes ex: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1654     (a * x = b * y + d \<or> b * x = a * y + d)"
  1655   shows "\<exists>d x y. d dvd a \<and> d dvd a + b \<and>
  1656     (a * x = (a + b) * y + d \<or> (a + b) * x = a * y + d)"
  1657   using ex
  1658   apply clarsimp
  1659   apply (rule_tac x="d" in exI, simp)
  1660   apply (case_tac "a * x = b * y + d" , simp_all)
  1661   apply (rule_tac x="x + y" in exI)
  1662   apply (rule_tac x="y" in exI)
  1663   apply algebra
  1664   apply (rule_tac x="x" in exI)
  1665   apply (rule_tac x="x + y" in exI)
  1666   apply algebra
  1667 done
  1668 
  1669 lemma bezout_add_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1670     (a * x = b * y + d \<or> b * x = a * y + d)"
  1671   apply(induct a b rule: ind_euclid)
  1672   apply blast
  1673   apply clarify
  1674   apply (rule_tac x="a" in exI, simp)
  1675   apply clarsimp
  1676   apply (rule_tac x="d" in exI)
  1677   apply (case_tac "a * x = b * y + d", simp_all)
  1678   apply (rule_tac x="x+y" in exI)
  1679   apply (rule_tac x="y" in exI)
  1680   apply algebra
  1681   apply (rule_tac x="x" in exI)
  1682   apply (rule_tac x="x+y" in exI)
  1683   apply algebra
  1684 done
  1685 
  1686 lemma bezout1_nat: "\<exists>(d::nat) x y. d dvd a \<and> d dvd b \<and>
  1687     (a * x - b * y = d \<or> b * x - a * y = d)"
  1688   using bezout_add_nat[of a b]
  1689   apply clarsimp
  1690   apply (rule_tac x="d" in exI, simp)
  1691   apply (rule_tac x="x" in exI)
  1692   apply (rule_tac x="y" in exI)
  1693   apply auto
  1694 done
  1695 
  1696 lemma bezout_add_strong_nat: assumes nz: "a \<noteq> (0::nat)"
  1697   shows "\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d"
  1698 proof-
  1699  from nz have ap: "a > 0" by simp
  1700  from bezout_add_nat[of a b]
  1701  have "(\<exists>d x y. d dvd a \<and> d dvd b \<and> a * x = b * y + d) \<or>
  1702    (\<exists>d x y. d dvd a \<and> d dvd b \<and> b * x = a * y + d)" by blast
  1703  moreover
  1704     {fix d x y assume H: "d dvd a" "d dvd b" "a * x = b * y + d"
  1705      from H have ?thesis by blast }
  1706  moreover
  1707  {fix d x y assume H: "d dvd a" "d dvd b" "b * x = a * y + d"
  1708    {assume b0: "b = 0" with H  have ?thesis by simp}
  1709    moreover
  1710    {assume b: "b \<noteq> 0" hence bp: "b > 0" by simp
  1711      from b dvd_imp_le [OF H(2)] have "d < b \<or> d = b"
  1712        by auto
  1713      moreover
  1714      {assume db: "d=b"
  1715        with nz H have ?thesis apply simp
  1716          apply (rule exI[where x = b], simp)
  1717          apply (rule exI[where x = b])
  1718         by (rule exI[where x = "a - 1"], simp add: diff_mult_distrib2)}
  1719     moreover
  1720     {assume db: "d < b"
  1721         {assume "x=0" hence ?thesis using nz H by simp }
  1722         moreover
  1723         {assume x0: "x \<noteq> 0" hence xp: "x > 0" by simp
  1724           from db have "d \<le> b - 1" by simp
  1725           hence "d*b \<le> b*(b - 1)" by simp
  1726           with xp mult_mono[of "1" "x" "d*b" "b*(b - 1)"]
  1727           have dble: "d*b \<le> x*b*(b - 1)" using bp by simp
  1728           from H (3) have "d + (b - 1) * (b*x) = d + (b - 1) * (a*y + d)"
  1729             by simp
  1730           hence "d + (b - 1) * a * y + (b - 1) * d = d + (b - 1) * b * x"
  1731             by (simp only: mult.assoc distrib_left)
  1732           hence "a * ((b - 1) * y) + d * (b - 1 + 1) = d + x*b*(b - 1)"
  1733             by algebra
  1734           hence "a * ((b - 1) * y) = d + x*b*(b - 1) - d*b" using bp by simp
  1735           hence "a * ((b - 1) * y) = d + (x*b*(b - 1) - d*b)"
  1736             by (simp only: diff_add_assoc[OF dble, of d, symmetric])
  1737           hence "a * ((b - 1) * y) = b*(x*(b - 1) - d) + d"
  1738             by (simp only: diff_mult_distrib2 ac_simps)
  1739           hence ?thesis using H(1,2)
  1740             apply -
  1741             apply (rule exI[where x=d], simp)
  1742             apply (rule exI[where x="(b - 1) * y"])
  1743             by (rule exI[where x="x*(b - 1) - d"], simp)}
  1744         ultimately have ?thesis by blast}
  1745     ultimately have ?thesis by blast}
  1746   ultimately have ?thesis by blast}
  1747  ultimately show ?thesis by blast
  1748 qed
  1749 
  1750 lemma bezout_nat: assumes a: "(a::nat) \<noteq> 0"
  1751   shows "\<exists>x y. a * x = b * y + gcd a b"
  1752 proof-
  1753   let ?g = "gcd a b"
  1754   from bezout_add_strong_nat[OF a, of b]
  1755   obtain d x y where d: "d dvd a" "d dvd b" "a * x = b * y + d" by blast
  1756   from d(1,2) have "d dvd ?g" by simp
  1757   then obtain k where k: "?g = d*k" unfolding dvd_def by blast
  1758   from d(3) have "a * x * k = (b * y + d) *k " by auto
  1759   hence "a * (x * k) = b * (y*k) + ?g" by (algebra add: k)
  1760   thus ?thesis by blast
  1761 qed
  1762 
  1763 
  1764 subsection \<open>LCM properties\<close>
  1765 
  1766 lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  1767   by (simp add: lcm_int_def lcm_nat_def zdiv_int
  1768     of_nat_mult gcd_int_def)
  1769 
  1770 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
  1771   unfolding lcm_nat_def
  1772   by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod_nat])
  1773 
  1774 lemma prod_gcd_lcm_int: "\<bar>m::int\<bar> * \<bar>n\<bar> = gcd m n * lcm m n"
  1775   unfolding lcm_int_def gcd_int_def
  1776   apply (subst int_mult [symmetric])
  1777   apply (subst prod_gcd_lcm_nat [symmetric])
  1778   apply (subst nat_abs_mult_distrib [symmetric])
  1779   apply (simp, simp add: abs_mult)
  1780 done
  1781 
  1782 lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
  1783   unfolding lcm_nat_def by simp
  1784 
  1785 lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
  1786   unfolding lcm_int_def by simp
  1787 
  1788 lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
  1789   unfolding lcm_nat_def by simp
  1790 
  1791 lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
  1792   unfolding lcm_int_def by simp
  1793 
  1794 lemma lcm_pos_nat:
  1795   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
  1796 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
  1797 
  1798 lemma lcm_pos_int:
  1799   "(m::int) ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> lcm m n > 0"
  1800   apply (subst lcm_abs_int)
  1801   apply (rule lcm_pos_nat [transferred])
  1802   apply auto
  1803 done
  1804 
  1805 lemma dvd_pos_nat:
  1806   fixes n m :: nat
  1807   assumes "n > 0" and "m dvd n"
  1808   shows "m > 0"
  1809 using assms by (cases m) auto
  1810 
  1811 lemma lcm_least_nat:
  1812   assumes "(m::nat) dvd k" and "n dvd k"
  1813   shows "lcm m n dvd k"
  1814   using assms by (rule lcm_least)
  1815 
  1816 lemma lcm_least_int:
  1817   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
  1818   by (rule lcm_least)
  1819 
  1820 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
  1821   by (fact dvd_lcm1)
  1822 
  1823 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
  1824   by (fact dvd_lcm1)
  1825 
  1826 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
  1827   by (fact dvd_lcm2)
  1828 
  1829 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
  1830   by (fact dvd_lcm2)
  1831 
  1832 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
  1833 by(metis lcm_dvd1_nat dvd_trans)
  1834 
  1835 lemma dvd_lcm_I2_nat[simp]: "(k::nat) dvd n \<Longrightarrow> k dvd lcm m n"
  1836 by(metis lcm_dvd2_nat dvd_trans)
  1837 
  1838 lemma dvd_lcm_I1_int[simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
  1839 by(metis lcm_dvd1_int dvd_trans)
  1840 
  1841 lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
  1842 by(metis lcm_dvd2_int dvd_trans)
  1843 
  1844 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
  1845     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1846   by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
  1847 
  1848 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
  1849     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
  1850   using lcm_least_int zdvd_antisym_nonneg by auto
  1851 
  1852 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
  1853   + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
  1854   by standard (simp_all del: One_nat_def)
  1855 
  1856 interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
  1857 
  1858 lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
  1859 lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
  1860 lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
  1861 lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
  1862 lemmas lcm_commute_int = lcm.commute [where ?'a = int]
  1863 lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
  1864 
  1865 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
  1866 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
  1867 
  1868 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
  1869   apply (rule sym)
  1870   apply (subst lcm_unique_nat [symmetric])
  1871   apply auto
  1872 done
  1873 
  1874 lemma lcm_proj2_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm x y = \<bar>y\<bar>"
  1875   apply (rule sym)
  1876   apply (subst lcm_unique_int [symmetric])
  1877   apply auto
  1878 done
  1879 
  1880 lemma lcm_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm y x = y"
  1881 by (subst lcm_commute_nat, erule lcm_proj2_if_dvd_nat)
  1882 
  1883 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
  1884 by (subst lcm_commute_int, erule lcm_proj2_if_dvd_int)
  1885 
  1886 lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
  1887 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
  1888 
  1889 lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
  1890 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
  1891 
  1892 lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
  1893 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
  1894 
  1895 lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
  1896 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
  1897 
  1898 lemma (in semiring_gcd) comp_fun_idem_gcd:
  1899   "comp_fun_idem gcd"
  1900   by standard (simp_all add: fun_eq_iff ac_simps)
  1901 
  1902 lemma (in semiring_gcd) comp_fun_idem_lcm:
  1903   "comp_fun_idem lcm"
  1904   by standard (simp_all add: fun_eq_iff ac_simps)
  1905 
  1906 lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1907   by (fact comp_fun_idem_gcd)
  1908 
  1909 lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
  1910   by (fact comp_fun_idem_gcd)
  1911 
  1912 lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
  1913   by (fact comp_fun_idem_lcm)
  1914 
  1915 lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
  1916   by (fact comp_fun_idem_lcm)
  1917 
  1918 lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1919   by (fact lcm_eq_0_iff)
  1920 
  1921 lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m=0 \<or> n=0"
  1922   by (fact lcm_eq_0_iff)
  1923 
  1924 lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
  1925   by (simp only: lcm_eq_1_iff) simp
  1926   
  1927 lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
  1928   by auto
  1929 
  1930 
  1931 subsection \<open>The complete divisibility lattice\<close>
  1932 
  1933 interpretation gcd_semilattice_nat: semilattice_inf gcd Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
  1934   by standard simp_all
  1935 
  1936 interpretation lcm_semilattice_nat: semilattice_sup lcm Rings.dvd "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
  1937   by standard simp_all
  1938 
  1939 interpretation gcd_lcm_lattice_nat: lattice gcd Rings.dvd "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
  1940 
  1941 text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
  1942 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
  1943 \<close>
  1944 
  1945 instantiation nat :: Gcd
  1946 begin
  1947 
  1948 interpretation semilattice_neutr_set lcm "1::nat" ..
  1949 
  1950 definition
  1951   "Lcm (M::nat set) = (if finite M then F M else 0)"
  1952 
  1953 lemma Lcm_nat_empty:
  1954   "Lcm {} = (1::nat)"
  1955   by (simp add: Lcm_nat_def del: One_nat_def)
  1956 
  1957 lemma Lcm_nat_insert:
  1958   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
  1959   by (cases "finite M") (auto simp add: Lcm_nat_def simp del: One_nat_def)
  1960 
  1961 lemma Lcm_nat_infinite:
  1962   "infinite M \<Longrightarrow> Lcm M = (0::nat)"
  1963   by (simp add: Lcm_nat_def)
  1964 
  1965 lemma dvd_Lcm_nat [simp]:
  1966   fixes M :: "nat set"
  1967   assumes "m \<in> M"
  1968   shows "m dvd Lcm M"
  1969 proof -
  1970   from assms have "insert m M = M" by auto
  1971   moreover have "m dvd Lcm (insert m M)"
  1972     by (simp add: Lcm_nat_insert)
  1973   ultimately show ?thesis by simp
  1974 qed
  1975 
  1976 lemma Lcm_dvd_nat [simp]:
  1977   fixes M :: "nat set"
  1978   assumes "\<forall>m\<in>M. m dvd n"
  1979   shows "Lcm M dvd n"
  1980 proof (cases "n = 0")
  1981   case True then show ?thesis by simp
  1982 next
  1983   case False
  1984   then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
  1985   moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
  1986   ultimately have "finite M" by (rule rev_finite_subset)
  1987   then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
  1988 qed
  1989 
  1990 definition
  1991   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
  1992 
  1993 instance ..
  1994 
  1995 end
  1996 
  1997 instance nat :: semiring_Gcd
  1998 proof
  1999   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
  2000   using that by (induct N rule: infinite_finite_induct)
  2001     (auto simp add: Gcd_nat_def)
  2002   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
  2003   using that by (induct N rule: infinite_finite_induct)
  2004     (auto simp add: Gcd_nat_def)
  2005 qed simp
  2006 
  2007 instance nat :: semiring_Lcm
  2008 proof
  2009   show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
  2010     by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
  2011 qed
  2012 
  2013 interpretation gcd_lcm_complete_lattice_nat:
  2014   complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat"
  2015 rewrites "Inf.INFIMUM Gcd A f = Gcd (f ` A :: nat set)"
  2016   and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
  2017 proof -
  2018   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
  2019     by standard (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
  2020   then interpret gcd_lcm_complete_lattice_nat:
  2021     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
  2022   from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
  2023   from gcd_lcm_complete_lattice_nat.SUP_def show "Sup.SUPREMUM Lcm A f = Lcm (f ` A)" .
  2024 qed
  2025 
  2026 declare gcd_lcm_complete_lattice_nat.Inf_image_eq [simp del]
  2027 declare gcd_lcm_complete_lattice_nat.Sup_image_eq [simp del]
  2028 
  2029 lemma Lcm_empty_nat:
  2030   "Lcm {} = (1::nat)"
  2031   by (fact Lcm_empty)
  2032 
  2033 lemma Lcm_insert_nat [simp]:
  2034   "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
  2035   by (fact Lcm_insert)
  2036 
  2037 lemma Lcm_eq_0 [simp]:
  2038   "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
  2039   by (rule Lcm_eq_0_I)
  2040 
  2041 lemma Lcm0_iff [simp]:
  2042   fixes M :: "nat set"
  2043   assumes "finite M" and "M \<noteq> {}"
  2044   shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
  2045   using assms by (simp add: Lcm_0_iff)
  2046 
  2047 text\<open>Alternative characterizations of Gcd:\<close>
  2048 
  2049 lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
  2050 apply(rule antisym)
  2051  apply(rule Max_ge)
  2052   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  2053  apply (simp add: Gcd_dvd)
  2054 apply (rule Max_le_iff[THEN iffD2])
  2055   apply (metis all_not_in_conv finite_divisors_nat finite_INT)
  2056  apply fastforce
  2057 apply clarsimp
  2058 apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
  2059 done
  2060 
  2061 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
  2062 apply(induct pred:finite)
  2063  apply simp
  2064 apply(case_tac "x=0")
  2065  apply simp
  2066 apply(subgoal_tac "insert x F - {0} = insert x (F - {0})")
  2067  apply simp
  2068 apply blast
  2069 done
  2070 
  2071 lemma Lcm_in_lcm_closed_set_nat:
  2072   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M : M"
  2073 apply(induct rule:finite_linorder_min_induct)
  2074  apply simp
  2075 apply simp
  2076 apply(subgoal_tac "ALL m n :: nat. m:A \<longrightarrow> n:A \<longrightarrow> lcm m n : A")
  2077  apply simp
  2078  apply(case_tac "A={}")
  2079   apply simp
  2080  apply simp
  2081 apply (metis lcm_pos_nat lcm_unique_nat linorder_neq_iff nat_dvd_not_less not_less0)
  2082 done
  2083 
  2084 lemma Lcm_eq_Max_nat:
  2085   "finite M \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> ALL m n :: nat. m:M \<longrightarrow> n:M \<longrightarrow> lcm m n : M \<Longrightarrow> Lcm M = Max M"
  2086 apply(rule antisym)
  2087  apply(rule Max_ge, assumption)
  2088  apply(erule (2) Lcm_in_lcm_closed_set_nat)
  2089 apply clarsimp
  2090 apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
  2091 done
  2092 
  2093 lemma Lcm_set_nat [code, code_unfold]:
  2094   "Lcm (set ns) = fold lcm ns (1::nat)"
  2095   by (fact gcd_lcm_complete_lattice_nat.Sup_set_fold)
  2096 
  2097 lemma Gcd_set_nat [code]:
  2098   "Gcd (set ns) = fold gcd ns (0::nat)"
  2099   by (fact gcd_lcm_complete_lattice_nat.Inf_set_fold)
  2100 
  2101 lemma mult_inj_if_coprime_nat:
  2102   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
  2103    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
  2104   by (auto simp add: inj_on_def coprime_crossproduct_nat simp del: One_nat_def)
  2105 
  2106 text\<open>Nitpick:\<close>
  2107 
  2108 lemma gcd_eq_nitpick_gcd [nitpick_unfold]: "gcd x y = Nitpick.nat_gcd x y"
  2109 by (induct x y rule: nat_gcd.induct)
  2110    (simp add: gcd_nat.simps Nitpick.nat_gcd.simps)
  2111 
  2112 lemma lcm_eq_nitpick_lcm [nitpick_unfold]: "lcm x y = Nitpick.nat_lcm x y"
  2113 by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
  2114 
  2115 
  2116 subsubsection \<open>Setwise gcd and lcm for integers\<close>
  2117 
  2118 instantiation int :: Gcd
  2119 begin
  2120 
  2121 definition
  2122   "Lcm M = int (Lcm (nat ` abs ` M))"
  2123 
  2124 definition
  2125   "Gcd M = int (Gcd (nat ` abs ` M))"
  2126 
  2127 instance ..
  2128 
  2129 end
  2130 
  2131 instance int :: semiring_Gcd
  2132   by standard (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def Lcm_int_def int_dvd_iff dvd_int_iff
  2133     dvd_int_unfold_dvd_nat [symmetric])
  2134 
  2135 instance int :: semiring_Lcm
  2136 proof
  2137   fix K :: "int set"
  2138   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})"
  2139   proof (rule set_eqI)
  2140     fix n
  2141     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")
  2142     proof
  2143       assume ?P
  2144       then have "(\<forall>k\<in>K. k dvd int n) \<and> n = nat \<bar>int n\<bar>"
  2145         by (auto simp add: dvd_int_unfold_dvd_nat)
  2146       then show ?Q by blast
  2147     next
  2148       assume ?Q then show ?P
  2149         by (auto simp add: dvd_int_unfold_dvd_nat)
  2150     qed
  2151     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}"
  2152       by auto
  2153   qed
  2154   then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
  2155     by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd)
  2156 qed
  2157 
  2158 lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
  2159   by (fact Lcm_empty)
  2160 
  2161 lemma Lcm_insert_int [simp]:
  2162   "Lcm (insert (n::int) N) = lcm n (Lcm N)"
  2163   by (fact Lcm_insert)
  2164 
  2165 lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat \<bar>x\<bar> dvd nat \<bar>y\<bar>"
  2166   by (fact dvd_int_unfold_dvd_nat)
  2167 
  2168 lemma dvd_Lcm_int [simp]:
  2169   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
  2170   using assms by (fact dvd_Lcm)
  2171 
  2172 lemma Lcm_dvd_int [simp]:
  2173   fixes M :: "int set"
  2174   assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
  2175   using assms by (simp add: Lcm_int_def dvd_int_iff)
  2176 
  2177 lemma Lcm_set_int [code, code_unfold]:
  2178   "Lcm (set xs) = fold lcm xs (1::int)"
  2179   by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
  2180 
  2181 lemma Gcd_set_int [code]:
  2182   "Gcd (set xs) = fold gcd xs (0::int)"
  2183   by (induct xs rule: rev_induct) (simp_all add: gcd_commute_int)
  2184 
  2185 
  2186 text \<open>Fact aliasses\<close>
  2187 
  2188 lemmas gcd_dvd1_nat = gcd_dvd1 [where ?'a = nat]
  2189   and gcd_dvd2_nat = gcd_dvd2 [where ?'a = nat]
  2190   and gcd_greatest_nat = gcd_greatest [where ?'a = nat]
  2191 
  2192 lemmas gcd_dvd1_int = gcd_dvd1 [where ?'a = int]
  2193   and gcd_dvd2_int = gcd_dvd2 [where ?'a = int]
  2194   and gcd_greatest_int = gcd_greatest [where ?'a = int]
  2195 
  2196 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
  2197   and dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
  2198 
  2199 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
  2200   and dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
  2201 
  2202 lemmas Gcd_empty_nat = Gcd_empty [where ?'a = nat]
  2203   and Gcd_insert_nat = Gcd_insert [where ?'a = nat]
  2204 
  2205 lemmas Gcd_empty_int = Gcd_empty [where ?'a = int]
  2206   and Gcd_insert_int = Gcd_insert [where ?'a = int]
  2207 
  2208 subsection \<open>gcd and lcm instances for @{typ integer}\<close>
  2209 
  2210 instantiation integer :: gcd begin
  2211 context includes integer.lifting begin
  2212 lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
  2213 lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
  2214 end
  2215 instance ..
  2216 end
  2217 lifting_update integer.lifting
  2218 lifting_forget integer.lifting
  2219 
  2220 context includes integer.lifting begin
  2221 
  2222 lemma gcd_code_integer [code]:
  2223   "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
  2224 by transfer(fact gcd_code_int)
  2225 
  2226 lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
  2227 by transfer(fact lcm_altdef_int)
  2228 
  2229 end
  2230 
  2231 code_printing constant "gcd :: integer \<Rightarrow> _"
  2232   \<rightharpoonup> (OCaml) "Big'_int.gcd'_big'_int"
  2233   and (Haskell) "Prelude.gcd"
  2234   and (Scala) "_.gcd'((_)')"
  2235   -- \<open>There is no gcd operation in the SML standard library, so no code setup for SML\<close>
  2236 
  2237 end