author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5041  a1d0a6d555cd 
child 9460  53d7ad5bec39 
permissions  rwrr 
1460  1 
(* Title: Pure/logic.ML 
0  2 
ID: $Id$ 
1460  3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 
0  4 
Copyright Cambridge University 1992 
5 

6 
Supporting code for defining the abstract type "thm" 

7 
*) 

8 

9 
infix occs; 

10 

11 
signature LOGIC = 

4345  12 
sig 
1460  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 dest_inclass : term > typ * class 

21 
val dest_type : term > typ 

22 
val flatten_params : int > term > term 

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

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

24 
val is_all : term > bool 
3963
29c5ec9ecbaa
Corrected alphabetical order of entries in signature.
nipkow
parents:
3915
diff
changeset

25 
val is_equals : term > bool 
5041
a1d0a6d555cd
Goals may now contain assumptions, which are not returned.
nipkow
parents:
4822
diff
changeset

26 
val is_implies : term > bool 
1460  27 
val lift_fns : term * int > (term > term) * (term > term) 
28 
val list_flexpairs : (term*term)list * term > term 

29 
val list_implies : term list * term > term 

0  30 
val list_rename_params: string list * term > term 
4822  31 
val mk_cond_defpair : term list > term * term > string * term 
32 
val mk_defpair : term * term > string * term 

1460  33 
val mk_equals : term * term > term 
34 
val mk_flexpair : term * term > term 

35 
val mk_implies : term * term > term 

36 
val mk_inclass : typ * class > term 

37 
val mk_type : typ > term 

38 
val occs : term * term > bool 

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

40 
val set_rename_prefix : string > unit 

41 
val skip_flexpairs : term > term 

0  42 
val strip_assums_concl: term > term 
1460  43 
val strip_assums_hyp : term > term list 
44 
val strip_flexpairs : term > (term*term)list * term 

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

46 
val strip_imp_concl : term > term 

47 
val strip_imp_prems : term > term list 

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

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

2508  50 
val unvarify : term > term 
51 
val varify : term > term 

4345  52 
end; 
0  53 

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

56 

4345  57 

0  58 
(*** Abstract syntax operations on the metaconnectives ***) 
59 

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

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

61 

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

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

63 
 is_all _ = false; 
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 

0  66 
(** equality **) 
67 

1835  68 
(*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

69 
fun mk_equals(t,u) = equals(fastype_of t) $ t $ u; 
0  70 

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

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

73 

637  74 
fun is_equals (Const ("==", _) $ _ $ _) = true 
75 
 is_equals _ = false; 

76 

77 

0  78 
(** implies **) 
79 

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

81 

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

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

84 

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

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

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

87 

4822  88 

0  89 
(** nested implications **) 
90 

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

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

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

94 

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

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

97 
 strip_imp_prems _ = []; 

98 

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

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

101 
 strip_imp_concl A = A : term; 

102 

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

1460  104 
goes to ([Ai, A(i1),...,A1] , B) (REVERSED) 
0  105 
if i<0 or else i too big then raises TERM*) 
106 
fun strip_prems (0, As, B) = (As, B) 

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

1460  108 
strip_prems (i1, A::As, B) 
0  109 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
110 

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

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

113 
 count_prems (_,n) = n; 

114 

4822  115 

0  116 
(** flexflex constraints **) 
117 

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

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

119 
fun mk_flexpair(t,u) = flexpair(fastype_of t) $ t $ u; 
0  120 

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

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

123 

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

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

126 
fun list_flexpairs ([], A) = A 

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

1460  128 
implies $ (mk_flexpair(t,u)) $ list_flexpairs(pairs,A); 
0  129 

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

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

132 

133 
(*Remove and return flexflex pairs: 

1460  134 
(a1=?=b1)==>...(an=?=bn)==>C to ( [(a1,b1),...,(an,bn)] , C ) 
0  135 
[Tail recursive in order to return a pair of results] *) 
136 
fun strip_flex_aux (pairs, Const("==>", _) $ (Const("=?=",_)$t$u) $ C) = 

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

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

139 

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

141 

142 
(*Discard flexflex pairs*) 

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

