author  paulson 
Fri, 05 Oct 2007 09:59:03 +0200  
changeset 24854  0ebcd575d3c6 
parent 24848  5dbbd33c3236 
child 25939  ddea202704b4 
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 

9460  9 
signature LOGIC = 
4345  10 
sig 
18762  11 
val dest_all: term > typ * term 
18181  12 
val mk_equals: term * term > term 
13 
val dest_equals: term > term * term 

14 
val mk_implies: term * term > term 

15 
val dest_implies: term > term * term 

16 
val list_implies: term list * term > term 

17 
val strip_imp_prems: term > term list 

18 
val strip_imp_concl: term > term 

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

21576  20 
val count_prems: term > int 
18181  21 
val nth_prem: int * term > term 
23418  22 
val true_prop: term 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

23 
val conjunction: term 
18181  24 
val mk_conjunction: term * term > term 
12757  25 
val mk_conjunction_list: term list > term 
23418  26 
val mk_conjunction_balanced: term list > term 
18469  27 
val dest_conjunction: term > term * term 
19425  28 
val dest_conjunction_list: term > term list 
23418  29 
val dest_conjunction_balanced: int > term > term list 
18469  30 
val dest_conjunctions: term > term list 
18181  31 
val strip_horn: term > term list * term 
21520  32 
val mk_type: typ > term 
18938  33 
val dest_type: term > typ 
21520  34 
val type_map: (term > term) > typ > typ 
18938  35 
val const_of_class: class > string 
36 
val class_of_const: string > class 

37 
val mk_inclass: typ * class > term 

38 
val dest_inclass: term > typ * class 

20630  39 
val name_classrel: string * string > string 
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

40 
val mk_classrel: class * class > term 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

41 
val dest_classrel: term > class * class 
20630  42 
val name_arities: arity > string list 
43 
val name_arity: string * sort list * class > string 

44 
val mk_arities: arity > term list 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

45 
val dest_arity: term > string * sort list * class 
18181  46 
val protectC: term 
47 
val protect: term > term 

48 
val unprotect: term > term 

19775  49 
val mk_term: term > term 
50 
val dest_term: term > term 

18181  51 
val occs: term * term > bool 
52 
val close_form: term > term 

18938  53 
val combound: term * int * int > term 
54 
val rlist_abs: (string * typ) list * term > term 

18181  55 
val incr_indexes: typ list * int > term > term 
56 
val incr_tvar: int > typ > typ 

57 
val lift_abs: int > term > term > term 

58 
val lift_all: int > term > term > term 

59 
val strip_assums_hyp: term > term list 

9460  60 
val strip_assums_concl: term > term 
18181  61 
val strip_params: term > (string * typ) list 
23597  62 
val has_meta_prems: term > bool 
18181  63 
val flatten_params: int > term > term 
64 
val auto_rename: bool ref 

65 
val set_rename_prefix: string > unit 

0  66 
val list_rename_params: string list * term > term 
18181  67 
val assum_pairs: int * term > (term*term)list 
19806  68 
val varifyT: typ > typ 
69 
val unvarifyT: typ > typ 

18181  70 
val varify: term > term 
71 
val unvarify: term > term 

19806  72 
val legacy_varifyT: typ > typ 
73 
val legacy_unvarifyT: typ > typ 

74 
val legacy_varify: term > term 

75 
val legacy_unvarify: term > term 

18181  76 
val get_goal: term > int > term 
77 
val goal_params: term > int > term * term list 

78 
val prems_of_goal: term > int > term list 

79 
val concl_of_goal: term > int > term 

4345  80 
end; 
0  81 

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

84 

4345  85 

0  86 
(*** Abstract syntax operations on the metaconnectives ***) 
87 

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

89 

18762  90 
fun dest_all (Const ("all", Type ("fun", [Type ("fun", [T, _]), _])) $ A) = (T, A) 
91 
 dest_all t = raise TERM ("dest_all", [t]); 

92 

93 

0  94 
(** equality **) 
95 

20883  96 
fun mk_equals (t, u) = Term.equals (Term.fastype_of t) $ t $ u; 
0  97 

20883  98 
fun dest_equals (Const ("==", _) $ t $ u) = (t, u) 
99 
 dest_equals t = raise TERM ("dest_equals", [t]); 

637  100 

101 

0  102 
(** implies **) 
103 

20883  104 
fun mk_implies (A, B) = implies $ A $ B; 
0  105 

20883  106 
fun dest_implies (Const ("==>", _) $ A $ B) = (A, B) 
107 
 dest_implies A = raise TERM ("dest_implies", [A]); 

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

108 

4822  109 

