src/HOL/Nat.ML
changeset 10710 0c8d58332658
parent 10558 09a91221ced1
child 10850 e1a793957a8f
     1.1 --- a/src/HOL/Nat.ML	Wed Dec 20 12:13:59 2000 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Dec 20 12:14:26 2000 +0100
     1.3 @@ -43,12 +43,6 @@
     1.4  qed "neq0_conv";
     1.5  AddIffs [neq0_conv];
     1.6  
     1.7 -Goal "!!n::nat. (0 ~= n) = (0 < n)";
     1.8 -by (case_tac "n" 1);
     1.9 -by Auto_tac;
    1.10 -qed "zero_neq_conv";
    1.11 -AddIffs [zero_neq_conv];
    1.12 -
    1.13  (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
    1.14  bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
    1.15  
    1.16 @@ -235,22 +229,11 @@
    1.17  qed "add_is_0";
    1.18  AddIffs [add_is_0];
    1.19  
    1.20 -Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
    1.21 -by (case_tac "m" 1);
    1.22 -by (Auto_tac);
    1.23 -qed "zero_is_add";
    1.24 -AddIffs [zero_is_add];
    1.25 -
    1.26  Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
    1.27  by (case_tac "m" 1);
    1.28  by (Auto_tac);
    1.29  qed "add_is_1";
    1.30  
    1.31 -Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
    1.32 -by (case_tac "m" 1);
    1.33 -by (Auto_tac);
    1.34 -qed "one_is_add";
    1.35 -
    1.36  Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
    1.37  by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    1.38  qed "add_gr_0";
    1.39 @@ -445,13 +428,7 @@
    1.40  by (induct_tac "n" 2);
    1.41  by (ALLGOALS Asm_simp_tac);
    1.42  qed "mult_is_0";
    1.43 -
    1.44 -Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
    1.45 -by (stac eq_commute 1 THEN stac mult_is_0 1);
    1.46 -by Auto_tac;
    1.47 -qed "zero_is_mult";
    1.48 -
    1.49 -Addsimps [mult_is_0, zero_is_mult];
    1.50 +Addsimps [mult_is_0];
    1.51  
    1.52  
    1.53  (*** Difference ***)
    1.54 @@ -552,12 +529,7 @@
    1.55  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.56  by (ALLGOALS Asm_simp_tac);
    1.57  qed "diff_is_0_eq";
    1.58 -
    1.59 -Goal "!!m::nat. (0 = m-n) = (m <= n)";
    1.60 -by (stac (diff_is_0_eq RS sym) 1);
    1.61 -by (rtac eq_sym_conv 1);
    1.62 -qed "zero_is_diff_eq";
    1.63 -Addsimps [diff_is_0_eq, zero_is_diff_eq];
    1.64 +Addsimps [diff_is_0_eq];
    1.65  
    1.66  Goal "!!m::nat. (0<n-m) = (m<n)";
    1.67  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);