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