src/HOL/Library/GCD.thy
author haftmann
Mon Jul 07 08:47:17 2008 +0200 (2008-07-07)
changeset 27487 c8a6ce181805
parent 27368 9f90ac19e32b
child 27556 292098f2efdf
permissions -rw-r--r--
absolute imports of HOL/*.thy theories
     1 (*  Title:      HOL/GCD.thy
     2     ID:         $Id$
     3     Author:     Christophe Tabacznyj and Lawrence C Paulson
     4     Copyright   1996  University of Cambridge
     5 *)
     6 
     7 header {* The Greatest Common Divisor *}
     8 
     9 theory GCD
    10 imports Plain "~~/src/HOL/Presburger"
    11 begin
    12 
    13 text {*
    14   See \cite{davenport92}. \bigskip
    15 *}
    16 
    17 subsection {* Specification of GCD on nats *}
    18 
    19 definition
    20   is_gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" where -- {* @{term gcd} as a relation *}
    21   [code func del]: "is_gcd p m n \<longleftrightarrow> p dvd m \<and> p dvd n \<and>
    22     (\<forall>d. d dvd m \<longrightarrow> d dvd n \<longrightarrow> d dvd p)"
    23 
    24 text {* Uniqueness *}
    25 
    26 lemma is_gcd_unique: "is_gcd m a b \<Longrightarrow> is_gcd n a b \<Longrightarrow> m = n"
    27   by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
    28 
    29 text {* Connection to divides relation *}
    30 
    31 lemma is_gcd_dvd: "is_gcd m a b \<Longrightarrow> k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd m"
    32   by (auto simp add: is_gcd_def)
    33 
    34 text {* Commutativity *}
    35 
    36 lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
    37   by (auto simp add: is_gcd_def)
    38 
    39 
    40 subsection {* GCD on nat by Euclid's algorithm *}
    41 
    42 fun
    43   gcd  :: "nat \<times> nat => nat"
    44 where
    45   "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    46 
    47 lemma gcd_induct:
    48   fixes m n :: nat
    49   assumes "\<And>m. P m 0"
    50     and "\<And>m n. 0 < n \<Longrightarrow> P n (m mod n) \<Longrightarrow> P m n"
    51   shows "P m n"
    52 apply (rule gcd.induct [of "split P" "(m, n)", unfolded Product_Type.split])
    53 apply (case_tac "n = 0")
    54 apply simp_all
    55 using assms apply simp_all
    56 done
    57 
    58 lemma gcd_0 [simp]: "gcd (m, 0) = m"
    59   by simp
    60 
    61 lemma gcd_0_left [simp]: "gcd (0, m) = m"
    62   by simp
    63 
    64 lemma gcd_non_0: "n > 0 \<Longrightarrow> gcd (m, n) = gcd (n, m mod n)"
    65   by simp
    66 
    67 lemma gcd_1 [simp]: "gcd (m, Suc 0) = 1"
    68   by simp
    69 
    70 declare gcd.simps [simp del]
    71 
    72 text {*
    73   \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    74   conjunctions don't seem provable separately.
    75 *}
    76 
    77 lemma gcd_dvd1 [iff]: "gcd (m, n) dvd m"
    78   and gcd_dvd2 [iff]: "gcd (m, n) dvd n"
    79   apply (induct m n rule: gcd_induct)
    80      apply (simp_all add: gcd_non_0)
    81   apply (blast dest: dvd_mod_imp_dvd)
    82   done
    83 
    84 text {*
    85   \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    86   naturals, if @{term k} divides @{term m} and @{term k} divides
    87   @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    88 *}
    89 
    90 lemma gcd_greatest: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd gcd (m, n)"
    91   by (induct m n rule: gcd_induct) (simp_all add: gcd_non_0 dvd_mod)
    92 
    93 text {*
    94   \medskip Function gcd yields the Greatest Common Divisor.
    95 *}
    96 
    97 lemma is_gcd: "is_gcd (gcd (m, n)) m n"
    98   by (simp add: is_gcd_def gcd_greatest)
    99 
   100 
   101 subsection {* Derived laws for GCD *}
   102 
   103 lemma gcd_greatest_iff [iff]: "k dvd gcd (m, n) \<longleftrightarrow> k dvd m \<and> k dvd n"
   104   by (blast intro!: gcd_greatest intro: dvd_trans)
   105 
   106 lemma gcd_zero: "gcd (m, n) = 0 \<longleftrightarrow> m = 0 \<and> n = 0"
   107   by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff)
   108 
   109 lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   110   apply (rule is_gcd_unique)
   111    apply (rule is_gcd)
   112   apply (subst is_gcd_commute)
   113   apply (simp add: is_gcd)
   114   done
   115 
   116 lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   117   apply (rule is_gcd_unique)
   118    apply (rule is_gcd)
   119   apply (simp add: is_gcd_def)
   120   apply (blast intro: dvd_trans)
   121   done
   122 
   123 lemma gcd_1_left [simp]: "gcd (Suc 0, m) = 1"
   124   by (simp add: gcd_commute)
   125 
   126 text {*
   127   \medskip Multiplication laws
   128 *}
   129 
   130 lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   131     -- {* \cite[page 27]{davenport92} *}
   132   apply (induct m n rule: gcd_induct)
   133    apply simp
   134   apply (case_tac "k = 0")
   135    apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   136   done
   137 
   138 lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   139   apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   140   done
   141 
   142 lemma gcd_self [simp]: "gcd (k, k) = k"
   143   apply (rule gcd_mult [of k 1, simplified])
   144   done
   145 
   146 lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   147   apply (insert gcd_mult_distrib2 [of m k n])
   148   apply simp
   149   apply (erule_tac t = m in ssubst)
   150   apply simp
   151   done
   152 
   153 lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   154   apply (blast intro: relprime_dvd_mult dvd_trans)
   155   done
   156 
   157 lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   158   apply (rule dvd_anti_sym)
   159    apply (rule gcd_greatest)
   160     apply (rule_tac n = k in relprime_dvd_mult)
   161      apply (simp add: gcd_assoc)
   162      apply (simp add: gcd_commute)
   163     apply (simp_all add: mult_commute)
   164   apply (blast intro: dvd_trans)
   165   done
   166 
   167 
   168 text {* \medskip Addition laws *}
   169 
   170 lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   171   apply (case_tac "n = 0")
   172    apply (simp_all add: gcd_non_0)
   173   done
   174 
   175 lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   176 proof -
   177   have "gcd (m, m + n) = gcd (m + n, m)" by (rule gcd_commute)
   178   also have "... = gcd (n + m, m)" by (simp add: add_commute)
   179   also have "... = gcd (n, m)" by simp
   180   also have  "... = gcd (m, n)" by (rule gcd_commute)
   181   finally show ?thesis .
   182 qed
   183 
   184 lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   185   apply (subst add_commute)
   186   apply (rule gcd_add2)
   187   done
   188 
   189 lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   190   by (induct k) (simp_all add: add_assoc)
   191 
   192 lemma gcd_dvd_prod: "gcd (m, n) dvd m * n"
   193   using mult_dvd_mono [of 1] by auto
   194 
   195 text {*
   196   \medskip Division by gcd yields rrelatively primes.
   197 *}
   198 
   199 lemma div_gcd_relprime:
   200   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   201   shows "gcd (a div gcd(a,b), b div gcd(a,b)) = 1"
   202 proof -
   203   let ?g = "gcd (a, b)"
   204   let ?a' = "a div ?g"
   205   let ?b' = "b div ?g"
   206   let ?g' = "gcd (?a', ?b')"
   207   have dvdg: "?g dvd a" "?g dvd b" by simp_all
   208   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by simp_all
   209   from dvdg dvdg' obtain ka kb ka' kb' where
   210       kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
   211     unfolding dvd_def by blast
   212   then have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'" by simp_all
   213   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   214     by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)]
   215       dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   216   have "?g \<noteq> 0" using nz by (simp add: gcd_zero)
   217   then have gp: "?g > 0" by simp
   218   from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   219   with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
   220 qed
   221 
   222 subsection {* LCM defined by GCD *}
   223 
   224 definition
   225   lcm :: "nat \<times> nat \<Rightarrow> nat"
   226 where
   227   lcm_prim_def: "lcm = (\<lambda>(m, n). m * n div gcd (m, n))"
   228 
   229 lemma lcm_def:
   230   "lcm (m, n) = m * n div gcd (m, n)"
   231   unfolding lcm_prim_def by simp
   232 
   233 lemma prod_gcd_lcm:
   234   "m * n = gcd (m, n) * lcm (m, n)"
   235   unfolding lcm_def by (simp add: dvd_mult_div_cancel [OF gcd_dvd_prod])
   236 
   237 lemma lcm_0 [simp]: "lcm (m, 0) = 0"
   238   unfolding lcm_def by simp
   239 
   240 lemma lcm_1 [simp]: "lcm (m, 1) = m"
   241   unfolding lcm_def by simp
   242 
   243 lemma lcm_0_left [simp]: "lcm (0, n) = 0"
   244   unfolding lcm_def by simp
   245 
   246 lemma lcm_1_left [simp]: "lcm (1, m) = m"
   247   unfolding lcm_def by simp
   248 
   249 lemma dvd_pos:
   250   fixes n m :: nat
   251   assumes "n > 0" and "m dvd n"
   252   shows "m > 0"
   253 using assms by (cases m) auto
   254 
   255 lemma lcm_least:
   256   assumes "m dvd k" and "n dvd k"
   257   shows "lcm (m, n) dvd k"
   258 proof (cases k)
   259   case 0 then show ?thesis by auto
   260 next
   261   case (Suc _) then have pos_k: "k > 0" by auto
   262   from assms dvd_pos [OF this] have pos_mn: "m > 0" "n > 0" by auto
   263   with gcd_zero [of m n] have pos_gcd: "gcd (m, n) > 0" by simp
   264   from assms obtain p where k_m: "k = m * p" using dvd_def by blast
   265   from assms obtain q where k_n: "k = n * q" using dvd_def by blast
   266   from pos_k k_m have pos_p: "p > 0" by auto
   267   from pos_k k_n have pos_q: "q > 0" by auto
   268   have "k * k * gcd (q, p) = k * gcd (k * q, k * p)"
   269     by (simp add: mult_ac gcd_mult_distrib2)
   270   also have "\<dots> = k * gcd (m * p * q, n * q * p)"
   271     by (simp add: k_m [symmetric] k_n [symmetric])
   272   also have "\<dots> = k * p * q * gcd (m, n)"
   273     by (simp add: mult_ac gcd_mult_distrib2)
   274   finally have "(m * p) * (n * q) * gcd (q, p) = k * p * q * gcd (m, n)"
   275     by (simp only: k_m [symmetric] k_n [symmetric])
   276   then have "p * q * m * n * gcd (q, p) = p * q * k * gcd (m, n)"
   277     by (simp add: mult_ac)
   278   with pos_p pos_q have "m * n * gcd (q, p) = k * gcd (m, n)"
   279     by simp
   280   with prod_gcd_lcm [of m n]
   281   have "lcm (m, n) * gcd (q, p) * gcd (m, n) = k * gcd (m, n)"
   282     by (simp add: mult_ac)
   283   with pos_gcd have "lcm (m, n) * gcd (q, p) = k" by simp
   284   then show ?thesis using dvd_def by auto
   285 qed
   286 
   287 lemma lcm_dvd1 [iff]:
   288   "m dvd lcm (m, n)"
   289 proof (cases m)
   290   case 0 then show ?thesis by simp
   291 next
   292   case (Suc _)
   293   then have mpos: "m > 0" by simp
   294   show ?thesis
   295   proof (cases n)
   296     case 0 then show ?thesis by simp
   297   next
   298     case (Suc _)
   299     then have npos: "n > 0" by simp
   300     have "gcd (m, n) dvd n" by simp
   301     then obtain k where "n = gcd (m, n) * k" using dvd_def by auto
   302     then have "m * n div gcd (m, n) = m * (gcd (m, n) * k) div gcd (m, n)" by (simp add: mult_ac)
   303     also have "\<dots> = m * k" using mpos npos gcd_zero by simp
   304     finally show ?thesis by (simp add: lcm_def)
   305   qed
   306 qed
   307 
   308 lemma lcm_dvd2 [iff]: 
   309   "n dvd lcm (m, n)"
   310 proof (cases n)
   311   case 0 then show ?thesis by simp
   312 next
   313   case (Suc _)
   314   then have npos: "n > 0" by simp
   315   show ?thesis
   316   proof (cases m)
   317     case 0 then show ?thesis by simp
   318   next
   319     case (Suc _)
   320     then have mpos: "m > 0" by simp
   321     have "gcd (m, n) dvd m" by simp
   322     then obtain k where "m = gcd (m, n) * k" using dvd_def by auto
   323     then have "m * n div gcd (m, n) = (gcd (m, n) * k) * n div gcd (m, n)" by (simp add: mult_ac)
   324     also have "\<dots> = n * k" using mpos npos gcd_zero by simp
   325     finally show ?thesis by (simp add: lcm_def)
   326   qed
   327 qed
   328 
   329 
   330 subsection {* GCD and LCM on integers *}
   331 
   332 definition
   333   igcd :: "int \<Rightarrow> int \<Rightarrow> int" where
   334   "igcd i j = int (gcd (nat (abs i), nat (abs j)))"
   335 
   336 lemma igcd_dvd1 [simp]: "igcd i j dvd i"
   337   by (simp add: igcd_def int_dvd_iff)
   338 
   339 lemma igcd_dvd2 [simp]: "igcd i j dvd j"
   340   by (simp add: igcd_def int_dvd_iff)
   341 
   342 lemma igcd_pos: "igcd i j \<ge> 0"
   343   by (simp add: igcd_def)
   344 
   345 lemma igcd0 [simp]: "(igcd i j = 0) = (i = 0 \<and> j = 0)"
   346   by (simp add: igcd_def gcd_zero) arith
   347 
   348 lemma igcd_commute: "igcd i j = igcd j i"
   349   unfolding igcd_def by (simp add: gcd_commute)
   350 
   351 lemma igcd_neg1 [simp]: "igcd (- i) j = igcd i j"
   352   unfolding igcd_def by simp
   353 
   354 lemma igcd_neg2 [simp]: "igcd i (- j) = igcd i j"
   355   unfolding igcd_def by simp
   356 
   357 lemma zrelprime_dvd_mult: "igcd i j = 1 \<Longrightarrow> i dvd k * j \<Longrightarrow> i dvd k"
   358   unfolding igcd_def
   359 proof -
   360   assume "int (gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>)) = 1" "i dvd k * j"
   361   then have g: "gcd (nat \<bar>i\<bar>, nat \<bar>j\<bar>) = 1" by simp
   362   from `i dvd k * j` obtain h where h: "k*j = i*h" unfolding dvd_def by blast
   363   have th: "nat \<bar>i\<bar> dvd nat \<bar>k\<bar> * nat \<bar>j\<bar>"
   364     unfolding dvd_def
   365     by (rule_tac x= "nat \<bar>h\<bar>" in exI, simp add: h nat_abs_mult_distrib [symmetric])
   366   from relprime_dvd_mult [OF g th] obtain h' where h': "nat \<bar>k\<bar> = nat \<bar>i\<bar> * h'"
   367     unfolding dvd_def by blast
   368   from h' have "int (nat \<bar>k\<bar>) = int (nat \<bar>i\<bar> * h')" by simp
   369   then have "\<bar>k\<bar> = \<bar>i\<bar> * int h'" by (simp add: int_mult)
   370   then show ?thesis
   371     apply (subst zdvd_abs1 [symmetric])
   372     apply (subst zdvd_abs2 [symmetric])
   373     apply (unfold dvd_def)
   374     apply (rule_tac x = "int h'" in exI, simp)
   375     done
   376 qed
   377 
   378 lemma int_nat_abs: "int (nat (abs x)) = abs x"  by arith
   379 
   380 lemma igcd_greatest:
   381   assumes "k dvd m" and "k dvd n"
   382   shows "k dvd igcd m n"
   383 proof -
   384   let ?k' = "nat \<bar>k\<bar>"
   385   let ?m' = "nat \<bar>m\<bar>"
   386   let ?n' = "nat \<bar>n\<bar>"
   387   from `k dvd m` and `k dvd n` have dvd': "?k' dvd ?m'" "?k' dvd ?n'"
   388     unfolding zdvd_int by (simp_all only: int_nat_abs zdvd_abs1 zdvd_abs2)
   389   from gcd_greatest [OF dvd'] have "int (nat \<bar>k\<bar>) dvd igcd m n"
   390     unfolding igcd_def by (simp only: zdvd_int)
   391   then have "\<bar>k\<bar> dvd igcd m n" by (simp only: int_nat_abs)
   392   then show "k dvd igcd m n" by (simp add: zdvd_abs1)
   393 qed
   394 
   395 lemma div_igcd_relprime:
   396   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
   397   shows "igcd (a div (igcd a b)) (b div (igcd a b)) = 1"
   398 proof -
   399   from nz have nz': "nat \<bar>a\<bar> \<noteq> 0 \<or> nat \<bar>b\<bar> \<noteq> 0" by arith 
   400   let ?g = "igcd a b"
   401   let ?a' = "a div ?g"
   402   let ?b' = "b div ?g"
   403   let ?g' = "igcd ?a' ?b'"
   404   have dvdg: "?g dvd a" "?g dvd b" by (simp_all add: igcd_dvd1 igcd_dvd2)
   405   have dvdg': "?g' dvd ?a'" "?g' dvd ?b'" by (simp_all add: igcd_dvd1 igcd_dvd2)
   406   from dvdg dvdg' obtain ka kb ka' kb' where
   407    kab: "a = ?g*ka" "b = ?g*kb" "?a' = ?g'*ka'" "?b' = ?g' * kb'"
   408     unfolding dvd_def by blast
   409   then have "?g* ?a' = (?g * ?g') * ka'" "?g* ?b' = (?g * ?g') * kb'" by simp_all
   410   then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
   411     by (auto simp add: zdvd_mult_div_cancel [OF dvdg(1)]
   412       zdvd_mult_div_cancel [OF dvdg(2)] dvd_def)
   413   have "?g \<noteq> 0" using nz by simp
   414   then have gp: "?g \<noteq> 0" using igcd_pos[where i="a" and j="b"] by arith
   415   from igcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
   416   with zdvd_mult_cancel1 [OF gp] have "\<bar>?g'\<bar> = 1" by simp
   417   with igcd_pos show "?g' = 1" by simp
   418 qed
   419 
   420 definition "ilcm = (\<lambda>i j. int (lcm(nat(abs i),nat(abs j))))"
   421 
   422 lemma dvd_ilcm_self1[simp]: "i dvd ilcm i j"
   423 by(simp add:ilcm_def dvd_int_iff)
   424 
   425 lemma dvd_ilcm_self2[simp]: "j dvd ilcm i j"
   426 by(simp add:ilcm_def dvd_int_iff)
   427 
   428 
   429 lemma dvd_imp_dvd_ilcm1:
   430   assumes "k dvd i" shows "k dvd (ilcm i j)"
   431 proof -
   432   have "nat(abs k) dvd nat(abs i)" using `k dvd i`
   433     by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
   434   thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
   435 qed
   436 
   437 lemma dvd_imp_dvd_ilcm2:
   438   assumes "k dvd j" shows "k dvd (ilcm i j)"
   439 proof -
   440   have "nat(abs k) dvd nat(abs j)" using `k dvd j`
   441     by(simp add:int_dvd_iff[symmetric] dvd_int_iff[symmetric] zdvd_abs1)
   442   thus ?thesis by(simp add:ilcm_def dvd_int_iff)(blast intro: dvd_trans)
   443 qed
   444 
   445 
   446 lemma zdvd_self_abs1: "(d::int) dvd (abs d)"
   447 by (case_tac "d <0", simp_all)
   448 
   449 lemma zdvd_self_abs2: "(abs (d::int)) dvd d"
   450 by (case_tac "d<0", simp_all)
   451 
   452 (* lcm a b is positive for positive a and b *)
   453 
   454 lemma lcm_pos: 
   455   assumes mpos: "m > 0"
   456   and npos: "n>0"
   457   shows "lcm (m,n) > 0"
   458 proof(rule ccontr, simp add: lcm_def gcd_zero)
   459 assume h:"m*n div gcd(m,n) = 0"
   460 from mpos npos have "gcd (m,n) \<noteq> 0" using gcd_zero by simp
   461 hence gcdp: "gcd(m,n) > 0" by simp
   462 with h
   463 have "m*n < gcd(m,n)"
   464   by (cases "m * n < gcd (m, n)") (auto simp add: div_if[OF gcdp, where m="m*n"])
   465 moreover 
   466 have "gcd(m,n) dvd m" by simp
   467  with mpos dvd_imp_le have t1:"gcd(m,n) \<le> m" by simp
   468  with npos have t1:"gcd(m,n)*n \<le> m*n" by simp
   469  have "gcd(m,n) \<le> gcd(m,n)*n" using npos by simp
   470  with t1 have "gcd(m,n) \<le> m*n" by arith
   471 ultimately show "False" by simp
   472 qed
   473 
   474 lemma ilcm_pos: 
   475   assumes anz: "a \<noteq> 0"
   476   and bnz: "b \<noteq> 0" 
   477   shows "0 < ilcm a b"
   478 proof-
   479   let ?na = "nat (abs a)"
   480   let ?nb = "nat (abs b)"
   481   have nap: "?na >0" using anz by simp
   482   have nbp: "?nb >0" using bnz by simp
   483   have "0 < lcm (?na,?nb)" by (rule lcm_pos[OF nap nbp])
   484   thus ?thesis by (simp add: ilcm_def)
   485 qed
   486 
   487 end