0  110 
(** nested implications **) 
111 

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

18181  113 
fun list_implies ([], B) = B 
114 
 list_implies (A::As, B) = implies $ A $ list_implies(As,B); 

0  115 

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

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

118 
 strip_imp_prems _ = []; 

119 

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

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

122 
 strip_imp_concl A = A : term; 

123 

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

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

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

0  130 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
131 

16130  132 
(*Count premises  quicker than (length o strip_prems) *) 
21576  133 
fun count_prems (Const ("==>", _) $ _ $ B) = 1 + count_prems B 
134 
 count_prems _ = 0; 

0  135 

16130  136 
(*Select Ai from A1 ==>...Ai==>B*) 
137 
fun nth_prem (1, Const ("==>", _) $ A $ _) = A 

138 
 nth_prem (i, Const ("==>", _) $ _ $ B) = nth_prem (i  1, B) 

139 
 nth_prem (_, A) = raise TERM ("nth_prem", [A]); 

140 

13659
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

141 
(*strip a proof state (Horn clause): 
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

142 
B1 ==> ... Bn ==> C goes to ([B1, ..., Bn], C) *) 
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

143 
fun strip_horn A = (strip_imp_prems A, strip_imp_concl A); 
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

144 

4822  145 

23418  146 

12137  147 
(** conjunction **) 
148 

23418  149 
val true_prop = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)); 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

150 
val conjunction = Const ("ProtoPure.conjunction", propT > propT > propT); 
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

151 

23418  152 

18499  153 
(*A && B*) 
19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

154 
fun mk_conjunction (A, B) = conjunction $ A $ B; 
12137  155 

18499  156 
(*A && B && C  improper*) 
23418  157 
fun mk_conjunction_list [] = true_prop 
12757  158 
 mk_conjunction_list ts = foldr1 mk_conjunction ts; 
12137  159 

23418  160 
(*(A && B) && (C && D)  balanced*) 
161 
fun mk_conjunction_balanced [] = true_prop 

162 
 mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; 

163 

18499  164 

165 
(*A && B*) 

19125
59b26248547b
simplified Pure conjunction, based on actual const;
wenzelm
parents:
19103
diff
changeset

166 
fun dest_conjunction (Const ("ProtoPure.conjunction", _) $ A $ B) = (A, B) 
18469  167 
 dest_conjunction t = raise TERM ("dest_conjunction", [t]); 
168 

19425  169 
(*A && B && C  improper*) 
170 
fun dest_conjunction_list t = 

171 
(case try dest_conjunction t of 

172 
NONE => [t] 

173 
 SOME (A, B) => A :: dest_conjunction_list B); 

174 

23418  175 
(*(A && B) && (C && D)  balanced*) 
176 
fun dest_conjunction_balanced 0 _ = [] 

177 
 dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t; 

178 

18499  179 
(*((A && B) && C) && D && E  flat*) 
18469  180 
fun dest_conjunctions t = 
181 
(case try dest_conjunction t of 

182 
NONE => [t] 

183 
 SOME (A, B) => dest_conjunctions A @ dest_conjunctions B); 

184 

185 

12137  186 

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

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

188 

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

190 

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

191 
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

192 
 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

193 

21520  194 
fun type_map f = dest_type o f o mk_type; 
195 

4822  196 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

197 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

198 
(** type classes **) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

199 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

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

201 

18938  202 
val classN = "_class"; 
203 

204 
val const_of_class = suffix classN; 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

205 

18938  206 
fun class_of_const c = unsuffix classN c 
207 
handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); 

208 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

209 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

