added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
authorwenzelm
Wed Nov 26 16:45:54 1997 +0100 (1997-11-26)
changeset 42975defc2105cc8
parent 4296 aa84d9c62454
child 4298 b69eedd3aa6c
added Suc_mult_less_cancel1, Suc_mult_le_cancel1, Suc_mult_cancel1;
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Nov 26 16:44:47 1997 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Nov 26 16:45:54 1997 +0100
     1.3 @@ -557,6 +557,16 @@
     1.4  qed "mult_less_cancel1";
     1.5  Addsimps [mult_less_cancel1, mult_less_cancel2];
     1.6  
     1.7 +goal Arith.thy "(Suc k * m < Suc k * n) = (m < n)";
     1.8 +br mult_less_cancel1 1;
     1.9 +by (Simp_tac 1);
    1.10 +qed "Suc_mult_less_cancel1";
    1.11 +
    1.12 +goalw Arith.thy [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
    1.13 +by (simp_tac (simpset_of HOL.thy) 1);
    1.14 +br Suc_mult_less_cancel1 1;
    1.15 +qed "Suc_mult_le_cancel1";
    1.16 +
    1.17  goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    1.18  by (cut_facts_tac [less_linear] 1);
    1.19  by Safe_tac;
    1.20 @@ -571,6 +581,11 @@
    1.21  qed "mult_cancel1";
    1.22  Addsimps [mult_cancel1, mult_cancel2];
    1.23  
    1.24 +goal Arith.thy "(Suc k * m = Suc k * n) = (m = n)";
    1.25 +br mult_cancel1 1;
    1.26 +by (Simp_tac 1);
    1.27 +qed "Suc_mult_cancel1";
    1.28 +
    1.29  
    1.30  (** Lemma for gcd **)
    1.31