new theorem le_diff_conv
authorpaulson
Mon Sep 14 10:17:19 1998 +0200 (1998-09-14)
changeset 54850cd451e46a20
parent 5484 e9430ed7e8d6
child 5486 d98a55f581c5
new theorem le_diff_conv
src/HOL/Arith.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Sep 11 18:09:54 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Sep 14 10:17:19 1998 +0200
     1.3 @@ -633,6 +633,11 @@
     1.4  be add_less_imp_less_diff 1;
     1.5  qed "less_diff_conv";
     1.6  
     1.7 +Goal "k <= j ==> (i <= j-k) = (i+k <= (j::nat))";
     1.8 +by (asm_full_simp_tac (simpset() addsimps [le_eq_less_Suc, less_diff_conv,
     1.9 +					   Suc_diff_le RS sym]) 1);
    1.10 +qed "le_diff_conv";
    1.11 +
    1.12  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.13  by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
    1.14  qed "Suc_diff_Suc";