# HG changeset patch
# User paulson
# Date 958478826 -7200
# Node ID 9d6514fcd584c31a46414a1414eb774a38d2ec94
# Parent  f797816932d7269788b6963e1db473c6de16f8d3
new policy to simplify the use of numerals:
#0 -> 0
#1 -> 1
#2 + n -> Suc (Suc n) similarly for n + #2

diff -r f797816932d7 -r 9d6514fcd584 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Tue May 16 14:04:29 2000 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Tue May 16 14:07:06 2000 +0200
@@ -450,7 +450,10 @@
 by (simp_tac (numeral_ss addsplits [nat_diff_split]) 1);
 qed "diff_Suc_eq_diff_pred";
 
-Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
+(*Obsolete because of natdiff_cancel_numerals
+    Addsimps [inst "m" "number_of ?v" diff_Suc_eq_diff_pred];
+  It LOOPS if #1 is being replaced by 1.
+*)
 
 
 (** Evens and Odds, for Mutilated Chess Board **)
@@ -475,3 +478,19 @@
 qed "mod2_gr_0";
 Addsimps [mod2_gr_0, rename_numerals thy mod2_gr_0];
 
+(** Removal of small numerals: #0, #1 and (in additive positions) #2 **)
+
+Goal "#2 + n = Suc (Suc n)";
+by (Simp_tac 1);
+qed "add_2_eq_Suc";
+
+Goal "n + #2 = Suc (Suc n)";
+by (Simp_tac 1);
+qed "add_2_eq_Suc'";
+
+Addsimps [numeral_0_eq_0, numeral_1_eq_1, add_2_eq_Suc, add_2_eq_Suc'];
+
+(*Can be used to eliminate long strings of Sucs, but not by default*)
+Goal "Suc (Suc (Suc n)) = #3 + n";
+by (Simp_tac 1);
+qed "Suc3_eq_add_3";