# HG changeset patch
# User paulson
# Date 968670191 -7200
# Node ID 4b02467a441257af3d20b209b73513baf6aa570b
# Parent  864c8faf3d9a5b624d53658cd76fabdddf3053b9
tidied

diff -r 864c8faf3d9a -r 4b02467a4412 src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Sep 08 12:13:21 2000 +0200
+++ b/src/HOL/Divides.ML	Mon Sep 11 13:03:11 2000 +0200
@@ -168,8 +168,8 @@
 (* a simple rearrangement of mod_div_equality: *)
 Goal "(n::nat) * (m div n) = m - (m mod n)";
 by (cut_inst_tac [("m","m"),("n","n")] mod_div_equality 1);
-by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
-           K(IF_UNSOLVED no_tac)]);
+by (full_simp_tac (simpset() addsimps mult_ac) 1);
+by (arith_tac 1);
 qed "mult_div_cancel";
 
 Goal "m div 1 = m";
@@ -310,7 +310,7 @@
 
 Goal "0<n ==> (m*n) div n = (m::nat)";
 by (cut_inst_tac [("m", "m*n"),("n","n")] mod_div_equality 1);
-by (asm_full_simp_tac (simpset() addsimps [mod_mult_self_is_0]) 1);
+by Auto_tac;
 qed "div_mult_self_is_m";
 
 Goal "0<n ==> (n*m) div n = (m::nat)";
diff -r 864c8faf3d9a -r 4b02467a4412 src/HOL/ex/Primes.thy
--- a/src/HOL/ex/Primes.thy	Fri Sep 08 12:13:21 2000 +0200
+++ b/src/HOL/ex/Primes.thy	Mon Sep 11 13:03:11 2000 +0200
@@ -65,24 +65,24 @@
   apply (blast dest: dvd_mod_imp_dvd)
   done
 
-lemmas gcd_dvd1 = gcd_dvd_both [THEN conjunct1];
-lemmas gcd_dvd2 = gcd_dvd_both [THEN conjunct2];
+lemmas gcd_dvd1 [iff] = gcd_dvd_both [THEN conjunct1]
+lemmas gcd_dvd2 [iff] = gcd_dvd_both [THEN conjunct2];
 
 
-(*Maximality: for all m,n,f naturals, 
-                if f divides m and f divides n then f divides gcd(m,n)*)
-lemma gcd_greatest [rulified]: "(f dvd m) --> (f dvd n) --> f dvd gcd(m,n)"
+(*Maximality: for all m,n,k naturals, 
+                if k divides m and k divides n then k divides gcd(m,n)*)
+lemma gcd_greatest [rulified]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
   apply (induct_tac m n rule: gcd_induct)
   apply (simp_all add: gcd_non_0 dvd_mod);
   done;
 
-lemma gcd_greatest_iff [iff]: "f dvd gcd(m,n) = (f dvd m & f dvd n)"
-  apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans gcd_greatest);
+lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
+  apply (blast intro!: gcd_greatest intro: dvd_trans);
   done;
 
 (*Function gcd yields the Greatest Common Divisor*)
 lemma is_gcd: "is_gcd (gcd(m,n)) m n"
-  apply (simp add: is_gcd_def gcd_greatest gcd_dvd_both);
+  apply (simp add: is_gcd_def gcd_greatest)
   done
 
 (*uniqueness of GCDs*)
@@ -112,7 +112,7 @@
   apply (rule is_gcd_unique)
   apply (rule is_gcd)
   apply (simp add: is_gcd_def);
-  apply (blast intro!: gcd_dvd1 gcd_dvd2 intro: dvd_trans);
+  apply (blast intro: dvd_trans);
   done 
 
 lemma gcd_0_left [simp]: "gcd(0,m) = m"
@@ -135,22 +135,12 @@
   done
 
 lemma gcd_self [simp]: "gcd(m,m) = m"
-  apply (cut_tac k="m" and m="1" and n="1" in gcd_mult_distrib2)
-  apply (simp)
-(*alternative:
-proof -;
-  note gcd_mult_distrib2 [of m 1 1, simplify, THEN sym];
-      thus ?thesis; by assumption; qed; *)
-done
+  apply (rule gcd_mult_distrib2 [of m 1 1, simplified, THEN sym])
+  done
 
 lemma gcd_mult [simp]: "gcd(k, k*n) = k"
-  apply (cut_tac k="k" and m="1" and n="n" in gcd_mult_distrib2)
-  apply (simp)
-(*alternative:
-proof -;
-  note gcd_mult_distrib2 [of k 1 n, simplify, THEN sym];
-      thus ?thesis; by assumption; qed; *)
-done
+  apply (rule gcd_mult_distrib2 [of k 1 n, simplified, THEN sym])
+  done
 
 lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
    apply (subgoal_tac "gcd(m*k, m*n) = m")
@@ -164,9 +154,11 @@
   done
 
 lemma prime_imp_relprime: "[| p: prime;  ~ p dvd n |] ==> gcd (p, n) = 1"
-  apply (simp add: prime_def);
-  apply (cut_tac m="p" and n="n" in gcd_dvd_both)
+  apply (auto simp add: prime_def)
+  apply (drule_tac x="gcd(p,n)" in spec)
   apply auto
+  apply (insert gcd_dvd2 [of p n])
+  apply (simp)
   done
 
 (*This theorem leads immediately to a proof of the uniqueness of factorization.