# HG changeset patch
# User paulson
# Date 993567894 -7200
# Node ID a816fead971a8e5ff03a2f2b12576073191d21e5
# Parent  4ab3b7b0938fe71bfa602adfe5ebd5548549f332
now more like the HOL versions, and with the Square Root example added

diff -r 4ab3b7b0938f -r a816fead971a src/ZF/ex/Primes.ML
--- a/src/ZF/ex/Primes.ML	Tue Jun 26 17:04:09 2001 +0200
+++ b/src/ZF/ex/Primes.ML	Tue Jun 26 17:04:54 2001 +0200
@@ -6,8 +6,6 @@
 The "divides" relation, the greatest common divisor and Euclid's algorithm
 *)
 
-eta_contract:=false;
-
 (************************************************)
 (** Divides Relation                           **)
 (************************************************)
@@ -16,6 +14,11 @@
 by (assume_tac 1);
 qed "dvdD";
 
+Goal "!!P. [|m dvd n;  !!k. [|m \\<in> nat; n \\<in> nat; k \\<in> nat; n = m#*k|] ==> P|] \
+\          ==> P";
+by (blast_tac (claset() addSDs [dvdD]) 1); 
+qed "dvdE";
+
 bind_thm ("dvd_imp_nat1", dvdD RS conjunct1);
 bind_thm ("dvd_imp_nat2", dvdD RS conjunct2 RS conjunct1);
 
@@ -23,6 +26,7 @@
 Goalw [dvd_def] "m \\<in> nat ==> m dvd 0";
 by (fast_tac (claset() addIs [nat_0I, mult_0_right RS sym]) 1);
 qed "dvd_0_right";
+Addsimps [dvd_0_right];
 
 Goalw [dvd_def] "0 dvd m ==> m = 0";
 by (fast_tac (claset() addss (simpset())) 1);
@@ -31,6 +35,7 @@
 Goalw [dvd_def] "m \\<in> nat ==> m dvd m";
 by (fast_tac (claset() addIs [nat_1I, mult_1_right RS sym]) 1);
 qed "dvd_refl";
+Addsimps [dvd_refl];
 
 Goalw [dvd_def] "[| m dvd n; n dvd p |] ==> m dvd p";
 by (fast_tac (claset() addIs [mult_assoc, mult_type] ) 1);
@@ -41,6 +46,18 @@
                     addss (simpset() addsimps [mult_assoc, mult_eq_1_iff])) 1);
 qed "dvd_anti_sym";
 
+Goalw [dvd_def] "[|(i#*j) dvd k; i \\<in> nat|] ==> i dvd k";
+by (full_simp_tac (simpset() addsimps [mult_assoc]) 1);
+by (Blast_tac 1);
+qed "dvd_mult_left";
+
+Goalw [dvd_def] "[|(i#*j) dvd k; j \\<in> nat|] ==> j dvd k";
+by (Clarify_tac 1);
+by (res_inst_tac [("x","i#*k")] bexI 1);
+by (simp_tac (simpset() addsimps mult_ac) 1);
+by (rtac mult_type 1); 
+qed "dvd_mult_right";
+
 
 (************************************************)
 (** Greatest Common Divisor                    **)
@@ -48,125 +65,371 @@
 
 (* GCD by Euclid's Algorithm *)
 
-Goalw [egcd_def] "m \\<in> nat ==> egcd(m,0) = m";
+Goalw [gcd_def] "gcd(m,0) = natify(m)";
 by (stac transrec 1);
 by (Asm_simp_tac 1);
-qed "egcd_0";
+qed "gcd_0";
+Addsimps [gcd_0];
+
+Goal "gcd(natify(m),n) = gcd(m,n)";
+by (simp_tac (simpset() addsimps [gcd_def]) 1); 
+qed "gcd_natify1";
 
-Goalw [egcd_def]
-    "[| 0<n; m \\<in> nat; n \\<in> nat |] ==> egcd(m,n) = egcd(n, m mod n)";
+Goal "gcd(m, natify(n)) = gcd(m,n)";
+by (simp_tac (simpset() addsimps [gcd_def]) 1); 
+qed "gcd_natify2";
+Addsimps [gcd_natify1,gcd_natify2];
+
+Goalw [gcd_def]
+    "[| 0<n;  n \\<in> nat |] ==> gcd(m,n) = gcd(n, m mod n)";
 by (res_inst_tac [("P", "%z. ?left(z) = ?right")] (transrec RS ssubst) 1);
 by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq RS not_sym,
-                                     mod_less_divisor RS ltD]) 1);
-qed "egcd_lt_0";
+                                      mod_less_divisor RS ltD]) 1);
+qed "gcd_non_0_raw";
 
