author  boehmes 
Sun, 19 Dec 2010 17:55:56 +0100  
changeset 41280  a7de9d36f4f2 
parent 41172  a17c2d669c40 
child 41301  0a00fd2f5351 
permissions  rwrr 
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 

41123  9 
(*basic combinators*) 
40662  10 
val repeat: ('a > 'a option) > 'a > 'a 
11 
val repeat_yield: ('a > 'b > ('a * 'b) option) > 'a > 'b > 'a * 'b 

12 

41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

13 
(*class dictionaries*) 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

14 
type class = string list 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

15 
val basicC: class 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

16 
val string_of_class: class > string 
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

17 
type 'a dict = (class * 'a) Ord_List.T 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

18 
val dict_map_default: class * 'a > ('a > 'a) > 'a dict > 'a dict 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

19 
val dict_update: class * 'a > 'a dict > 'a dict 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

20 
val dict_merge: ('a * 'a > 'a) > 'a dict * 'a dict > 'a dict 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

21 
val dict_lookup: 'a dict > class > 'a list 
41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

22 
val dict_get: 'a dict > class > 'a option 
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

23 

41123  24 
(*types*) 
40663  25 
val dest_funT: int > typ > typ list * typ 
26 

41123  27 
(*terms*) 
40662  28 
val dest_conj: term > term * term 
29 
val dest_disj: term > term * term 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

30 
val under_quant: (term > 'a) > term > 'a 
41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

31 
val is_number: term > bool 
40662  32 

41123  33 
(*patterns and instantiations*) 
40662  34 
val mk_const_pat: theory > string > (ctyp > 'a) > 'a * cterm 
35 
val destT1: ctyp > ctyp 

36 
val destT2: ctyp > ctyp 

37 
val instTs: ctyp list > ctyp list * cterm > cterm 

38 
val instT: ctyp > ctyp * cterm > cterm 

39 
val instT': cterm > ctyp * cterm > cterm 

40 

41123  41 
(*certified terms*) 
40662  42 
val certify: Proof.context > term > cterm 
40663  43 
val typ_of: cterm > typ 
40662  44 
val dest_cabs: cterm > Proof.context > cterm * Proof.context 
45 
val dest_all_cabs: cterm > Proof.context > cterm * Proof.context 

46 
val dest_cbinder: cterm > Proof.context > cterm * Proof.context 

47 
val dest_all_cbinders: cterm > Proof.context > cterm * Proof.context 

48 
val mk_cprop: cterm > cterm 

49 
val dest_cprop: cterm > cterm 

50 
val mk_cequals: cterm > cterm > cterm 

41172
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41127
diff
changeset

51 
val term_of: cterm > term 
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41127
diff
changeset

52 
val prop_of: thm > term 
40662  53 

41123  54 
(*conversions*) 
40662  55 
val if_conv: (term > bool) > conv > conv > conv 
56 
val if_true_conv: (term > bool) > conv > conv 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

57 
val if_exists_conv: (term > bool) > conv > conv 
40662  58 
val binders_conv: (Proof.context > conv) > Proof.context > conv 
41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

59 
val under_quant_conv: (Proof.context * cterm list > conv) > 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

60 
Proof.context > conv 
40662  61 
val prop_conv: conv > conv 
62 
end 

63 

64 
structure SMT_Utils: SMT_UTILS = 

65 
struct 

66 

41123  67 
(* basic combinators *) 
68 

40662  69 
fun repeat f = 
70 
let fun rep x = (case f x of SOME y => rep y  NONE => x) 

71 
in rep end 

72 

73 
fun repeat_yield f = 

74 
let fun rep x y = (case f x y of SOME (x', y') => rep x' y'  NONE => (x, y)) 

75 
in rep end 

76 

77 

41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

78 
(* class dictionaries *) 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

79 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

80 
type class = string list 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

81 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

82 
val basicC = [] 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

83 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

84 
fun string_of_class [] = "basic" 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

85 
 string_of_class cs = "basic." ^ space_implode "." cs 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

86 

41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

87 
type 'a dict = (class * 'a) Ord_List.T 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

88 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

89 
fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2) 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

90 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

91 
fun dict_insert (cs, x) d = 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

92 
if AList.defined (op =) d cs then d 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

93 
else Ord_List.insert class_ord (cs, x) d 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

94 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

95 
fun dict_map_default (cs, x) f = 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

96 
dict_insert (cs, x) #> AList.map_entry (op =) cs f 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

97 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

98 
fun dict_update (e as (_, x)) = dict_map_default e (K x) 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

99 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

100 
fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge) 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

101 

1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

102 
fun dict_lookup d cs = 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

103 
let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

104 
in map_filter match d end 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

105 

41127
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

106 
fun dict_get d cs = 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

107 
(case AList.lookup (op =) d cs of 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

108 
NONE => (case cs of [] => NONE  _ => dict_get d (take (length cs  1) cs)) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

109 
 SOME x => SOME x) 
2ea84c8535c6
reimplemented etaexpansion, lambdalifting, and explicit application on terms (exploiting the control over the term structure);
boehmes
parents:
41126
diff
changeset

110 

41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

111 

40663  112 
(* types *) 
113 

114 
val dest_funT = 

115 
let 

116 
fun dest Ts 0 T = (rev Ts, T) 

117 
 dest Ts i (Type ("fun", [T, U])) = dest (T::Ts) (i1) U 

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

119 
in dest [] end 

120 

121 

40662  122 
(* terms *) 
123 

124 
fun dest_conj (@{const HOL.conj} $ t $ u) = (t, u) 

125 
 dest_conj t = raise TERM ("not a conjunction", [t]) 

126 

