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