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