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