1.1 --- a/src/HOL/SMT2.thy	Thu Mar 13 13:18:14 2014 +0100
     1.2 +++ b/src/HOL/SMT2.thy	Thu Mar 13 13:18:14 2014 +0100
     1.3 @@ -93,6 +93,21 @@
     1.4  definition z3mod :: "int \<Rightarrow> int \<Rightarrow> int" where
     1.5    "z3mod k l = (if 0 \<le> l then k mod l else k mod (-l))"
     1.6  
     1.7 +lemma div_as_z3div:
     1.8 +  "\<forall>k l. k div l = (
     1.9 +    if k = 0 \<or> l = 0 then 0
    1.10 +    else if (0 < k & 0 < l) \<or> (k < 0 & 0 < l) then z3div k l
    1.11 +    else z3div (-k) (-l))"
    1.12 +  by (simp add: z3div_def)
    1.13 +
    1.14 +lemma mod_as_z3mod:
    1.15 +  "\<forall>k l. k mod l = (
    1.16 +    if l = 0 then k
    1.17 +    else if k = 0 then 0
    1.18 +    else if (0 < k & 0 < l) \<or> (k < 0 & 0 < l) then z3mod k l
    1.19 +    else - z3mod (-k) (-l))"
    1.20 +  by (simp add: z3mod_def)
    1.21 +
    1.22  
    1.23  subsection {* Setup *}
    1.24  

     2.1 --- a/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 13:18:14 2014 +0100
     2.2 +++ b/src/HOL/Tools/SMT2/z3_new_interface.ML	Thu Mar 13 13:18:14 2014 +0100
     2.3 @@ -42,27 +42,12 @@
     2.4      | is_div_mod @{const mod (int)} = true
     2.5      | is_div_mod _ = false
     2.6  
     2.7 -  val div_as_z3div = @{lemma
     2.8 -    "ALL k l. k div l = (
     2.9 -      if k = 0 | l = 0 then 0
    2.10 -      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3div k l
    2.11 -      else z3div (-k) (-l))"
    2.12 -    by (simp add: SMT2.z3div_def)}
    2.13 -
    2.14 -  val mod_as_z3mod = @{lemma
    2.15 -    "ALL k l. k mod l = (
    2.16 -      if l = 0 then k
    2.17 -      else if k = 0 then 0
    2.18 -      else if (0 < k & 0 < l) | (k < 0 & 0 < l) then z3mod k l
    2.19 -      else - z3mod (-k) (-l))"
    2.20 -    by (simp add: z3mod_def)}
    2.21 -
    2.22    val have_int_div_mod =
    2.23      exists (Term.exists_subterm is_div_mod o Thm.prop_of)
    2.24  
    2.25    fun add_div_mod _ (thms, extra_thms) =
    2.26      if have_int_div_mod thms orelse have_int_div_mod extra_thms then
    2.27 -      (thms, div_as_z3div :: mod_as_z3mod :: extra_thms)
    2.28 +      (thms, @{thms div_as_z3div mod_as_z3mod} @ extra_thms)
    2.29      else (thms, extra_thms)
    2.30  
    2.31    val setup_builtins =