author  paulson 
Tue, 20 May 1997 11:49:57 +0200  
changeset 3245  241838c01caf 
parent 2112  3902e9af752f 
child 3302  404fe31fd8d2 
permissions  rwrr 
2112  1 
(* 
2 
* Derived efficient cterm destructors. 

3 
**) 

4 

5 
structure Dcterm : 

6 
sig 

7 
val mk_conj : cterm * cterm > cterm 

8 
val mk_disj : cterm * cterm > cterm 

9 
val mk_select : cterm * cterm > cterm 

10 
val mk_forall : cterm * cterm > cterm 

11 
val mk_exists : cterm * cterm > cterm 

12 

13 
val dest_conj : cterm > cterm * cterm 

14 
val dest_const : cterm > {Name:string, Ty:typ} 

15 
val dest_disj : cterm > cterm * cterm 

16 
val dest_eq : cterm > cterm * cterm 

17 
val dest_exists : cterm > cterm * cterm 

18 
val dest_forall : cterm > cterm * cterm 

19 
val dest_imp : cterm > cterm * cterm 

20 
val dest_let : cterm > cterm * cterm 

21 
val dest_neg : cterm > cterm 

22 
val dest_pair : cterm > cterm * cterm 

23 
val dest_select : cterm > cterm * cterm 

24 
val dest_var : cterm > {Name:string, Ty:typ} 

25 
val is_abs : cterm > bool 

26 
val is_comb : cterm > bool 

27 
val is_conj : cterm > bool 

28 
val is_cons : cterm > bool 

29 
val is_const : cterm > bool 

30 
val is_disj : cterm > bool 

31 
val is_eq : cterm > bool 

32 
val is_exists : cterm > bool 

33 
val is_forall : cterm > bool 

34 
val is_imp : cterm > bool 

35 
val is_let : cterm > bool 

36 
val is_neg : cterm > bool 

37 
val is_pair : cterm > bool 

38 
val is_select : cterm > bool 

39 
val is_var : cterm > bool 

40 
val list_mk_abs : cterm list > cterm > cterm 

41 
val list_mk_exists : cterm list * cterm > cterm 

42 
val list_mk_forall : cterm list * cterm > cterm 

43 
val list_mk_disj : cterm list > cterm 

44 
val strip_abs : cterm > cterm list * cterm 

45 
val strip_comb : cterm > cterm * cterm list 

46 
val strip_conj : cterm > cterm list 

47 
val strip_disj : cterm > cterm list 

48 
val strip_exists : cterm > cterm list * cterm 

49 
val strip_forall : cterm > cterm list * cterm 

50 
val strip_imp : cterm > cterm list * cterm 

51 
val strip_pair : cterm > cterm list 

52 
val drop_prop : cterm > cterm 

53 
val mk_prop : cterm > cterm 

54 
end = 

55 
struct 

56 

57 
fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg}; 

58 

59 
(* 

60 
* General support routines 

61 
**) 

62 
val can = Utils.can; 

63 
val quote = Utils.quote; 

64 
fun swap (x,y) = (y,x); 

65 

66 
fun itlist f L base_value = 

67 
let fun it [] = base_value 

68 
 it (a::rst) = f a (it rst) 

69 
in it L 

70 
end; 

71 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset

72 
val end_itlist = Utils.end_itlist; 
2112  73 

74 

75 
(* 

76 
* Some simple constructor functions. 

77 
**) 

78 

79 
fun mk_const sign pr = cterm_of sign (Const pr); 

80 
val mk_hol_const = mk_const (sign_of HOL.thy); 

81 

82 
fun mk_select (r as (Bvar,Body)) = 

83 
let val ty = #T(rep_cterm Bvar) 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset

84 
val c = mk_hol_const("Eps", (ty > HOLogic.boolT) > ty) 
2112  85 
in capply c (uncurry cabs r) 
86 
end; 

87 

88 
fun mk_forall (r as (Bvar,Body)) = 

89 
let val ty = #T(rep_cterm Bvar) 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset

90 
val c = mk_hol_const("All", (ty > HOLogic.boolT) > HOLogic.boolT) 
2112  91 
in capply c (uncurry cabs r) 
92 
end; 

93 

94 
fun mk_exists (r as (Bvar,Body)) = 

95 
let val ty = #T(rep_cterm Bvar) 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset

96 
val c = mk_hol_const("Ex", (ty > HOLogic.boolT) > HOLogic.boolT) 
2112  97 
in capply c (uncurry cabs r) 
98 
end; 

99 

100 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset

