src/HOL/Arith.ML
changeset 5598 6b8dee1a6ebb
parent 5537 c2bd39a2c0ee
child 5604 cd17004d09e1
     1.1 --- a/src/HOL/Arith.ML	Thu Oct 01 18:28:47 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Oct 01 18:29:25 1998 +0200
     1.3 @@ -93,11 +93,27 @@
     1.4  (** Reasoning about m+0=0, etc. **)
     1.5  
     1.6  Goal "(m+n = 0) = (m=0 & n=0)";
     1.7 -by (induct_tac "m" 1);
     1.8 -by (ALLGOALS Asm_simp_tac);
     1.9 +by (exhaust_tac "m" 1);
    1.10 +by (Auto_tac);
    1.11  qed "add_is_0";
    1.12  AddIffs [add_is_0];
    1.13  
    1.14 +Goal "(0 = m+n) = (m=0 & n=0)";
    1.15 +by (exhaust_tac "m" 1);
    1.16 +by (Auto_tac);
    1.17 +qed "zero_is_add";
    1.18 +AddIffs [zero_is_add];
    1.19 +
    1.20 +Goal "(m+n=1) = (m=1 & n=0 | m=0 & n=1)";
    1.21 +by(exhaust_tac "m" 1);
    1.22 +by(Auto_tac);
    1.23 +qed "add_is_1";
    1.24 +
    1.25 +Goal "(1=m+n) = (m=1 & n=0 | m=0 & n=1)";
    1.26 +by(exhaust_tac "m" 1);
    1.27 +by(Auto_tac);
    1.28 +qed "one_is_add";
    1.29 +
    1.30  Goal "(0<m+n) = (0<m | 0<n)";
    1.31  by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    1.32  qed "add_gr_0";