author  wenzelm 
Sun, 30 Jul 2000 12:48:55 +0200  
changeset 9460  53d7ad5bec39 
parent 5041  a1d0a6d555cd 
child 9483  708a8a05497d 
permissions  rwrr 
9460  1 
(* Title: Pure/logic.ML 
0  2 
ID: $Id$ 
9460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
5 

9460  6 
Abstract syntax operations of the Pure metalogic. 
0  7 
*) 
8 

9 
infix occs; 

10 

9460  11 
signature LOGIC = 
4345  12 
sig 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

13 
val is_all : term > bool 
9460  14 
val mk_equals : term * term > term 
15 
val dest_equals : term > term * term 

3963
29c5ec9ecbaa
Corrected alphabetical order of entries in signature.
nipkow
parents:
3915
diff
changeset

16 
val is_equals : term > bool 
9460  17 
val mk_implies : term * term > term 
18 
val dest_implies : term > term * term 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

19 
val is_implies : term > bool 
9460  20 
val list_implies : term list * term > term 
21 
val strip_imp_prems : term > term list 

22 
val strip_imp_concl : term > term 

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

24 
val count_prems : term * int > int 

25 
val mk_flexpair : term * term > term 

26 
val dest_flexpair : term > term * term 

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

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

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

30 
val skip_flexpairs : term > term 

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

32 
val mk_cond_defpair : term list > term * term > string * term 

33 
val mk_defpair : term * term > string * term 

34 
val mk_type : typ > term 

35 
val dest_type : term > typ 

36 
val mk_inclass : typ * class > term 

37 
val dest_inclass : term > typ * class 

38 
val goal_const : term 

39 
val mk_goal : term > term 

40 
val dest_goal : term > term 

41 
val occs : term * term > bool 

42 
val close_form : term > term 

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

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

45 
val strip_assums_hyp : term > term list 

46 
val strip_assums_concl: term > term 

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

48 
val flatten_params : int > term > term 

49 
val auto_rename : bool ref 

50 
val set_rename_prefix : string > unit 

0  51 
val list_rename_params: string list * term > term 
9460  52 
val assum_pairs : term > (term*term)list 
53 
val varify : term > term 

54 
val unvarify : term > term 

4345  55 
end; 
0  56 

1500  57 
structure Logic : LOGIC = 
0  58 
struct 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

59 

4345  60 

0  61 
(*** Abstract syntax operations on the metaconnectives ***) 
62 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

63 
(** all **) 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

64 

a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

65 
fun is_all (Const ("all", _) $ _) = true 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

66 
 is_all _ = false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

67 

a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

68 

0  69 
(** equality **) 
70 

1835  71 
(*Make an equality. DOES NOT CHECK TYPE OF u*) 
64
0bbe5d86cb38
logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
lcp
parents:
0
diff
changeset

72 
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; 
0  73 

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

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

76 

637  77 
fun is_equals (Const ("==", _) $ _ $ _) = true 
78 
 is_equals _ = false; 

79 

80 

0  81 
(** implies **) 
82 

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

84 

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

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

87 

5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

88 
fun is_implies (Const ("==>", _) $ _ $ _) = true 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

89 
 is_implies _ = false; 
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

90 

4822  91 

0  92 
(** nested implications **) 
93 

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

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

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

97 

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

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

100 
 strip_imp_prems _ = []; 

101 

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

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

104 
 strip_imp_concl A = A : term; 

105 

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

9460  107 
goes to ([Ai, A(i1),...,A1] , B) (REVERSED) 
0  108 
if i<0 or else i too big then raises TERM*) 
9460  109 
fun strip_prems (0, As, B) = (As, B) 
110 
 strip_prems (i, As, Const("==>", _) $ A $ B) = 

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

0  112 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
113 

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

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

116 
 count_prems (_,n) = n; 

117 

4822  118 

0  119 
(** flexflex constraints **) 
120 

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

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

122 
fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; 
0  123 

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

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

126 

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

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

129 
fun list_flexpairs ([], A) = A 

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

9460  131 
implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A); 
0  132 

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

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

135 

9460  136 
(*Remove and return flexflex pairs: 
137 
(a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C ) 

0  138 
[Tail recursive in order to return a pair of results] *) 
139 
fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) = 

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

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

142 

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

144 

145 
(*Discard flexflex pairs*) 

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

9460  147 
skip_flexpairs C 
0  148 
 skip_flexpairs C = C; 
149 

9460  150 
(*strip a proof state (Horn clause): 
0  151 
(a1==b1)==>...(am==bm)==>B1==>...Bn==>C 
152 
goes to ( [(a1,b1),...,(am,bm)] , [B1,...,Bn] , C) *) 

153 
fun strip_horn A = 

9460  154 
let val (tpairs,horn) = strip_flexpairs A 
0  155 
in (tpairs, strip_imp_prems horn, strip_imp_concl horn) end; 
156 

4822  157 

158 
(** definitions **) 

159 

160 
fun mk_cond_defpair As (lhs, rhs) = 

161 
(case Term.head_of lhs of 

162 
Const (name, _) => 

163 
(Sign.base_name name ^ "_def", list_implies (As, mk_equals (lhs, rhs))) 

164 
 _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs])); 

