src/HOL/Tools/SMT/smt_utils.ML
author boehmes
Wed Nov 24 15:33:35 2010 +0100 (2010-11-24)
changeset 40686 4725ed462387
parent 40663 e080c9e68752
child 40840 2f97215e79bf
permissions -rw-r--r--
swap names for built-in tester functions (to better reflect the intuition of what they do);
eta-expand all built-in functions (even those which are only partially supported)
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@40662
     9
  val repeat: ('a -> 'a option) -> 'a -> 'a
boehmes@40662
    10
  val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
boehmes@40662
    11
boehmes@40663
    12
  (* types *)
boehmes@40663
    13
  val split_type: typ -> typ * typ
boehmes@40663
    14
  val dest_funT: int -> typ -> typ list * typ
boehmes@40663
    15
boehmes@40662
    16
  (* terms *)
boehmes@40662
    17
  val dest_conj: term -> term * term
boehmes@40662
    18
  val dest_disj: term -> term * term
boehmes@40662
    19
boehmes@40662
    20
  (* patterns and instantiations *)
boehmes@40662
    21
  val mk_const_pat: theory -> string -> (ctyp -> 'a) -> 'a * cterm
boehmes@40662
    22
  val destT1: ctyp -> ctyp
boehmes@40662
    23
  val destT2: ctyp -> ctyp
boehmes@40662
    24
  val instTs: ctyp list -> ctyp list * cterm -> cterm
boehmes@40662
    25
  val instT: ctyp -> ctyp * cterm -> cterm
boehmes@40662
    26
  val instT': cterm -> ctyp * cterm -> cterm
boehmes@40662
    27
boehmes@40662
    28
  (* certified terms *)
boehmes@40662
    29
  val certify: Proof.context -> term -> cterm
boehmes@40663
    30
  val typ_of: cterm -> typ
boehmes@40662
    31
  val dest_cabs: cterm -> Proof.context -> cterm * Proof.context
boehmes@40662
    32
  val dest_all_cabs: cterm -> Proof.context -> cterm * Proof.context
boehmes@40662
    33
  val dest_cbinder: cterm -> Proof.context -> cterm * Proof.context
boehmes@40662
    34
  val dest_all_cbinders: cterm -> Proof.context -> cterm * Proof.context
boehmes@40662
    35
  val mk_cprop: cterm -> cterm
boehmes@40662
    36
  val dest_cprop: cterm -> cterm
boehmes@40662
    37
  val mk_cequals: cterm -> cterm -> cterm
boehmes@40662
    38
boehmes@40662
    39
  (* conversions *)
boehmes@40662
    40
  val if_conv: (term -> bool) -> conv -> conv -> conv
boehmes@40662
    41
  val if_true_conv: (term -> bool) -> conv -> conv
boehmes@40662
    42
  val binders_conv: (Proof.context -> conv) -> Proof.context -> conv
boehmes@40662
    43
  val prop_conv: conv -> conv
boehmes@40662
    44
end
boehmes@40662
    45
boehmes@40662
    46
structure SMT_Utils: SMT_UTILS =
boehmes@40662
    47
struct
boehmes@40662
    48
boehmes@40662
    49
fun repeat f =
boehmes@40662
    50
  let fun rep x = (case f x of SOME y => rep y | NONE => x)
boehmes@40662
    51
  in rep end
boehmes@40662
    52
boehmes@40662
    53
fun repeat_yield f =
boehmes@40662
    54
  let fun rep x y = (case f x y of SOME (x', y') => rep x' y' | NONE => (x, y))
boehmes@40662
    55
  in rep end
boehmes@40662
    56
boehmes@40662
    57
boehmes@40663
    58
(* types *)
boehmes@40663
    59
boehmes@40663
    60
fun split_type T = (Term.domain_type T, Term.range_type T)
boehmes@40663
    61
boehmes@40663
    62
val dest_funT =
boehmes@40663
    63
  let
boehmes@40663
    64
    fun dest Ts 0 T = (rev Ts, T)
boehmes@40663
    65
      | dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i-1) U
