src/HOL/ex/Primes.thy
 author wenzelm Tue Sep 12 22:13:23 2000 +0200 (2000-09-12) changeset 9941 fe05af7ec816 parent 9912 4b02467a4412 permissions -rw-r--r--
renamed atts: rulify to rule_format, elimify to elim_format;
```     1 (*  Title:      HOL/ex/Primes.thy
```
```     2     ID:         \$Id\$
```
```     3     Author:     Christophe Tabacznyj and Lawrence C Paulson
```
```     4     Copyright   1996  University of Cambridge
```
```     5
```
```     6 The Greatest Common Divisor and Euclid's algorithm
```
```     7
```
```     8 See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
```
```     9 *)
```
```    10
```
```    11 theory Primes = Main:
```
```    12 consts
```
```    13   gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
```
```    14
```
```    15 recdef gcd "measure ((%(m,n).n) ::nat*nat=>nat)"
```
```    16     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
```
```    17
```
```    18 constdefs
```
```    19   is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
```
```    20     "is_gcd p m n == p dvd m  &  p dvd n  &
```
```    21                      (ALL d. d dvd m & d dvd n --> d dvd p)"
```
```    22
```
```    23   coprime :: "[nat,nat]=>bool"
```
```    24     "coprime m n == gcd(m,n) = 1"
```
```    25
```
```    26   prime   :: "nat set"
```
```    27     "prime == {p. 1<p & (ALL m. m dvd p --> m=1 | m=p)}"
```
```    28
```
```    29
```
```    30 (************************************************)
```
```    31 (** Greatest Common Divisor                    **)
```
```    32 (************************************************)
```
```    33
```
```    34 (*** Euclid's Algorithm ***)
```
```    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_tac 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,1) = 1"
```
```    58   apply (simp add: gcd_non_0)
```
```    59   done
```
```    60
```
```    61 (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
```
```    62 lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
```
```    63   apply (induct_tac m n rule: gcd_induct)
```
```    64   apply (simp_all add: gcd_non_0)
```
```    65   apply (blast dest: dvd_mod_imp_dvd)
```
```    66   done
```
```    67
```
```    68 lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
```
```    69 lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
```
```    70
```
```    71
```
```    72 (*Maximality: for all m,n,k naturals,
```
```    73                 if k divides m and k divides n then k divides gcd(m,n)*)
```
```    74 lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
```
```    75   apply (induct_tac m n rule: gcd_induct)
```
```    76   apply (simp_all add: gcd_non_0 dvd_mod);
```
```    77   done;
```
```    78
```
```    79 lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
```
```    80   apply (blast intro!: gcd_greatest intro: dvd_trans);
```
```    81   done;
```
```    82
```
```    83 (*Function gcd yields the Greatest Common Divisor*)
```
```    84 lemma is_gcd: "is_gcd (gcd(m,n)) m n"
```
```    85   apply (simp add: is_gcd_def gcd_greatest)
```
```    86   done
```
```    87
```
```    88 (*uniqueness of GCDs*)
```
```    89 lemma is_gcd_unique: "[| is_gcd m a b; is_gcd n a b |] ==> m=n"
```
```    90   apply (simp add: is_gcd_def);
```
```    91   apply (blast intro: dvd_anti_sym)
```
```    92   done
```
```    93
```
```    94 lemma is_gcd_dvd: "[| is_gcd m a b; k dvd a; k dvd b |] ==> k dvd m"
```
```    95   apply (auto simp add: is_gcd_def);
```
```    96   done
```
```    97
```
```    98 (** Commutativity **)
```
```    99
```
```   100 lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m"
```
```   101   apply (auto simp add: is_gcd_def);
```
```   102   done
```
```   103
```
```   104 lemma gcd_commute: "gcd(m,n) = gcd(n,m)"
```
```   105   apply (rule is_gcd_unique)
```
```   106   apply (rule is_gcd)
```
```   107   apply (subst is_gcd_commute)
```
```   108   apply (simp add: is_gcd)
```
```   109   done
```
```   110
```
```   111 lemma gcd_assoc: "gcd(gcd(k,m),n) = gcd(k,gcd(m,n))"
```
```   112   apply (rule is_gcd_unique)
```
```   113   apply (rule is_gcd)
```
```   114   apply (simp add: is_gcd_def);
```
```   115   apply (blast intro: dvd_trans);
```
```   116   done
```
```   117
```
```   118 lemma gcd_0_left [simp]: "gcd(0,m) = m"
```
```   119   apply (simp add: gcd_commute [of 0])
```
```   120   done
```
```   121
```
```   122 lemma gcd_1_left [simp]: "gcd(1,m) = 1"
```
```   123   apply (simp add: gcd_commute [of 1])
```
```   124   done
```
```   125
```
```   126
```
```   127 (** Multiplication laws **)
```
```   128
```
```   129 (*Davenport, page 27*)
```
```   130 lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)"
```
```   131   apply (induct_tac m n rule: gcd_induct)
```
```   132   apply (simp)
```
```   133   apply (case_tac "k=0")
```
```   134   apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2)
```
```   135   done
```
```   136
```
```   137 lemma gcd_self [simp]: "gcd(m,m) = m"
```
```   138   apply (rule gcd_mult_distrib2 [of m 1 1, simplified, THEN sym])
```
```   139   done
```
```   140
```
```   141 lemma gcd_mult [simp]: "gcd(k, k*n) = k"
```
```   142   apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
```
```   143   done
```
```   144
```
```   145 lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
```
```   146    apply (subgoal_tac "gcd(m*k, m*n) = m")
```
```   147    apply (erule_tac t="m" in subst);
```
```   148    apply (simp)
```
```   149    apply (simp add: gcd_mult_distrib2 [THEN sym]);
```
```   150   done
```
```   151
```
```   152 lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
```
```   153   apply (blast intro: relprime_dvd_mult dvd_trans)
```
```   154   done
```
```   155
```
```   156 lemma prime_imp_relprime: "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1"
```
```   157   apply (auto simp add: prime_def)
```
```   158   apply (drule_tac x="gcd(p,n)" in spec)
```
```   159   apply auto
```
```   160   apply (insert gcd_dvd2 [of p n])
```
```   161   apply (simp)
```
```   162   done
```
```   163
```
```   164 (*This theorem leads immediately to a proof of the uniqueness of factorization.
```
```   165   If p divides a product of primes then it is one of those primes.*)
```
```   166 lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
```
```   167   apply (blast intro: relprime_dvd_mult prime_imp_relprime)
```
```   168   done
```
```   169
```
```   170
```
```   171 (** Addition laws **)
```
```   172
```
```   173 lemma gcd_add1 [simp]: "gcd(m+n, n) = gcd(m,n)"
```
```   174   apply (case_tac "n=0")
```
```   175   apply (simp_all add: gcd_non_0)
```
```   176   done
```
```   177
```
```   178 lemma gcd_add2 [simp]: "gcd(m, m+n) = gcd(m,n)"
```
```   179   apply (rule gcd_commute [THEN trans])
```
```   180   apply (subst add_commute)
```
```   181   apply (simp add: gcd_add1)
```
```   182   apply (rule gcd_commute)
```
```   183   done
```
```   184
```
```   185 lemma gcd_add2' [simp]: "gcd(m, n+m) = gcd(m,n)"
```
```   186   apply (subst add_commute)
```
```   187   apply (rule gcd_add2)
```
```   188   done
```
```   189
```
```   190 lemma gcd_add_mult: "gcd(m, k*m+n) = gcd(m,n)"
```
```   191   apply (induct_tac "k")
```
```   192   apply (simp_all add: gcd_add2 add_assoc)
```
```   193   done
```
```   194
```
```   195
```
```   196 (** More multiplication laws **)
```
```   197
```
```   198 lemma gcd_mult_cancel: "gcd(k,n) = 1 ==> gcd(k*m, n) = gcd(m,n)"
```
```   199   apply (rule dvd_anti_sym)
```
```   200    apply (rule gcd_greatest)
```
```   201     apply (rule_tac n="k" in relprime_dvd_mult)
```
```   202      apply (simp add: gcd_assoc)
```
```   203      apply (simp add: gcd_commute)
```
```   204     apply (simp_all add: mult_commute gcd_dvd1 gcd_dvd2)
```
```   205   apply (blast intro: gcd_dvd1 dvd_trans);
```
```   206   done
```
```   207
```
```   208 end
```