src/HOL/Arith.ML
changeset 4297 5defc2105cc8
parent 4158 47c7490c74fe
child 4356 0dfd34f0d33d
     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