diff -r 78c9acf5bc38 -r 1c9d5895d824 Arith.ML
--- a/Arith.ML	Mon Feb 27 17:20:33 1995 +0100
+++ b/Arith.ML	Tue Feb 28 02:00:28 1995 +0100
@@ -1,10 +1,8 @@
-(*  Title: 	HOL/arith.ML
+(*  Title: 	HOL/Arith.ML
     ID:         $Id$
     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1993  University of Cambridge
 
-For HOL/arith.thy.
-
 Proofs about elementary arithmetic: addition, multiplication, etc.
 Tests definitions and simplifier.
 *)
@@ -67,6 +65,29 @@
 (*Addition is an AC-operator*)
 val add_ac = [add_assoc, add_commute, add_left_commute];
 
+goal Arith.thy "!!k::nat. (k + m = k + n) = (m=n)";
+by (nat_ind_tac "k" 1);
+by (simp_tac arith_ss 1);
+by (asm_simp_tac arith_ss 1);
+qed "add_left_cancel";
+
+goal Arith.thy "!!k::nat. (m + k = n + k) = (m=n)";
+by (nat_ind_tac "k" 1);
+by (simp_tac arith_ss 1);
+by (asm_simp_tac arith_ss 1);
+qed "add_right_cancel";
+
+goal Arith.thy "!!k::nat. (k + m <= k + n) = (m<=n)";
+by (nat_ind_tac "k" 1);
+by (simp_tac arith_ss 1);
+by (asm_simp_tac (arith_ss addsimps [Suc_le_mono]) 1);
+qed "add_left_cancel_le";
+
+goal Arith.thy "!!k::nat. (k + m < k + n) = (m<n)";
+by (nat_ind_tac "k" 1);
+by (simp_tac arith_ss 1);
+by (asm_simp_tac arith_ss 1);
+qed "add_left_cancel_less";
 
 (*** Multiplication ***)
 
@@ -127,6 +148,23 @@
 by (ALLGOALS(asm_simp_tac arith_ss));
 qed "diff_less_Suc";
 
+goal Arith.thy "!!m::nat. m - n <= m";
+by (res_inst_tac [("m","m"), ("n","n")] diff_induct 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+by (etac le_trans 1);
+by (simp_tac (HOL_ss addsimps [le_eq_less_or_eq, lessI]) 1);
+qed "diff_le_self";
+
+goal Arith.thy "!!n::nat. (n+m) - n = m";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+qed "diff_add_inverse";
+
+goal Arith.thy "!!n::nat. n - (n+m) = 0";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+qed "diff_add_0";
+
 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
 goal Arith.thy "!!m. [| 0<n; ~ m<n |] ==> m - n < m";
 by (subgoal_tac "0<n --> ~ m<n --> m - n < m" 1);
@@ -223,6 +261,21 @@
 
 (**** Additional theorems about "less than" ****)
 
+goal Arith.thy "!!m. m<n --> (? k. n=Suc(m+k))";
+by (nat_ind_tac "n" 1);
+by (ALLGOALS(simp_tac arith_ss));
+by (REPEAT_FIRST (ares_tac [conjI, impI]));
+by (res_inst_tac [("x","0")] exI 2);
+by (simp_tac arith_ss 2);
+by (safe_tac HOL_cs);
+by (res_inst_tac [("x","Suc(k)")] exI 1);
+by (simp_tac arith_ss 1);
+val less_eq_Suc_add_lemma = result();
+
+(*"m<n ==> ? k. n = Suc(m+k)"*)
+bind_thm ("less_eq_Suc_add", less_eq_Suc_add_lemma RS mp);
+
+
 goal Arith.thy "n <= ((m + n)::nat)";
 by (nat_ind_tac "m" 1);
 by (ALLGOALS(simp_tac arith_ss));
@@ -238,9 +291,83 @@
 bind_thm ("less_add_Suc1", (lessI RS (le_add1 RS le_less_trans)));
 bind_thm ("less_add_Suc2", (lessI RS (le_add2 RS le_less_trans)));
 
+(*"i <= j ==> i <= j+m"*)
+bind_thm ("trans_le_add1", le_add1 RSN (2,le_trans));
+
+(*"i <= j ==> i <= m+j"*)
+bind_thm ("trans_le_add2", le_add2 RSN (2,le_trans));
+
+(*"i < j ==> i < j+m"*)
+bind_thm ("trans_less_add1", le_add1 RSN (2,less_le_trans));
+
+(*"i < j ==> i < m+j"*)
+bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
+
+goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
+by (eresolve_tac [le_trans] 1);
+by (resolve_tac [le_add1] 1);
+qed "le_imp_add_le";
+
+goal Arith.thy "!!k::nat. m < n ==> m < n+k";
+by (eresolve_tac [less_le_trans] 1);
+by (resolve_tac [le_add1] 1);
+qed "less_imp_add_less";
+
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
 by (nat_ind_tac "k" 1);
 by (ALLGOALS (asm_simp_tac arith_ss));
 by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
-qed "plus_leD1_lemma";
-val plus_leD1 = plus_leD1_lemma RS mp;
+val add_leD1_lemma = result();
+bind_thm ("add_leD1", add_leD1_lemma RS mp);;
+
+goal Arith.thy "!!k l::nat. [| k<l; m+l = k+n |] ==> m<n";
+by (safe_tac (HOL_cs addSDs [less_eq_Suc_add]));
+by (asm_full_simp_tac
+    (HOL_ss addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
+by (eresolve_tac [subst] 1);
+by (simp_tac (arith_ss addsimps [less_add_Suc1]) 1);
+qed "less_add_eq_less";
+
+
+(** Monotonicity of addition (from ZF/Arith) **)
+
+(** Monotonicity results **)
+
+(*strict, in 1st argument*)
+goal Arith.thy "!!i j k::nat. i < j ==> i + k < j + k";
+by (nat_ind_tac "k" 1);
+by (ALLGOALS (asm_simp_tac arith_ss));
+qed "add_less_mono1";
+
+(*strict, in both arguments*)
+goal Arith.thy "!!i j k::nat. [|i < j; k < l|] ==> i + k < j + l";
+by (rtac (add_less_mono1 RS less_trans) 1);
+by (REPEAT (etac asm_rl 1));
+by (nat_ind_tac "j" 1);
+by (ALLGOALS(asm_simp_tac arith_ss));
+qed "add_less_mono";
+
+(*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
+val [lt_mono,le] = goal Arith.thy
+     "[| !!i j::nat. i<j ==> f(i) < f(j);	\
+\        i <= j					\
+\     |] ==> f(i) <= (f(j)::nat)";
+by (cut_facts_tac [le] 1);
+by (asm_full_simp_tac (HOL_ss addsimps [le_eq_less_or_eq]) 1);
+by (fast_tac (HOL_cs addSIs [lt_mono]) 1);
+qed "less_mono_imp_le_mono";
+
+(*non-strict, in 1st argument*)
+goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
+by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
+by (eresolve_tac [add_less_mono1] 1);
+by (assume_tac 1);
+qed "add_le_mono1";
+
+(*non-strict, in both arguments*)
+goal Arith.thy "!!k l::nat. [|i<=j;  k<=l |] ==> i + k <= j + l";
+by (etac (add_le_mono1 RS le_trans) 1);
+by (simp_tac (HOL_ss addsimps [add_commute]) 1);
+(*j moves to the end because it is free while k, l are bound*)
+by (eresolve_tac [add_le_mono1] 1);
+qed "add_le_mono";