author  paulson 
Mon, 24 Jan 2005 12:41:06 +0100  
changeset 15454  4b339d3907a0 
parent 15451  c6c8786b9921 
child 15596  8665d08085df 
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 

12137  25 
val mk_conjunction : term * term > term 
12757  26 
val mk_conjunction_list: term list > term 
13659
3cf622f6b0b2
Removed obsolete functions dealing with flexflex constraints.
berghofe
parents:
12902
diff
changeset

27 
val strip_horn : term > term list * term 
9460  28 
val mk_cond_defpair : term list > term * term > string * term 
29 
val mk_defpair : term * term > string * term 

30 
val mk_type : typ > term 

31 
val dest_type : term > typ 

32 
val mk_inclass : typ * class > term 

33 
val dest_inclass : term > typ * class 

34 
val goal_const : term 

35 
val mk_goal : term > term 

36 
val dest_goal : term > term 

37 
val occs : term * term > bool 

38 
val close_form : term > term 

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

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

41 
val strip_assums_hyp : term > term list 

42 
val strip_assums_concl: term > term 

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

9667  44 
val has_meta_prems : term > int > bool 
9460  45 
val flatten_params : int > term > term 
46 
val auto_rename : bool ref 

47 
val set_rename_prefix : string > unit 

0  48 
val list_rename_params: string list * term > term 
15454  49 
val assum_pairs : int * term > (term*term)list 
9460  50 
val varify : term > term 
51 
val unvarify : term > term 

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

52 
val get_goal : term > int > term 
14107  53 
val goal_params : term > int > term * term list 
13799
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

54 
val prems_of_goal : term > int > term list 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

55 
val concl_of_goal : term > int > term 
4345  56 
end; 
0  57 

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

60 

4345  61 

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

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

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

65 

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

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

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

68 

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

69 

0  70 
(** equality **) 
71 

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

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

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

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

77 

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

80 

81 

0  82 
(** implies **) 
83 

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

85 

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

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

88 

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

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

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

91 

4822  92 

0  93 
(** nested implications **) 
94 

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

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

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

98 

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

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

101 
 strip_imp_prems _ = []; 

102 

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

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

105 
 strip_imp_concl A = A : term; 

106 

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

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

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

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

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

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

117 
 count_prems (_,n) = n; 

118 

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

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

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

121 
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

122 

4822  123 

12137  124 
(** conjunction **) 
125 

126 
fun mk_conjunction (t, u) = 

127 
Term.list_all ([("C", propT)], mk_implies (list_implies ([t, u], Bound 0), Bound 0)); 

128 

12757  129 
fun mk_conjunction_list [] = Term.all propT $ Abs ("dummy", propT, mk_implies (Bound 0, Bound 0)) 
130 
 mk_conjunction_list ts = foldr1 mk_conjunction ts; 

12137  131 

132 

4822  133 
(** definitions **) 
134 

135 
fun mk_cond_defpair As (lhs, rhs) = 

136 
(case Term.head_of lhs of 

137 
Const (name, _) => 

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

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

140 

141 
fun mk_defpair lhs_rhs = mk_cond_defpair [] lhs_rhs; 

142 

143 

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

144 
(** types as terms **) 
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_type ty = Const ("TYPE", itselfT ty); 
41f279b477e2
added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
wenzelm
parents:
210
diff
changeset

147 

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

148 
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

149 
 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

150 

4822  151 

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

153 

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

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

155 
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

156 

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

157 
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

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

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

160 
 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

161 

0  162 

9460  163 
(** atomic goals **) 
164 

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

166 
fun mk_goal t = goal_const $ t; 

167 

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

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

170 

171 

0  172 
(*** Lowlevel term operations ***) 
173 

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

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

4631  176 
fun t occs u = exists_subterm (fn s => t aconv s) u; 
0  177 

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

179 
fun close_form A = 

4443  180 
list_all_free (sort_wrt fst (map dest_Free (term_frees A)), A); 
0  181 

182 

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

184 

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

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

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

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

190 
lev, length Us) 

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

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

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

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

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

