src/HOL/Arith.ML
changeset 4736 f7d3b9aec7a1
parent 4732 10af4886b33f
child 4830 bd73675adbed
     1.1 --- a/src/HOL/Arith.ML	Wed Mar 11 14:54:41 1998 +0100
     1.2 +++ b/src/HOL/Arith.ML	Thu Mar 12 10:37:58 1998 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      HOL/Arith.ML
     1.5      ID:         $Id$
     1.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 -    Copyright   1993  University of Cambridge
     1.8 +    Copyright   1998  University of Cambridge
     1.9  
    1.10  Proofs about elementary arithmetic: addition, multiplication, etc.
    1.11  Some from the Hoare example from Norbert Galm
    1.12 @@ -370,13 +370,10 @@
    1.13  by (ALLGOALS Asm_simp_tac);
    1.14  qed "diff_diff_left";
    1.15  
    1.16 -(* This is a trivial consequence of diff_diff_left;
    1.17 -   could be got rid of if diff_diff_left were in the simpset...
    1.18 -*)
    1.19 -goal thy "(Suc m - n)-1 = m - n";
    1.20 +goal Arith.thy "(Suc m - n) - Suc k = m - n - k";
    1.21  by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
    1.22 -qed "pred_Suc_diff";
    1.23 -Addsimps [pred_Suc_diff];
    1.24 +qed "Suc_diff_diff";
    1.25 +Addsimps [Suc_diff_diff];
    1.26  
    1.27  goal thy "!!n. 0<n ==> n - Suc i < n";
    1.28  by (res_inst_tac [("n","n")] natE 1);
    1.29 @@ -610,7 +607,7 @@
    1.30  qed "mult_eq_self_implies_10";
    1.31  
    1.32  
    1.33 -(*** Subtraction laws -- from Clemens Ballarin ***)
    1.34 +(*** Subtraction laws -- mostly from Clemens Ballarin ***)
    1.35  
    1.36  goal thy "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c";
    1.37  by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
    1.38 @@ -650,6 +647,11 @@
    1.39  by (Simp_tac 1);
    1.40  qed "le_add_diff";
    1.41  
    1.42 +goal Arith.thy "!!i::nat. 0<k ==> j<i --> j+k-i < k";
    1.43 +by (res_inst_tac [("m","j"),("n","i")] diff_induct 1);
    1.44 +by (ALLGOALS Asm_simp_tac);
    1.45 +qed_spec_mp "add_diff_less";
    1.46 +
    1.47  
    1.48  
    1.49  (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)