210 
(* class constraints *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

211 

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

212 
fun mk_inclass (ty, c) = 
19391  213 
Const (const_of_class c, Term.itselfT ty > propT) $ mk_type ty; 
398
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

214 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

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

216 
 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

217 

0  218 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

219 
(* class relations *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

220 

20630  221 
fun name_classrel (c1, c2) = 
222 
NameSpace.base c1 ^ "_" ^ NameSpace.base c2; 

223 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

224 
fun mk_classrel (c1, c2) = mk_inclass (Term.aT [c1], c2); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

225 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

226 
fun dest_classrel tm = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

227 
(case dest_inclass tm of 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

228 
(TVar (_, [c1]), c2) => (c1, c2) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

229 
 _ => raise TERM ("dest_classrel", [tm])); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

230 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

231 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

232 
(* type arities *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

233 

20630  234 
fun name_arities (t, _, S) = 
235 
let val b = NameSpace.base t 

236 
in S > map (fn c => NameSpace.base c ^ "_" ^ b) end; 

237 

238 
fun name_arity (t, dom, c) = hd (name_arities (t, dom, [c])); 

239 

19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

240 
fun mk_arities (t, Ss, S) = 
24848  241 
let val T = Type (t, ListPair.map TFree (Name.invents Name.context Name.aT (length Ss), Ss)) 
19406
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

242 
in map (fn c => mk_inclass (T, c)) S end; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

243 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

244 
fun dest_arity tm = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

245 
let 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

246 
fun err () = raise TERM ("dest_arity", [tm]); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

247 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

248 
val (ty, c) = dest_inclass tm; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

249 
val (t, tvars) = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

250 
(case ty of 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

251 
Type (t, tys) => (t, map dest_TVar tys handle TYPE _ => err ()) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

252 
 _ => err ()); 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

253 
val Ss = 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

254 
if has_duplicates (eq_fst (op =)) tvars then err () 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

255 
else map snd tvars; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

256 
in (t, Ss, c) end; 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

257 

410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

258 

18938  259 

24258
2f399483535a
moved support for primitive defs to primitive_defs.ML;
wenzelm
parents:
23597
diff
changeset

260 
(** protected propositions and embedded terms **) 
9460  261 

18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

262 
val protectC = Const ("prop", propT > propT); 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

263 
fun protect t = protectC $ t; 
9460  264 

18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

265 
fun unprotect (Const ("prop", _) $ t) = t 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

266 
 unprotect t = raise TERM ("unprotect", [t]); 
9460  267 

268 

19775  269 
fun mk_term t = Const ("ProtoPure.term", Term.fastype_of t > propT) $ t; 
270 

271 
fun dest_term (Const ("ProtoPure.term", _) $ t) = t 

272 
 dest_term t = raise TERM ("dest_term", [t]); 

273 

274 

18181  275 

0  276 
(*** Lowlevel term operations ***) 
277 

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

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

16846  280 
fun occs (t, u) = exists_subterm (fn s => t aconv s) u; 
0  281 

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

283 
fun close_form A = 

19425  284 
Term.list_all_free (rev (Term.add_frees A []), A); 
0  285 

286 

18938  287 

0  288 
(*** Specialized operations for resolution... ***) 
289 

18938  290 
(*computes t(Bound(n+k1),...,Bound(n)) *) 
291 
fun combound (t, n, k) = 

292 
if k>0 then combound (t,n+1,k1) $ (Bound n) else t; 

293 

294 
(* ([xn,...,x1], t) ======> (x1,...,xn)t *) 

295 
fun rlist_abs ([], body) = body 

296 
 rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body)); 

297 

298 

16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

299 
local exception SAME in 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

300 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

301 
fun incrT k = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

302 
let 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

303 
fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

304 
 incr (Type (a, Ts)) = Type (a, incrs Ts) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

305 
 incr _ = raise SAME 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

306 
and incrs (T :: Ts) = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

307 
(incr T :: (incrs Ts handle SAME => Ts) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

308 
handle SAME => T :: incrs Ts) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

309 
 incrs [] = raise SAME; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

310 
in incr end; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

311 

0  312 
(*For all variables in the term, increment indexnames and lift over the Us 
313 
result is ?Gidx(B.(lev+n1),...,B.lev) where lev is abstraction level *) 

17120  314 
fun incr_indexes ([], 0) t = t 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

315 
 incr_indexes (Ts, k) t = 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

316 
let 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

317 
val n = length Ts; 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

318 
val incrT = if k = 0 then I else incrT k; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

319 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

320 
fun incr lev (Var ((x, i), T)) = 
18938  321 
combound (Var ((x, i + k), Ts > (incrT T handle SAME => T)), lev, n) 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

322 
 incr lev (Abs (x, T, body)) = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

323 
(Abs (x, incrT T, incr (lev + 1) body handle SAME => body) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

324 
handle SAME => Abs (x, T, incr (lev + 1) body)) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

325 
 incr lev (t $ u) = 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

326 
(incr lev t $ (incr lev u handle SAME => u) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

327 
handle SAME => t $ incr lev u) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

328 
 incr _ (Const (c, T)) = Const (c, incrT T) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

329 
 incr _ (Free (x, T)) = Free (x, incrT T) 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

330 
 incr _ (t as Bound _) = t; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

331 
in incr 0 t handle SAME => t end; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

332 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

333 
fun incr_tvar 0 T = T 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

334 
 incr_tvar k T = incrT k T handle SAME => T; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

335 

b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

336 
end; 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

337 

0  338 

18248  339 
(* Lifting functions from subgoal and increment: 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

340 
lift_abs operates on terms 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

341 
lift_all operates on propositions *) 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

342 

19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

343 
fun lift_abs inc = 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

344 
let 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

345 
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t 
18248  346 
 lift Ts (Const ("all", _) $ Abs (a, T, B)) t = Abs (a, T, lift (T :: Ts) B t) 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

347 
 lift Ts _ t = incr_indexes (rev Ts, inc) t; 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

348 
in lift [] end; 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

349 

19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

350 
fun lift_all inc = 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

351 
let 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

352 
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t 
18248  353 
 lift Ts ((c as Const ("all", _)) $ Abs (a, T, B)) t = c $ Abs (a, T, lift (T :: Ts) B t) 
18029
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

354 
 lift Ts _ t = incr_indexes (rev Ts, inc) t; 
19f1ad18bece
renamed Goal constant to prop, more general protect/unprotect interfaces;
wenzelm
parents:
17120
diff
changeset

355 
in lift [] end; 
0  356 

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

21016
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

358 
fun strip_assums_hyp B = 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

359 
let 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

360 
fun strip Hs (Const ("==>", _) $ H $ B) = strip (H :: Hs) B 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

361 
 strip Hs (Const ("all", _) $ Abs (a, T, t)) = 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

362 
strip (map (incr_boundvars 1) Hs) t 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

363 
 strip Hs B = rev Hs 
430b35c9cd27
Repaired strip_assums_hyp (now also works for goals not
berghofe
parents:
20883
diff
changeset

364 
in strip [] B end; 
0  365 

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

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

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

369 
 strip_assums_concl B = B; 

370 

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

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

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

374 
 strip_params B = []; 

375 

23597  376 
(*test for nested meta connectives in prems*) 
377 
val has_meta_prems = 

9667  378 
let 
23597  379 
fun is_meta (Const ("==", _) $ _ $ _) = true 
380 
 is_meta (Const ("==>", _) $ _ $ _) = true 

9667  381 
 is_meta (Const ("all", _) $ _) = true 
382 
 is_meta _ = false; 

23597  383 
fun ex_meta (Const ("==>", _) $ A $ B) = is_meta A orelse ex_meta B 
384 
 ex_meta (Const ("all", _) $ Abs (_, _, B)) = ex_meta B 

385 
 ex_meta _ = false; 

386 
in ex_meta end; 

9483  387 

0  388 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 
9460  389 
where j is the total number of parameters (precomputed) 
0  390 
If n>0 then deletes assumption n. *) 
9460  391 
fun remove_params j n A = 
0  392 
if j=0 andalso n<=0 then A (*nothing left to do...*) 
393 
else case A of 

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

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

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

399 
else A; 

400 

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

402 

403 
val auto_rename = ref false 

404 
and rename_prefix = ref "ka"; 

405 

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

407 
fun set_rename_prefix a = 

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

411 

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

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

414 
then res_inst_tac would not work properly.*) 

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

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