-Goal "m \\<in> nat ==> egcd(m,0) dvd m";
-by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl]) 1);
-qed "egcd_0_dvd_m";
+Goal "0 < natify(n) ==> gcd(m,n) = gcd(n, m mod n)";
+by (cut_inst_tac [("m","m"),("n","natify(n)")] gcd_non_0_raw 1);
+by Auto_tac; 
+qed "gcd_non_0";
 
-Goal "m \\<in> nat ==> egcd(m,0) dvd 0";
-by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_0_right]) 1);
-qed "egcd_0_dvd_0";
+Goal "gcd(m,1) = 1";
+by (asm_simp_tac (simpset() addsimps [gcd_non_0]) 1); 
+qed "gcd_1";
+Addsimps [gcd_1];
 
 Goalw [dvd_def] "[| k dvd a; k dvd b |] ==> k dvd (a #+ b)";
 by (fast_tac (claset() addIs [add_mult_distrib_left RS sym, add_type]) 1);
 qed "dvd_add";
 
-Goalw [dvd_def] "[| k dvd a; q \\<in> nat |] ==> k dvd (q #* a)";
+Goalw [dvd_def] "k dvd n ==> k dvd (m #* n)";
 by (fast_tac (claset() addIs [mult_left_commute, mult_type]) 1);
 qed "dvd_mult";
 
-Goal "[| k dvd b; k dvd (a mod b); 0 < b; a \\<in> nat |] ==> k dvd a";
-by (deepen_tac 
+Goal "k dvd m ==> k dvd (m #* n)";
+by (stac mult_commute 1); 
+by (blast_tac (claset() addIs [dvd_mult]) 1); 
+qed "dvd_mult2";
+
+(* k dvd (m*k) *)
+bind_thm ("dvdI1", dvd_refl RS dvd_mult);
+bind_thm ("dvdI2", dvd_refl RS dvd_mult2);
+Addsimps [dvdI1, dvdI2];
+
+Goal "[| a \\<in> nat; b \\<in> nat; k dvd b; k dvd (a mod b) |] ==> k dvd a";
+by (div_undefined_case_tac "b=0" 1);
+by (blast_tac 
     (claset() addIs [mod_div_equality RS subst]
-           addDs [dvdD]
-           addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 0 1);
-qed "gcd_ind";
-
-
-(* egcd type *)
+              addEs  [dvdE]
+              addSIs [dvd_add, dvd_mult, mult_type,mod_type,div_type]) 1);
+qed "dvd_mod_imp_dvd_raw";
 
-Goal "b \\<in> nat ==> \\<forall>a \\<in> nat. egcd(a,b):nat";
-by (etac complete_induct 1);
-by (rtac ballI 1);
-by (excluded_middle_tac "x=0" 1);
-(* case x = 0 *)
-by (asm_simp_tac (simpset() addsimps [egcd_0]) 2);
-(* case x > 0 *)
-by (asm_simp_tac (simpset() addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt]) 1);
-by (eres_inst_tac [("x","a mod x")] ballE 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [mod_less_divisor RS ltD, 
-                                          nat_into_Ord RS Ord_0_lt]) 1);
-qed "egcd_type";
-
+Goal "[| k dvd (a mod b); k dvd b; a \\<in> nat |] ==> k dvd a";
+by (cut_inst_tac [("b","natify(b)")] dvd_mod_imp_dvd_raw 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [dvd_def]) 1);  
+qed "dvd_mod_imp_dvd";
 
