# HG changeset patch
# User paulson
# Date 889695478 -3600
# Node ID f7d3b9aec7a153f9b8220f592ebec6d692b216de
# Parent  6d544b44a70e8f989b9711f58025783d3d4284ee
New laws, mostly generalizing old "pred" ones

diff -r 6d544b44a70e -r f7d3b9aec7a1 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Mar 11 14:54:41 1998 +0100
+++ b/src/HOL/Arith.ML	Thu Mar 12 10:37:58 1998 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/Arith.ML
     ID:         $Id$
     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1993  University of Cambridge
+    Copyright   1998  University of Cambridge
 
 Proofs about elementary arithmetic: addition, multiplication, etc.
 Some from the Hoare example from Norbert Galm
@@ -370,13 +370,10 @@
 by (ALLGOALS Asm_simp_tac);
 qed "diff_diff_left";
 
-(* This is a trivial consequence of diff_diff_left;
-   could be got rid of if diff_diff_left were in the simpset...
-*)
-goal thy "(Suc m - n)-1 = m - n";
+goal Arith.thy "(Suc m - n) - Suc k = m - n - k";
 by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
-qed "pred_Suc_diff";
-Addsimps [pred_Suc_diff];
+qed "Suc_diff_diff";
+Addsimps [Suc_diff_diff];
 
 goal thy "!!n. 0<n ==> n - Suc i < n";
 by (res_inst_tac [("n","n")] natE 1);
@@ -610,7 +607,7 @@
 qed "mult_eq_self_implies_10";
 
 
-(*** Subtraction laws -- from Clemens Ballarin ***)
+(*** Subtraction laws -- mostly from Clemens Ballarin ***)
 
 goal thy "!! a b c::nat. [| a < b; c <= a |] ==> a-c < b-c";
 by (subgoal_tac "c+(a-c) < c+(b-c)" 1);
@@ -650,6 +647,11 @@
 by (Simp_tac 1);
 qed "le_add_diff";
 
+goal Arith.thy "!!i::nat. 0<k ==> j<i --> j+k-i < k";
+by (res_inst_tac [("m","j"),("n","i")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed_spec_mp "add_diff_less";
+
 
 
 (** (Anti)Monotonicity of subtraction -- by Stefan Merz **)