presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
authorchaieb
Fri Nov 18 07:13:58 2005 +0100 (2005-11-18)
changeset 1820246af82efd311
parent 18201 6c63f0eb16d7
child 18203 9bd26bda96ef
presburger method updated to deal better with mod and div, tweo lemmas added to Divides.thy
src/HOL/Divides.thy
src/HOL/Integ/Presburger.thy
src/HOL/Integ/presburger.ML
src/HOL/Presburger.thy
src/HOL/Tools/Presburger/presburger.ML
     1.1 --- a/src/HOL/Divides.thy	Fri Nov 18 07:10:37 2005 +0100
     1.2 +++ b/src/HOL/Divides.thy	Fri Nov 18 07:13:58 2005 +0100
     1.3 @@ -858,6 +858,18 @@
     1.4  qed
     1.5  
     1.6  
     1.7 +lemma mod_add_left_eq: "((a::nat) + b) mod c = (a mod c + b) mod c"
     1.8 +  apply (rule trans [symmetric])
     1.9 +  apply (rule mod_add1_eq, simp)
    1.10 +  apply (rule mod_add1_eq [symmetric])
    1.11 +  done
    1.12 +
    1.13 +lemma mod_add_right_eq: "(a+b) mod (c::nat) = (a + (b mod c)) mod c"
    1.14 +apply (rule trans [symmetric])
    1.15 +apply (rule mod_add1_eq, simp)
    1.16 +apply (rule mod_add1_eq [symmetric])
    1.17 +done
    1.18 +
    1.19  ML
    1.20  {*
    1.21  val div_def = thm "div_def"
    1.22 @@ -907,6 +919,8 @@
    1.23  val mod_mult_distrib_mod = thm "mod_mult_distrib_mod";
    1.24  val div_add1_eq = thm "div_add1_eq";
    1.25  val mod_add1_eq = thm "mod_add1_eq";
    1.26 +val mod_add_left_eq = thm "mod_add_left_eq";
    1.27 + val mod_add_right_eq = thm "mod_add_right_eq";
    1.28  val mod_lemma = thm "mod_lemma";
    1.29  val div_mult2_eq = thm "div_mult2_eq";
    1.30  val mod_mult2_eq = thm "mod_mult2_eq";
     2.1 --- a/src/HOL/Integ/Presburger.thy	Fri Nov 18 07:10:37 2005 +0100
     2.2 +++ b/src/HOL/Integ/Presburger.thy	Fri Nov 18 07:13:58 2005 +0100
     2.3 @@ -982,6 +982,99 @@
     2.4  theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
     2.5    by (simp cong: conj_cong)
     2.6  
     2.7 +    (* Theorems used in presburger.ML for the computation simpset*)
     2.8 +    (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
     2.9 +
    2.10 +lemma lift_bool: "x \<Longrightarrow> x=True"
    2.11 +  by simp
    2.12 +
    2.13 +lemma nlift_bool: "~x \<Longrightarrow> x=False"
    2.14 +  by simp
    2.15 +
    2.16 +lemma not_false_eq_true: "(~ False) = True" by simp
    2.17 +
    2.18 +lemma not_true_eq_false: "(~ True) = False" by simp
    2.19 +
    2.20 +
    2.21 +lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
    2.22 +  by simp
    2.23 +lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
    2.24 +  by (simp only: iszero_number_of_Pls)
    2.25 +
    2.26 +lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
    2.27 +  by simp
    2.28 +
    2.29 +lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
    2.30 +  by simp
    2.31 +
    2.32 +lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
    2.33 +  by simp
    2.34 +
    2.35 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
    2.36 +  by simp
    2.37 +
    2.38 +lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
    2.39 +  by simp
    2.40 +
    2.41 +lemma int_neg_number_of_Min: "neg (-1::int)"
    2.42 +  by simp
    2.43 +
    2.44 +lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
    2.45 +  by simp
    2.46 +
    2.47 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
    2.48 +  by simp
    2.49 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
    2.50 +  by simp
    2.51 +
    2.52 +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
    2.53 +  by simp
    2.54 +
    2.55 +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
    2.56 +  by simp
    2.57 +
    2.58 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
    2.59 +  by simp
    2.60 +lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
    2.61 +  by simp
    2.62 +
    2.63 +lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
    2.64 +  by simp
    2.65 +
    2.66 +lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
    2.67 +  by simp
    2.68 +
    2.69 +lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
    2.70 +  by simp
    2.71 +
    2.72 +lemma int_pow_0: "(a::int)^(Numeral0) = 1"
    2.73 +  by simp
    2.74 +
    2.75 +lemma int_pow_1: "(a::int)^(Numeral1) = a"
    2.76 +  by simp
    2.77 +
    2.78 +lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
    2.79 +  by simp
    2.80 +
    2.81 +lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
    2.82 +  by simp
    2.83 +
    2.84 +lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
    2.85 +  by simp
    2.86 +
    2.87 +lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
    2.88 +  by simp
    2.89 +
    2.90 +lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
    2.91 +  by simp
    2.92 +
    2.93 +lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
    2.94 +proof -
    2.95 +  have 1:"((-1)::nat) = 0"
    2.96 +    by simp
    2.97 +  show ?thesis by (simp add: 1)
    2.98 +qed
    2.99 +
   2.100  use "cooper_dec.ML"
   2.101  use "reflected_presburger.ML" 
   2.102  use "reflected_cooper.ML"
     3.1 --- a/src/HOL/Integ/presburger.ML	Fri Nov 18 07:10:37 2005 +0100
     3.2 +++ b/src/HOL/Integ/presburger.ML	Fri Nov 18 07:13:58 2005 +0100
     3.3 @@ -31,6 +31,38 @@
     3.4  
     3.5  
     3.6  val presburger_ss = simpset_of (theory "Presburger");
     3.7 +val binarith = map thm
     3.8 +  ["Pls_0_eq", "Min_1_eq",
     3.9 + "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    3.10 +  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    3.11 +  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
    3.12 +  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
    3.13 +  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
    3.14 +  "bin_add_Pls_right", "bin_add_Min_right"];
    3.15 + val intarithrel = 
    3.16 +     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
    3.17 +		"int_le_number_of_eq","int_iszero_number_of_0",
    3.18 +		"int_less_number_of_eq_neg"]) @
    3.19 +     (map (fn s => thm s RS thm "lift_bool") 
    3.20 +	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    3.21 +	   "int_neg_number_of_Min"])@
    3.22 +     (map (fn s => thm s RS thm "nlift_bool") 
    3.23 +	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    3.24 +     
    3.25 +val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    3.26 +			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    3.27 +val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    3.28 +			"mult_nat_number_of", "eq_nat_number_of",
    3.29 +			"less_nat_number_of"]
    3.30 +val powerarith = 
    3.31 +    (map thm ["nat_number_of", "zpower_number_of_even", 
    3.32 +	      "zpower_Pls", "zpower_Min"]) @ 
    3.33 +    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
    3.34 +			   thm "one_eq_Numeral1_nring"] 
    3.35 +  (thm "zpower_number_of_odd"))]
    3.36 +
    3.37 +val arith = binarith @ intarith @ intarithrel @ natarith 
    3.38 +	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    3.39  
    3.40  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    3.41    let val (xn1,p1) = variant_abs (xn,xT,p)
    3.42 @@ -59,6 +91,17 @@
    3.43  val Suc_plus1 = thm "Suc_plus1";
    3.44  val imp_le_cong = thm "imp_le_cong";
    3.45  val conj_le_cong = thm "conj_le_cong";
    3.46 +val nat_mod_add_eq = mod_add1_eq RS sym;
    3.47 +val nat_mod_add_left_eq = mod_add_left_eq RS sym;
    3.48 +val nat_mod_add_right_eq = mod_add_right_eq RS sym;
    3.49 +val int_mod_add_eq = zmod_zadd1_eq RS sym;
    3.50 +val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
    3.51 +val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
    3.52 +val nat_div_add_eq = div_add1_eq RS sym;
    3.53 +val int_div_add_eq = zdiv_zadd1_eq RS sym;
    3.54 +val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
    3.55 +val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
    3.56 +
    3.57  
    3.58  (* extract all the constants in a term*)
    3.59  fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
    3.60 @@ -246,8 +289,21 @@
    3.61      (* Transform the term*)
    3.62      val (t,np,nh) = prepare_for_presburger sg q g'
    3.63      (* Some simpsets for dealing with mod div abs and nat*)
    3.64 +    val mod_div_simpset = HOL_basic_ss 
    3.65 +			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
    3.66 +				  nat_mod_add_right_eq, int_mod_add_eq, 
    3.67 +				  int_mod_add_right_eq, int_mod_add_left_eq,
    3.68 +				  nat_div_add_eq, int_div_add_eq,
    3.69 +				  mod_self, zmod_self,
    3.70 +				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
    3.71 +				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
    3.72 +				  zdiv_zero,zmod_zero,div_0,mod_0,
    3.73 +				  zdiv_1,zmod_1,div_1,mod_1]
    3.74 +			addsimps add_ac
    3.75 +			addsimprocs [cancel_div_mod_proc]
    3.76      val simpset0 = HOL_basic_ss
    3.77        addsimps [mod_div_equality', Suc_plus1]
    3.78 +      addsimps arith
    3.79        addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
    3.80      (* Simp rules for changing (n::int) to int n *)
    3.81      val simpset1 = HOL_basic_ss
    3.82 @@ -264,7 +320,7 @@
    3.83      val ct = cterm_of sg (HOLogic.mk_Trueprop t)
    3.84      (* Theorem for the nat --> int transformation *)
    3.85      val pre_thm = Seq.hd (EVERY
    3.86 -      [simp_tac simpset0 1,
    3.87 +      [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
    3.88         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    3.89         TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
    3.90        (trivial ct))
     4.1 --- a/src/HOL/Presburger.thy	Fri Nov 18 07:10:37 2005 +0100
     4.2 +++ b/src/HOL/Presburger.thy	Fri Nov 18 07:13:58 2005 +0100
     4.3 @@ -982,6 +982,99 @@
     4.4  theorem conj_le_cong: "(0 <= x \<Longrightarrow> P = P') \<Longrightarrow> (0 <= (x::int) \<and> P) = (0 <= x \<and> P')"
     4.5    by (simp cong: conj_cong)
     4.6  
     4.7 +    (* Theorems used in presburger.ML for the computation simpset*)
     4.8 +    (* FIXME: They are present in Float.thy, so may be Float.thy should be lightened.*)
     4.9 +
    4.10 +lemma lift_bool: "x \<Longrightarrow> x=True"
    4.11 +  by simp
    4.12 +
    4.13 +lemma nlift_bool: "~x \<Longrightarrow> x=False"
    4.14 +  by simp
    4.15 +
    4.16 +lemma not_false_eq_true: "(~ False) = True" by simp
    4.17 +
    4.18 +lemma not_true_eq_false: "(~ True) = False" by simp
    4.19 +
    4.20 +
    4.21 +lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
    4.22 +  by simp
    4.23 +lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
    4.24 +  by (simp only: iszero_number_of_Pls)
    4.25 +
    4.26 +lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
    4.27 +  by simp
    4.28 +
    4.29 +lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
    4.30 +  by simp
    4.31 +
    4.32 +lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
    4.33 +  by simp
    4.34 +
    4.35 +lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
    4.36 +  by simp
    4.37 +
    4.38 +lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
    4.39 +  by simp
    4.40 +
    4.41 +lemma int_neg_number_of_Min: "neg (-1::int)"
    4.42 +  by simp
    4.43 +
    4.44 +lemma int_neg_number_of_BIT: "neg ((number_of (w BIT x))::int) = neg ((number_of w)::int)"
    4.45 +  by simp
    4.46 +
    4.47 +lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
    4.48 +  by simp
    4.49 +lemma int_number_of_add_sym: "((number_of v)::int) + number_of w = number_of (bin_add v w)"
    4.50 +  by simp
    4.51 +
    4.52 +lemma int_number_of_diff_sym: "((number_of v)::int) - number_of w = number_of (bin_add v (bin_minus w))"
    4.53 +  by simp
    4.54 +
    4.55 +lemma int_number_of_mult_sym: "((number_of v)::int) * number_of w = number_of (bin_mult v w)"
    4.56 +  by simp
    4.57 +
    4.58 +lemma int_number_of_minus_sym: "- ((number_of v)::int) = number_of (bin_minus v)"
    4.59 +  by simp
    4.60 +lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
    4.61 +  by simp
    4.62 +
    4.63 +lemma add_right_zero: "a + 0 = (a::'a::comm_monoid_add)"
    4.64 +  by simp
    4.65 +
    4.66 +lemma mult_left_one: "1 * a = (a::'a::semiring_1)"
    4.67 +  by simp
    4.68 +
    4.69 +lemma mult_right_one: "a * 1 = (a::'a::semiring_1)"
    4.70 +  by simp
    4.71 +
    4.72 +lemma int_pow_0: "(a::int)^(Numeral0) = 1"
    4.73 +  by simp
    4.74 +
    4.75 +lemma int_pow_1: "(a::int)^(Numeral1) = a"
    4.76 +  by simp
    4.77 +
    4.78 +lemma zero_eq_Numeral0_nring: "(0::'a::number_ring) = Numeral0"
    4.79 +  by simp
    4.80 +
    4.81 +lemma one_eq_Numeral1_nring: "(1::'a::number_ring) = Numeral1"
    4.82 +  by simp
    4.83 +
    4.84 +lemma zero_eq_Numeral0_nat: "(0::nat) = Numeral0"
    4.85 +  by simp
    4.86 +
    4.87 +lemma one_eq_Numeral1_nat: "(1::nat) = Numeral1"
    4.88 +  by simp
    4.89 +
    4.90 +lemma zpower_Pls: "(z::int)^Numeral0 = Numeral1"
    4.91 +  by simp
    4.92 +
    4.93 +lemma zpower_Min: "(z::int)^((-1)::nat) = Numeral1"
    4.94 +proof -
    4.95 +  have 1:"((-1)::nat) = 0"
    4.96 +    by simp
    4.97 +  show ?thesis by (simp add: 1)
    4.98 +qed
    4.99 +
   4.100  use "cooper_dec.ML"
   4.101  use "reflected_presburger.ML" 
   4.102  use "reflected_cooper.ML"
     5.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Fri Nov 18 07:10:37 2005 +0100
     5.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Nov 18 07:13:58 2005 +0100
     5.3 @@ -31,6 +31,38 @@
     5.4  
     5.5  
     5.6  val presburger_ss = simpset_of (theory "Presburger");
     5.7 +val binarith = map thm
     5.8 +  ["Pls_0_eq", "Min_1_eq",
     5.9 + "bin_pred_Pls","bin_pred_Min","bin_pred_1","bin_pred_0",
    5.10 +  "bin_succ_Pls", "bin_succ_Min", "bin_succ_1", "bin_succ_0",
    5.11 +  "bin_add_Pls", "bin_add_Min", "bin_add_BIT_0", "bin_add_BIT_10",
    5.12 +  "bin_add_BIT_11", "bin_minus_Pls", "bin_minus_Min", "bin_minus_1", 
    5.13 +  "bin_minus_0", "bin_mult_Pls", "bin_mult_Min", "bin_mult_1", "bin_mult_0", 
    5.14 +  "bin_add_Pls_right", "bin_add_Min_right"];
    5.15 + val intarithrel = 
    5.16 +     (map thm ["int_eq_number_of_eq","int_neg_number_of_BIT", 
    5.17 +		"int_le_number_of_eq","int_iszero_number_of_0",
    5.18 +		"int_less_number_of_eq_neg"]) @
    5.19 +     (map (fn s => thm s RS thm "lift_bool") 
    5.20 +	  ["int_iszero_number_of_Pls","int_iszero_number_of_1",
    5.21 +	   "int_neg_number_of_Min"])@
    5.22 +     (map (fn s => thm s RS thm "nlift_bool") 
    5.23 +	  ["int_nonzero_number_of_Min","int_not_neg_number_of_Pls"]);
    5.24 +     
    5.25 +val intarith = map thm ["int_number_of_add_sym", "int_number_of_minus_sym",
    5.26 +			"int_number_of_diff_sym", "int_number_of_mult_sym"];
    5.27 +val natarith = map thm ["add_nat_number_of", "diff_nat_number_of",
    5.28 +			"mult_nat_number_of", "eq_nat_number_of",
    5.29 +			"less_nat_number_of"]
    5.30 +val powerarith = 
    5.31 +    (map thm ["nat_number_of", "zpower_number_of_even", 
    5.32 +	      "zpower_Pls", "zpower_Min"]) @ 
    5.33 +    [(Tactic.simplify true [thm "zero_eq_Numeral0_nring", 
    5.34 +			   thm "one_eq_Numeral1_nring"] 
    5.35 +  (thm "zpower_number_of_odd"))]
    5.36 +
    5.37 +val arith = binarith @ intarith @ intarithrel @ natarith 
    5.38 +	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
    5.39  
    5.40  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
    5.41    let val (xn1,p1) = variant_abs (xn,xT,p)
    5.42 @@ -59,6 +91,17 @@
    5.43  val Suc_plus1 = thm "Suc_plus1";
    5.44  val imp_le_cong = thm "imp_le_cong";
    5.45  val conj_le_cong = thm "conj_le_cong";
    5.46 +val nat_mod_add_eq = mod_add1_eq RS sym;
    5.47 +val nat_mod_add_left_eq = mod_add_left_eq RS sym;
    5.48 +val nat_mod_add_right_eq = mod_add_right_eq RS sym;
    5.49 +val int_mod_add_eq = zmod_zadd1_eq RS sym;
    5.50 +val int_mod_add_left_eq = zmod_zadd_left_eq RS sym;
    5.51 +val int_mod_add_right_eq = zmod_zadd_right_eq RS sym;
    5.52 +val nat_div_add_eq = div_add1_eq RS sym;
    5.53 +val int_div_add_eq = zdiv_zadd1_eq RS sym;
    5.54 +val ZDIVISION_BY_ZERO_MOD = DIVISION_BY_ZERO RS conjunct2;
    5.55 +val ZDIVISION_BY_ZERO_DIV = DIVISION_BY_ZERO RS conjunct1;
    5.56 +
    5.57  
    5.58  (* extract all the constants in a term*)
    5.59  fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
    5.60 @@ -246,8 +289,21 @@
    5.61      (* Transform the term*)
    5.62      val (t,np,nh) = prepare_for_presburger sg q g'
    5.63      (* Some simpsets for dealing with mod div abs and nat*)
    5.64 +    val mod_div_simpset = HOL_basic_ss 
    5.65 +			addsimps [refl,nat_mod_add_eq, nat_mod_add_left_eq, 
    5.66 +				  nat_mod_add_right_eq, int_mod_add_eq, 
    5.67 +				  int_mod_add_right_eq, int_mod_add_left_eq,
    5.68 +				  nat_div_add_eq, int_div_add_eq,
    5.69 +				  mod_self, zmod_self,
    5.70 +				  DIVISION_BY_ZERO_MOD,DIVISION_BY_ZERO_DIV,
    5.71 +				  ZDIVISION_BY_ZERO_MOD,ZDIVISION_BY_ZERO_DIV,
    5.72 +				  zdiv_zero,zmod_zero,div_0,mod_0,
    5.73 +				  zdiv_1,zmod_1,div_1,mod_1]
    5.74 +			addsimps add_ac
    5.75 +			addsimprocs [cancel_div_mod_proc]
    5.76      val simpset0 = HOL_basic_ss
    5.77        addsimps [mod_div_equality', Suc_plus1]
    5.78 +      addsimps arith
    5.79        addsplits [split_zdiv, split_zmod, split_div', split_min, split_max]
    5.80      (* Simp rules for changing (n::int) to int n *)
    5.81      val simpset1 = HOL_basic_ss
    5.82 @@ -264,7 +320,7 @@
    5.83      val ct = cterm_of sg (HOLogic.mk_Trueprop t)
    5.84      (* Theorem for the nat --> int transformation *)
    5.85      val pre_thm = Seq.hd (EVERY
    5.86 -      [simp_tac simpset0 1,
    5.87 +      [simp_tac mod_div_simpset 1, simp_tac simpset0 1,
    5.88         TRY (simp_tac simpset1 1), TRY (simp_tac simpset2 1),
    5.89         TRY (simp_tac simpset3 1), TRY (simp_tac presburger_ss 1)]
    5.90        (trivial ct))