196 
 incr (t,lev) = t 

0  197 
in incr(t,0) end; 
198 

199 
(*Make lifting functions from subgoal and increment. 

200 
lift_abs operates on tpairs (unification constraints) 

201 
lift_all operates on propositions *) 

202 
fun lift_fns (B,inc) = 

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

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

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

0  207 
fun lift_all (Us, Const("==>", _) $ A $ B) u = 
9460  208 
implies $ A $ lift_all (Us,B) u 
209 
 lift_all (Us, Const("all",_)$Abs(a,T,t)) u = 

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

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

0  212 
in (lift_abs([],B), lift_all([],B)) end; 
213 

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

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

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

217 
 strip_assums_hyp B = []; 

218 

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

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

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

222 
 strip_assums_concl B = B; 

223 

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

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

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

227 
 strip_params B = []; 

228 

9667  229 
(*test for meta connectives in prems of a 'subgoal'*) 
230 
fun has_meta_prems prop i = 

231 
let 

232 
fun is_meta (Const ("==>", _) $ _ $ _) = true 

10442  233 
 is_meta (Const ("==", _) $ _ $ _) = true 
9667  234 
 is_meta (Const ("all", _) $ _) = true 
235 
 is_meta _ = false; 

236 
in 

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

237 
(case strip_prems (i, [], prop) of 
9667  238 
(B :: _, _) => exists is_meta (strip_assums_hyp B) 
239 
 _ => false) handle TERM _ => false 

240 
end; 

9483  241 

0  242 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 
9460  243 
where j is the total number of parameters (precomputed) 
0  244 
If n>0 then deletes assumption n. *) 
9460  245 
fun remove_params j n A = 
0  246 
if j=0 andalso n<=0 then A (*nothing left to do...*) 
247 
else case A of 

9460  248 
Const("==>", _) $ H $ B => 
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) = 

12902  271 
(a,T) :: rename_vars (Symbol.bump_string a, vars); 
0  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; 

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

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) 

9460  287 
 list_rename_params (c::cs, Const("all",_)$Abs(_,T,t)) = 
0  288 
all T $ Abs(c, T, list_rename_params (cs, t)) 
289 
 list_rename_params (cs, B) = B; 

290 

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

291 
(*** Treatmsent of "assume", "erule", etc. ***) 
0  292 

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

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

294 
HS = [Hn,...,H1], params = [xm,...,x1], and B, 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

295 
where x1...xm are the parameters. This version (21.1.2005) REQUIRES 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

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

297 
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

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

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

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

303 
 strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = 

304 
strip_assums_imp (nasms1, H::Hs, B) 

305 
 strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) 

306 

0  307 

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

308 
(*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

309 
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

310 
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

311 
 strip_assums_all (params, B) = (params, B); 
0  312 

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

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

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

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

318 
fun assum_pairs(nasms,A) = 

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

319 
let val (params, A') = strip_assums_all ([],A) 
15454  320 
val (Hs,B) = strip_assums_imp (nasms,[],A') 
15451
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

321 
fun abspar t = Unify.rlist_abs(params, t) 
c6c8786b9921
fixed thin_tac with higherlevel assumptions by removing the old code to
paulson
parents:
14137
diff
changeset

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

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

324 
 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

325 
in pairrev (Hs,[]) 
0  326 
end; 
327 

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

329 
without (?) everywhere*) 

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

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

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

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

334 
 varify (f$t) = varify f $ varify t 

335 
 varify t = t; 

336 

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

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

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

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

344 

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

345 

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

346 
(*Get subgoal i*) 
77614fe09362
Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
berghofe
parents:
13659
diff
changeset

347 
fun get_goal st i = List.nth (strip_imp_prems st, i1) 
14107  348 
handle Subscript => 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

349 

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

350 
(*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

351 
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

352 
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

353 
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

354 
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

355 

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

356 
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

357 
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

358 
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

359 
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

360 

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

361 
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

362 
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

363 
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

364 
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

365 

0  366 
end; 