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