40662

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 

40663

12 
(* types *)


13 
val split_type: typ > typ * typ


14 
val dest_funT: int > typ > typ list * typ


15 

40662

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

40663

30 
val typ_of: cterm > typ

40662

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 

40663

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) (i1) U


66 
 dest _ _ T = raise TYPE ("not a function type", [T], [])


67 
in dest [] end


68 


69 

40662

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 

40663

97 
fun typ_of ct = #T (Thm.rep_cterm ct)


98 

40662

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 

40663

115 
val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})

40662

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 

40663

128 
fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct

40662

129 

40663

130 
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv

40662

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
