# HG changeset patch
# User nipkow
# Date 978701290 -3600
# Node ID 260fa2c67e3e9a60c3e013abf580fb3ccd542449
# Parent  ea48dd8b0232fe377ff1aee2dfeb4fe5dbd746ee
Changed priority of dvd from 70 to 50 as befits a relation.

diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/Algebra/abstract/Factor.ML
--- a/src/HOL/Algebra/abstract/Factor.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/Algebra/abstract/Factor.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -5,7 +5,7 @@
 *)
 
 goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
-\  [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b";
+\  [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
 by (ftac factorial_prime 1);
 by (rewrite_goals_tac [irred_def, prime_def]);
 by (Blast_tac 1);
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/Algebra/abstract/Ideal.ML
--- a/src/HOL/Algebra/abstract/Ideal.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ideal.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -151,12 +151,12 @@
   simpset() addsimps [pideal_structure]));
 qed "subideal_imp_dvd";
 
-Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = b dvd a";
+Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)";
 by (rtac iffI 1);
 by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
 qed "subideal_is_dvd";
 
-Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ (a dvd b)";
+Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b";
 by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
 by (etac conjE 1);
 by (dres_inst_tac [("c", "a")] subsetD 1);
@@ -164,13 +164,13 @@
   simpset()));
 qed "psubideal_not_dvd";
 
-Goal "[| b dvd a; ~ (a dvd b) |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
+Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
 by (rtac psubsetI 1);
 by (etac dvd_imp_subideal 1);
 by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); 
 qed "not_dvd_psubideal";
 
-Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ (a dvd b))";
+Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)";
 by (rtac iffI 1);
 by (REPEAT (ares_tac
   [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
@@ -263,7 +263,7 @@
 Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
 \   EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}";
 
-Goal "wf {(a::'a::pid, b). a dvd b & ~ (b dvd a)}";
+Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
 by (simp_tac (simpset()
   addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
   delsimps [psubideal_is_dvd]) 1);
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/Algebra/abstract/Ring.ML
--- a/src/HOL/Algebra/abstract/Ring.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/Algebra/abstract/Ring.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -241,28 +241,28 @@
 qed "unit_power";
 
 Goalw [dvd_def]
-  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd (b + c)";
+  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c";
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "k + ka")] exI 1);
 by (simp_tac (simpset() addsimps [r_distr]) 1);
 qed "dvd_add_right";
 
 Goalw [dvd_def]
-  "!! a::'a::ring. a dvd b ==> a dvd (-b)";
+  "!! a::'a::ring. a dvd b ==> a dvd -b";
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "-k")] exI 1);
 by (simp_tac (simpset() addsimps [r_minus]) 1);
 qed "dvd_uminus_right";
 
 Goalw [dvd_def]
-  "!! a::'a::ring. a dvd b ==> a dvd (c * b)";
+  "!! a::'a::ring. a dvd b ==> a dvd c*b";
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "c * k")] exI 1);
 by (simp_tac (simpset() addsimps m_ac) 1);
 qed "dvd_l_mult_right";
 
 Goalw [dvd_def]
-  "!! a::'a::ring. a dvd b ==> a dvd (b * c)";
+  "!! a::'a::ring. a dvd b ==> a dvd b*c";
 by (Clarify_tac 1);
 by (res_inst_tac [("x", "k * c")] exI 1);
 by (simp_tac (simpset() addsimps m_ac) 1);
@@ -357,7 +357,7 @@
 
 section "Fields";
 
-Goal "!! a::'a::field. a dvd <1> = (a ~= <0>)";
+Goal "!! a::'a::field. (a dvd <1>) = (a ~= <0>)";
 by (blast_tac (claset() addDs [field_ax, unit_imp_nonzero]) 1);
 qed "field_unit";
 
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/Divides.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -540,7 +540,7 @@
 by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
 qed "dvd_diff";
 
-Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd (m::nat)";
+Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
 by (blast_tac (claset() addIs [dvd_add]) 1);
 qed "dvd_diffD";
@@ -557,7 +557,7 @@
 (* k dvd (m*k) *)
 AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
 
-Goal "k dvd (n + k) = k dvd (n::nat)";
+Goal "(k dvd n + k) = (k dvd (n::nat))";
 by (rtac iffI 1);
 by (etac dvd_add 2);
 by (rtac dvd_refl 2);
@@ -568,7 +568,7 @@
 by (rtac dvd_refl 1);
 qed "dvd_reduce";
 
-Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
+Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd m mod n";
 by (Clarify_tac 1);
 by (Full_simp_tac 1);
 by (res_inst_tac 
@@ -579,13 +579,13 @@
 			 add_mult_distrib2]) 1);
 qed "dvd_mod";
 
