a few new lemmas.

--- a/src/HOL/Arith.ML	Thu Oct 01 18:28:47 1998 +0200
+++ b/src/HOL/Arith.ML	Thu Oct 01 18:29:25 1998 +0200
@@ -93,11 +93,27 @@
 (** Reasoning about m+0=0, etc. **)
 
 Goal "(m+n = 0) = (m=0 & n=0)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
+by (exhaust_tac "m" 1);
+by (Auto_tac);
 qed "add_is_0";
 AddIffs [add_is_0];
 
+Goal "(0 = m+n) = (m=0 & n=0)";
+by (exhaust_tac "m" 1);
+by (Auto_tac);
+qed "zero_is_add";
+AddIffs [zero_is_add];
+
+Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
+by(exhaust_tac "m" 1);
+by(Auto_tac);
+qed "add_is_1";
+
+Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
+by(exhaust_tac "m" 1);
+by(Auto_tac);
+qed "one_is_add";
+
 Goal "(0<m+n) = (0<m | 0<n)";
 by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
 qed "add_gr_0";