author  wenzelm 
Thu, 26 May 1994 16:40:45 +0200  
changeset 398  41f279b477e2 
parent 210  49497bdf573e 
child 447  d1f827fa0a18 
permissions  rwrr 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

1 
(* Title: Pure/logic.ML 
0  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 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

20 
val dest_inclass: term > typ * class 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

21 
val dest_type: term > typ 
0  22 
val flatten_params: int > term > term 
23 
val freeze_vars: term > term 

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

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

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

27 
val list_implies: term list * term > term 

28 
val list_rename_params: string list * term > term 

29 
val mk_equals: term * term > term 

30 
val mk_flexpair: term * term > term 

31 
val mk_implies: term * term > term 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

32 
val mk_inclass: typ * class > term 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

33 
val mk_type: typ > term 
0  34 
val occs: term * term > bool 
35 
val rule_of: (term*term)list * term list * term > term 

36 
val set_rename_prefix: string > unit 

37 
val skip_flexpairs: term > term 

38 
val strip_assums_concl: term > term 

39 
val strip_assums_hyp: term > term list 

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

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

42 
val strip_imp_concl: term > term 

43 
val strip_imp_prems: term > term list 

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

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

46 
val thaw_vars: term > term 

47 
val varify: term > term 

48 
end; 

49 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

50 
functor LogicFun (structure Unify: UNIFY and Net:NET): LOGIC = 
0  51 
struct 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

52 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

53 
structure Sign = Unify.Sign; 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

54 
structure Type = Sign.Type; 
0  55 

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

57 

58 
(** equality **) 

59 

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

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

61 
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; 
0  62 

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

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

65 

66 
(** implies **) 

67 

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

69 

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

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

72 

73 
(** nested implications **) 

74 

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

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

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

78 

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

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

81 
 strip_imp_prems _ = []; 

82 

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

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

85 
 strip_imp_concl A = A : term; 

86 

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

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

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

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

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

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

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

94 

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

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

97 
 count_prems (_,n) = n; 

98 

99 
(** flexflex constraints **) 

100 

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

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

102 
fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; 
0  103 

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

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

106 

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

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

109 
fun list_flexpairs ([], A) = A 

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

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

112 

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

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

115 

116 
(*Remove and return flexflex pairs: 

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

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

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

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

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

122 

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

124 

125 
(*Discard flexflex pairs*) 

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

127 
skip_flexpairs C 

128 
 skip_flexpairs C = C; 

129 

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

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

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

133 
fun strip_horn A = 

134 
let val (tpairs,horn) = strip_flexpairs A 

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

136 

398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

137 
(** types as terms **) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

138 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

139 
fun mk_type ty = Const ("TYPE", itselfT ty); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

140 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

141 
fun dest_type (Const ("TYPE", Type ("itself", [ty]))) = ty 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

142 
 dest_type t = raise TERM ("dest_type", [t]); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

143 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

144 
(* class constraints: ( ty : c_class ) *) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

145 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

146 
fun mk_inclass (ty, c) = 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

147 
Const (Sign.const_of_class c, itselfT ty > propT) $ mk_type ty; 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

148 

41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

149 
fun dest_inclass (t as Const (c_class, _) $ ty) = 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

150 
((dest_type ty, Sign.class_of_const c_class) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

151 
handle TERM _ => raise TERM ("dest_inclass", [t])) 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

152 
 dest_inclass t = raise TERM ("dest_inclass", [t]); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

153 

0  154 

155 
(*** Lowlevel term operations ***) 

156 

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

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

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

160 
(case u of 

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

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

163 
 _ => false); 

164 

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

166 
fun close_form A = 

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

168 
A); 

169 

170 

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

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

173 
Type.freeze_vars T) 

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

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

176 
 freeze_vars(s$t) = freeze_vars s $ freeze_vars t 

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

178 
 freeze_vars(b) = b; 

179 

180 
(*Reverse the effect of freeze_vars*) 

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

182 
 thaw_vars(Free(a,T)) = 

183 
let val T' = Type.thaw_vars T 

184 
in case explode a of 

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

186 
in Var(ixn,T') end 

187 
 _ => Free(a,T') 

188 
end 

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

190 
 thaw_vars(s$t) = thaw_vars s $ thaw_vars t 

191 
 thaw_vars(b) = b; 

192 

193 

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

195 

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

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

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

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

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

201 
lev, length Us) 

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

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

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

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

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

207 
 incr (t,lev) = t 

208 
in incr(t,0) end; 

209 

210 
(*Make lifting functions from subgoal and increment. 

211 
lift_abs operates on tpairs (unification constraints) 

212 
lift_all operates on propositions *) 

213 
fun lift_fns (B,inc) = 

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

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

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

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

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

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

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

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

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

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

224 

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

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

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

228 
 strip_assums_hyp B = []; 

229 

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

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

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

233 
 strip_assums_concl B = B; 

234 

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

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

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

238 
 strip_params B = []; 

239 

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

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

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

243 
fun remove_params j n A = 

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

245 
else case A of 

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

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

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

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

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

251 
else A; 

252 

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

254 

255 
val auto_rename = ref false 

256 
and rename_prefix = ref "ka"; 

257 

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

259 
fun set_rename_prefix a = 

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

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

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

263 

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

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

266 
then res_inst_tac would not work properly.*) 

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

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

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

270 

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

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

273 
fun flatten_params n A = 

274 
let val params = strip_params A; 

275 
val vars = if !auto_rename 

276 
then rename_vars (!rename_prefix, params) 

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

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

279 
end; 

280 

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

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

283 
implies $ A $ list_rename_params (cs, B) 

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

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

286 
 list_rename_params (cs, B) = B; 

287 

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

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

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

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

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

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

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

295 

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

297 

298 

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

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

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

302 
fun assum_pairs A = 

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

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

305 
fun pairrev ([],pairs) = pairs 

306 
 pairrev (H::Hs,pairs) = 

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

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

309 
end; 

310 

311 

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

313 
without (?) everywhere*) 

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

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

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

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

318 
 varify (f$t) = varify f $ varify t 

319 
 varify t = t; 

320 

321 
end; 