1460  144 
skip_flexpairs C 
0  145 
 skip_flexpairs C = C; 
146 

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

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

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

150 
fun strip_horn A = 

151 
let val (tpairs,horn) = strip_flexpairs A 

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

153 

4822  154 

155 
(** definitions **) 

156 

157 
fun mk_cond_defpair As (lhs, rhs) = 

158 
(case Term.head_of lhs of 

159 
Const (name, _) => 

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

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

162 

163 
fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; 

164 

165 

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

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

167 

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

168 
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

169 

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

170 
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

171 
 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

172 

4822  173 

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

175 

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

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

177 
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

178 

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

179 
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

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

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

182 
 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

183 

0  184 

185 
(*** Lowlevel term operations ***) 

186 

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

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

4631  189 
fun t occs u = exists_subterm (fn s => t aconv s) u; 
0  190 

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

192 
fun close_form A = 

4443  193 
list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A); 
0  194 

195 

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

197 

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

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

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

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

1460  202 
Unify.combound (Var((a, i+inc), Us> incr_tvar inc T), 
203 
lev, length Us) 

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

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

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

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

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

209 
 incr (t,lev) = t 

0  210 
in incr(t,0) end; 
211 

212 
(*Make lifting functions from subgoal and increment. 

213 
lift_abs operates on tpairs (unification constraints) 

214 
lift_all operates on propositions *) 

215 
fun lift_fns (B,inc) = 

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

1460  217 
 lift_abs (Us, Const("all",_)$Abs(a,T,t)) u = 
218 
Abs(a, T, lift_abs (T::Us, t) u) 

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

0  220 
fun lift_all (Us, Const("==>", _) $ A $ B) u = 
1460  221 
implies $ A $ lift_all (Us,B) u 
222 
 lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 

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

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

0  225 
in (lift_abs([],B), lift_all([],B)) end; 
226 

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

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

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

230 
 strip_assums_hyp B = []; 

231 

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

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

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

235 
 strip_assums_concl B = B; 

236 

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

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

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

240 
 strip_params B = []; 

241 

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

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

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

245 
fun remove_params j n A = 

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

247 
else case A of 

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

1460  249 
if n=1 then (remove_params j (n1) B) 
250 
else implies $ (incr_boundvars j H) $ (remove_params j (n1) B) 

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

253 
else A; 

254 

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

256 

257 
val auto_rename = ref false 

258 
and rename_prefix = ref "ka"; 

259 

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

261 
fun set_rename_prefix a = 

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

265 

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

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

268 
then res_inst_tac would not work properly.*) 

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

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

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

272 

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

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

275 
fun flatten_params n A = 

276 
let val params = strip_params A; 

1460  277 
val vars = if !auto_rename 
278 
then rename_vars (!rename_prefix, params) 

2266  279 
else ListPair.zip (variantlist(map #1 params,[]), 
280 
map #2 params) 

0  281 
in list_all (vars, remove_params (length vars) n A) 
282 
end; 

283 

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

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

286 
implies $ A $ list_rename_params (cs, B) 

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

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

289 
 list_rename_params (cs, B) = B; 

290 

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

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

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

1460  294 
strip_assums_aux (H::Hs, params, B) 
0  295 
 strip_assums_aux (Hs, params, Const("all",_)$Abs(a,T,t)) = 
1460  296 
strip_assums_aux (Hs, (a,T)::params, t) 
0  297 
 strip_assums_aux (Hs, params, B) = (Hs, params, B); 
298 

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

300 

301 

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

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

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

305 
fun assum_pairs A = 

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

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

308 
fun pairrev ([],pairs) = pairs 

309 
 pairrev (H::Hs,pairs) = 

1460  310 
pairrev(Hs, (Unify.rlist_abs(params,H), D) :: pairs) 
0  311 
in pairrev (Hs,[]) (*WAS: map pair (rev Hs) *) 
312 
end; 

313 

314 

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

316 
without (?) everywhere*) 

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

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

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

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

321 
 varify (f$t) = varify f $ varify t 

322 
 varify t = t; 

323 

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

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

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

546  329 
 unvarify (f$t) = unvarify f $ unvarify t 
330 
 unvarify t = t; 

331 

0  332 
end; 