rewrite integer numeral div/mod simprocs to not return conditional rewrites; add regression tests

--- a/src/HOL/Divides.thy	Wed Nov 16 13:58:31 2011 +0100
+++ b/src/HOL/Divides.thy	Wed Nov 16 15:20:27 2011 +0100
@@ -1663,13 +1663,22 @@
 
 text {*Simplify expresions in which div and mod combine numerical constants*}
 
-lemma divmod_int_relI:
-  "\<lbrakk>a == b * q + r; if 0 < b then 0 \<le> r \<and> r < b else b < r \<and> r \<le> 0\<rbrakk>
-    \<Longrightarrow> divmod_int_rel a b (q, r)"
-  unfolding divmod_int_rel_def by simp
-
-lemmas divmod_int_rel_div_eq = divmod_int_relI [THEN divmod_int_rel_div, THEN eq_reflection]
-lemmas divmod_int_rel_mod_eq = divmod_int_relI [THEN divmod_int_rel_mod, THEN eq_reflection]
+lemma int_div_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a div b = q"
+  by (rule divmod_int_rel_div [of a b q r],
+    simp add: divmod_int_rel_def, simp)
+
+lemma int_div_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a div b = q"
+  by (rule divmod_int_rel_div [of a b q r],
+    simp add: divmod_int_rel_def, simp)
+
+lemma int_mod_pos_eq: "\<lbrakk>(a::int) = b * q + r; 0 \<le> r; r < b\<rbrakk> \<Longrightarrow> a mod b = r"
+  by (rule divmod_int_rel_mod [of a b q r],
+    simp add: divmod_int_rel_def, simp)
+
+lemma int_mod_neg_eq: "\<lbrakk>(a::int) = b * q + r; r \<le> 0; b < r\<rbrakk> \<Longrightarrow> a mod b = r"
+  by (rule divmod_int_rel_mod [of a b q r],
+    simp add: divmod_int_rel_def, simp)
+
 lemmas arithmetic_simps =
   arith_simps
   add_special
@@ -1683,12 +1692,16 @@
 (* simprocs adapted from HOL/ex/Binary.thy *)
 ML {*
 local
-  val mk_number = HOLogic.mk_number HOLogic.intT;
-  fun mk_cert u k l = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"} $
-    (@{term "times :: int \<Rightarrow> int \<Rightarrow> int"} $ u $ mk_number k) $
-      mk_number l;
-  fun prove ctxt prop = Goal.prove ctxt [] [] prop
-    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps @{thms arithmetic_simps}))));
+  val mk_number = HOLogic.mk_number HOLogic.intT
+  val plus = @{term "plus :: int \<Rightarrow> int \<Rightarrow> int"}
+  val times = @{term "times :: int \<Rightarrow> int \<Rightarrow> int"}
+  val zero = @{term "0 :: int"}
+  val less = @{term "op < :: int \<Rightarrow> int \<Rightarrow> bool"}
+  val le = @{term "op \<le> :: int \<Rightarrow> int \<Rightarrow> bool"}
+  val simps = @{thms arith_simps} @ @{thms rel_simps} @
+    map (fn th => th RS sym) [@{thm numeral_0_eq_0}, @{thm numeral_1_eq_1}]
+  fun prove ctxt goal = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop goal)
+    (K (ALLGOALS (full_simp_tac (HOL_basic_ss addsimps simps))));
   fun binary_proc proc ss ct =
     (case Thm.term_of ct of
       _ $ t $ u =>
@@ -1697,18 +1710,23 @@
       | NONE => NONE)
     | _ => NONE);
 in
-  fun divmod_proc rule = binary_proc (fn ctxt => fn ((m, t), (n, u)) =>
-    if n = 0 then NONE
-    else let val (k, l) = Integer.div_mod m n;
-    in SOME (rule OF [prove ctxt (Logic.mk_equals (t, mk_cert u k l))]) end);
+  fun divmod_proc posrule negrule =
+    binary_proc (fn ctxt => fn ((a, t), (b, u)) =>
+      if b = 0 then NONE else let
+        val (q, r) = pairself mk_number (Integer.div_mod a b)
+        val goal1 = HOLogic.mk_eq (t, plus $ (times $ u $ q) $ r)
+        val (goal2, goal3, rule) = if b > 0
+          then (le $ zero $ r, less $ r $ u, posrule RS eq_reflection)
+          else (le $ r $ zero, less $ u $ r, negrule RS eq_reflection)
+      in SOME (rule OF map (prove ctxt) [goal1, goal2, goal3]) end)
 end
 *}
 
 simproc_setup binary_int_div ("number_of m div number_of n :: int") =
-  {* K (divmod_proc (@{thm divmod_int_rel_div_eq})) *}
+  {* K (divmod_proc @{thm int_div_pos_eq} @{thm int_div_neg_eq}) *}
 
 simproc_setup binary_int_mod ("number_of m mod number_of n :: int") =
-  {* K (divmod_proc (@{thm divmod_int_rel_mod_eq})) *}
+  {* K (divmod_proc @{thm int_mod_pos_eq} @{thm int_mod_neg_eq}) *}
 
 lemmas posDivAlg_eqn_number_of [simp] =
     posDivAlg_eqn [of "number_of v" "number_of w", standard]

--- a/src/HOL/ex/Simproc_Tests.thy	Wed Nov 16 13:58:31 2011 +0100
+++ b/src/HOL/ex/Simproc_Tests.thy	Wed Nov 16 15:20:27 2011 +0100
@@ -420,9 +420,11 @@
     assume "4*k = u" have "k + 3*k = u"
       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
   next
+    (* FIXME "Suc (i + 3) \<equiv> i + 4" *)
     assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u"
       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
   next
+    (* FIXME "Suc (i + j + 3 + k) \<equiv> i + j + 4 + k" *)
     assume "4 * Suc 0 + (i + (j + k)) = u" have "Suc (i + j + 3 + k) = u"
       by (tactic {* test [@{simproc nat_combine_numerals}] *}) fact
   next
@@ -712,4 +714,43 @@
   }
 end
 
+subsection {* Integer numeral div/mod simprocs *}
+
+notepad begin
+  have "(10::int) div 3 = 3"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "(10::int) mod 3 = 1"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "(10::int) div -3 = -4"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "(10::int) mod -3 = -2"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "(-10::int) div 3 = -4"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "(-10::int) mod 3 = 2"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "(-10::int) div -3 = 3"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "(-10::int) mod -3 = -1"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "(8452::int) mod 3 = 1"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "(59485::int) div 434 = 137"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "(1000006::int) mod 10 = 6"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "10000000 div 2 = (5000000::int)"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "10000001 mod 2 = (1::int)"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "10000055 div 32 = (312501::int)"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "10000055 mod 32 = (23::int)"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
+  have "100094 div 144 = (695::int)"
+    by (tactic {* test [@{simproc binary_int_div}] *})
+  have "100094 mod 144 = (14::int)"
+    by (tactic {* test [@{simproc binary_int_mod}] *})
 end
+
+end