165 

166 
fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; 

167 

168 

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

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

170 

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

171 
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

172 

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

173 
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

174 
 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

175 

4822  176 

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

178 

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

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

180 
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

181 

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

182 
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

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

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

185 
 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

186 

0  187 

9460  188 
(** atomic goals **) 
189 

190 
val goal_const = Const ("Goal", propT > propT); 

191 
fun mk_goal t = goal_const $ t; 

192 

193 
fun dest_goal (Const ("Goal", _) $ t) = t 

194 
 dest_goal t = raise TERM ("dest_goal", [t]); 

195 

196 

0  197 
(*** Lowlevel term operations ***) 
198 

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

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

4631  201 
fun t occs u = exists_subterm (fn s => t aconv s) u; 
0  202 

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

204 
fun close_form A = 

4443  205 
list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A); 
0  206 

207 

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

209 

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

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

9460  212 
fun incr_indexes (Us: typ list, inc:int) t = 
213 
let fun incr (Var ((a,i), T), lev) = 

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

215 
lev, length Us) 

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

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

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

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

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

221 
 incr (t,lev) = t 

0  222 
in incr(t,0) end; 
223 

224 
(*Make lifting functions from subgoal and increment. 

225 
lift_abs operates on tpairs (unification constraints) 

226 
lift_all operates on propositions *) 

227 
fun lift_fns (B,inc) = 

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

9460  229 
 lift_abs (Us, Const("all",_)$Abs(a,T,t)) u = 
230 
Abs(a, T, lift_abs (T::Us, t) u) 

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

0  232 
fun lift_all (Us, Const("==>", _) $ A $ B) u = 
9460  233 
implies $ A $ lift_all (Us,B) u 
234 
 lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 

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

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

0  237 
in (lift_abs([],B), lift_all([],B)) end; 
238 

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

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

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

242 
 strip_assums_hyp B = []; 

243 

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

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

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

247 
 strip_assums_concl B = B; 

248 

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

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

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

252 
 strip_params B = []; 

253 

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

9460  255 
where j is the total number of parameters (precomputed) 
0  256 
If n>0 then deletes assumption n. *) 
9460  257 
fun remove_params j n A = 
0  258 
if j=0 andalso n<=0 then A (*nothing left to do...*) 
259 
else case A of 

9460  260 
Const("==>", _) $ H $ B => 
261 
if n=1 then (remove_params j (n1) B) 

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

0  263 
 Const("all",_)$Abs(a,T,t) => remove_params (j1) n t 
264 
 _ => if n>0 then raise TERM("remove_params", [A]) 

265 
else A; 

266 

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

268 

269 
val auto_rename = ref false 

270 
and rename_prefix = ref "ka"; 

271 

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

273 
fun set_rename_prefix a = 

4693  274 
if a<>"" andalso forall Symbol.is_letter (Symbol.explode a) 
0  275 
then (rename_prefix := a; auto_rename := true) 
276 
else error"rename prefix must be nonempty and consist of letters"; 

277 

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

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

280 
then res_inst_tac would not work properly.*) 

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

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

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

284 

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

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

287 
fun flatten_params n A = 

288 
let val params = strip_params A; 

9460  289 
val vars = if !auto_rename 
290 
then rename_vars (!rename_prefix, params) 

291 
else ListPair.zip (variantlist(map #1 params,[]), 

292 
map #2 params) 

0  293 
in list_all (vars, remove_params (length vars) n A) 
294 
end; 

295 

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

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

298 
implies $ A $ list_rename_params (cs, B) 

9460  299 
 list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 
0  300 
all T $ Abs(c, T, list_rename_params (cs, t)) 
301 
 list_rename_params (cs, B) = B; 

302 

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

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

9460  305 
fun strip_assums_aux (Hs, params, Const("==>", _) $ H $ B) = 
306 
strip_assums_aux (H::Hs, params, B) 

0  307 
 strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) = 
9460  308 
strip_assums_aux (Hs, (a,T)::params, t) 
0  309 
 strip_assums_aux (Hs, params, B) = (Hs, params, B); 
310 

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

312 

313 

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

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

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

317 
fun assum_pairs A = 

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

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

9460  320 
fun pairrev ([],pairs) = pairs 
321 
 pairrev (H::Hs,pairs) = 

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

0  323 
in pairrev (Hs,[]) (*WAS: map pair (rev Hs) *) 
324 
end; 

325 

326 

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

328 
without (?) everywhere*) 

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

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

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

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

333 
 varify (f$t) = varify f $ varify t 

334 
 varify t = t; 

335 

546  336 
(*Inverse of varify. Converts axioms back to their original form.*) 
585  337 
fun unvarify (Const(a,T)) = Const(a, Type.unvarifyT T) 
338 
 unvarify (Var((a,0), T)) = Free(a, Type.unvarifyT T) 

339 
 unvarify (Var(ixn,T)) = Var(ixn, Type.unvarifyT T) (*non0 index!*) 

340 
 unvarify (Abs (a,T,body)) = Abs (a, Type.unvarifyT T, unvarify body) 

546  341 
 unvarify (f$t) = unvarify f $ unvarify t 
342 
 unvarify t = t; 

343 

0  344 
end; 