|
1 (* Title: HOL/Tools/SMT/smt_builtin.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 Crafted collection of SMT built-in symbols. |
|
5 |
|
6 FIXME: This list is currently not automatically kept synchronized with the |
|
7 remaining implementation. |
|
8 *) |
|
9 |
|
10 signature SMT_BUILTIN = |
|
11 sig |
|
12 val is_partially_builtin: Proof.context -> string * typ -> bool |
|
13 val is_builtin: Proof.context -> string * typ -> bool |
|
14 end |
|
15 |
|
16 structure SMT_Builtin: SMT_BUILTIN = |
|
17 struct |
|
18 |
|
19 fun is_arithT (Type (@{type_name fun}, [T, _])) = |
|
20 (case T of |
|
21 @{typ int} => true |
|
22 | @{typ nat} => true |
|
23 | Type ("RealDef.real", []) => true |
|
24 | _ => false) |
|
25 | is_arithT _ = false |
|
26 |
|
27 val builtins = Symtab.make [ |
|
28 |
|
29 (* Pure constants *) |
|
30 (@{const_name all}, K true), |
|
31 (@{const_name "=="}, K true), |
|
32 (@{const_name "==>"}, K true), |
|
33 (@{const_name Trueprop}, K true), |
|
34 |
|
35 (* logical constants *) |
|
36 (@{const_name All}, K true), |
|
37 (@{const_name Ex}, K true), |
|
38 (@{const_name Ball}, K true), |
|
39 (@{const_name Bex}, K true), |
|
40 (@{const_name Ex1}, K true), |
|
41 (@{const_name True}, K true), |
|
42 (@{const_name False}, K true), |
|
43 (@{const_name Not}, K true), |
|
44 (@{const_name HOL.conj}, K true), |
|
45 (@{const_name HOL.disj}, K true), |
|
46 (@{const_name HOL.implies}, K true), |
|
47 |
|
48 (* term abbreviations *) |
|
49 (@{const_name If}, K true), |
|
50 (@{const_name bool.bool_case}, K true), |
|
51 (@{const_name Let}, K true), |
|
52 (@{const_name SMT.distinct}, K true), |
|
53 |
|
54 (* technicalities *) |
|
55 (@{const_name SMT.pat}, K true), |
|
56 (@{const_name SMT.nopat}, K true), |
|
57 (@{const_name SMT.trigger}, K true), |
|
58 (@{const_name SMT.fun_app}, K true), |
|
59 (@{const_name SMT.z3div}, K true), |
|
60 (@{const_name SMT.z3mod}, K true), |
|
61 |
|
62 (* equality *) |
|
63 (@{const_name HOL.eq}, K true), |
|
64 |
|
65 (* numerals *) |
|
66 (@{const_name zero_class.zero}, K true), |
|
67 (@{const_name one_class.one}, K true), |
|
68 (@{const_name Int.Pls}, K true), |
|
69 (@{const_name Int.Min}, K true), |
|
70 (@{const_name Int.Bit0}, K true), |
|
71 (@{const_name Int.Bit1}, K true), |
|
72 (@{const_name number_of}, K true), |
|
73 |
|
74 (* arithmetic *) |
|
75 (@{const_name nat}, K true), |
|
76 (@{const_name of_nat}, K true), |
|
77 (@{const_name Suc}, K true), |
|
78 (@{const_name plus}, is_arithT), |
|
79 (@{const_name uminus}, is_arithT), |
|
80 (@{const_name minus}, is_arithT), |
|
81 (@{const_name abs}, is_arithT), |
|
82 (@{const_name min}, is_arithT), |
|
83 (@{const_name max}, is_arithT), |
|
84 (@{const_name less}, is_arithT), |
|
85 (@{const_name less_eq}, is_arithT), |
|
86 |
|
87 (* pairs *) |
|
88 (@{const_name fst}, K true), |
|
89 (@{const_name snd}, K true), |
|
90 (@{const_name Pair}, K true) |
|
91 |
|
92 ] |
|
93 |
|
94 val all_builtins = |
|
95 builtins |
|
96 |> Symtab.update (@{const_name times}, is_arithT) |
|
97 |> Symtab.update (@{const_name div_class.div}, is_arithT) |
|
98 |> Symtab.update (@{const_name div_class.mod}, is_arithT) |
|
99 |> Symtab.update ("Rings.inverse_class.divide", is_arithT) |
|
100 |
|
101 fun lookup_builtin bs (name, T) = |
|
102 (case Symtab.lookup bs name of |
|
103 SOME proper_type => proper_type T |
|
104 | NONE => false) |
|
105 |
|
106 fun is_partially_builtin _ = lookup_builtin builtins |
|
107 |
|
108 fun is_builtin _ = lookup_builtin all_builtins |
|
109 |
|
110 end |