|
1 (* Title: HOL/Tools/SMT/smt_util.ML |
|
2 Author: Sascha Boehme, TU Muenchen |
|
3 |
|
4 General utility functions. |
|
5 *) |
|
6 |
|
7 signature SMT_UTIL = |
|
8 sig |
|
9 (*basic combinators*) |
|
10 val repeat: ('a -> 'a option) -> 'a -> 'a |
|
11 val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b |
|
12 |
|
13 (*class dictionaries*) |
|
14 type class = string list |
|
15 val basicC: class |
|
16 val string_of_class: class -> string |
|
17 type 'a dict = (class * 'a) Ord_List.T |
|
18 val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict |
|
19 val dict_update: class * 'a -> 'a dict -> 'a dict |
|
20 val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict |
|
21 val dict_lookup: 'a dict -> class -> 'a list |
|
22 val dict_get: 'a dict -> class -> 'a option |
|
23 |
|
24 (*types*) |
|
25 val dest_funT: int -> typ -> typ list * typ |
|
26 |
|
27 (*terms*) |
|
28 val dest_conj: term -> term * term |
|
29 val dest_disj: term -> term * term |
|
30 val under_quant: (term -> 'a) -> term -> 'a |
|
31 val is_number: term -> bool |
|
32 |
|
33 (*symbolic lists*) |
|
34 val symb_nil_const: typ -> term |
|
35 val symb_cons_const: typ -> term |
|
36 val mk_symb_list: typ -> term list -> term |
|
37 val dest_symb_list: term -> term list |
|
38 |
|
39 (*patterns and instantiations*) |
|
40 val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm |
|
41 val destT1: ctyp -> ctyp |
|
42 val destT2: ctyp -> ctyp |
|
43 val instTs: ctyp list -> ctyp list * cterm -> cterm |
|
44 val instT: ctyp -> ctyp * cterm -> cterm |
|
45 val instT': cterm -> ctyp * cterm -> cterm |
|
46 |
|
47 (*certified terms*) |
|
48 val certify: Proof.context -> term -> cterm |
|
49 val typ_of: cterm -> typ |
|
50 val dest_cabs: cterm -> Proof.context -> cterm * Proof.context |
|
51 val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context |
|
52 val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context |
|
53 val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context |
|
54 val mk_cprop: cterm -> cterm |
|
55 val dest_cprop: cterm -> cterm |
|
56 val mk_cequals: cterm -> cterm -> cterm |
|
57 val term_of: cterm -> term |
|
58 val prop_of: thm -> term |
|
59 |
|
60 (*conversions*) |
|
61 val if_conv: (term -> bool) -> conv -> conv -> conv |
|
62 val if_true_conv: (term -> bool) -> conv -> conv |
|
63 val if_exists_conv: (term -> bool) -> conv -> conv |
|
64 val binders_conv: (Proof.context -> conv) -> Proof.context -> conv |
|
65 val under_quant_conv: (Proof.context * cterm list -> conv) -> |
|
66 Proof.context -> conv |
|
67 val prop_conv: conv -> conv |
|
68 end; |
|
69 |
|
70 structure SMT_Util: SMT_UTIL = |
|
71 struct |
|
72 |
|
73 (* basic combinators *) |
|
74 |
|
75 fun repeat f = |
|
76 let fun rep x = (case f x of SOME y => rep y | NONE => x) |
|
77 in rep end |
|
78 |
|
79 fun repeat_yield f = |
|
80 let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y)) |
|
81 in rep end |
|
82 |
|
83 |
|
84 (* class dictionaries *) |
|
85 |
|
86 type class = string list |
|
87 |
|
88 val basicC = [] |
|
89 |
|
90 fun string_of_class [] = "basic" |
|
91 | string_of_class cs = "basic." ^ space_implode "." cs |
|
92 |
|
93 type 'a dict = (class * 'a) Ord_List.T |
|
94 |
|
95 fun class_ord ((cs1, _), (cs2, _)) = |
|
96 rev_order (list_ord fast_string_ord (cs1, cs2)) |
|
97 |
|
98 fun dict_insert (cs, x) d = |
|
99 if AList.defined (op =) d cs then d |
|
100 else Ord_List.insert class_ord (cs, x) d |
|
101 |
|
102 fun dict_map_default (cs, x) f = |
|
103 dict_insert (cs, x) #> AList.map_entry (op =) cs f |
|
104 |
|
105 fun dict_update (e as (_, x)) = dict_map_default e (K x) |
|
106 |
|
107 fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge) |
|
108 |
|
109 fun dict_lookup d cs = |
|
110 let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE |
|
111 in map_filter match d end |
|
112 |
|
113 fun dict_get d cs = |
|
114 (case AList.lookup (op =) d cs of |
|
115 NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs)) |
|
116 | SOME x => SOME x) |
|
117 |
|
118 |
|
119 (* types *) |
|
120 |
|
121 val dest_funT = |
|
122 let |
|
123 fun dest Ts 0 T = (rev Ts, T) |
|
124 | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U |
|
125 | dest _ _ T = raise TYPE ("not a function type", [T], []) |
|
126 in dest [] end |
|
127 |
|
128 |
|
129 (* terms *) |
|
130 |
|
131 fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u) |
|
132 | dest_conj t = raise TERM ("not a conjunction", [t]) |
|
133 |
|
134 fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u) |
|
135 | dest_disj t = raise TERM ("not a disjunction", [t]) |
|
136 |
|
137 fun under_quant f t = |
|
138 (case t of |
|
139 Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u |
|
140 | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u |
|
141 | _ => f t) |
|
142 |
|
143 val is_number = |
|
144 let |
|
145 fun is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = is_num (t :: env) u |
|
146 | is_num env (Bound i) = i < length env andalso is_num env (nth env i) |
|
147 | is_num _ t = can HOLogic.dest_number t |
|
148 in is_num [] end |
|
149 |
|
150 |
|
151 (* symbolic lists *) |
|
152 |
|
153 fun symb_listT T = Type (@{type_name symb_list}, [T]) |
|
154 |
|
155 fun symb_nil_const T = Const (@{const_name Symb_Nil}, symb_listT T) |
|
156 |
|
157 fun symb_cons_const T = |
|
158 let val listT = symb_listT T in Const (@{const_name Symb_Cons}, T --> listT --> listT) end |
|
159 |
|
160 fun mk_symb_list T ts = |
|
161 fold_rev (fn t => fn u => symb_cons_const T $ t $ u) ts (symb_nil_const T) |
|
162 |
|
163 fun dest_symb_list (Const (@{const_name Symb_Nil}, _)) = [] |
|
164 | dest_symb_list (Const (@{const_name Symb_Cons}, _) $ t $ u) = t :: dest_symb_list u |
|
165 |
|
166 |
|
167 (* patterns and instantiations *) |
|
168 |
|
169 fun mk_const_pat thy name destT = |
|
170 let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name)) |
|
171 in (destT (Thm.ctyp_of_term cpat), cpat) end |
|
172 |
|
173 val destT1 = hd o Thm.dest_ctyp |
|
174 val destT2 = hd o tl o Thm.dest_ctyp |
|
175 |
|
176 fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct |
|
177 fun instT cU (cT, ct) = instTs [cU] ([cT], ct) |
|
178 fun instT' ct = instT (Thm.ctyp_of_term ct) |
|
179 |
|
180 |
|
181 (* certified terms *) |
|
182 |
|
183 fun certify ctxt = Thm.cterm_of (Proof_Context.theory_of ctxt) |
|
184 |
|
185 fun typ_of ct = #T (Thm.rep_cterm ct) |
|
186 |
|
187 fun dest_cabs ct ctxt = |
|
188 (case Thm.term_of ct of |
|
189 Abs _ => |
|
190 let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt |
|
191 in (snd (Thm.dest_abs (SOME n) ct), ctxt') end |
|
192 | _ => raise CTERM ("no abstraction", [ct])) |
|
193 |
|
194 val dest_all_cabs = repeat_yield (try o dest_cabs) |
|
195 |
|
196 fun dest_cbinder ct ctxt = |
|
197 (case Thm.term_of ct of |
|
198 Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt |
|
199 | _ => raise CTERM ("not a binder", [ct])) |
|
200 |
|
201 val dest_all_cbinders = repeat_yield (try o dest_cbinder) |
|
202 |
|
203 val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop}) |
|
204 |
|
205 fun dest_cprop ct = |
|
206 (case Thm.term_of ct of |
|
207 @{const Trueprop} $ _ => Thm.dest_arg ct |
|
208 | _ => raise CTERM ("not a property", [ct])) |
|
209 |
|
210 val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1 |
|
211 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu |
|
212 |
|
213 val dest_prop = (fn @{const Trueprop} $ t => t | t => t) |
|
214 fun term_of ct = dest_prop (Thm.term_of ct) |
|
215 fun prop_of thm = dest_prop (Thm.prop_of thm) |
|
216 |
|
217 |
|
218 (* conversions *) |
|
219 |
|
220 fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct |
|
221 |
|
222 fun if_true_conv pred cv = if_conv pred cv Conv.all_conv |
|
223 |
|
224 fun if_exists_conv pred = if_true_conv (Term.exists_subterm pred) |
|
225 |
|
226 fun binders_conv cv ctxt = |
|
227 Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt |
|
228 |
|
229 fun under_quant_conv cv ctxt = |
|
230 let |
|
231 fun quant_conv inside ctxt cvs ct = |
|
232 (case Thm.term_of ct of |
|
233 Const (@{const_name All}, _) $ Abs _ => |
|
234 Conv.binder_conv (under_conv cvs) ctxt |
|
235 | Const (@{const_name Ex}, _) $ Abs _ => |
|
236 Conv.binder_conv (under_conv cvs) ctxt |
|
237 | _ => if inside then cv (ctxt, cvs) else Conv.all_conv) ct |
|
238 and under_conv cvs (cv, ctxt) = quant_conv true ctxt (cv :: cvs) |
|
239 in quant_conv false ctxt [] end |
|
240 |
|
241 fun prop_conv cv ct = |
|
242 (case Thm.term_of ct of |
|
243 @{const Trueprop} $ _ => Conv.arg_conv cv ct |
|
244 | _ => raise CTERM ("not a property", [ct])) |
|
245 |
|
246 end; |