-(* Property 1: egcd(a,b) divides a and b *)
+(*Imitating TFL*)
+Goal "[| n \\<in> nat; \
+\        \\<forall>m \\<in> nat. P(m,0); \
+\        \\<forall>m \\<in> nat. \\<forall>n \\<in> nat. 0<n --> P(n, m mod n) --> P(m,n) |] \
+\     ==> \\<forall>m \\<in> nat. P (m,n)";
+by (eres_inst_tac [("i","n")] complete_induct 1);
+by (case_tac "x=0" 1);
+by (Asm_simp_tac 1); 
+by (Clarify_tac 1); 
+by (dres_inst_tac [("x1","m"),("x","x")] (bspec RS bspec) 1);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [Ord_0_lt_iff])));
+by (blast_tac (claset() addIs [mod_less_divisor RS ltD]) 1); 
+qed_spec_mp "gcd_induct_lemma";
 
-Goal "b \\<in> nat ==> \\<forall>a \\<in> nat. (egcd(a,b) dvd a) & (egcd(a,b) dvd b)";
-by (res_inst_tac [("i","b")] complete_induct 1);
-by (assume_tac 1);
-by (rtac ballI 1);
-by (excluded_middle_tac "x=0" 1);
-(* case x = 0 *)
-by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right]) 2);
-(* case x > 0 *)
-by (asm_simp_tac (simpset() addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt]) 1);
-by (eres_inst_tac [("x","a mod x")] ballE 1);
-by (Asm_simp_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [mod_less_divisor RS ltD, 
-                                          nat_into_Ord RS Ord_0_lt]) 2);
-by (best_tac (claset() addIs [gcd_ind, nat_into_Ord RS Ord_0_lt]) 1);
-qed "egcd_prop1";
+Goal "!!P. [| m \\<in> nat; n \\<in> nat; \
+\        !!m. m \\<in> nat ==> P(m,0); \
+\        !!m n. [|m \\<in> nat; n \\<in> nat; 0<n; P(n, m mod n)|] ==> P(m,n) |] \
+\     ==> P (m,n)";
+by (blast_tac (claset() addIs [gcd_induct_lemma]) 1); 
+qed "gcd_induct"; 
 
 
-(* if f divides a and b then f divides egcd(a,b) *)
+(* gcd type *)
+
+Goal "gcd(m, n) \\<in> nat";
+by (subgoal_tac "gcd(natify(m), natify(n)) \\<in> nat" 1);
+by (Asm_full_simp_tac 1); 
+by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_induct 1); 
+by Auto_tac; 
+by (asm_full_simp_tac (simpset() addsimps [gcd_non_0]) 1); 
+qed "gcd_type";
+Addsimps [gcd_type];
+
+(* Property 1: gcd(a,b) divides a and b *)
+
+Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd (m, n) dvd m & gcd (m, n) dvd n";
+by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1); 
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [gcd_non_0])));
+by (blast_tac
+    (claset() addIs [dvd_mod_imp_dvd_raw, nat_into_Ord RS Ord_0_lt]) 1);
+qed "gcd_dvd_both";
 
-Goalw [dvd_def] "[| f dvd a; f dvd b; 0<b |] ==> f dvd (a mod b)";
-by (safe_tac (claset() addSIs [mod_type]));
-ren "m n" 1;
-by (Asm_full_simp_tac 1);
-by (res_inst_tac 
-    [("x", "(((m div n)#*n #+ m mod n) #- ((f#*m) div (f#*n)) #* n)")] 
-    bexI 1);
-by (asm_simp_tac (simpset() addsimps [diff_mult_distrib2, div_cancel,
-                                     mult_mod_distrib, add_mult_distrib_left,
-                                     diff_add_inverse]) 1);
-by (Asm_simp_tac 1);
+Goal "m \\<in> nat ==> gcd(m,n) dvd m";
+by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1); 
+by Auto_tac; 
+qed "gcd_dvd1";
+Addsimps [gcd_dvd1];
+
+Goal "n \\<in> nat ==> gcd(m,n) dvd n";
+by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_dvd_both 1); 
+by Auto_tac; 
+qed "gcd_dvd2";
+Addsimps [gcd_dvd2];
+
+(* if f divides a and b then f divides gcd(a,b) *)
+
+Goalw [dvd_def] "[| f dvd a; f dvd b |] ==> f dvd (a mod b)";
+by (div_undefined_case_tac "b=0" 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [mod_mult_distrib2 RS sym]) 1);  
 qed "dvd_mod";
 
