Two new subtraction lemmas
authorpaulson
Tue Sep 01 10:09:11 1998 +0200 (1998-09-01)
changeset 5409e97558ee8e76
parent 5408 0a0a35dddabd
child 5410 5ed7547a7f74
Two new subtraction lemmas
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Sun Aug 30 15:14:42 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Tue Sep 01 10:09:11 1998 +0200
     1.3 @@ -493,6 +493,7 @@
     1.4  qed "diff_add_0";
     1.5  Addsimps [diff_add_0];
     1.6  
     1.7 +
     1.8  (** Difference distributes over multiplication **)
     1.9  
    1.10  Goal "!!m::nat. (m - n) * k = (m * k) - (n * k)";
    1.11 @@ -675,6 +676,17 @@
    1.12  qed "diff_Suc_le_diff";
    1.13  AddIffs [diff_Suc_le_diff];
    1.14  
    1.15 +Goal "0 < n ==> (m <= n-1) = (m<n)";
    1.16 +by (exhaust_tac "n" 1);
    1.17 +by Auto_tac;
    1.18 +by (ALLGOALS trans_tac);
    1.19 +qed "le_pred_eq";
    1.20 +
    1.21 +Goal "0 < n ==> (m-1 < n) = (m<=n)";
    1.22 +by (exhaust_tac "m" 1);
    1.23 +by (auto_tac (claset(), simpset() addsimps [Suc_le_eq]));
    1.24 +qed "less_pred_eq";
    1.25 +
    1.26  
    1.27  
    1.28  (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)