boehmes@40663
    66
      | dest _ _ T = raise TYPE ("not a function type", [T], [])
boehmes@40663
    67
  in dest [] end
boehmes@40663
    68
boehmes@40663
    69
boehmes@40662
    70
(* terms *)
boehmes@40662
    71
boehmes@40662
    72
fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u)
boehmes@40662
    73
  | dest_conj t = raise TERM ("not a conjunction", [t])
boehmes@40662
    74
boehmes@40662
    75
fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u)
boehmes@40662
    76
  | dest_disj t = raise TERM ("not a disjunction", [t])
boehmes@40662
    77
boehmes@40662
    78
boehmes@40662
    79
(* patterns and instantiations *)
boehmes@40662
    80
boehmes@40662
    81
fun mk_const_pat thy name destT =
boehmes@40662
    82
  let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name))
boehmes@40662
    83
  in (destT (Thm.ctyp_of_term cpat), cpat) end
boehmes@40662
    84
boehmes@40662
    85
val destT1 = hd o Thm.dest_ctyp
boehmes@40662
    86
val destT2 = hd o tl o Thm.dest_ctyp
boehmes@40662
    87
boehmes@40662
    88
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct
boehmes@40662
    89
fun instT cU (cT, ct) = instTs [cU] ([cT], ct)
boehmes@40662
    90
fun instT' ct = instT (Thm.ctyp_of_term ct)
boehmes@40662
    91
boehmes@40662
    92
boehmes@40662
    93
(* certified terms *)
boehmes@40662
    94
boehmes@40662
    95
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt)
boehmes@40662
    96
boehmes@40663
    97
fun typ_of ct = #T (Thm.rep_cterm ct) 
boehmes@40663
    98
boehmes@40662
    99
fun dest_cabs ct ctxt =
boehmes@40662
   100
  (case Thm.term_of ct of
boehmes@40662
   101
    Abs _ =>
boehmes@40662
   102
      let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt
boehmes@40662
   103
      in (snd (Thm.dest_abs (SOME n) ct), ctxt') end
boehmes@40662
   104
  | _ => raise CTERM ("no abstraction", [ct]))
boehmes@40662
   105
boehmes@40662
   106
val dest_all_cabs = repeat_yield (try o dest_cabs) 
boehmes@40662
   107
boehmes@40662
   108
fun dest_cbinder ct ctxt =
boehmes@40662
   109
  (case Thm.term_of ct of
boehmes@40662
   110
    Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt
boehmes@40662
   111
  | _ => raise CTERM ("not a binder", [ct]))
boehmes@40662
   112
boehmes@40662
   113
val dest_all_cbinders = repeat_yield (try o dest_cbinder)
boehmes@40662
   114
boehmes@40663
   115
val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
boehmes@40662
   116
boehmes@40662
   117
fun dest_cprop ct =
boehmes@40662
   118
  (case Thm.term_of ct of
boehmes@40662
   119
    @{const Trueprop} $ _ => Thm.dest_arg ct
boehmes@40662
   120
  | _ => raise CTERM ("not a property", [ct]))
boehmes@40662
   121
boehmes@40662
   122
val equals = mk_const_pat @{theory} @{const_name "=="} destT1
boehmes@40662
   123
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu
boehmes@40662
   124
boehmes@40662
   125
boehmes@40662
   126
(* conversions *)
boehmes@40662
   127
boehmes@40663
   128
fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct
boehmes@40662
   129
boehmes@40663
   130
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv
boehmes@40662
   131
boehmes@40662
   132
fun binders_conv cv ctxt =
boehmes@40662
   133
  Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt
boehmes@40662
   134
boehmes@40662
   135
fun prop_conv cv ct =
boehmes@40662
   136
  (case Thm.term_of ct of
boehmes@40662
   137
    @{const Trueprop} $ _ => Conv.arg_conv cv ct
boehmes@40662
   138
  | _ => raise CTERM ("not a property", [ct]))
boehmes@40662
   139
boehmes@40662
   140
end