src/HOL/Library/Primes.thy
 author nipkow Mon Aug 16 14:22:27 2004 +0200 (2004-08-16) changeset 15131 c69542757a4d parent 14706 71590b7733b7 child 15140 322485b816ac permissions -rw-r--r--
```     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 import 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   apply (rule gcd_commute [THEN trans])
```
```   214   apply (subst add_commute)
```
```   215   apply (simp add: gcd_add1)
```
```   216   apply (rule gcd_commute)
```
```   217   done
```
```   218
```
```   219 lemma gcd_add2' [simp]: "gcd (m, n + m) = gcd (m, n)"
```
```   220   apply (subst add_commute)
```
```   221   apply (rule gcd_add2)
```
```   222   done
```
```   223
```
```   224 lemma gcd_add_mult: "gcd (m, k * m + n) = gcd (m, n)"
```
```   225   apply (induct k)
```
```   226    apply (simp_all add: gcd_add2 add_assoc)
```
```   227   done
```
```   228
```
```   229
```
```   230 text {* \medskip More multiplication laws *}
```
```   231
```
```   232 lemma gcd_mult_cancel: "gcd (k, n) = 1 ==> gcd (k * m, n) = gcd (m, n)"
```
```   233   apply (rule dvd_anti_sym)
```
```   234    apply (rule gcd_greatest)
```
```   235     apply (rule_tac n = k in relprime_dvd_mult)
```
```   236      apply (simp add: gcd_assoc)
```
```   237      apply (simp add: gcd_commute)
```
```   238     apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
```
```   239   apply (blast intro: gcd_dvd1 dvd_trans)
```
```   240   done
```
```   241
```
```   242 end
```