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