author  wenzelm 
Wed, 08 Mar 2017 10:50:59 +0100  
changeset 65151  a7394aa4d21c 
parent 60642  48dd1cefb4ae 
permissions  rwrr 
58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

1 
(* Title: HOL/Library/Old_SMT/old_smt_utils.ML 
40662  2 
Author: Sascha Boehme, TU Muenchen 
3 

4 
General utility functions. 

5 
*) 

6 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

7 
signature OLD_SMT_UTILS = 
40662  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 dest_cabs: cterm > Proof.context > cterm * Proof.context 
43 
val dest_all_cabs: cterm > Proof.context > cterm * Proof.context 

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

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

46 
val mk_cprop: cterm > cterm 

47 
val dest_cprop: cterm > cterm 

48 
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

49 
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

50 
val prop_of: thm > term 
40662  51 

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

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

57 
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

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

61 

58058
1a0b18176548
add 'old_' prefix to SMT file names; add 'Old_' to ML module names;
blanchet
parents:
58057
diff
changeset

62 
structure Old_SMT_Utils: OLD_SMT_UTILS = 
40662  63 
struct 
64 

41123  65 
(* basic combinators *) 
66 

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

69 
in rep end 

70 

71 
fun repeat_yield f = 

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

73 
in rep end 

74 

75 

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

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

77 

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

78 
type class = string list 
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 
val basicC = [] 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

81 

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

82 
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

83 
 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

84 

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

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

86 

41301
0a00fd2f5351
derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)
boehmes
parents:
41280
diff
changeset

87 
fun class_ord ((cs1, _), (cs2, _)) = 
0a00fd2f5351
derived SMT solver classes override inherited properties (properties of derived classes have a higher priority than properties of base classes)
boehmes
parents:
41280
diff
changeset

88 
rev_order (list_ord fast_string_ord (cs1, cs2)) 
41124
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

89 

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

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

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

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

93 

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

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

95 
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

96 

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

97 
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

98 

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

99 
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

100 

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

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

102 
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

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

104 

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

105 
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

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

107 
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

108 
 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

109 

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

110 

40663  111 
(* types *) 
112 

113 
val dest_funT = 

114 
let 

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

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

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

118 
in dest [] end 

119 

120 

40662  121 
(* terms *) 
122 

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

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

125 

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

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

128 

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

129 
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

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

131 
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

132 
 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

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

134 

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

135 
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

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

137 
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

138 
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

139 
 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

140 
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

141 
 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

142 
 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

143 
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

144 

40662  145 

146 
(* patterns and instantiations *) 

147 

148 
fun mk_const_pat thy name destT = 

59621
291934bac95e
Thm.cterm_of and Thm.ctyp_of operate on local context;
wenzelm
parents:
59590
diff
changeset

149 
let val cpat = Thm.global_cterm_of thy (Const (name, Sign.the_const_type thy name)) 
59586  150 
in (destT (Thm.ctyp_of_cterm cpat), cpat) end 
40662  151 

152 
val destT1 = hd o Thm.dest_ctyp 

153 
val destT2 = hd o tl o Thm.dest_ctyp 

154 

60642
48dd1cefb4ae
simplified Thm.instantiate and derivatives: the LHS refers to noncertified variables  this merely serves as index into already certified structures (or is ignored);
wenzelm
parents:
59634
diff
changeset

155 
fun instTs cUs (cTs, ct) = Thm.instantiate_cterm (map (dest_TVar o Thm.typ_of) cTs ~~ cUs, []) ct 
40662  156 
fun instT cU (cT, ct) = instTs [cU] ([cT], ct) 
59586  157 
fun instT' ct = instT (Thm.ctyp_of_cterm ct) 
40662  158 

159 

160 
(* certified terms *) 

161 

162 
fun dest_cabs ct ctxt = 

163 
(case Thm.term_of ct of 

164 
Abs _ => 

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

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

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

168 

169 
val dest_all_cabs = repeat_yield (try o dest_cabs) 

170 

171 
fun dest_cbinder ct ctxt = 

172 
(case Thm.term_of ct of 

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

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

175 

176 
val dest_all_cbinders = repeat_yield (try o dest_cbinder) 

177 

59634  178 
val mk_cprop = Thm.apply (Thm.cterm_of @{context} @{const Trueprop}) 
40662  179 

180 
fun dest_cprop ct = 

181 
(case Thm.term_of ct of 

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

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

184 

56245  185 
val equals = mk_const_pat @{theory} @{const_name Pure.eq} destT1 
40662  186 
fun mk_cequals ct cu = Thm.mk_binop (instT' ct equals) ct cu 
187 

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

188 
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

189 
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

190 
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

191 

40662  192 

193 
(* conversions *) 

194 

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

40663  197 
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv 
40662  198 

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

199 
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

200 

40662  201 
fun binders_conv cv ctxt = 
202 
Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt 

203 

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

204 
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

205 
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

206 
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

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

208 
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

209 
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

210 
 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

211 
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

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

213 
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

214 
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

215 

40662  216 
fun prop_conv cv ct = 
217 
(case Thm.term_of ct of 

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

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

220 

221 
end 