author  lcp 
Tue, 18 Jan 1994 15:57:40 +0100  
changeset 230  ec8a2b6aa8a7 
parent 210  49497bdf573e 
child 398  41f279b477e2 
permissions  rwrr 
0  1 
(* Title: logic 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

4 
Copyright Cambridge University 1992 

5 

6 
Supporting code for defining the abstract type "thm" 

7 
*) 

8 

9 
infix occs; 

10 

11 
signature LOGIC = 

12 
sig 

13 
val assum_pairs: term > (term*term)list 

14 
val auto_rename: bool ref 

15 
val close_form: term > term 

16 
val count_prems: term * int > int 

17 
val dest_equals: term > term * term 

18 
val dest_flexpair: term > term * term 

19 
val dest_implies: term > term * term 

20 
val flatten_params: int > term > term 

21 
val freeze_vars: term > term 

22 
val incr_indexes: typ list * int > term > term 

23 
val lift_fns: term * int > (term > term) * (term > term) 

24 
val list_flexpairs: (term*term)list * term > term 

25 
val list_implies: term list * term > term 

26 
val list_rename_params: string list * term > term 

27 
val mk_equals: term * term > term 

28 
val mk_flexpair: term * term > term 

29 
val mk_implies: term * term > term 

30 
val occs: term * term > bool 

31 
val rule_of: (term*term)list * term list * term > term 

32 
val set_rename_prefix: string > unit 

33 
val skip_flexpairs: term > term 

34 
val strip_assums_concl: term > term 

35 
val strip_assums_hyp: term > term list 

36 
val strip_flexpairs: term > (term*term)list * term 

37 
val strip_horn: term > (term*term)list * term list * term 

38 
val strip_imp_concl: term > term 

39 
val strip_imp_prems: term > term list 

40 
val strip_params: term > (string * typ) list 

41 
val strip_prems: int * term list * term > term list * term 

42 
val thaw_vars: term > term 

43 
val varify: term > term 

44 
end; 

45 

210
49497bdf573e
commented out sig constraint of functor (for debugging purposes);
wenzelm
parents:
64
diff
changeset

46 
functor LogicFun (structure Unify: UNIFY and Net:NET)(* : LOGIC *) = (* FIXME *) 
0  47 
struct 
48 
structure Type = Unify.Sign.Type; 

49 

50 
(*** Abstract syntax operations on the metaconnectives ***) 

51 

52 
(** equality **) 

53 

64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

54 
(*Make an equality.*) 
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

55 
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; 
0  56 

57 
fun dest_equals (Const("==",_) $ t $ u) = (t,u) 

58 
 dest_equals t = raise TERM("dest_equals", [t]); 

59 

60 
(** implies **) 

61 

62 
fun mk_implies(A,B) = implies $ A $ B; 

63 

64 
fun dest_implies (Const("==>",_) $ A $ B) = (A,B) 

65 
 dest_implies A = raise TERM("dest_implies", [A]); 

66 

67 
(** nested implications **) 

68 

69 
(* [A1,...,An], B goes to A1==>...An==>B *) 

70 
fun list_implies ([], B) = B : term 

71 
 list_implies (A::AS, B) = implies $ A $ list_implies(AS,B); 

72 

73 
(* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) 

74 
fun strip_imp_prems (Const("==>", _) $ A $ B) = A :: strip_imp_prems B 

75 
 strip_imp_prems _ = []; 

76 

77 
(* A1==>...An==>B goes to B, where B is not an implication *) 

78 
fun strip_imp_concl (Const("==>", _) $ A $ B) = strip_imp_concl B 

79 
 strip_imp_concl A = A : term; 

80 

81 
(*Strip and return premises: (i, [], A1==>...Ai==>B) 

82 
goes to ([Ai, A(i1),...,A1] , B) (REVERSED) 

83 
if i<0 or else i too big then raises TERM*) 

84 
fun strip_prems (0, As, B) = (As, B) 

85 
 strip_prems (i, As, Const("==>", _) $ A $ B) = 

86 
strip_prems (i1, A::As, B) 

87 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 

88 

89 
(*Count premises  quicker than (length ostrip_prems) *) 

90 
fun count_prems (Const("==>", _) $ A $ B, n) = count_prems (B,n+1) 

91 
 count_prems (_,n) = n; 

92 

93 
(** flexflex constraints **) 

94 

64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

95 
(*Make a constraint.*) 
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

96 
fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; 
0  97 

98 
fun dest_flexpair (Const("=?=",_) $ t $ u) = (t,u) 

99 
 dest_flexpair t = raise TERM("dest_flexpair", [t]); 

100 

101 
(*make flexflex antecedents: ( [(a1,b1),...,(an,bn)] , C ) 

102 
goes to (a1=?=b1) ==>...(an=?=bn)==>C *) 

103 
fun list_flexpairs ([], A) = A 

104 
 list_flexpairs ((t,u)::pairs, A) = 

105 
implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A); 

106 

107 
(*Make the objectrule tpairs==>As==>B *) 

