src/HOL/Arith.ML
changeset 5427 26c9a7c0b36b
parent 5414 8a458866637c
child 5429 0833486c23ce
     1.1 --- a/src/HOL/Arith.ML	Thu Sep 03 16:40:02 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Sep 04 11:01:59 1998 +0200
     1.3 @@ -613,6 +613,17 @@
     1.4  by (Asm_full_simp_tac 1);
     1.5  qed "add_less_imp_less_diff";
     1.6  
     1.7 +Goal "(i < j-k) = (i+k < (j::nat))";
     1.8 +br iffI 1;
     1.9 + by(case_tac "k <= j" 1);
    1.10 +  bd le_add_diff_inverse2 1;
    1.11 +  by(dres_inst_tac [("k","k")] add_less_mono1 1);
    1.12 +  by(Asm_full_simp_tac 1);
    1.13 + by(rotate_tac 1 1);
    1.14 + by(asm_full_simp_tac (simpset() addSolver cut_trans_tac) 1);
    1.15 +be add_less_imp_less_diff 1;
    1.16 +qed "less_diff_conv";
    1.17 +
    1.18  Goal "Suc i <= n ==> Suc (n - Suc i) = n - i";
    1.19  by (asm_simp_tac (simpset() addsimps [Suc_diff_le RS sym]) 1);
    1.20  qed "Suc_diff_Suc";