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