author  boehmes 
Wed, 15 Dec 2010 10:12:44 +0100  
changeset 41127  2ea84c8535c6 
parent 41126  e0bd443c0fdd 
child 41172  a17c2d669c40 
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 
40662  31 

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

35 
val destT2: ctyp > ctyp 

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

37 
val instT: ctyp > ctyp * cterm > cterm 

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

39 

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

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

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

47 
val mk_cprop: cterm > cterm 

48 
val dest_cprop: cterm > cterm 

49 
val mk_cequals: cterm > cterm > cterm 

50 

41123  51 
(*conversions*) 
40662  52 
val if_conv: (term > bool) > conv > conv > conv 
53 
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

54 
val if_exists_conv: (term > bool) > conv > conv 
40662  55 
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

56 
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

57 
Proof.context > conv 
40662  58 
val prop_conv: conv > conv 
59 
end 

60 

61 
structure SMT_Utils: SMT_UTILS = 

62 
struct 

63 

41123  64 
(* basic combinators *) 
65 

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

68 
in rep end 

69 

70 
fun repeat_yield f = 

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

72 
in rep end 

73 

74 

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

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

76 

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

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

78 

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

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

80 

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

81 
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

82 
 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

83 

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

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

85 

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

86 
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

87 

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

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

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

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

91 

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

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

93 
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

94 

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

95 
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

96 

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

97 
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

98 

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

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

100 
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

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

102 

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

103 
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

104 
(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

105 
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

106 
 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

107 

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

108 

40663  109 
(* types *) 
110 

111 
val dest_funT = 

112 
let 

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

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

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

116 
in dest [] end 

117 

118 

40662  119 
(* terms *) 
120 

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

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

123 

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

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

126 

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

127 
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

128 
(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

129 
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

130 
 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

131 
 _ => 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

132 

40662  133 

134 
(* patterns and instantiations *) 

135 

136 
fun mk_const_pat thy name destT = 

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

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

139 

140 
val destT1 = hd o Thm.dest_ctyp 

141 
val destT2 = hd o tl o Thm.dest_ctyp 

142 

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

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

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

146 

147 

148 
(* certified terms *) 

149 

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

151 

40663  152 
fun typ_of ct = #T (Thm.rep_cterm ct) 
153 

40662  154 
fun dest_cabs ct ctxt = 
155 
(case Thm.term_of ct of 

156 
Abs _ => 

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

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

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

160 

161 
val dest_all_cabs = repeat_yield (try o dest_cabs) 

162 

163 
fun dest_cbinder ct ctxt = 

164 
(case Thm.term_of ct of 

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

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

167 

168 
val dest_all_cbinders = repeat_yield (try o dest_cbinder) 

169 

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

172 
fun dest_cprop ct = 

173 
(case Thm.term_of ct of 

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

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

176 

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

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

179 

180 

181 
(* conversions *) 

182 

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

40663  185 
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv 
40662  186 

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

187 
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

188 

40662  189 
fun binders_conv cv ctxt = 
190 
Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt 

191 

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

192 
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

193 
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

194 
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

195 
(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

196 
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

197 
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

198 
 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

199 
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

200 
 _ => 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

201 
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

202 
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

203 

40662  204 
fun prop_conv cv ct = 
205 
(case Thm.term_of ct of 

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

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

208 

209 
end 