src/HOL/Tools/SMT/smt_util.ML
author wenzelm
Sun Nov 26 21:08:32 2017 +0100 (18 months ago)
changeset 67091 1393c2340eec
parent 66551 4df6b0ae900d
child 69593 3dda49e08b9d
permissions -rw-r--r--
more symbols;
     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   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 destT1: ctyp -> ctyp
    44   val destT2: ctyp -> ctyp
    45   val instTs: ctyp list -> ctyp list * cterm -> cterm
    46   val instT: ctyp -> ctyp * cterm -> cterm
    47   val instT': cterm -> ctyp * cterm -> cterm
    48 
    49   (*certified terms*)
    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 (* order *)
    85 
    86 datatype order = First_Order | Higher_Order
    87 
    88 
    89 (* class dictionaries *)
    90 
    91 type class = string list
    92 
    93 val basicC = []
    94 
    95 fun string_of_class [] = "basic"
    96   | string_of_class cs = "basic." ^ space_implode "." cs
    97 
    98 type 'a dict = (class * 'a) Ord_List.T
    99 
   100 fun class_ord ((cs1, _), (cs2, _)) =
   101   rev_order (list_ord fast_string_ord (cs1, cs2))
   102 
   103 fun dict_insert (cs, x) d =
   104   if AList.defined (op =) d cs then d
   105   else Ord_List.insert class_ord (cs, x) d
   106 
   107 fun dict_map_default (cs, x) f =
   108   dict_insert (cs, x) #> AList.map_entry (op =) cs f
   109 
   110 fun dict_update (e as (_, x)) = dict_map_default e (K x)
   111 
   112 fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge)
   113 
   114 fun dict_lookup d cs =
   115   let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE
   116   in map_filter match d end
   117 
   118 fun dict_get d cs =
   119   (case AList.lookup (op =) d cs of
   120     NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs))
   121   | SOME x => SOME x)
   122 
   123 
   124 (* types *)
   125 
   126 val dest_funT =
   127   let
   128     fun dest Ts 0 T = (rev Ts, T)
   129       | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
   130       | dest _ _ T = raise TYPE ("not a function type", [T], [])
   131   in dest [] end
   132 
   133 
   134 (* terms *)
   135 
   136 fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
   137   | dest_conj t = raise TERM ("not a conjunction", [t])
   138 
   139 fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u)
   140   | dest_disj t = raise TERM ("not a disjunction", [t])
   141 
   142 fun under_quant f t =
   143   (case t of
   144     Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u
   145   | Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u
   146   | _ => f t)
   147 
   148 val is_number =
   149   let
   150     fun is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = is_num (t :: env) u
   151       | is_num env (Bound i) = i < length env andalso is_num env (nth env i)
   152       | is_num _ t = can HOLogic.dest_number t
   153   in is_num [] end
   154 
   155 
   156 (* symbolic lists *)
   157 
   158 fun symb_listT T = Type (@{type_name symb_list}, [T])
   159 
   160 fun symb_nil_const T = Const (@{const_name Symb_Nil}, symb_listT T)
   161 
   162 fun symb_cons_const T =
   163   let val listT = symb_listT T in Const (@{const_name Symb_Cons}, T --> listT --> listT) end
   164 
   165 fun mk_symb_list T ts =
   166   fold_rev (fn t => fn u => symb_cons_const T $ t $ u) ts (symb_nil_const T)
   167 
   168 fun dest_symb_list (Const (@{const_name Symb_Nil}, _)) = []
   169   | dest_symb_list (Const (@{const_name Symb_Cons}, _) $ t $ u) = t :: dest_symb_list u
   170 
   171 
   172 (* patterns and instantiations *)
   173 
   174 fun mk_const_pat thy name destT =
   175   let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name))
   176   in (destT (Thm.ctyp_of_cterm cpat), cpat) end
   177 
   178 val destT1 = hd o Thm.dest_ctyp
   179 val destT2 = hd o tl o Thm.dest_ctyp
   180 
   181 fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct
   182 fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
   183 fun instT' ct = instT (Thm.ctyp_of_cterm ct)
   184 
   185 
   186 (* certified terms *)
   187 
   188 fun dest_cabs ct ctxt =
   189   (case Thm.term_of ct of
   190     Abs _ =>
   191       let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
   192       in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
   193   | _ => raise CTERM ("no abstraction", [ct]))
   194 
   195 val dest_all_cabs = repeat_yield (try o dest_cabs)
   196 
   197 fun dest_cbinder ct ctxt =
   198   (case Thm.term_of ct of
   199     Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt
   200   | _ => raise CTERM ("not a binder", [ct]))
   201 
   202 val dest_all_cbinders = repeat_yield (try o dest_cbinder)
   203 
   204 val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop})
   205 
   206 fun dest_cprop ct =
   207   (case Thm.term_of ct of
   208     @{const Trueprop} $ _ => Thm.dest_arg ct
   209   | _ => raise CTERM ("not a property", [ct]))
   210 
   211 val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1
   212 fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
   213 
   214 val dest_prop = (fn @{const Trueprop} $ t => t | t => t)
   215 fun term_of ct = dest_prop (Thm.term_of ct)
   216 fun prop_of thm = dest_prop (Thm.prop_of thm)
   217 
   218 
   219 (* conversions *)
   220 
   221 fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
   222 
   223 fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
   224 
   225 fun if_exists_conv pred = if_true_conv (Term.exists_subterm pred)
   226 
   227 fun binders_conv cv ctxt =
   228   Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt
   229 
   230 fun under_quant_conv cv ctxt =
   231   let
   232     fun quant_conv inside ctxt cvs ct =
   233       (case Thm.term_of ct of
   234         Const (@{const_name All}, _) $ Abs _ =>
   235           Conv.binder_conv (under_conv cvs) ctxt
   236       | Const (@{const_name Ex}, _) $ Abs _ =>
   237           Conv.binder_conv (under_conv cvs) ctxt
   238       | _ => if inside then cv (ctxt, cvs) else Conv.all_conv) ct
   239     and under_conv cvs (cv, ctxt) = quant_conv true ctxt (cv :: cvs)
   240   in quant_conv false ctxt [] end
   241 
   242 fun prop_conv cv ct =
   243   (case Thm.term_of ct of
   244     @{const Trueprop} $ _ => Conv.arg_conv cv ct
   245   | _ => raise CTERM ("not a property", [ct]))
   246 
   247 end;