src/HOL/Tools/SMT/smt_utils.ML
author wenzelm
Fri Mar 21 20:33:56 2014 +0100 (2014-03-21)
changeset 56245 84fc7dfa3cd4
parent 54489 03ff4d1e6784
permissions -rw-r--r--
more qualified names;
     1 (*  Title:      HOL/Tools/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