127 
fun dest_disj (@{const HOL.disj} $ t $ u) = (t, u) 

128 
 dest_disj t = raise TERM ("not a disjunction", [t]) 

129 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

130 
fun under_quant f t = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

131 
(case t of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

132 
Const (@{const_name All}, _) $ Abs (_, _, u) => under_quant f u 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

133 
 Const (@{const_name Ex}, _) $ Abs (_, _, u) => under_quant f u 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

134 
 _ => f t) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

135 

41280
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

136 
val is_number = 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

137 
let 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

138 
fun is_num env (Const (@{const_name If}, _) $ _ $ t $ u) = 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

139 
is_num env t andalso is_num env u 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

140 
 is_num env (Const (@{const_name Let}, _) $ t $ Abs (_, _, u)) = 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

141 
is_num (t :: env) u 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

142 
 is_num env (Const (@{const_name uminus}, _) $ t) = is_num env t 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

143 
 is_num env (Const (@{const_name divide}, _) $ t $ u) = 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

144 
is_num env t andalso is_num env u 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

145 
 is_num env (Bound i) = i < length env andalso is_num env (nth env i) 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

146 
 is_num _ t = can HOLogic.dest_number t 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

147 
in is_num [] end 
a7de9d36f4f2
only linear occurrences of multiplication are treated as builtin (SMT solvers only support linear arithmetic in general);
boehmes
parents:
41172
diff
changeset

148 

40662  149 

150 
(* patterns and instantiations *) 

151 

152 
fun mk_const_pat thy name destT = 

153 
let val cpat = Thm.cterm_of thy (Const (name, Sign.the_const_type thy name)) 

154 
in (destT (Thm.ctyp_of_term cpat), cpat) end 

155 

156 
val destT1 = hd o Thm.dest_ctyp 

157 
val destT2 = hd o tl o Thm.dest_ctyp 

158 

159 
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (cTs ~~ cUs, []) ct 

160 
fun instT cU (cT, ct) = instTs [cU] ([cT], ct) 

161 
fun instT' ct = instT (Thm.ctyp_of_term ct) 

162 

163 

164 
(* certified terms *) 

165 

166 
fun certify ctxt = Thm.cterm_of (ProofContext.theory_of ctxt) 

167 

40663  168 
fun typ_of ct = #T (Thm.rep_cterm ct) 
169 

40662  170 
fun dest_cabs ct ctxt = 
171 
(case Thm.term_of ct of 

172 
Abs _ => 

173 
let val (n, ctxt') = yield_singleton Variable.variant_fixes Name.uu ctxt 

174 
in (snd (Thm.dest_abs (SOME n) ct), ctxt') end 

175 
 _ => raise CTERM ("no abstraction", [ct])) 

176 

177 
val dest_all_cabs = repeat_yield (try o dest_cabs) 

178 

179 
fun dest_cbinder ct ctxt = 

180 
(case Thm.term_of ct of 

181 
Const _ $ Abs _ => dest_cabs (Thm.dest_arg ct) ctxt 

182 
 _ => raise CTERM ("not a binder", [ct])) 

183 

184 
val dest_all_cbinders = repeat_yield (try o dest_cbinder) 

185 

40663  186 
val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop}) 
40662  187 

188 
fun dest_cprop ct = 

189 
(case Thm.term_of ct of 

190 
@{const Trueprop} $ _ => Thm.dest_arg ct 

191 
 _ => raise CTERM ("not a property", [ct])) 

192 

193 
val equals = mk_const_pat @{theory} @{const_name "=="} destT1 

194 
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu 

195 

41172
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41127
diff
changeset

196 
val dest_prop = (fn @{const Trueprop} $ t => t  t => t) 
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41127
diff
changeset

197 
fun term_of ct = dest_prop (Thm.term_of ct) 
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41127
diff
changeset

198 
fun prop_of thm = dest_prop (Thm.prop_of thm) 
a17c2d669c40
the functions term_of and prop_of are also needed in earlier stages, not only for Z3 proof reconstruction, so they really belong in SMT_Utils
boehmes
parents:
41127
diff
changeset

199 

40662  200 

201 
(* conversions *) 

202 

40663  203 
fun if_conv pred cv1 cv2 ct = if pred (Thm.term_of ct) then cv1 ct else cv2 ct 
40662  204 

40663  205 
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv 
40662  206 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

207 
fun if_exists_conv pred = if_true_conv (Term.exists_subterm pred) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

208 

40662  209 
fun binders_conv cv ctxt = 
210 
Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt 

211 

41126
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

212 
fun under_quant_conv cv ctxt = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

213 
let 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

214 
fun quant_conv inside ctxt cvs ct = 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

215 
(case Thm.term_of ct of 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

216 
Const (@{const_name All}, _) $ Abs _ => 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

217 
Conv.binder_conv (under_conv cvs) ctxt 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

218 
 Const (@{const_name Ex}, _) $ Abs _ => 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

219 
Conv.binder_conv (under_conv cvs) ctxt 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

220 
 _ => if inside then cv (ctxt, cvs) else Conv.all_conv) ct 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

221 
and under_conv cvs (cv, ctxt) = quant_conv true ctxt (cv :: cvs) 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

222 
in quant_conv false ctxt [] end 
e0bd443c0fdd
reordered SMT normalization code (etanormalization, lambda abstractions and partial functions will be dealt with on the term level);
boehmes
parents:
41124
diff
changeset

223 

40662  224 
fun prop_conv cv ct = 
225 
(case Thm.term_of ct of 

226 
@{const Trueprop} $ _ => Conv.arg_conv cv ct 

227 
 _ => raise CTERM ("not a property", [ct])) 

228 

229 
end 