62 else NONE |
62 else NONE |
63 |
63 |
64 fun mk_nary _ cu [] = cu |
64 fun mk_nary _ cu [] = cu |
65 | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
65 | mk_nary ct _ cts = uncurry (fold_rev (Thm.mk_binop ct)) (split_last cts) |
66 |
66 |
67 val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)}) |
67 val mk_uminus = Thm.apply (Thm.global_cterm_of @{theory} @{const uminus (real)}) |
68 val add = Thm.cterm_of @{theory} @{const plus (real)} |
68 val add = Thm.global_cterm_of @{theory} @{const plus (real)} |
69 val real0 = Numeral.mk_cnumber @{ctyp real} 0 |
69 val real0 = Numeral.mk_cnumber @{ctyp real} 0 |
70 val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)}) |
70 val mk_sub = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const minus (real)}) |
71 val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)}) |
71 val mk_mul = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const times (real)}) |
72 val mk_div = Thm.mk_binop (Thm.cterm_of @{theory} @{const divide (real)}) |
72 val mk_div = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const divide (real)}) |
73 val mk_lt = Thm.mk_binop (Thm.cterm_of @{theory} @{const less (real)}) |
73 val mk_lt = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less (real)}) |
74 val mk_le = Thm.mk_binop (Thm.cterm_of @{theory} @{const less_eq (real)}) |
74 val mk_le = Thm.mk_binop (Thm.global_cterm_of @{theory} @{const less_eq (real)}) |
75 |
75 |
76 fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
76 fun z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct] = SOME (mk_uminus ct) |
77 | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts) |
77 | z3_mk_builtin_fun (Z3_Interface.Sym ("+", _)) cts = SOME (mk_nary add real0 cts) |
78 | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu) |
78 | z3_mk_builtin_fun (Z3_Interface.Sym ("-", _)) [ct, cu] = SOME (mk_sub ct cu) |
79 | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu) |
79 | z3_mk_builtin_fun (Z3_Interface.Sym ("*", _)) [ct, cu] = SOME (mk_mul ct cu) |