--- 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";