108 
fun rule_of (tpairs, As, B) = list_flexpairs(tpairs, list_implies(As, B)); 

109 

110 
(*Remove and return flexflex pairs: 

111 
(a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C ) 

112 
[Tail recursive in order to return a pair of results] *) 

113 
fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) = 

114 
strip_flex_aux ((t,u)::pairs, C) 

115 
 strip_flex_aux (pairs,C) = (rev pairs, C); 

116 

117 
fun strip_flexpairs A = strip_flex_aux([], A); 

118 

119 
(*Discard flexflex pairs*) 

120 
fun skip_flexpairs (Const("==>", _) $ (Const("=?=",_)$_$_) $ C) = 

121 
skip_flexpairs C 

122 
 skip_flexpairs C = C; 

123 

124 
(*strip a proof state (Horn clause): 

125 
(a1==b1)==>...(am==bm)==>B1==>...Bn==>C 

126 
goes to ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C) *) 

127 
fun strip_horn A = 

128 
let val (tpairs,horn) = strip_flexpairs A 

129 
in (tpairs, strip_imp_prems horn, strip_imp_concl horn) end; 

130 

131 

132 
(*** Lowlevel term operations ***) 

133 

134 
(*Does t occur in u? Or is alphaconvertible to u? 

135 
The term t must contain no loose bound variables*) 

136 
fun t occs u = (t aconv u) orelse 

137 
(case u of 

138 
Abs(_,_,body) => t occs body 

139 
 f$t' => t occs f orelse t occs t' 

140 
 _ => false); 

141 

142 
(*Close up a formula over all free variables by quantification*) 

143 
fun close_form A = 

144 
list_all_free (map dest_Free (sort atless (term_frees A)), 

145 
A); 

146 

147 

148 
(*Freeze all (T)Vars by turning them into (T)Frees*) 

149 
fun freeze_vars(Var(ixn,T)) = Free(Syntax.string_of_vname ixn, 

150 
Type.freeze_vars T) 

151 
 freeze_vars(Const(a,T)) = Const(a,Type.freeze_vars T) 

152 
 freeze_vars(Free(a,T)) = Free(a,Type.freeze_vars T) 

153 
 freeze_vars(s$t) = freeze_vars s $ freeze_vars t 

154 
 freeze_vars(Abs(a,T,t)) = Abs(a,Type.freeze_vars T,freeze_vars t) 

155 
 freeze_vars(b) = b; 

156 

157 
(*Reverse the effect of freeze_vars*) 

158 
fun thaw_vars(Const(a,T)) = Const(a,Type.thaw_vars T) 

159 
 thaw_vars(Free(a,T)) = 

160 
let val T' = Type.thaw_vars T 

161 
in case explode a of 

162 
"?"::vn => let val (ixn,_) = Syntax.scan_varname vn 

