author  wenzelm 
Mon, 16 Mar 2009 23:52:30 +0100  
changeset 30554  73f8bd5f0af8 
parent 30364  577edc39b501 
child 31943  5e960a0780a2 
permissions  rwrr 
9460  1 
(* Title: Pure/logic.ML 
2 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory 

29276  3 
Author: Makarius 
0  4 

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

9460  8 
signature LOGIC = 
4345  9 
sig 
27334  10 
val all: term > term > term 
11 
val is_all: term > bool 

12 
val dest_all: term > (string * typ) * term 

18181  13 
val mk_equals: term * term > term 
14 
val dest_equals: term > term * term 

27334  15 
val implies: term 
18181  16 
val mk_implies: term * term > term 
17 
val dest_implies: term > term * term 

18 
val list_implies: term list * term > term 

19 
val strip_imp_prems: term > term list 

20 
val strip_imp_concl: term > term 

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

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

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

39 
val mk_inclass: typ * class > term 

40 
val dest_inclass: term > typ * class 

20630  41 
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

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

43 
val dest_classrel: term > class * class 
20630  44 
val name_arities: arity > string list 
45 
val name_arity: string * sort list * class > string 

46 
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

47 
val dest_arity: term > string * sort list * class 
18181  48 
val protectC: term 
49 
val protect: term > term 

50 
val unprotect: term > term 

19775  51 
val mk_term: term > term 
52 
val dest_term: term > term 

18181  53 
val occs: term * term > bool 
54 
val close_form: term > term 

18938  55 
val combound: term * int * int > term 
56 
val rlist_abs: (string * typ) list * term > term 

18181  57 
val incr_indexes: typ list * int > term > term 
58 
val incr_tvar: int > typ > typ 

59 
val lift_abs: int > term > term > term 

60 
val lift_all: int > term > term > term 

61 
val strip_assums_hyp: term > term list 

9460  62 
val strip_assums_concl: term > term 
18181  63 
val strip_params: term > (string * typ) list 
23597  64 
val has_meta_prems: term > bool 
18181  65 
val flatten_params: int > term > term 
0  66 
val list_rename_params: string list * term > term 
18181  67 
val assum_pairs: int * term > (term*term)list 
30554
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

68 
val assum_problems: int * term > (term > term) * term list * term 
19806  69 
val varifyT: typ > typ 
70 
val unvarifyT: typ > typ 

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

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

75 
val legacy_varify: term > term 

76 
val legacy_unvarify: term > term 

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

79 
val prems_of_goal: term > int > term list 

80 
val concl_of_goal: term > int > term 

4345  81 
end; 
0  82 

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

85 

4345  86 

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

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

90 

27334  91 
fun all v t = Const ("all", (Term.fastype_of v > propT) > propT) $ lambda v t; 
92 

93 
fun is_all (Const ("all", _) $ Abs _) = true 

94 
 is_all _ = false; 

95 

96 
fun dest_all (Const ("all", _) $ Abs (abs as (_, T, _))) = 

97 
let val (x, b) = Term.dest_abs abs (*potentially slow*) 

98 
in ((x, T), b) end 

18762  99 
 dest_all t = raise TERM ("dest_all", [t]); 
100 

101 

0  102 
(** equality **) 
103 

27334  104 
fun mk_equals (t, u) = 
105 
let val T = Term.fastype_of t 

106 
in Const ("==", T > T > propT) $ t $ u end; 

0  107 

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

637  110 

111 

0  112 
(** implies **) 
113 

27334  114 
val implies = Const ("==>", propT > propT > propT); 
115 

20883  116 
fun mk_implies (A, B) = implies $ A $ B; 
0  117 

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

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

120 

4822  121 

0  122 
(** nested implications **) 
123 

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

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

0  127 

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

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

130 
 strip_imp_prems _ = []; 

131 

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

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

134 
 strip_imp_concl A = A : term; 

135 

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

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

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

0  142 
 strip_prems (_, As, A) = raise TERM("strip_prems", A::As); 
143 

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

0  147 

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

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

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

152 

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

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

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

155 
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

156 

4822  157 

23418  158 

12137  159 
(** conjunction **) 
160 

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

163 

23418  164 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

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

166 
fun mk_conjunction (A, B) = conjunction $ A $ B; 
12137  167 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

168 
(*A &&& B &&& C  improper*) 
23418  169 
fun mk_conjunction_list [] = true_prop 
12757  170 
 mk_conjunction_list ts = foldr1 mk_conjunction ts; 
12137  171 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

172 
(*(A &&& B) &&& (C &&& D)  balanced*) 
23418  173 
fun mk_conjunction_balanced [] = true_prop 
174 
 mk_conjunction_balanced ts = BalancedTree.make mk_conjunction ts; 

175 

18499  176 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

177 
(*A &&& B*) 
26424  178 
fun dest_conjunction (Const ("Pure.conjunction", _) $ A $ B) = (A, B) 
18469  179 
 dest_conjunction t = raise TERM ("dest_conjunction", [t]); 
180 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

181 
(*A &&& B &&& C  improper*) 
19425  182 
fun dest_conjunction_list t = 
183 
(case try dest_conjunction t of 

184 
NONE => [t] 

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

186 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

187 
(*(A &&& B) &&& (C &&& D)  balanced*) 
23418  188 
fun dest_conjunction_balanced 0 _ = [] 
189 
 dest_conjunction_balanced n t = BalancedTree.dest dest_conjunction n t; 

190 

28856
5e009a80fe6d
Pure syntax: more coherent treatment of aprop, permanent TERM and &&&;
wenzelm
parents:
28448
diff
changeset

191 
(*((A &&& B) &&& C) &&& D &&& E  flat*) 
18469  192 
fun dest_conjunctions t = 
193 
(case try dest_conjunction t of 

194 
NONE => [t] 

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

196 

197 

12137  198 

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

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

200 

19391  201 
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

202 

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

203 
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

204 
 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

205 

21520  206 
fun type_map f = dest_type o f o mk_type; 
207 

4822  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 
(** type classes **) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

211 

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

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

213 

18938  214 
val classN = "_class"; 
215 

216 
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

217 

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

220 

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

221 

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

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

223 

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

224 
fun mk_inclass (ty, c) = 
19391  225 
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

226 

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

227 
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

228 
 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

229 

0  230 

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

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

232 

20630  233 
fun name_classrel (c1, c2) = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

234 
Long_Name.base_name c1 ^ "_" ^ Long_Name.base_name c2; 
20630  235 

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

236 
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

237 

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

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

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

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

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

242 

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 
(* type arities *) 
410b9d9bf9a1
added mk_classrel, dest_classrel, mk_arities, dest_arity (from axclass.ML);
wenzelm
parents:
19391
diff
changeset

245 

20630  246 
fun name_arities (t, _, S) = 
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

247 
let val b = Long_Name.base_name t 
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset

248 
in S > map (fn c => Long_Name.base_name c ^ "_" ^ b) end; 
20630  249 

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

251 

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

252 
fun mk_arities (t, Ss, S) = 
24848  253 
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

254 
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

255 

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

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

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

258 
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

259 

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

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

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

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

263 
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

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

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

266 
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

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

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

269 

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

270 

18938  271 

28448  272 
(** protected propositions and embedded terms **) 
9460  273 

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

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

275 
fun protect t = protectC $ t; 
9460  276 

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

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

278 
 unprotect t = raise TERM ("unprotect", [t]); 
9460  279 

280 

26424  281 
fun mk_term t = Const ("Pure.term", Term.fastype_of t > propT) $ t; 
19775  282 

26424  283 
fun dest_term (Const ("Pure.term", _) $ t) = t 
19775  284 
 dest_term t = raise TERM ("dest_term", [t]); 
285 

286 

18181  287 

0  288 
(*** Lowlevel term operations ***) 
289 

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

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

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

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

295 
fun close_form A = 

19425  296 
Term.list_all_free (rev (Term.add_frees A []), A); 
0  297 

298 

18938  299 

0  300 
(*** Specialized operations for resolution... ***) 
301 

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

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

305 

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

307 
fun rlist_abs ([], body) = body 

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

309 

310 

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

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

312 

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

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

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

315 
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

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

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

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

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

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

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

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

323 

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

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

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

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

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

330 
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

331 

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

332 
fun incr lev (Var ((x, i), T)) = 
18938  333 
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

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

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

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

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

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

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

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

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

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

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

344 

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

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

346 
 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

347 

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

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

349 

0  350 

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

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

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

354 

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

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

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

357 
fun lift Ts (Const ("==>", _) $ _ $ B) t = lift Ts B t 
18248  358 
 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

359 
 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

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

361 

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

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

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

364 
fun lift Ts ((c as Const ("==>", _)) $ A $ B) t = c $ A $ lift Ts B t 
18248  365 
 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

366 
 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

367 
in lift [] end; 
0  368 

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

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

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

372 
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

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

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

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

376 
in strip [] B end; 
0  377 

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

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

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

381 
 strip_assums_concl B = B; 

382 

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

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

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

386 
 strip_params B = []; 

387 

23597  388 
(*test for nested meta connectives in prems*) 
389 
val has_meta_prems = 

9667  390 
let 
23597  391 
fun is_meta (Const ("==", _) $ _ $ _) = true 
392 
 is_meta (Const ("==>", _) $ _ $ _) = true 

9667  393 
 is_meta (Const ("all", _) $ _) = true 
394 
 is_meta _ = false; 

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

397 
 ex_meta _ = false; 

398 
in ex_meta end; 

9483  399 

0  400 
(*Removes the parameters from a subgoal and renumber bvars in hypotheses, 
9460  401 
where j is the total number of parameters (precomputed) 
0  402 
If n>0 then deletes assumption n. *) 
9460  403 
fun remove_params j n A = 
0  404 
if j=0 andalso n<=0 then A (*nothing left to do...*) 
405 
else case A of 

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

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

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

411 
else A; 

412 

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

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

415 
fun flatten_params n A = 

416 
let val params = strip_params A; 

25939  417 
val vars = ListPair.zip (Name.variant_list [] (map #1 params), 
418 
map #2 params) 

0  419 
in list_all (vars, remove_params (length vars) n A) 
420 
end; 

421 

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

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

424 
implies $ A $ list_rename_params (cs, B) 

27334  425 
 list_rename_params (c::cs, (a as Const("all",_)) $ Abs(_,T,t)) = 
426 
a $ Abs(c, T, list_rename_params (cs, t)) 

0  427 
 list_rename_params (cs, B) = B; 
428 

19806  429 
(*** Treatment of "assume", "erule", etc. ***) 
0  430 

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

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

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

433 
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

434 
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

435 
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

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

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

440 
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

441 
 strip_assums_imp (nasms, Hs, Const("==>", _) $ H $ B) = 
15454  442 
strip_assums_imp (nasms1, H::Hs, B) 
443 
 strip_assums_imp (_, Hs, B) = (Hs, B); (*recursion terminated by B*) 

444 

0  445 

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

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

447 
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

448 
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

449 
 strip_assums_all (params, B) = (params, B); 
0  450 

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

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

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

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

456 
fun assum_pairs(nasms,A) = 

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

457 
let val (params, A') = strip_assums_all ([],A) 
15454  458 
val (Hs,B) = strip_assums_imp (nasms,[],A') 
18938  459 
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

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

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

462 
 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

463 
in pairrev (Hs,[]) 
0  464 
end; 
465 

30554
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

466 
fun assum_problems (nasms, A) = 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

467 
let 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

468 
val (params, A') = strip_assums_all ([], A) 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

469 
val (Hs, B) = strip_assums_imp (nasms, [], A') 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

470 
fun abspar t = rlist_abs (params, t) 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

471 
in (abspar, rev Hs, B) end; 
73f8bd5f0af8
substantial speedup of assumption and elimresolution: Logic.assum_problems refrains from eager application of parameters, discriminate via Term.could_unify before invoking full unification (assumes terms in betanormal form, as do higher term net operations anyway);
wenzelm
parents:
30364
diff
changeset

472 

19806  473 

474 
(* global schematic variables *) 

475 

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

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

478 

479 
fun varifyT ty = ty > Term.map_atyps 

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

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

482 

483 
fun unvarifyT ty = ty > Term.map_atyps 

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

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

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

0  487 

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

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

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

492 
 t => t) 

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

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

496 
fun unvarify tm = 

497 
tm > Term.map_aterms 

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

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

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

501 
 t => t) 

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

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

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

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

507 

508 
val legacy_varify = 

509 
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

510 
Term.map_types legacy_varifyT; 
19806  511 

512 
val legacy_unvarify = 

513 
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

514 
Term.map_types legacy_unvarifyT; 
546  515 

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

516 

16862  517 
(* goal states *) 
518 

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

520 
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

521 

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

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

523 
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

524 
let val gi = get_goal st i 
29276  525 
val rfrees = map Free (Term.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

526 
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

527 

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

528 
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

529 
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

530 
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

531 
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

532 

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

533 
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

534 
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

535 
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

536 
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

537 

0  538 
end; 