-Goal "[| (k::nat) dvd (m mod n);  k dvd n |] ==> k dvd m";
-by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
+Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> 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]) 1);
 qed "dvd_mod_imp_dvd";
 
-Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd (m mod n)";
+Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
 by (div_undefined_case_tac "n=0" 1);
 by (Clarify_tac 1);
 by (Full_simp_tac 1);
@@ -598,16 +598,16 @@
 			 add_mult_distrib2]) 1);
 qed "dvd_mod";
 
-Goal "k dvd n ==> (k::nat) dvd (m mod n) = k dvd m";
+Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
 by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
 qed "dvd_mod_iff";
 
-Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
+Goalw [dvd_def]  "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
 by (etac exE 1);
 by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
 qed "dvd_mult_cancel";
 
-Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";
+Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
 by (Clarify_tac 1);
 by (res_inst_tac [("x","k*ka")] exI 1);
 by (asm_simp_tac (simpset() addsimps mult_ac) 1);
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/Divides.thy	Fri Jan 05 14:28:10 2001 +0100
@@ -19,7 +19,7 @@
 consts
   div  :: ['a::div, 'a]  => 'a          (infixl 70)
   mod  :: ['a::div, 'a]  => 'a          (infixl 70)
-  dvd  :: ['a::times, 'a] => bool       (infixl 70) 
+  dvd  :: ['a::times, 'a] => bool       (infixl 50) 
 
 
 (*Remainder and quotient are defined here by algorithms and later proved to
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/NumberTheory/IntPrimes.ML
--- a/src/HOL/NumberTheory/IntPrimes.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/NumberTheory/IntPrimes.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -90,43 +90,43 @@
 by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1);
 qed "zdvd_zdiff";
 
-Goal "[| k dvd (m-n); k dvd n |] ==> k dvd (m::int)";
+Goal "[| k dvd m-n; k dvd n |] ==> k dvd (m::int)";
 by (subgoal_tac "m=n+(m-n)" 1);
 by (etac ssubst 1);
 by (blast_tac (claset() addIs [zdvd_zadd]) 1);
 by (Simp_tac 1);
 qed "zdvd_zdiffD";
 
-Goalw [dvd_def] "k dvd (n::int) ==> k dvd (m*n)";
+Goalw [dvd_def] "k dvd (n::int) ==> k dvd m*n";
 by (blast_tac (claset() addIs [zmult_left_commute]) 1);
 qed "zdvd_zmult";
 
-Goal "k dvd (m::int) ==> k dvd (m*n)";
+Goal "k dvd (m::int) ==> k dvd m*n";
 by (stac zmult_commute 1);
 by (etac zdvd_zmult 1);
 qed "zdvd_zmult2";
 
-(* k dvd (m*k) *)
+(* k dvd m*k *)
 AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2];
 
-Goalw [dvd_def] "(j*k) dvd n ==> j dvd (n::int)";
+Goalw [dvd_def] "j*k dvd n ==> j dvd (n::int)";
 by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
 by (Blast_tac 1);
 qed "zdvd_zmultD2";
 
-Goal "(j*k) dvd n ==> k dvd (n::int)";
+Goal "j*k dvd n ==> k dvd (n::int)";
 by (rtac zdvd_zmultD2 1);
 by (stac zmult_commute 1);
 by (assume_tac 1);
 qed "zdvd_zmultD";
 
-Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> (i*j) dvd (m*n)";
+Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> i*j dvd m*n";
 by (Clarify_tac 1);
 by (res_inst_tac [("x","k*ka")] exI 1);
 by (asm_simp_tac (simpset() addsimps zmult_ac) 1);
 qed "zdvd_zmult_mono";
 
-Goal "k dvd (n + k*m) = k dvd (n::int)";
+Goal "(k dvd n + k*m) = (k dvd (n::int))";
 by (rtac iffI 1);
 by (etac zdvd_zadd 2);
 by (subgoal_tac "n = (n+k*m)-k*m" 1);
@@ -135,12 +135,12 @@
 by (ALLGOALS Simp_tac);
 qed "zdvd_reduce";
 
-Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd (m mod n)";
+Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd m mod n";
 by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1]));
 qed "zdvd_zmod";
 
-Goal "[| k dvd (m mod n);  k dvd n |] ==> k dvd (m::int)";
-by (subgoal_tac "k dvd (n*(m div n) + m mod n)" 1);
+Goal "[| k dvd m mod n;  k dvd n |] ==> k dvd (m::int)";
+by (subgoal_tac "k dvd n*(m div n) + m mod n" 1);
 by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2);
 by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1);
 qed "zdvd_zmod_imp_zdvd";
