# HG changeset patch
# User chaieb
# Date 1134487452 -3600
# Node ID af72cbfa00a572dcbbb41edd3a46ec5070789367
# Parent  fdefc3cd45c5952a8525d313e49fc0c48a33885c
deals with Suc in mod expressions

diff -r fdefc3cd45c5 -r af72cbfa00a5 src/HOL/Integ/presburger.ML
--- a/src/HOL/Integ/presburger.ML	Tue Dec 13 15:46:41 2005 +0100
+++ b/src/HOL/Integ/presburger.ML	Tue Dec 13 16:24:12 2005 +0100
@@ -61,7 +61,7 @@
 			   thm "one_eq_Numeral1_nring"] 
   (thm "zpower_number_of_odd"))]
 
-val arith = binarith @ intarith @ intarithrel @ natarith 
+val comp_arith = binarith @ intarith @ intarithrel @ natarith 
 	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
 
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
@@ -298,12 +298,13 @@
 				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
 				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
 				  zdiv_zero,zmod_zero,div_0,mod_0,
-				  zdiv_1,zmod_1,div_1,mod_1]
+				  zdiv_1,zmod_1,div_1,mod_1,
+				  Suc_plus1]
 			addsimps add_ac
 			addsimprocs [cancel_div_mod_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
-      addsimps arith
+      addsimps comp_arith
       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss
diff -r fdefc3cd45c5 -r af72cbfa00a5 src/HOL/Tools/Presburger/presburger.ML
--- a/src/HOL/Tools/Presburger/presburger.ML	Tue Dec 13 15:46:41 2005 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML	Tue Dec 13 16:24:12 2005 +0100
@@ -61,7 +61,7 @@
 			   thm "one_eq_Numeral1_nring"] 
   (thm "zpower_number_of_odd"))]
 
-val arith = binarith @ intarith @ intarithrel @ natarith 
+val comp_arith = binarith @ intarith @ intarithrel @ natarith 
 	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
 
 fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
@@ -298,12 +298,13 @@
 				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
 				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
 				  zdiv_zero,zmod_zero,div_0,mod_0,
-				  zdiv_1,zmod_1,div_1,mod_1]
+				  zdiv_1,zmod_1,div_1,mod_1,
+				  Suc_plus1]
 			addsimps add_ac
 			addsimprocs [cancel_div_mod_proc]
     val simpset0 = HOL_basic_ss
       addsimps [mod_div_equality', Suc_plus1]
-      addsimps arith
+      addsimps comp_arith
       addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
     (* Simp rules for changing (n::int) to int n *)
     val simpset1 = HOL_basic_ss