# HG changeset patch
# User paulson
# Date 1014727068 -3600
# Node ID b94843ffc0d102a2f50f9974929ab504ddd38488
# Parent  2e22321e34ea39fb13bcf0cc4ff8a6892c30ef90
Fixed the natxx_cancel_numerals simprocs so that they pull out Sucs and
return False for e.g. Suc x = 0.  Removed ad-hoc lemmas for that purpose.

diff -r 2e22321e34ea -r b94843ffc0d1 src/HOL/Integ/nat_simprocs.ML
--- a/src/HOL/Integ/nat_simprocs.ML	Tue Feb 26 12:51:40 2002 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML	Tue Feb 26 13:37:48 2002 +0100
@@ -215,10 +215,16 @@
 val mult_1s = map rename_numerals [mult_1, mult_1_right];
 
 (*Final simplification: cancel + and *; replace Numeral0 by 0 and Numeral1 by 1*)
+
+(*And these help the simproc return False when appropriate, which helps
+  the arith prover.*)
+val contra_rules = [add_Suc, add_Suc_right, Zero_not_Suc, Suc_not_Zero, 
+                    le_0_eq];
+
 val simplify_meta_eq =
     Int_Numeral_Simprocs.simplify_meta_eq
-         [numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right,
-         mult_0, mult_0_right, mult_1, mult_1_right];
+        ([numeral_0_eq_0, numeral_1_eq_Suc_0, add_0, add_0_right,
+          mult_0, mult_0_right, mult_1, mult_1_right] @ contra_rules);
 
 
 (** Restricted version of dest_Sucs_sum for nat_combine_numerals:
diff -r 2e22321e34ea -r b94843ffc0d1 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Tue Feb 26 12:51:40 2002 +0100
+++ b/src/HOL/Nat.ML	Tue Feb 26 13:37:48 2002 +0100
@@ -258,19 +258,6 @@
                                  delsimps [add_0_right]) 1);
 qed "add_eq_self_zero";
 
-(* a rather special thm needed for arith_tac: m+n = 0 may arise where m or n
-contain Suc. This contradiction must be detected. It cannot be detected by
-pulling Suc outside because this interferes with simprocs on
-numerals. Sigh. *)
-
-Goal "m ~= 0 ==> m+n ~= (0::nat)";
-by(Asm_full_simp_tac 1);
-qed "add_not_0_if_left_not_0";
-
-Goal "n ~= 0 ==> m+n ~= (0::nat)";
-by(Asm_full_simp_tac 1);
-qed "add_not_0_if_right_not_0";
-
 (**** Additional theorems about "less than" ****)
 
 (*Deleted less_natE; instead use less_imp_Suc_add RS exE*)
diff -r 2e22321e34ea -r b94843ffc0d1 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue Feb 26 12:51:40 2002 +0100
+++ b/src/HOL/arith_data.ML	Tue Feb 26 13:37:48 2002 +0100
@@ -368,8 +368,6 @@
 *)
 val add_rules =
  [add_0,add_0_right,Zero_not_Suc,Suc_not_Zero,le_0_eq,
-  add_not_0_if_left_not_0,add_not_0_if_right_not_0,
-  add_not_0_if_left_not_0 RS not_sym,add_not_0_if_right_not_0 RS not_sym,
   One_nat_def];
 
 val add_mono_thms_nat = map (fn s => prove_goal (the_context ()) s