12902  417 
(a,T) :: rename_vars (Symbol.bump_string a, vars); 
0  418 

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

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

421 
fun flatten_params n A = 

422 
let val params = strip_params A; 

9460  423 
val vars = if !auto_rename 
424 
then rename_vars (!rename_prefix, params) 

20078
f4122d7494f3
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19879
diff
changeset

425 
else ListPair.zip (Name.variant_list [] (map #1 params), 
9460  426 
map #2 params) 
0  427 
in list_all (vars, remove_params (length vars) n A) 
428 
end; 

429 

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

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

432 
implies $ A $ list_rename_params (cs, B) 

9460  433 
 list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 
0  434 
all T $ Abs(c, T, list_rename_params (cs, t)) 
435 
 list_rename_params (cs, B) = B; 

436 

19806  437 
(*** Treatment of "assume", "erule", etc. ***) 
0  438 

16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

439 
(*Strips assumptions in goal yielding 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

440 
HS = [Hn,...,H1], params = [xm,...,x1], and B, 
16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

441 
where x1...xm are the parameters. This version (21.1.2005) REQUIRES 
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

442 
the the parameters to be flattened, but it allows erule to work on 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

443 
assumptions of the form !!x. phi. Any !! after the outermost string 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

444 
will be regarded as belonging to the conclusion, and left untouched. 
15454  445 
Used ONLY by assum_pairs. 
446 
Unless nasms<0, it can terminate the recursion early; that allows 

447 
erule to work on assumptions of the form P==>Q.*) 

448 
fun strip_assums_imp (0, Hs, B) = (Hs, B) (*recursion terminated by nasms*) 

16879
b81d3f2ee565
incr_tvar (from term.ML), incr_indexes: avoid garbage;
wenzelm
parents:
16862
diff
changeset

449 
 strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = 
15454  450 
strip_assums_imp (nasms1, H::Hs, B) 
451 
 strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) 

452 

0  453 

15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

454 
(*Strips OUTER parameters only, unlike similar legacy versions.*) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

455 
fun strip_assums_all (params, Const("all",_)$Abs(a,T,t)) = 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

456 
strip_assums_all ((a,T)::params, t) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

457 
 strip_assums_all (params, B) = (params, B); 
0  458 

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

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

15454  461 
H1 ==> ... Hk ==> B and the pairs are (H1,B),...,(Hk,B). 
462 
nasms is the number of assumptions in the original subgoal, needed when B 

463 
has the form B1 ==> B2: it stops B1 from being taken as an assumption. *) 

