src/HOL/Tools/SMT/smt_real.ML
changeset 47965 8ba6438557bc
parent 46497 89ccf66aa73d
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed May 23 15:40:10 2012 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed May 23 16:03:38 2012 +0200
     1.3 @@ -67,8 +67,12 @@
     1.4      if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
     1.5      else NONE
     1.6  
     1.7 +  fun mk_nary _ cu [] = cu
     1.8 +    | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts)
     1.9 +
    1.10    val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
    1.11 -  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
    1.12 +  val add = Thm.cterm_of @{theory} @{const plus (real)}
    1.13 +  val real0 = Numeral.mk_cnumber @{ctyp real} 0
    1.14    val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
    1.15    val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    1.16    val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)})
    1.17 @@ -76,8 +80,8 @@
    1.18    val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)})
    1.19  
    1.20    fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct)
    1.21 -    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) [ct, cu] =
    1.22 -        SOME (mk_add ct cu)
    1.23 +    | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts =
    1.24 +        SOME (mk_nary add real0 cts)
    1.25      | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] =
    1.26          SOME (mk_sub ct cu)
    1.27      | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] =