@@ -334,14 +334,14 @@
 qed "zgcd_zmult_eq_self2";
 Addsimps [zgcd_zmult_eq_self2];
 
-Goal "[| zgcd(n,k)=#1; k dvd (m*n); #0 <= m |] ==> k dvd m";
+Goal "[| zgcd(n,k)=#1; k dvd m*n; #0 <= m |] ==> k dvd m";
 by (subgoal_tac "m = zgcd(m*n, m*k)" 1);
 by (etac ssubst 1 THEN rtac (zgcd_greatest_iff RS iffD2) 1);
 by (ALLGOALS (asm_simp_tac (simpset() 
       addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff])));
 val lemma = result();
 
-Goal "[| zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
+Goal "[| zgcd(n,k)=#1; k dvd m*n |] ==> k dvd m";
 by (case_tac "#0 <= m" 1);
 by (blast_tac (claset() addIs [lemma]) 1); 
 by (subgoal_tac "k dvd -m" 1);
@@ -359,7 +359,7 @@
 by (assume_tac 1);
 qed "zless_zprime_imp_zrelprime";
 
-Goal "[| #0<=(m::int); p:zprime; p dvd (m*n) |] ==> p dvd m | p dvd n";
+Goal "[| #0<=(m::int); p:zprime; p dvd m*n |] ==> p dvd m | p dvd n";
 by Safe_tac;
 by (rtac zrelprime_zdvd_zmult 1);
 by (rtac zprime_imp_zrelprime 1);
@@ -510,7 +510,7 @@
       "[| [a = b] (mod m);  [a = b] (mod n);  zgcd(m,n) = #1 |] \
 \     ==> [a=b](mod m*n)";
 by Auto_tac;
-by (subgoal_tac "m dvd (n*ka)" 1);
+by (subgoal_tac "m dvd n*ka" 1);
 by (subgoal_tac "m dvd ka" 1);
 by (case_tac "#0<=ka" 2);
 by (stac (zdvd_zminus_iff RS sym) 3);
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/NumberTheory/Primes.thy
--- a/src/HOL/NumberTheory/Primes.thy	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/NumberTheory/Primes.thy	Fri Jan 05 14:28:10 2001 +0100
@@ -59,7 +59,7 @@
   done
 
 (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
-lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
+lemma gcd_dvd_both: "gcd(m,n) dvd m & gcd(m,n) dvd n"
   apply (induct_tac m n rule: gcd_induct)
   apply (simp_all add: gcd_non_0)
   apply (blast dest: dvd_mod_imp_dvd)
@@ -71,12 +71,12 @@
 
 (*Maximality: for all m,n,k naturals, 
                 if k divides m and k divides n then k divides gcd(m,n)*)
-lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
+lemma gcd_greatest [rule_format]: "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]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
+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;
 
@@ -142,14 +142,14 @@
   apply (rule gcd_mult [of k 1, simplified])
   done
 
-lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
+lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd m*n |] ==> k dvd m";
   apply (insert gcd_mult_distrib2 [of m k n])
   apply (simp)
   apply (erule_tac t="m" in ssubst);
   apply (simp)
   done
 
-lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> k dvd (m*n) = k dvd m";
+lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> (k dvd m*n) = (k dvd m)";
   apply (blast intro: relprime_dvd_mult dvd_trans)
   done
 
@@ -163,7 +163,7 @@
 
 (*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.*)
-lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
+lemma prime_dvd_mult: "[| p: prime; p dvd m*n |] ==> p dvd m | p dvd n"
   apply (blast intro: relprime_dvd_mult prime_imp_relprime)
   done
 
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/NumberTheory/WilsonBij.ML
--- a/src/HOL/NumberTheory/WilsonBij.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/NumberTheory/WilsonBij.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -56,7 +56,7 @@
 by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
 by (stac zdvd_zminus_iff 1);
 by (stac zdvd_reduce 1);
-by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
+by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1);
 by (stac zdvd_reduce 1);
 by Auto_tac;
 val lemma = result();
diff -r ea48dd8b0232 -r 260fa2c67e3e src/HOL/NumberTheory/WilsonRuss.ML
--- a/src/HOL/NumberTheory/WilsonRuss.ML	Fri Jan 05 13:10:37 2001 +0100
+++ b/src/HOL/NumberTheory/WilsonRuss.ML	Fri Jan 05 14:28:10 2001 +0100
@@ -65,7 +65,7 @@
 by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
 by (stac zdvd_zminus_iff 1);
 by (stac zdvd_reduce 1);
-by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
+by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1);
 by (stac zdvd_reduce 1);
 by Auto_tac;
 val lemma = result();