# HG changeset patch
# User blanchet
# Date 1394713094 -3600
# Node ID 6d9fe46429e6202c372754a6dd996c411a757e7d
# Parent  0dc5f68a7802ec39dc3c9d5a0af56da38ed1273c
tuning

diff -r 0dc5f68a7802 -r 6d9fe46429e6 src/HOL/SMT2.thy
--- a/src/HOL/SMT2.thy	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/SMT2.thy	Thu Mar 13 13:18:14 2014 +0100
@@ -93,6 +93,21 @@
 definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
   "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
 
+lemma div_as_z3div:
+  "\<forall>k l. k div l = (
+    if k = 0 \<or> l = 0 then 0
+    else if (0 < k & 0 < l) \<or> (k < 0 & 0 < l) then z3div k l
+    else z3div (-k) (-l))"
+  by (simp add: z3div_def)
+
+lemma mod_as_z3mod:
+  "\<forall>k l. k mod l = (
+    if l = 0 then k
+    else if k = 0 then 0
+    else if (0 < k & 0 < l) \<or> (k < 0 & 0 < l) then z3mod k l
+    else - z3mod (-k) (-l))"
+  by (simp add: z3mod_def)
+
 
 subsection {* Setup *}
 
diff -r 0dc5f68a7802 -r 6d9fe46429e6 src/HOL/Tools/SMT2/z3_new_interface.ML
--- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 13:18:14 2014 +0100
+++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 13:18:14 2014 +0100
@@ -42,27 +42,12 @@
     | is_div_mod @{const mod (int)} = true
     | is_div_mod _ = false
 
-  val div_as_z3div = @{lemma
-    "ALL k l. k div l = (
-      if k = 0 | l = 0 then 0
-      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l
-      else z3div (-k) (-l))"
-    by (simp add: SMT2.z3div_def)}
-
-  val mod_as_z3mod = @{lemma
-    "ALL k l. k mod l = (
-      if l = 0 then k
-      else if k = 0 then 0
-      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l
-      else - z3mod (-k) (-l))"
-    by (simp add: z3mod_def)}
-
   val have_int_div_mod =
     exists (Term.exists_subterm is_div_mod o Thm.prop_of)
 
   fun add_div_mod _ (thms, extra_thms) =
     if have_int_div_mod thms orelse have_int_div_mod extra_thms then
-      (thms, div_as_z3div :: mod_as_z3mod :: extra_thms)
+      (thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms)
     else (thms, extra_thms)
 
   val setup_builtins =