-
 (* Property 2: for all a,b,f naturals, 
-               if f divides a and f divides b then f divides egcd(a,b)*)
-Goal "[| b \\<in> nat; f \\<in> nat |] ==>    \
-\              \\<forall>a. (f dvd a) & (f dvd b) --> f dvd egcd(a,b)";
-by (etac complete_induct 1);
-by (rtac allI 1);
-by (excluded_middle_tac "x=0" 1);
-(* case x = 0 *)
-by (asm_simp_tac (simpset() addsimps [egcd_0,dvd_refl,dvd_0_right,
-                                     dvd_imp_nat2]) 2);
-(* case x > 0 *)
-by Safe_tac;
-by (asm_simp_tac (simpset() addsimps [egcd_lt_0, nat_into_Ord RS Ord_0_lt,
-                                     dvd_imp_nat2]) 1);
-by (eres_inst_tac [("x","a mod x")] ballE 1);
-by (asm_full_simp_tac 
-    (simpset() addsimps [mod_less_divisor RS ltD, dvd_imp_nat2, 
-                        nat_into_Ord RS Ord_0_lt, egcd_lt_0]) 2);
-by (fast_tac (claset() addSIs [dvd_mod, nat_into_Ord RS Ord_0_lt]) 1);
-qed "egcd_prop2";
+               if f divides a and f divides b then f divides gcd(a,b)*)
+
+Goal "[| m \\<in> nat; n \\<in> nat; f \\<in> nat |]   \
+\     ==> (f dvd m) --> (f dvd n) --> f dvd gcd(m,n)";
+by (res_inst_tac [("m","m"),("n","n")] gcd_induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [gcd_non_0, dvd_mod])));
+qed_spec_mp "gcd_greatest_raw";
+
+Goal "[| f dvd m;  f dvd n;  f \\<in> nat |] ==> f dvd gcd(m,n)";
+by (rtac gcd_greatest_raw 1); 
+by (auto_tac (claset(), simpset() addsimps [dvd_def])); 
+qed "gcd_greatest";
 
-(* GCD PROOF \\<in> GCD exists and egcd fits the definition *)
+Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
+\     ==> (k dvd gcd (m, n)) <-> (k dvd m & k dvd n)";
+by (blast_tac (claset() addSIs [gcd_greatest, gcd_dvd1, gcd_dvd2] 
+                        addIs [dvd_trans]) 1); 
+qed "gcd_greatest_iff";
+Addsimps [gcd_greatest_iff];
 
-Goalw [gcd_def] "[| a \\<in> nat; b \\<in> nat |] ==> gcd(egcd(a,b), a, b)";
-by (asm_simp_tac (simpset() addsimps [egcd_prop1]) 1);
-by (fast_tac (claset() addIs [egcd_prop2 RS spec RS mp, dvd_imp_nat1]) 1);
-qed "gcd";
+(* GCD PROOF: GCD exists and gcd fits the definition *)
+
+Goalw [is_gcd_def] "[| m \\<in> nat; n \\<in> nat |] ==> is_gcd(gcd(m,n), m, n)";
+by (Asm_simp_tac 1);
+qed "is_gcd";
 
 (* GCD is unique *)
 