163 
in Var(ixn,T') end 

164 
 _ => Free(a,T') 

165 
end 

166 
 thaw_vars(Abs(a,T,t)) = Abs(a,Type.thaw_vars T, thaw_vars t) 

167 
 thaw_vars(s$t) = thaw_vars s $ thaw_vars t 

168 
 thaw_vars(b) = b; 

169 

170 

171 
(*** Specialized operations for resolution... ***) 

172 

173 
(*For all variables in the term, increment indexnames and lift over the Us 

174 
result is ?Gidx(B.(lev+n1),...,B.lev) where lev is abstraction level *) 

175 
fun incr_indexes (Us: typ list, inc:int) t = 

176 
let fun incr (Var ((a,i), T), lev) = 

177 
Unify.combound (Var((a, i+inc), Us> incr_tvar inc T), 

178 
lev, length Us) 

179 
 incr (Abs (a,T,body), lev) = 

180 
Abs (a, incr_tvar inc T, incr(body,lev+1)) 

181 
 incr (Const(a,T),_) = Const(a, incr_tvar inc T) 

182 
 incr (Free(a,T),_) = Free(a, incr_tvar inc T) 

183 
 incr (f$t, lev) = incr(f,lev) $ incr(t,lev) 

184 
 incr (t,lev) = t 

185 
in incr(t,0) end; 

186 

187 
(*Make lifting functions from subgoal and increment. 

188 
lift_abs operates on tpairs (unification constraints) 

189 
lift_all operates on propositions *) 

190 
fun lift_fns (B,inc) = 

191 
let fun lift_abs (Us, Const("==>", _) $ _ $ B) u = lift_abs (Us,B) u 

192 
 lift_abs (Us, Const("all",_)$Abs(a,T,t)) u = 

193 
Abs(a, T, lift_abs (T::Us, t) u) 

194 
 lift_abs (Us, _) u = incr_indexes(rev Us, inc) u 

195 
fun lift_all (Us, Const("==>", _) $ A $ B) u = 

196 
implies $ A $ lift_all (Us,B) u 

197 
 lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 

198 
all T $ Abs(a, T, lift_all (T::Us,t) u) 

199 
 lift_all (Us, _) u = incr_indexes(rev Us, inc) u; 

200 
in (lift_abs([],B), lift_all([],B)) end; 

201 

202 
(*Strips assumptions in goal, yielding list of hypotheses. *) 

203 
fun strip_assums_hyp (Const("==>", _) $ H $ B) = H :: strip_assums_hyp B 

204 
 strip_assums_hyp (Const("all",_)$Abs(a,T,t)) = strip_assums_hyp t 

205 
 strip_assums_hyp B = []; 

206 

207 
(*Strips assumptions in goal, yielding conclusion. *) 

208 
fun strip_assums_concl (Const("==>", _) $ H $ B) = strip_assums_concl B 

209 
 strip_assums_concl (Const("all",_)$Abs(a,T,t)) = strip_assums_concl t 

210 
 strip_assums_concl B = B; 

211 

212 
(*Make a list of all the parameters in a subgoal, even if nested*) 

213 
fun strip_params (Const("==>", _) $ H $ B) = strip_params B 

214 
 strip_params (Const("all",_)$Abs(a,T,t)) = (a,T) :: strip_params t 

215 
 strip_params B = []; 

216 

217 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 

218 
where j is the total number of parameters (precomputed) 

219 
If n>0 then deletes assumption n. *) 

220 
fun remove_params j n A = 

221 
if j=0 andalso n<=0 then A (*nothing left to do...*) 

222 
else case A of 

223 
Const("==>", _) $ H $ B => 

224 
if n=1 then (remove_params j (n1) B) 

225 
else implies $ (incr_boundvars j H) $ (remove_params j (n1) B) 

226 
 Const("all",_)$Abs(a,T,t) => remove_params (j1) n t 

227 
 _ => if n>0 then raise TERM("remove_params", [A]) 

228 
else A; 

229 

230 
(** Autorenaming of parameters in subgoals **) 

231 

232 
val auto_rename = ref false 

233 
and rename_prefix = ref "ka"; 

234 

235 
(*rename_prefix is not exported; it is set by this function.*) 

236 
fun set_rename_prefix a = 

237 
if a<>"" andalso forall is_letter (explode a) 

238 
then (rename_prefix := a; auto_rename := true) 

239 
else error"rename prefix must be nonempty and consist of letters"; 

240 

241 
(*Makes parameters in a goal have distinctive names (not guaranteed unique!) 

242 
A name clash could cause the printer to rename bound vars; 

243 
then res_inst_tac would not work properly.*) 

244 
fun rename_vars (a, []) = [] 

245 
 rename_vars (a, (_,T)::vars) = 

246 
(a,T) :: rename_vars (bump_string a, vars); 

247 

248 
(*Move all parameters to the front of the subgoal, renaming them apart; 

249 
if n>0 then deletes assumption n. *) 

250 
fun flatten_params n A = 

251 
let val params = strip_params A; 

252 
val vars = if !auto_rename 

253 
then rename_vars (!rename_prefix, params) 

254 
else variantlist(map #1 params,[]) ~~ map #2 params 

255 
in list_all (vars, remove_params (length vars) n A) 

256 
end; 

257 

258 
(*Makes parameters in a goal have the names supplied by the list cs.*) 

259 
fun list_rename_params (cs, Const("==>", _) $ A $ B) = 

260 
implies $ A $ list_rename_params (cs, B) 

261 
 list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 

262 
all T $ Abs(c, T, list_rename_params (cs, t)) 

263 
 list_rename_params (cs, B) = B; 

264 

265 
(*Strips assumptions in goal yielding ( [Hn,...,H1], [xm,...,x1], B ) 

266 
where H1,...,Hn are the hypotheses and x1...xm are the parameters. *) 

267 
fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 

268 
strip_assums_aux (H::Hs, params, B) 

269 
 strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) = 

270 
strip_assums_aux (Hs, (a,T)::params, t) 

271 
 strip_assums_aux (Hs, params, B) = (Hs, params, B); 

272 

273 
fun strip_assums A = strip_assums_aux ([],[],A); 

274 

275 

276 
(*Produces disagreement pairs, one for each assumption proof, in order. 

277 
A is the first premise of the lifted rule, and thus has the form 

278 
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B) *) 

279 
fun assum_pairs A = 

280 
let val (Hs, params, B) = strip_assums A 

281 
val D = Unify.rlist_abs(params, B) 

282 
fun pairrev ([],pairs) = pairs 

283 
 pairrev (H::Hs,pairs) = 

284 
pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs) 

285 
in pairrev (Hs,[]) (*WAS: map pair (rev Hs) *) 

286 
end; 

287 

288 

289 
(*Converts Frees to Vars and TFrees to TVars so that axioms can be written 

290 
without (?) everywhere*) 

291 
fun varify (Const(a,T)) = Const(a, Type.varifyT T) 

292 
 varify (Free(a,T)) = Var((a,0), Type.varifyT T) 

293 
 varify (Var(ixn,T)) = Var(ixn, Type.varifyT T) 

294 
 varify (Abs (a,T,body)) = Abs (a, Type.varifyT T, varify body) 

295 
 varify (f$t) = varify f $ varify t 

296 
 varify t = t; 

297 

298 
end; 