65 |
65 |
66 fun z3_mk_builtin_num _ i T = |
66 fun z3_mk_builtin_num _ i T = |
67 if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) |
67 if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i) |
68 else NONE |
68 else NONE |
69 |
69 |
|
70 fun mk_nary _ cu [] = cu |
|
71 | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
|
72 |
70 val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) |
73 val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) |
71 val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)}) |
74 val add = Thm.cterm_of @{theory} @{const plus (real)} |
|
75 val real0 = Numeral.mk_cnumber @{ctyp real} 0 |
72 val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
76 val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
73 val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
77 val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
74 val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
78 val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
75 val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |
79 val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |
76 val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) |
80 val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) |
77 |
81 |
78 fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
82 fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
79 | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) [ct, cu] = |
83 | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = |
80 SOME (mk_add ct cu) |
84 SOME (mk_nary add real0 cts) |
81 | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = |
85 | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = |
82 SOME (mk_sub ct cu) |
86 SOME (mk_sub ct cu) |
83 | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = |
87 | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = |
84 SOME (mk_mul ct cu) |
88 SOME (mk_mul ct cu) |
85 | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = |
89 | z3_mk_builtin_fun (Z3_Interface.Sym ("/", _)) [ct, cu] = |