-Goalw [gcd_def] "gcd(m,a,b) & gcd(n,a,b) --> m=n";
-by (fast_tac (claset() addIs [dvd_anti_sym]) 1);
-qed "gcd_unique";
+Goalw [is_gcd_def] "[|is_gcd(m,a,b); is_gcd(n,a,b); m\\<in>nat; n\\<in>nat|] ==> m=n";
+by (blast_tac (claset() addIs [dvd_anti_sym]) 1);
+qed "is_gcd_unique";
+
+Goalw [is_gcd_def] "is_gcd(k,m,n) <-> is_gcd(k,n,m)";
+by (Blast_tac 1); 
+qed "is_gcd_commute";
+
+Goal "[| m \\<in> nat; n \\<in> nat |] ==> gcd(m,n) = gcd(n,m)";
+by (rtac is_gcd_unique 1); 
+by (rtac is_gcd 1); 
+by (rtac (is_gcd_commute RS iffD1) 3); 
+by (rtac is_gcd 3); 
+by Auto_tac; 
+qed "gcd_commute_raw";
+
+Goal "gcd(m,n) = gcd(n,m)";
+by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_commute_raw 1); 
+by Auto_tac; 
+qed "gcd_commute";
+
+Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
+\     ==> gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
+by (rtac is_gcd_unique 1); 
+by (rtac is_gcd 1); 
+by (asm_full_simp_tac (simpset() addsimps [is_gcd_def]) 3);
+by (blast_tac (claset() addIs [gcd_dvd1, gcd_dvd2, gcd_type] 
+                        addIs [dvd_trans]) 3); 
+by Auto_tac; 
+qed "gcd_assoc_raw";
+
+Goal "gcd (gcd (k, m), n) = gcd (k, gcd (m, n))";
+by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] 
+    gcd_assoc_raw 1); 
+by Auto_tac; 
+qed "gcd_assoc";
+
+Goal "gcd (0, m) = natify(m)";
+by (asm_simp_tac (simpset() addsimps [inst "m" "0" gcd_commute]) 1); 
+qed "gcd_0_left"; 
+Addsimps [gcd_0_left];
+
+Goal "gcd (1, m) = 1";
+by (asm_simp_tac (simpset() addsimps [inst "m" "1" gcd_commute]) 1); 
+qed "gcd_1_left"; 
+Addsimps [gcd_1_left];
+
+
+(* Multiplication laws *)
+
+Goal "[| k \\<in> nat; m \\<in> nat; n \\<in> nat |] \
+\     ==> k #* gcd (m, n) = gcd (k #* m, k #* n)";
+by (eres_inst_tac [("m","m"),("n","n")] gcd_induct 1); 
+by (assume_tac 1); 
+by (Asm_simp_tac 1); 
+by (case_tac "k = 0" 1);
+by (Asm_full_simp_tac 1); 
+by (asm_full_simp_tac (simpset() addsimps [mod_geq, gcd_non_0, 
+                                    mod_mult_distrib2, Ord_0_lt_iff]) 1); 
+qed "gcd_mult_distrib2_raw";
+
+Goal "k #* gcd (m, n) = gcd (k #* m, k #* n)";
+by (cut_inst_tac [("k","natify(k)"),("m","natify(m)"),("n","natify(n)")] 
+    gcd_mult_distrib2_raw 1); 
+by Auto_tac; 
+qed "gcd_mult_distrib2";
+
+Goal "gcd (k, k #* n) = natify(k)";
+by (cut_inst_tac [("k","k"),("m","1"),("n","n")] gcd_mult_distrib2 1);
+by Auto_tac; 
+qed "gcd_mult";
+Addsimps [gcd_mult];
+
+Goal "gcd (k, k) = natify(k)";
+by (cut_inst_tac [("k","k"),("n","1")] gcd_mult 1);
+by Auto_tac; 
+qed "gcd_self";
+Addsimps [gcd_self];
+
+Goal "[| gcd (k,n) = 1;  k dvd (m #* n);  m \\<in> nat |] \
+\     ==> k dvd m";
+by (cut_inst_tac [("k","m"),("m","k"),("n","n")] gcd_mult_distrib2 1);
+by Auto_tac; 
+by (eres_inst_tac [("b","m")] ssubst 1);
+by (asm_full_simp_tac (simpset() addsimps [dvd_imp_nat1]) 1);  
+qed "relprime_dvd_mult";
+
+Goal "[| gcd (k,n) = 1;  m \\<in> nat |] \
+\     ==> k dvd (m #* n) <-> k dvd m";
+by (blast_tac (claset() addIs [dvdI2, relprime_dvd_mult, dvd_trans]) 1); 
+qed "relprime_dvd_mult_iff";
+
+Goalw [prime_def]
+     "[| p \\<in> prime;  ~ (p dvd n);  n \\<in> nat |] ==> gcd (p, n) = 1";
+by (Clarify_tac 1); 
+by (dres_inst_tac [("x","gcd(p,n)")] bspec 1);
+by Auto_tac;  
+by (cut_inst_tac [("m","p"),("n","n")] gcd_dvd2 1);
+by Auto_tac;
+qed "prime_imp_relprime";
+
+Goalw [prime_def] "p \\<in> prime ==> p \\<in> nat";
+by Auto_tac; 
+qed "prime_into_nat";
 
