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