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