+Goalw [prime_def] "p \\<in> prime \\<Longrightarrow> p\\<noteq>0";
+by Auto_tac; 
+qed "prime_nonzero";
+
+
+(*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.*)
+
+Goal "[|p dvd m #* n; p \\<in> prime; m \\<in> nat; n \\<in> nat |] ==> p dvd m \\<or> p dvd n";
+by (blast_tac (claset() addIs [relprime_dvd_mult, prime_imp_relprime, 
+                               prime_into_nat]) 1); 
+qed "prime_dvd_mult";
+
+
+(** Addition laws **)
+
+Goal "gcd (m #+ n, n) = gcd (m, n)";
+by (subgoal_tac "gcd (m #+ natify(n), natify(n)) = gcd (m, natify(n))" 1);
+by (Asm_full_simp_tac 1); 
+by (case_tac "natify(n) = 0" 1);
+by (auto_tac (claset(), simpset() addsimps [Ord_0_lt_iff, gcd_non_0])); 
+qed "gcd_add1"; 
+Addsimps [gcd_add1];
+
+Goal "gcd (m, m #+ n) = gcd (m, n)";
+by (rtac (gcd_commute RS trans) 1); 
+by (stac add_commute 1); 
+by (Simp_tac 1);
+by (rtac gcd_commute 1); 
+qed "gcd_add2"; 
+Addsimps [gcd_add2];
+
+Goal "gcd (m, n #+ m) = gcd (m, n)";
+by (stac add_commute 1); 
+by (rtac gcd_add2 1); 
+qed "gcd_add2'"; 
+Addsimps [gcd_add2'];
+
+Goal "k \\<in> nat ==> gcd (m, k #* m #+ n) = gcd (m, n)";
+by (etac nat_induct 1); 
+by (auto_tac (claset(), simpset() addsimps [gcd_add2, add_assoc])); 
+qed "gcd_add_mult_raw";
+
+Goal "gcd (m, k #* m #+ n) = gcd (m, n)";
+by (cut_inst_tac [("k","natify(k)")] gcd_add_mult_raw 1);
+by Auto_tac; 
+qed "gcd_add_mult";
+
+
+(* More multiplication laws *)
+
+Goal "[|gcd (k,n) = 1; m \\<in> nat; n \\<in> nat|] ==> gcd (k #* m, n) = gcd (m, n)";
+by (rtac dvd_anti_sym 1);
+ by (rtac gcd_greatest 1);
+  by (rtac (inst "n" "k" relprime_dvd_mult) 1);
+by (asm_full_simp_tac (simpset() addsimps [gcd_assoc]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [gcd_commute]) 1); 
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_commute])));
+by (blast_tac (claset() addIs [dvdI1, gcd_dvd1, dvd_trans]) 1); 
+qed "gcd_mult_cancel_raw";
+
+
+Goal "gcd (k,n) = 1 ==> gcd (k #* m, n) = gcd (m, n)";
+by (cut_inst_tac [("m","natify(m)"),("n","natify(n)")] gcd_mult_cancel_raw 1); 
+by Auto_tac; 
+qed "gcd_mult_cancel";
+
+
+(*** The square root of a prime is irrational: key lemma ***)
+
+Goal "\\<lbrakk>n#*n = p#*(k#*k); p \\<in> prime; n \\<in> nat\\<rbrakk> \\<Longrightarrow> p dvd n";
+by (subgoal_tac "p dvd n#*n" 1); 
+ by (blast_tac (claset() addDs [prime_dvd_mult]) 1);
+by (res_inst_tac [("j","k#*k")] dvd_mult_left 1);
+ by (auto_tac (claset(), simpset() addsimps [prime_def])); 
+qed "prime_dvd_other_side";
+
+Goal "\\<lbrakk>k#*k = p#*(j#*j); p \\<in> prime; 0 < k; j \\<in> nat; k \\<in> nat\\<rbrakk> \
+\     \\<Longrightarrow> k < p#*j & 0 < j";
+by (rtac ccontr 1);
+by (asm_full_simp_tac (simpset() addsimps [not_lt_iff_le, prime_into_nat]) 1); 
+by (etac disjE 1);
+ by (ftac mult_le_mono 1 THEN REPEAT (assume_tac 1));
+by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
+by (auto_tac (claset() addSDs [natify_eqE], 
+              simpset() addsimps [not_lt_iff_le, prime_into_nat, 
+                                  mult_le_cancel_le1])); 
+by (asm_full_simp_tac (simpset() addsimps [prime_def]) 1); 
+by (blast_tac (claset() addDs [lt_trans1]) 1); 
+qed "reduction";
+
+
+Goal "j #* (p#*j) = k#*k \\<Longrightarrow> k#*k = p#*(j#*j)";
+by (asm_full_simp_tac (simpset() addsimps mult_ac) 1); 
+qed "rearrange";
+
+Goal "\\<lbrakk>m \\<in> nat; p \\<in> prime\\<rbrakk> \\<Longrightarrow> \\<forall>k \\<in> nat. 0<k \\<longrightarrow> m#*m \\<noteq> p#*(k#*k)";
+by (etac complete_induct 1); 
+by (Clarify_tac 1); 
+by (ftac prime_dvd_other_side 1);
+by (assume_tac 1); 
+by (assume_tac 1); 
+by (etac dvdE 1);
+by (asm_full_simp_tac (simpset() addsimps [mult_assoc, mult_cancel1, 
+                                           prime_nonzero, prime_into_nat]) 1); 
+by (blast_tac (claset() addDs [rearrange, reduction, ltD]) 1); 
+qed "prime_not_square";
diff -r 4ab3b7b0938f -r a816fead971a src/ZF/ex/Primes.thy
--- a/src/ZF/ex/Primes.thy	Tue Jun 26 17:04:09 2001 +0200
+++ b/src/ZF/ex/Primes.thy	Tue Jun 26 17:04:54 2001 +0200
@@ -8,23 +8,26 @@
 
 Primes = Main +
 consts