464 
fun assum_pairs(nasms,A) = 

15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

465 
let val (params, A') = strip_assums_all ([],A) 
15454  466 
val (Hs,B) = strip_assums_imp (nasms,[],A') 
18938  467 
fun abspar t = rlist_abs(params, t) 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

468 
val D = abspar B 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

469 
fun pairrev ([], pairs) = pairs 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

470 
 pairrev (H::Hs, pairs) = pairrev(Hs, (abspar H, D) :: pairs) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

471 
in pairrev (Hs,[]) 
0  472 
end; 
473 

19806  474 

475 
(* global schematic variables *) 

476 

477 
fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi); 

478 
fun bad_fixed x = "Illegal fixed variable: " ^ quote x; 

479 

480 
fun varifyT ty = ty > Term.map_atyps 

481 
(fn TFree (a, S) => TVar ((a, 0), S) 

482 
 TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])); 

483 

484 
fun unvarifyT ty = ty > Term.map_atyps 

485 
(fn TVar ((a, 0), S) => TFree (a, S) 

486 
 TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []) 

487 
 TFree (a, _) => raise TYPE (bad_fixed a, [ty], [])); 

0  488 

19806  489 
fun varify tm = 
490 
tm > Term.map_aterms 

491 
(fn Free (x, T) => Var ((x, 0), T) 

492 
 Var (xi, _) => raise TERM (bad_schematic xi, [tm]) 

493 
 t => t) 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset

494 
> Term.map_types varifyT 
19879  495 
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); 
19806  496 

497 
fun unvarify tm = 

498 
tm > Term.map_aterms 

499 
(fn Var ((x, 0), T) => Free (x, T) 

500 
 Var (xi, _) => raise TERM (bad_schematic xi, [tm]) 

501 
 Free (x, _) => raise TERM (bad_fixed x, [tm]) 

502 
 t => t) 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset

503 
> Term.map_types unvarifyT 
19879  504 
handle TYPE (msg, _, _) => raise TERM (msg, [tm]); 
19806  505 

506 
val legacy_varifyT = Term.map_atyps (fn TFree (a, S) => TVar ((a, 0), S)  T => T); 

507 
val legacy_unvarifyT = Term.map_atyps (fn TVar ((a, 0), S) => TFree (a, S)  T => T); 

508 

509 
val legacy_varify = 

510 
Term.map_aterms (fn Free (x, T) => Var ((x, 0), T)  t => t) #> 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset

511 
Term.map_types legacy_varifyT; 
19806  512 

513 
val legacy_unvarify = 

514 
Term.map_aterms (fn Var ((x, 0), T) => Free (x, T)  t => t) #> 

20548
8ef25fe585a8
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
wenzelm
parents:
20078
diff
changeset

515 
Term.map_types legacy_unvarifyT; 
546  516 

13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

517 

16862  518 
(* goal states *) 
519 

520 
fun get_goal st i = nth_prem (i, st) 

521 
handle TERM _ => error "Goal number out of range"; 

13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

522 

77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

523 
(*reverses parameters for substitution*) 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

524 
fun goal_params st i = 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

525 
let val gi = get_goal st i 
14137
c57ec95e7763
Removed extraneous rev in function goal_params (the list of parameters
berghofe
parents:
14107
diff
changeset

526 
val rfrees = map Free (rename_wrt_term gi (strip_params gi)) 
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

527 
in (gi, rfrees) end; 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

528 

77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

529 
fun concl_of_goal st i = 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

530 
let val (gi, rfrees) = goal_params st i 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

531 
val B = strip_assums_concl gi 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

532 
in subst_bounds (rfrees, B) end; 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

533 

77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

534 
fun prems_of_goal st i = 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

535 
let val (gi, rfrees) = goal_params st i 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

536 
val As = strip_assums_hyp gi 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

537 
in map (fn A => subst_bounds (rfrees, A)) As end; 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

538 

0  539 
end; 