author  boehmes 
Wed, 15 Dec 2010 08:39:24 +0100  
changeset 41124  1de17a2de5ad 
parent 41123  3bb9be510a9d 
child 41126  e0bd443c0fdd 
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 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

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

17 
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

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

19 
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

20 
val dict_lookup: 'a dict > class > 'a list 
1de17a2de5ad
moved SMT classes and dictionary functions to SMT_Utils
boehmes
parents:
41123
diff
changeset

21 

41123  22 
(*types*) 
40663  23 
val dest_funT: int > typ > typ list * typ 
24 

41123  25 
(*terms*) 
40662  26 
val dest_conj: term > term * term 
27 
val dest_disj: term > term * term 

28 

41123  29 
(*patterns and instantiations*) 
40662  30 
val mk_const_pat: theory > string > (ctyp > 'a) > 'a * cterm 
31 
val destT1: ctyp > ctyp 

32 
val destT2: ctyp > ctyp 

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

34 
val instT: ctyp > ctyp * cterm > cterm 

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

36 

41123  37 
(*certified terms*) 
40662  38 
val certify: Proof.context > term > cterm 
40663  39 
val typ_of: cterm > typ 
40662  40 
val dest_cabs: cterm > Proof.context > cterm * Proof.context 
41 
val dest_all_cabs: cterm > Proof.context > cterm * Proof.context 

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

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

44 
val mk_cprop: cterm > cterm 

45 
val dest_cprop: cterm > cterm 

46 
val mk_cequals: cterm > cterm > cterm 

47 

41123  48 
(*conversions*) 
40662  49 
val if_conv: (term > bool) > conv > conv > conv 
50 
val if_true_conv: (term > bool) > conv > conv 

51 
val binders_conv: (Proof.context > conv) > Proof.context > conv 

52 
val prop_conv: conv > conv 

53 
end 

54 

55 
structure SMT_Utils: SMT_UTILS = 

56 
struct 

57 

41123  58 
(* basic combinators *) 
59 

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

62 
in rep end 

63 

64 
fun repeat_yield f = 

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

66 
in rep end 

67 

68 

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

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

70 

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

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

72 

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

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

74 

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

75 
type 'a dict = (class * 'a) Ord_List.T 
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 
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

78 

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

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

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

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

82 

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

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

84 
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

85 

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

86 
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

87 

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

88 
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

89 

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

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

91 
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

92 
in map_filter match d end 
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 

40663  95 
(* types *) 
96 

97 
val dest_funT = 

98 
let 

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

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

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

102 
in dest [] end 

103 

104 

40662  105 
(* terms *) 
106 

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

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

109 

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

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

112 

113 

114 
(* patterns and instantiations *) 

115 

116 
fun mk_const_pat thy name destT = 

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

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

119 

120 
val destT1 = hd o Thm.dest_ctyp 

121 
val destT2 = hd o tl o Thm.dest_ctyp 

122 

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

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

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

126 

127 

128 
(* certified terms *) 

129 

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

131 

40663  132 
fun typ_of ct = #T (Thm.rep_cterm ct) 
133 

40662  134 
fun dest_cabs ct ctxt = 
135 
(case Thm.term_of ct of 

136 
Abs _ => 

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

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

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

140 

141 
val dest_all_cabs = repeat_yield (try o dest_cabs) 

142 

143 
fun dest_cbinder ct ctxt = 

144 
(case Thm.term_of ct of 

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

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

147 

148 
val dest_all_cbinders = repeat_yield (try o dest_cbinder) 

149 

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

152 
fun dest_cprop ct = 

153 
(case Thm.term_of ct of 

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

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

156 

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

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

159 

160 

161 
(* conversions *) 

162 

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

40663  165 
fun if_true_conv pred cv = if_conv pred cv Conv.all_conv 
40662  166 

167 
fun binders_conv cv ctxt = 

168 
Conv.binder_conv (binders_conv cv o snd) ctxt else_conv cv ctxt 

169 

170 
fun prop_conv cv ct = 

171 
(case Thm.term_of ct of 

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

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

174 

175 
end 