-  dvd     :: [i,i]=>o              (infixl 70) 
-  gcd     :: [i,i,i]=>o            (* great common divisor *)
-  egcd    :: [i,i]=>i              (* gcd by Euclid's algorithm *)
-  coprime :: [i,i]=>o              (* coprime definition *)
-  prime   :: i=>o                  (* prime definition *)
+  dvd     :: [i,i]=>o              (infixl 50) 
+  is_gcd  :: [i,i,i]=>o            (* great common divisor *)
+  gcd     :: [i,i]=>i              (* gcd by Euclid's algorithm *)
   
 defs
   dvd_def     "m dvd n == m \\<in> nat & n \\<in> nat & (\\<exists>k \\<in> nat. n = m#*k)"
 
-  gcd_def     "gcd(p,m,n) == ((p dvd m) & (p dvd n))   &
-               (\\<forall>d. (d dvd m) & (d dvd n) --> d dvd p)"
+  is_gcd_def  "is_gcd(p,m,n) == ((p dvd m) & (p dvd n))   &
+               (\\<forall>d\\<in>nat. (d dvd m) & (d dvd n) --> d dvd p)"
 
-  egcd_def    "egcd(m,n) ==   
-               transrec(n, %n f. \\<lambda>m \\<in> nat. if(n=0, m, f`(m mod n)`n)) ` m"
+  gcd_def     "gcd(m,n) ==   
+               transrec(natify(n),
+			%n f. \\<lambda>m \\<in> nat.
+			        if n=0 then m else f`(m mod n)`n) ` natify(m)"
 
-  coprime_def "coprime(m,n) == egcd(m,n) = 1"
-
-  prime_def   "prime(n) == (1<n) & (\\<forall>m \\<in> nat. 1<m & m<n --> ~(m dvd n))"
+constdefs
+  coprime :: [i,i]=>o              (* coprime relation *)
+    "coprime(m,n) == gcd(m,n) = 1"
+  
+  prime   :: i                     (* set of prime numbers *)
+   "prime == {p \\<in> nat. 1<p & (\\<forall>m \\<in> nat. m dvd p --> m=1 | m=p)}"
 
 end