101 
local val c = mk_hol_const("op &", HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 
2112  102 
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2 
103 
end; 

104 

3245
241838c01caf
Removal of redundant code (unused or already present in Isabelle.
paulson
parents:
2112
diff
changeset

105 
local val c = mk_hol_const("op ", HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 
2112  106 
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2 
107 
end; 

108 

109 

110 
(* 

111 
* The primitives. 

112 
**) 

113 
fun dest_const ctm = 

114 
(case #t(rep_cterm ctm) 

115 
of Const(s,ty) => {Name = s, Ty = ty} 

116 
 _ => raise ERR "dest_const" "not a constant"); 

117 

118 
fun dest_var ctm = 

119 
(case #t(rep_cterm ctm) 

120 
of Var((s,i),ty) => {Name=s, Ty=ty} 

121 
 Free(s,ty) => {Name=s, Ty=ty} 

122 
 _ => raise ERR "dest_var" "not a variable"); 

123 

124 

125 
(* 

126 
* Derived destructor operations. 

127 
**) 

128 

129 
fun dest_monop expected tm = 

130 
let exception Fail 

131 
val (c,N) = dest_comb tm 

132 
in if (#Name(dest_const c) = expected) then N else raise Fail 

133 
end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected); 

134 

135 
fun dest_binop expected tm = 

136 
let val (M,N) = dest_comb tm 

137 
in (dest_monop expected M, N) 

138 
end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected); 

139 

140 
(* For "ifthenelse" 

141 
fun dest_triop expected tm = 

142 
let val (MN,P) = dest_comb tm 

143 
val (M,N) = dest_binop expected MN 

144 
in (M,N,P) 

145 
end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected); 

146 
*) 

147 

148 
fun dest_binder expected tm = 

149 
dest_abs(dest_monop expected tm) 

150 
handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected); 

151 

152 

153 
val dest_neg = dest_monop "not" 

154 
val dest_pair = dest_binop "Pair"; 

155 
val dest_eq = dest_binop "op =" 

156 
val dest_imp = dest_binop "op >" 

157 
val dest_conj = dest_binop "op &" 

158 
val dest_disj = dest_binop "op " 

159 
val dest_cons = dest_binop "op #" 

160 
val dest_let = swap o dest_binop "Let"; 

161 
(* val dest_cond = dest_triop "if" *) 

162 
val dest_select = dest_binder "Eps" 

163 
val dest_exists = dest_binder "Ex" 

164 
val dest_forall = dest_binder "All" 

165 

166 
(* Query routines *) 

167 

168 
val is_var = can dest_var 

169 
val is_const = can dest_const 

170 
val is_comb = can dest_comb 

171 
val is_abs = can dest_abs 

172 
val is_eq = can dest_eq 

173 
val is_imp = can dest_imp 

174 
val is_select = can dest_select 

175 
val is_forall = can dest_forall 

176 
val is_exists = can dest_exists 

177 
val is_neg = can dest_neg 

178 
val is_conj = can dest_conj 

179 
val is_disj = can dest_disj 

180 
(* val is_cond = can dest_cond *) 

181 
val is_pair = can dest_pair 

182 
val is_let = can dest_let 

183 
val is_cons = can dest_cons 

184 

185 

186 
(* 

187 
* Iterated creation. 

188 
**) 

189 
val list_mk_abs = itlist cabs; 

190 

191 
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t; 

192 
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t; 

193 
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm)) 

194 

195 
(* 

196 
* Iterated destruction. (To the "right" in a term.) 

197 
**) 

198 
fun strip break tm = 

199 
let fun dest (p as (ctm,accum)) = 

200 
let val (M,N) = break ctm 

201 
in dest (N, M::accum) 

202 
end handle _ => p 

203 
in dest (tm,[]) 

204 
end; 

205 

206 
fun rev2swap (x,l) = (rev l, x); 

207 

208 
val strip_comb = strip (swap o dest_comb) (* Goes to the "left" *) 

209 
val strip_imp = rev2swap o strip dest_imp 

210 
val strip_abs = rev2swap o strip dest_abs 

211 
val strip_forall = rev2swap o strip dest_forall 

212 
val strip_exists = rev2swap o strip dest_exists 

213 

214 
val strip_conj = rev o (op::) o strip dest_conj 

215 
val strip_disj = rev o (op::) o strip dest_disj 

216 
val strip_pair = rev o (op::) o strip dest_pair; 

217 

218 

219 
(* 

220 
* Going into and out of prop 

221 
**) 

222 
local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop") 

223 
in fun mk_prop ctm = 

224 
case (#t(rep_cterm ctm)) 

225 
of (Const("Trueprop",_)$_) => ctm 

226 
 _ => capply prop ctm 

227 
end; 

228 

229 
fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm; 

230 

231 
end; 