src/HOL/ex/Primes.ML

--- a/src/HOL/ex/Primes.ML	Fri May 30 15:23:49 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Fri May 30 15:24:27 1997 +0200
@@ -4,6 +4,8 @@
     Copyright   1996  University of Cambridge
 
 The "divides" relation, the greatest common divisor and Euclid's algorithm
+
+See H. Davenport, "The Higher Arithmetic".  6th edition.  (CUP, 1992)
 *)
 
 eta_contract:=false;
@@ -11,63 +13,6 @@
 open Primes;
 
 (************************************************)
-(** Divides Relation                           **)
-(************************************************)
-
-goalw thy [dvd_def] "m dvd 0";
-by (fast_tac (!claset addIs [mult_0_right RS sym]) 1);
-qed "dvd_0_right";
-Addsimps [dvd_0_right];
-
-goalw thy [dvd_def] "!!m. 0 dvd m ==> m = 0";
-by (fast_tac (!claset addss !simpset) 1);
-qed "dvd_0_left";
-
-goalw thy [dvd_def] "m dvd m";
-by (fast_tac (!claset addIs [mult_1_right RS sym]) 1);
-qed "dvd_refl";
-Addsimps [dvd_refl];
-
-goalw thy [dvd_def] "!!m n p. [| m dvd n; n dvd p |] ==> m dvd p";
-by (fast_tac (!claset addIs [mult_assoc] ) 1);
-qed "dvd_trans";
-
-goalw thy [dvd_def] "!!m n. [| m dvd n; n dvd m |] ==> m=n";
-by (fast_tac (!claset addDs [mult_eq_self_implies_10]
-                     addss (!simpset addsimps [mult_assoc, mult_eq_1_iff])) 1);
-qed "dvd_anti_sym";
-
-goalw thy [dvd_def] "!!k. [| k dvd m; k dvd n |] ==> k dvd (m + n)";
-by (blast_tac (!claset addIs [add_mult_distrib2 RS sym]) 1);
-qed "dvd_add";
-
-goalw thy [dvd_def] "!!k. k dvd m ==> k dvd (q * m)";
-by (blast_tac (!claset addIs [mult_left_commute]) 1);
-qed "dvd_mult";
-
-(*Based on a theorem of F. Kammüller's.  Doesn't really belong here...*)
-goal Primes.thy "!!C. finite C ==> finite (Union C) --> \
-\          (! c : C. k dvd card c) -->  \
-\          (! c1: C. ! c2: C. c1 ~= c2 --> c1 Int c2 = {}) \
-\          --> k dvd card(Union C)";
-by (etac finite_induct 1);
-by (ALLGOALS Asm_simp_tac);
-by (strip_tac 1);
-by (REPEAT (etac conjE 1));
-by (stac card_Un_disjoint 1);
-by (ALLGOALS
-    (asm_full_simp_tac (!simpset
-			 addsimps [dvd_add, disjoint_eq_subset_Compl])));
-by (thin_tac "?PP-->?QQ" 1);
-by (thin_tac "!c:F. ?PP(c)" 1);
-by (thin_tac "!c:F. ?PP(c) & ?QQ(c)" 1);
-by (Step_tac 1);
-by (ball_tac 1);
-by (Blast_tac 1);
-qed "dvd_partition";
-
-
-(************************************************)
 (** Greatest Common Divisor                    **)
 (************************************************)
 
@@ -100,39 +45,18 @@
 by (Simp_tac 1);
 qed "gcd_0_dvd_0";
 
-goal thy "!!k. [| k dvd (m mod n); k dvd n; n~=0 |] ==> k dvd m";
-by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
-by (asm_simp_tac (!simpset addsimps [dvd_add, dvd_mult]) 2);
-by (asm_full_simp_tac (!simpset addsimps [mod_div_equality, zero_less_eq]) 1);
-qed "gcd_recursion";
-
-
 (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
 goal thy "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
 by (ALLGOALS 
     (asm_simp_tac (!simpset addsimps [mod_less_divisor,zero_less_eq])));
-by (blast_tac (!claset addDs [gcd_recursion]) 1);
+by (blast_tac (!claset addDs [dvd_mod_imp_dvd]) 1);
 qed "gcd_divides_both";
 
-
-(* if f divides m and n then f divides gcd(m,n) *)
-
-goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
-by (Step_tac 1);
-by (full_simp_tac (!simpset addsimps [zero_less_mult_iff]) 1);
-by (res_inst_tac 
-    [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
-    exI 1);
-by (asm_simp_tac (!simpset addsimps [diff_mult_distrib2, 
-                                     mult_mod_distrib, add_mult_distrib2]) 1);
-qed "dvd_mod";
-
-
 (*Maximality: for all m,n,f naturals, 
                 if f divides m and f divides n then f divides gcd(m,n)*)
-goal thy "!!k. (f dvd m) & (f dvd n) --> f dvd gcd(m,n)";
+goal thy "!!k. (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
 by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
 by (case_tac "n=0" 1);
 by (ALLGOALS 
@@ -140,15 +64,35 @@
 				      zero_less_eq])));
 qed_spec_mp "gcd_greatest";
 
-(* GCD PROOF : GCD exists and gcd fits the definition *)
-
+(*Function gcd yields the Greatest Common Divisor*)
 goalw thy [is_gcd_def] "is_gcd (gcd(m,n)) m n";
 by (asm_simp_tac (!simpset addsimps [gcd_greatest, gcd_divides_both]) 1);
 qed "is_gcd";
 
-(* GCD is unique *)
-
+(*uniqueness of GCDs*)
 goalw thy [is_gcd_def] "is_gcd m a b & is_gcd n a b --> m=n";
 by (blast_tac (!claset addIs [dvd_anti_sym]) 1);
 qed "is_gcd_unique";
 
+(*Davenport, page 27*)
+goal thy "k * gcd(m,n) = gcd(k*m, k*n)";
+by (res_inst_tac [("u","m"),("v","n")] gcd_induct 1);
+by (case_tac "k=0" 1);
+by (case_tac "n=0" 2);
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps [mod_less_divisor, zero_less_eq,
+				      mod_geq, mod_mult_distrib2])));
+qed "gcd_mult_distrib2";
+
+(*This theorem leads immediately to a proof of the uniqueness of factorization.
+  If p divides a product of primes then it is one of those primes.*)
+goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
+by (Step_tac 1);
+by (subgoal_tac "m = gcd(m*p, m*n)" 1);
+be ssubst 1;
+br gcd_greatest 1;
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym])));
+(*Now deduce  gcd(p,n)=1  to finish the proof*)
+by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1);
+by (fast_tac (!claset addSss (!simpset)) 1);
+qed "prime_dvd_mult";