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