Changed priority of dvd from 70 to 50 as befits a relation.
authornipkow
Fri Jan 05 14:28:10 2001 +0100 (2001-01-05)
changeset 10789260fa2c67e3e
parent 10788 ea48dd8b0232
child 10790 520dd8696927
Changed priority of dvd from 70 to 50 as befits a relation.
src/HOL/Algebra/abstract/Factor.ML
src/HOL/Algebra/abstract/Ideal.ML
src/HOL/Algebra/abstract/Ring.ML
src/HOL/Divides.ML
src/HOL/Divides.thy
src/HOL/NumberTheory/IntPrimes.ML
src/HOL/NumberTheory/Primes.thy
src/HOL/NumberTheory/WilsonBij.ML
src/HOL/NumberTheory/WilsonRuss.ML
     1.1 --- a/src/HOL/Algebra/abstract/Factor.ML	Fri Jan 05 13:10:37 2001 +0100
     1.2 +++ b/src/HOL/Algebra/abstract/Factor.ML	Fri Jan 05 14:28:10 2001 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  *)
     1.5  
     1.6  goalw Ring.thy [assoc_def] "!! c::'a::factorial. \
     1.7 -\  [| irred c; irred a; irred b; c dvd (a*b) |] ==> c assoc a | c assoc b";
     1.8 +\  [| irred c; irred a; irred b; c dvd a*b |] ==> c assoc a | c assoc b";
     1.9  by (ftac factorial_prime 1);
    1.10  by (rewrite_goals_tac [irred_def, prime_def]);
    1.11  by (Blast_tac 1);
     2.1 --- a/src/HOL/Algebra/abstract/Ideal.ML	Fri Jan 05 13:10:37 2001 +0100
     2.2 +++ b/src/HOL/Algebra/abstract/Ideal.ML	Fri Jan 05 14:28:10 2001 +0100
     2.3 @@ -151,12 +151,12 @@
     2.4    simpset() addsimps [pideal_structure]));
     2.5  qed "subideal_imp_dvd";
     2.6  
     2.7 -Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = b dvd a";
     2.8 +Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)";
     2.9  by (rtac iffI 1);
    2.10  by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1));
    2.11  qed "subideal_is_dvd";
    2.12  
    2.13 -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ (a dvd b)";
    2.14 +Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b";
    2.15  by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1);
    2.16  by (etac conjE 1);
    2.17  by (dres_inst_tac [("c", "a")] subsetD 1);
    2.18 @@ -164,13 +164,13 @@
    2.19    simpset()));
    2.20  qed "psubideal_not_dvd";
    2.21  
    2.22 -Goal "[| b dvd a; ~ (a dvd b) |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
    2.23 +Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}";
    2.24  by (rtac psubsetI 1);
    2.25  by (etac dvd_imp_subideal 1);
    2.26  by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); 
    2.27  qed "not_dvd_psubideal";
    2.28  
    2.29 -Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ (a dvd b))";
    2.30 +Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)";
    2.31  by (rtac iffI 1);
    2.32  by (REPEAT (ares_tac
    2.33    [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1));
    2.34 @@ -263,7 +263,7 @@
    2.35  Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \
    2.36  \   EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}";
    2.37  
    2.38 -Goal "wf {(a::'a::pid, b). a dvd b & ~ (b dvd a)}";
    2.39 +Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}";
    2.40  by (simp_tac (simpset()
    2.41    addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain]
    2.42    delsimps [psubideal_is_dvd]) 1);
     3.1 --- a/src/HOL/Algebra/abstract/Ring.ML	Fri Jan 05 13:10:37 2001 +0100
     3.2 +++ b/src/HOL/Algebra/abstract/Ring.ML	Fri Jan 05 14:28:10 2001 +0100
     3.3 @@ -241,28 +241,28 @@
     3.4  qed "unit_power";
     3.5  
     3.6  Goalw [dvd_def]
     3.7 -  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd (b + c)";
     3.8 +  "!! a::'a::ring. [| a dvd b; a dvd c |] ==> a dvd b + c";
     3.9  by (Clarify_tac 1);
    3.10  by (res_inst_tac [("x", "k + ka")] exI 1);
    3.11  by (simp_tac (simpset() addsimps [r_distr]) 1);
    3.12  qed "dvd_add_right";
    3.13  
    3.14  Goalw [dvd_def]
    3.15 -  "!! a::'a::ring. a dvd b ==> a dvd (-b)";
    3.16 +  "!! a::'a::ring. a dvd b ==> a dvd -b";
    3.17  by (Clarify_tac 1);
    3.18  by (res_inst_tac [("x", "-k")] exI 1);
    3.19  by (simp_tac (simpset() addsimps [r_minus]) 1);
    3.20  qed "dvd_uminus_right";
    3.21  
    3.22  Goalw [dvd_def]
    3.23 -  "!! a::'a::ring. a dvd b ==> a dvd (c * b)";
    3.24 +  "!! a::'a::ring. a dvd b ==> a dvd c*b";
    3.25  by (Clarify_tac 1);
    3.26  by (res_inst_tac [("x", "c * k")] exI 1);
    3.27  by (simp_tac (simpset() addsimps m_ac) 1);
    3.28  qed "dvd_l_mult_right";
    3.29  
    3.30  Goalw [dvd_def]
    3.31 -  "!! a::'a::ring. a dvd b ==> a dvd (b * c)";
    3.32 +  "!! a::'a::ring. a dvd b ==> a dvd b*c";
    3.33  by (Clarify_tac 1);
    3.34  by (res_inst_tac [("x", "k * c")] exI 1);
    3.35  by (simp_tac (simpset() addsimps m_ac) 1);
    3.36 @@ -357,7 +357,7 @@
    3.37  
    3.38  section "Fields";
    3.39  
    3.40 -Goal "!! a::'a::field. a dvd <1> = (a ~= <0>)";
    3.41 +Goal "!! a::'a::field. (a dvd <1>) = (a ~= <0>)";
    3.42  by (blast_tac (claset() addDs [field_ax, unit_imp_nonzero]) 1);
    3.43  qed "field_unit";
    3.44  
     4.1 --- a/src/HOL/Divides.ML	Fri Jan 05 13:10:37 2001 +0100
     4.2 +++ b/src/HOL/Divides.ML	Fri Jan 05 14:28:10 2001 +0100
     4.3 @@ -540,7 +540,7 @@
     4.4  by (blast_tac (claset() addIs [diff_mult_distrib2 RS sym]) 1);
     4.5  qed "dvd_diff";
     4.6  
     4.7 -Goal "[| k dvd (m-n); k dvd n; n<=m |] ==> k dvd (m::nat)";
     4.8 +Goal "[| k dvd m-n; k dvd n; n<=m |] ==> k dvd (m::nat)";
     4.9  by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    4.10  by (blast_tac (claset() addIs [dvd_add]) 1);
    4.11  qed "dvd_diffD";
    4.12 @@ -557,7 +557,7 @@
    4.13  (* k dvd (m*k) *)
    4.14  AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
    4.15  
    4.16 -Goal "k dvd (n + k) = k dvd (n::nat)";
    4.17 +Goal "(k dvd n + k) = (k dvd (n::nat))";
    4.18  by (rtac iffI 1);
    4.19  by (etac dvd_add 2);
    4.20  by (rtac dvd_refl 2);
    4.21 @@ -568,7 +568,7 @@
    4.22  by (rtac dvd_refl 1);
    4.23  qed "dvd_reduce";
    4.24  
    4.25 -Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
    4.26 +Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n; 0<n |] ==> f dvd m mod n";
    4.27  by (Clarify_tac 1);
    4.28  by (Full_simp_tac 1);
    4.29  by (res_inst_tac 
    4.30 @@ -579,13 +579,13 @@
    4.31  			 add_mult_distrib2]) 1);
    4.32  qed "dvd_mod";
    4.33  
    4.34 -Goal "[| (k::nat) dvd (m mod n);  k dvd n |] ==> k dvd m";
    4.35 -by (subgoal_tac "k dvd ((m div n)*n + m mod n)" 1);
    4.36 +Goal "[| (k::nat) dvd m mod n;  k dvd n |] ==> k dvd m";
    4.37 +by (subgoal_tac "k dvd (m div n)*n + m mod n" 1);
    4.38  by (asm_simp_tac (simpset() addsimps [dvd_add, dvd_mult]) 2);
    4.39  by (asm_full_simp_tac (simpset() addsimps [mod_div_equality]) 1);
    4.40  qed "dvd_mod_imp_dvd";
    4.41  
    4.42 -Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd (m mod n)";
    4.43 +Goalw [dvd_def] "!!n::nat. [| f dvd m; f dvd n |] ==> f dvd m mod n";
    4.44  by (div_undefined_case_tac "n=0" 1);
    4.45  by (Clarify_tac 1);
    4.46  by (Full_simp_tac 1);
    4.47 @@ -598,16 +598,16 @@
    4.48  			 add_mult_distrib2]) 1);
    4.49  qed "dvd_mod";
    4.50  
    4.51 -Goal "k dvd n ==> (k::nat) dvd (m mod n) = k dvd m";
    4.52 +Goal "k dvd n ==> ((k::nat) dvd m mod n) = (k dvd m)";
    4.53  by (blast_tac (claset() addIs [dvd_mod_imp_dvd, dvd_mod]) 1); 
    4.54  qed "dvd_mod_iff";
    4.55  
    4.56 -Goalw [dvd_def]  "!!k::nat. [| (k*m) dvd (k*n); 0<k |] ==> m dvd n";
    4.57 +Goalw [dvd_def]  "!!k::nat. [| k*m dvd k*n; 0<k |] ==> m dvd n";
    4.58  by (etac exE 1);
    4.59  by (asm_full_simp_tac (simpset() addsimps mult_ac) 1);
    4.60  qed "dvd_mult_cancel";
    4.61  
    4.62 -Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> (i*j) dvd (m*n :: nat)";
    4.63 +Goalw [dvd_def] "[| i dvd m; j dvd n|] ==> i*j dvd (m*n :: nat)";
    4.64  by (Clarify_tac 1);
    4.65  by (res_inst_tac [("x","k*ka")] exI 1);
    4.66  by (asm_simp_tac (simpset() addsimps mult_ac) 1);
     5.1 --- a/src/HOL/Divides.thy	Fri Jan 05 13:10:37 2001 +0100
     5.2 +++ b/src/HOL/Divides.thy	Fri Jan 05 14:28:10 2001 +0100
     5.3 @@ -19,7 +19,7 @@
     5.4  consts
     5.5    div  :: ['a::div, 'a]  => 'a          (infixl 70)
     5.6    mod  :: ['a::div, 'a]  => 'a          (infixl 70)
     5.7 -  dvd  :: ['a::times, 'a] => bool       (infixl 70) 
     5.8 +  dvd  :: ['a::times, 'a] => bool       (infixl 50) 
     5.9  
    5.10  
    5.11  (*Remainder and quotient are defined here by algorithms and later proved to
     6.1 --- a/src/HOL/NumberTheory/IntPrimes.ML	Fri Jan 05 13:10:37 2001 +0100
     6.2 +++ b/src/HOL/NumberTheory/IntPrimes.ML	Fri Jan 05 14:28:10 2001 +0100
     6.3 @@ -90,43 +90,43 @@
     6.4  by (blast_tac (claset() addIs [zdiff_zmult_distrib2 RS sym]) 1);
     6.5  qed "zdvd_zdiff";
     6.6  
     6.7 -Goal "[| k dvd (m-n); k dvd n |] ==> k dvd (m::int)";
     6.8 +Goal "[| k dvd m-n; k dvd n |] ==> k dvd (m::int)";
     6.9  by (subgoal_tac "m=n+(m-n)" 1);
    6.10  by (etac ssubst 1);
    6.11  by (blast_tac (claset() addIs [zdvd_zadd]) 1);
    6.12  by (Simp_tac 1);
    6.13  qed "zdvd_zdiffD";
    6.14  
    6.15 -Goalw [dvd_def] "k dvd (n::int) ==> k dvd (m*n)";
    6.16 +Goalw [dvd_def] "k dvd (n::int) ==> k dvd m*n";
    6.17  by (blast_tac (claset() addIs [zmult_left_commute]) 1);
    6.18  qed "zdvd_zmult";
    6.19  
    6.20 -Goal "k dvd (m::int) ==> k dvd (m*n)";
    6.21 +Goal "k dvd (m::int) ==> k dvd m*n";
    6.22  by (stac zmult_commute 1);
    6.23  by (etac zdvd_zmult 1);
    6.24  qed "zdvd_zmult2";
    6.25  
    6.26 -(* k dvd (m*k) *)
    6.27 +(* k dvd m*k *)
    6.28  AddIffs [zdvd_refl RS zdvd_zmult, zdvd_refl RS zdvd_zmult2];
    6.29  
    6.30 -Goalw [dvd_def] "(j*k) dvd n ==> j dvd (n::int)";
    6.31 +Goalw [dvd_def] "j*k dvd n ==> j dvd (n::int)";
    6.32  by (full_simp_tac (simpset() addsimps [zmult_assoc]) 1);
    6.33  by (Blast_tac 1);
    6.34  qed "zdvd_zmultD2";
    6.35  
    6.36 -Goal "(j*k) dvd n ==> k dvd (n::int)";
    6.37 +Goal "j*k dvd n ==> k dvd (n::int)";
    6.38  by (rtac zdvd_zmultD2 1);
    6.39  by (stac zmult_commute 1);
    6.40  by (assume_tac 1);
    6.41  qed "zdvd_zmultD";
    6.42  
    6.43 -Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> (i*j) dvd (m*n)";
    6.44 +Goalw [dvd_def] "[| i dvd m; j dvd (n::int) |] ==> i*j dvd m*n";
    6.45  by (Clarify_tac 1);
    6.46  by (res_inst_tac [("x","k*ka")] exI 1);
    6.47  by (asm_simp_tac (simpset() addsimps zmult_ac) 1);
    6.48  qed "zdvd_zmult_mono";
    6.49  
    6.50 -Goal "k dvd (n + k*m) = k dvd (n::int)";
    6.51 +Goal "(k dvd n + k*m) = (k dvd (n::int))";
    6.52  by (rtac iffI 1);
    6.53  by (etac zdvd_zadd 2);
    6.54  by (subgoal_tac "n = (n+k*m)-k*m" 1);
    6.55 @@ -135,12 +135,12 @@
    6.56  by (ALLGOALS Simp_tac);
    6.57  qed "zdvd_reduce";
    6.58  
    6.59 -Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd (m mod n)";
    6.60 +Goalw [dvd_def] "[| f dvd m; f dvd (n::int) |] ==> f dvd m mod n";
    6.61  by (auto_tac (claset(), simpset() addsimps [zmod_zmult_zmult1]));
    6.62  qed "zdvd_zmod";
    6.63  
    6.64 -Goal "[| k dvd (m mod n);  k dvd n |] ==> k dvd (m::int)";
    6.65 -by (subgoal_tac "k dvd (n*(m div n) + m mod n)" 1);
    6.66 +Goal "[| k dvd m mod n;  k dvd n |] ==> k dvd (m::int)";
    6.67 +by (subgoal_tac "k dvd n*(m div n) + m mod n" 1);
    6.68  by (asm_simp_tac (simpset() addsimps [zdvd_zadd, zdvd_zmult2]) 2);
    6.69  by (asm_full_simp_tac (simpset() addsimps [zmod_zdiv_equality RS sym]) 1);
    6.70  qed "zdvd_zmod_imp_zdvd";
    6.71 @@ -334,14 +334,14 @@
    6.72  qed "zgcd_zmult_eq_self2";
    6.73  Addsimps [zgcd_zmult_eq_self2];
    6.74  
    6.75 -Goal "[| zgcd(n,k)=#1; k dvd (m*n); #0 <= m |] ==> k dvd m";
    6.76 +Goal "[| zgcd(n,k)=#1; k dvd m*n; #0 <= m |] ==> k dvd m";
    6.77  by (subgoal_tac "m = zgcd(m*n, m*k)" 1);
    6.78  by (etac ssubst 1 THEN rtac (zgcd_greatest_iff RS iffD2) 1);
    6.79  by (ALLGOALS (asm_simp_tac (simpset() 
    6.80        addsimps [zgcd_zmult_distrib2 RS sym,int_0_le_mult_iff])));
    6.81  val lemma = result();
    6.82  
    6.83 -Goal "[| zgcd(n,k)=#1; k dvd (m*n) |] ==> k dvd m";
    6.84 +Goal "[| zgcd(n,k)=#1; k dvd m*n |] ==> k dvd m";
    6.85  by (case_tac "#0 <= m" 1);
    6.86  by (blast_tac (claset() addIs [lemma]) 1); 
    6.87  by (subgoal_tac "k dvd -m" 1);
    6.88 @@ -359,7 +359,7 @@
    6.89  by (assume_tac 1);
    6.90  qed "zless_zprime_imp_zrelprime";
    6.91  
    6.92 -Goal "[| #0<=(m::int); p:zprime; p dvd (m*n) |] ==> p dvd m | p dvd n";
    6.93 +Goal "[| #0<=(m::int); p:zprime; p dvd m*n |] ==> p dvd m | p dvd n";
    6.94  by Safe_tac;
    6.95  by (rtac zrelprime_zdvd_zmult 1);
    6.96  by (rtac zprime_imp_zrelprime 1);
    6.97 @@ -510,7 +510,7 @@
    6.98        "[| [a = b] (mod m);  [a = b] (mod n);  zgcd(m,n) = #1 |] \
    6.99  \     ==> [a=b](mod m*n)";
   6.100  by Auto_tac;
   6.101 -by (subgoal_tac "m dvd (n*ka)" 1);
   6.102 +by (subgoal_tac "m dvd n*ka" 1);
   6.103  by (subgoal_tac "m dvd ka" 1);
   6.104  by (case_tac "#0<=ka" 2);
   6.105  by (stac (zdvd_zminus_iff RS sym) 3);
     7.1 --- a/src/HOL/NumberTheory/Primes.thy	Fri Jan 05 13:10:37 2001 +0100
     7.2 +++ b/src/HOL/NumberTheory/Primes.thy	Fri Jan 05 14:28:10 2001 +0100
     7.3 @@ -59,7 +59,7 @@
     7.4    done
     7.5  
     7.6  (*gcd(m,n) divides m and n.  The conjunctions don't seem provable separately*)
     7.7 -lemma gcd_dvd_both: "(gcd(m,n) dvd m) & (gcd(m,n) dvd n)"
     7.8 +lemma gcd_dvd_both: "gcd(m,n) dvd m & gcd(m,n) dvd n"
     7.9    apply (induct_tac m n rule: gcd_induct)
    7.10    apply (simp_all add: gcd_non_0)
    7.11    apply (blast dest: dvd_mod_imp_dvd)
    7.12 @@ -71,12 +71,12 @@
    7.13  
    7.14  (*Maximality: for all m,n,k naturals, 
    7.15                  if k divides m and k divides n then k divides gcd(m,n)*)
    7.16 -lemma gcd_greatest [rule_format]: "(k dvd m) --> (k dvd n) --> k dvd gcd(m,n)"
    7.17 +lemma gcd_greatest [rule_format]: "k dvd m --> k dvd n --> k dvd gcd(m,n)"
    7.18    apply (induct_tac m n rule: gcd_induct)
    7.19    apply (simp_all add: gcd_non_0 dvd_mod);
    7.20    done;
    7.21  
    7.22 -lemma gcd_greatest_iff [iff]: "k dvd gcd(m,n) = (k dvd m & k dvd n)"
    7.23 +lemma gcd_greatest_iff [iff]: "(k dvd gcd(m,n)) = (k dvd m & k dvd n)"
    7.24    apply (blast intro!: gcd_greatest intro: dvd_trans);
    7.25    done;
    7.26  
    7.27 @@ -142,14 +142,14 @@
    7.28    apply (rule gcd_mult [of k 1, simplified])
    7.29    done
    7.30  
    7.31 -lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd (m*n) |] ==> k dvd m";
    7.32 +lemma relprime_dvd_mult: "[| gcd(k,n)=1; k dvd m*n |] ==> k dvd m";
    7.33    apply (insert gcd_mult_distrib2 [of m k n])
    7.34    apply (simp)
    7.35    apply (erule_tac t="m" in ssubst);
    7.36    apply (simp)
    7.37    done
    7.38  
    7.39 -lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> k dvd (m*n) = k dvd m";
    7.40 +lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> (k dvd m*n) = (k dvd m)";
    7.41    apply (blast intro: relprime_dvd_mult dvd_trans)
    7.42    done
    7.43  
    7.44 @@ -163,7 +163,7 @@
    7.45  
    7.46  (*This theorem leads immediately to a proof of the uniqueness of factorization.
    7.47    If p divides a product of primes then it is one of those primes.*)
    7.48 -lemma prime_dvd_mult: "[| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n"
    7.49 +lemma prime_dvd_mult: "[| p: prime; p dvd m*n |] ==> p dvd m | p dvd n"
    7.50    apply (blast intro: relprime_dvd_mult prime_imp_relprime)
    7.51    done
    7.52  
     8.1 --- a/src/HOL/NumberTheory/WilsonBij.ML	Fri Jan 05 13:10:37 2001 +0100
     8.2 +++ b/src/HOL/NumberTheory/WilsonBij.ML	Fri Jan 05 14:28:10 2001 +0100
     8.3 @@ -56,7 +56,7 @@
     8.4  by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
     8.5  by (stac zdvd_zminus_iff 1);
     8.6  by (stac zdvd_reduce 1);
     8.7 -by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
     8.8 +by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1);
     8.9  by (stac zdvd_reduce 1);
    8.10  by Auto_tac;
    8.11  val lemma = result();
     9.1 --- a/src/HOL/NumberTheory/WilsonRuss.ML	Fri Jan 05 13:10:37 2001 +0100
     9.2 +++ b/src/HOL/NumberTheory/WilsonRuss.ML	Fri Jan 05 14:28:10 2001 +0100
     9.3 @@ -65,7 +65,7 @@
     9.4  by (simp_tac (simpset() addsimps [zmult_commute,zminus_zdiff_eq]) 1);
     9.5  by (stac zdvd_zminus_iff 1);
     9.6  by (stac zdvd_reduce 1);
     9.7 -by (res_inst_tac [("s","p dvd ((a+#1)+(p*(-#1)))")] trans 1);
     9.8 +by (res_inst_tac [("s","p dvd (a+#1)+(p*(-#1))")] trans 1);
     9.9  by (stac zdvd_reduce 1);
    9.10  by Auto_tac;
    9.11  val lemma = result();