# HG changeset patch
# User paulson
# Date 977310866 -3600
# Node ID 0c8d583326587f066ec0f7d5a4851a15e77c0507
# Parent  7a29b71d635265983c556615500da48738428f44
tidying, removing obsolete lemmas about 0=... and 1=...

diff -r 7a29b71d6352 -r 0c8d58332658 src/HOL/Integ/nat_bin.ML
--- a/src/HOL/Integ/nat_bin.ML	Wed Dec 20 12:13:59 2000 +0100
+++ b/src/HOL/Integ/nat_bin.ML	Wed Dec 20 12:14:26 2000 +0100
@@ -309,8 +309,7 @@
 
 AddIffs (map rename_numerals
 	 [Suc_not_Zero, Zero_not_Suc, zero_less_Suc, not_less0, less_one, 
-	  le0, le_0_eq, 
-	  neq0_conv, zero_neq_conv, not_gr0]);
+	  le0, le_0_eq, neq0_conv, not_gr0]);
 
 (** Arith **)
 
@@ -323,12 +322,12 @@
 (*Non-trivial simplifications*)	 
 val other_renamed_arith_simps =
     map rename_numerals
-	[diff_is_0_eq, zero_is_diff_eq, zero_less_diff,
-	 mult_is_0, zero_is_mult, zero_less_mult_iff, mult_eq_1_iff];
+	[diff_is_0_eq, zero_less_diff,
+	 mult_is_0, zero_less_mult_iff, mult_eq_1_iff];
 
 Addsimps (basic_renamed_arith_simps @ other_renamed_arith_simps);
 
-AddIffs (map rename_numerals [add_is_0, zero_is_add, add_gr_0]);
+AddIffs (map rename_numerals [add_is_0, add_gr_0]);
 
 Goal "Suc n = n + #1";
 by (asm_simp_tac numeral_ss 1);
@@ -359,7 +358,6 @@
 
 (*various theorems that aren't in the default simpset*)
 bind_thm ("add_is_one'", rename_numerals add_is_1);
-bind_thm ("one_is_add'", rename_numerals one_is_add);
 bind_thm ("zero_induct'", rename_numerals zero_induct);
 bind_thm ("diff_self_eq_0'", rename_numerals diff_self_eq_0);
 bind_thm ("mult_eq_self_implies_10'", rename_numerals mult_eq_self_implies_10);
diff -r 7a29b71d6352 -r 0c8d58332658 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Dec 20 12:13:59 2000 +0100
+++ b/src/HOL/Nat.ML	Wed Dec 20 12:14:26 2000 +0100
@@ -43,12 +43,6 @@
 qed "neq0_conv";
 AddIffs [neq0_conv];
 
-Goal "!!n::nat. (0 ~= n) = (0 < n)";
-by (case_tac "n" 1);
-by Auto_tac;
-qed "zero_neq_conv";
-AddIffs [zero_neq_conv];
-
 (*This theorem is useful with blast_tac: (n=0 ==> False) ==> 0<n *)
 bind_thm ("gr0I", [neq0_conv, notI] MRS iffD1);
 
@@ -235,22 +229,11 @@
 qed "add_is_0";
 AddIffs [add_is_0];
 
-Goal "!!m::nat. (0 = m+n) = (m=0 & n=0)";
-by (case_tac "m" 1);
-by (Auto_tac);
-qed "zero_is_add";
-AddIffs [zero_is_add];
-
 Goal "!!m::nat. (m+n=1) = (m=1 & n=0 | m=0 & n=1)";
 by (case_tac "m" 1);
 by (Auto_tac);
 qed "add_is_1";
 
-Goal "!!m::nat. (1=m+n) = (m=1 & n=0 | m=0 & n=1)";
-by (case_tac "m" 1);
-by (Auto_tac);
-qed "one_is_add";
-
 Goal "!!m::nat. (0<m+n) = (0<m | 0<n)";
 by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
 qed "add_gr_0";
@@ -445,13 +428,7 @@
 by (induct_tac "n" 2);
 by (ALLGOALS Asm_simp_tac);
 qed "mult_is_0";
-
-Goal "!!m::nat. (0 = m*n) = (0=m | 0=n)";
-by (stac eq_commute 1 THEN stac mult_is_0 1);
-by Auto_tac;
-qed "zero_is_mult";
-
-Addsimps [mult_is_0, zero_is_mult];
+Addsimps [mult_is_0];
 
 
 (*** Difference ***)
@@ -552,12 +529,7 @@
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
 by (ALLGOALS Asm_simp_tac);
 qed "diff_is_0_eq";
-
-Goal "!!m::nat. (0 = m-n) = (m <= n)";
-by (stac (diff_is_0_eq RS sym) 1);
-by (rtac eq_sym_conv 1);
-qed "zero_is_diff_eq";
-Addsimps [diff_is_0_eq, zero_is_diff_eq];
+Addsimps [diff_is_0_eq];
 
 Goal "!!m::nat. (0<n-m) = (m<n)";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);