10142

1 
(* Title: HOL/NumberTheory/Primes.thy

9944

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_mult [simp]: "gcd(k, k*n) = k"


138 
apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])


139 
done


140 


141 
lemma gcd_self [simp]: "gcd(k,k) = k"


142 
apply (rule gcd_mult [of k 1, simplified])


143 
done


144 


145 
lemma relprime_dvd_mult: "[ gcd(k,n)=1; k dvd (m*n) ] ==> k dvd m";


146 
apply (insert gcd_mult_distrib2 [of m k n])


147 
apply (simp)


148 
apply (erule_tac t="m" in ssubst);


149 
apply (simp)


150 
done


151 

10142

152 
lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> k dvd (m*n) = k dvd m";

9944

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
