src/HOL/Library/Primes.thy
author paulson
Sat Jun 09 08:41:25 2001 +0200 (2001-06-09)
changeset 11363 a548865b1b6a
child 11368 9c1995c73383
permissions -rw-r--r--
moved Primes.thy from NumberTheory to Library
     1 (*  Title:      HOL/NumberTheory/Primes.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 and Euclid's algorithm *}
     8 
     9 theory Primes = Main:
    10 
    11 text {*
    12   (See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992))
    13 
    14   \bigskip
    15 *}
    16 
    17 consts
    18   gcd  :: "nat * nat => nat"  -- {* Euclid's algorithm *}
    19 
    20 recdef gcd  "measure ((\<lambda>(m, n). n) :: nat * nat => nat)"
    21   "gcd (m, n) = (if n = 0 then m else gcd (n, m mod n))"
    22 
    23 constdefs
    24   is_gcd :: "nat => nat => nat => bool"  -- {* @{term gcd} as a relation *}
    25   "is_gcd p m n == p dvd m \<and> p dvd n \<and>
    26     (\<forall>d. d dvd m \<and> d dvd n --> d dvd p)"
    27 
    28   coprime :: "nat => nat => bool"
    29   "coprime m n == gcd (m, n) = 1"
    30 
    31   prime :: "nat set"
    32   "prime == {p. 1 < p \<and> (\<forall>m. m dvd p --> m = 1 \<or> m = p)}"
    33 
    34 
    35 lemma gcd_induct:
    36   "(!!m. P m 0) ==>
    37     (!!m n. 0 < n ==> P n (m mod n) ==> P m n)
    38   ==> P (m::nat) (n::nat)"
    39   apply (induct m n rule: gcd.induct)
    40   apply (case_tac "n = 0")
    41    apply simp_all
    42   done
    43 
    44 
    45 lemma gcd_0 [simp]: "gcd (m, 0) = m"
    46   apply simp
    47   done
    48 
    49 lemma gcd_non_0: "0 < n ==> gcd (m, n) = gcd (n, m mod n)"
    50   apply simp
    51   done
    52 
    53 declare gcd.simps [simp del]
    54 
    55 lemma gcd_1 [simp]: "gcd (m, 1) = 1"
    56   apply (simp add: gcd_non_0)
    57   done
    58 
    59 text {*
    60   \medskip @{term "gcd (m, n)"} divides @{text m} and @{text n}.  The
    61   conjunctions don't seem provable separately.
    62 *}
    63 
    64 lemma gcd_dvd_both: "gcd (m, n) dvd m \<and> gcd (m, n) dvd n"
    65   apply (induct m n rule: gcd_induct)
    66    apply (simp_all add: gcd_non_0)
    67   apply (blast dest: dvd_mod_imp_dvd)
    68   done
    69 
    70 lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1, standard]
    71 lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2, standard]
    72 
    73 
    74 text {*
    75   \medskip Maximality: for all @{term m}, @{term n}, @{term k}
    76   naturals, if @{term k} divides @{term m} and @{term k} divides
    77   @{term n} then @{term k} divides @{term "gcd (m, n)"}.
    78 *}
    79 
    80 lemma gcd_greatest: "k dvd m ==> k dvd n ==> k dvd gcd (m, n)"
    81   apply (induct m n rule: gcd_induct)
    82    apply (simp_all add: gcd_non_0 dvd_mod)
    83   done
    84 
    85 lemma gcd_greatest_iff [iff]: "(k dvd gcd (m, n)) = (k dvd m \<and> k dvd n)"
    86   apply (blast intro!: gcd_greatest intro: dvd_trans)
    87   done
    88 
    89 
    90 text {*
    91   \medskip Function gcd yields the Greatest Common Divisor.
    92 *}
    93 
    94 lemma is_gcd: "is_gcd (gcd (m, n)) m n"
    95   apply (simp add: is_gcd_def gcd_greatest)
    96   done
    97 
    98 text {*
    99   \medskip Uniqueness of GCDs.
   100 *}
   101 
   102 lemma is_gcd_unique: "is_gcd m a b ==> is_gcd n a b ==> m = n"
   103   apply (simp add: is_gcd_def)
   104   apply (blast intro: dvd_anti_sym)
   105   done
   106 
   107 lemma is_gcd_dvd: "is_gcd m a b ==> k dvd a ==> k dvd b ==> k dvd m"
   108   apply (auto simp add: is_gcd_def)
   109   done
   110 
   111 
   112 text {*
   113   \medskip Commutativity
   114 *}
   115 
   116 lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
   117   apply (auto simp add: is_gcd_def)
   118   done
   119 
   120 lemma gcd_commute: "gcd (m, n) = gcd (n, m)"
   121   apply (rule is_gcd_unique)
   122    apply (rule is_gcd)
   123   apply (subst is_gcd_commute)
   124   apply (simp add: is_gcd)
   125   done
   126 
   127 lemma gcd_assoc: "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))"
   128   apply (rule is_gcd_unique)
   129    apply (rule is_gcd)
   130   apply (simp add: is_gcd_def)
   131   apply (blast intro: dvd_trans)
   132   done
   133 
   134 lemma gcd_0_left [simp]: "gcd (0, m) = m"
   135   apply (simp add: gcd_commute [of 0])
   136   done
   137 
   138 lemma gcd_1_left [simp]: "gcd (1, m) = 1"
   139   apply (simp add: gcd_commute [of 1])
   140   done
   141 
   142 
   143 text {*
   144   \medskip Multiplication laws
   145 *}
   146 
   147 lemma gcd_mult_distrib2: "k * gcd (m, n) = gcd (k * m, k * n)"
   148     -- {* Davenport, page 27 *}
   149   apply (induct m n rule: gcd_induct)
   150    apply simp
   151   apply (case_tac "k = 0")
   152    apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
   153   done
   154 
   155 lemma gcd_mult [simp]: "gcd (k, k * n) = k"
   156   apply (rule gcd_mult_distrib2 [of k 1 n, simplified, symmetric])
   157   done
   158 
   159 lemma gcd_self [simp]: "gcd (k, k) = k"
   160   apply (rule gcd_mult [of k 1, simplified])
   161   done
   162 
   163 lemma relprime_dvd_mult: "gcd (k, n) = 1 ==> k dvd m * n ==> k dvd m"
   164   apply (insert gcd_mult_distrib2 [of m k n])
   165   apply simp
   166   apply (erule_tac t = m in ssubst)
   167   apply simp
   168   done
   169 
   170 lemma relprime_dvd_mult_iff: "gcd (k, n) = 1 ==> (k dvd m * n) = (k dvd m)"
   171   apply (blast intro: relprime_dvd_mult dvd_trans)
   172   done
   173 
   174 lemma prime_imp_relprime: "p \<in> prime ==> \<not> p dvd n ==> gcd (p, n) = 1"
   175   apply (auto simp add: prime_def)
   176   apply (drule_tac x = "gcd (p, n)" in spec)
   177   apply auto
   178   apply (insert gcd_dvd2 [of p n])
   179   apply simp
   180   done
   181 
   182 text {*
   183   This theorem leads immediately to a proof of the uniqueness of
   184   factorization.  If @{term p} divides a product of primes then it is
   185   one of those primes.
   186 *}
   187 
   188 lemma prime_dvd_mult: "p \<in> prime ==> p dvd m * n ==> p dvd m \<or> p dvd n"
   189   apply (blast intro: relprime_dvd_mult prime_imp_relprime)
   190   done
   191 
   192 
   193 text {* \medskip Addition laws *}
   194 
   195 lemma gcd_add1 [simp]: "gcd (m + n, n) = gcd (m, n)"
   196   apply (case_tac "n = 0")
   197    apply (simp_all add: gcd_non_0)
   198   done
   199 
   200 lemma gcd_add2 [simp]: "gcd (m, m + n) = gcd (m, n)"
   201   apply (rule gcd_commute [THEN trans])
   202   apply (subst add_commute)
   203   apply (simp add: gcd_add1)
   204   apply (rule gcd_commute)
   205   done
   206 
   207 lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
   208   apply (subst add_commute)
   209   apply (rule gcd_add2)
   210   done
   211 
   212 lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
   213   apply (induct k)
   214    apply (simp_all add: gcd_add2 add_assoc)
   215   done
   216 
   217 
   218 text {* \medskip More multiplication laws *}
   219 
   220 lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
   221   apply (rule dvd_anti_sym)
   222    apply (rule gcd_greatest)
   223     apply (rule_tac n = k in relprime_dvd_mult)
   224      apply (simp add: gcd_assoc)
   225      apply (simp add: gcd_commute)
   226     apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
   227   apply (blast intro: gcd_dvd1 dvd_trans)
   228   done
   229 
   230 end