author | quigley |
Wed, 06 Apr 2005 12:01:37 +0200 | |
changeset 15658 | 2edb384bf61f |
parent 15642 | 028059faa963 |
child 15684 | 5ec4d21889d6 |
permissions | -rw-r--r-- |
15642 | 1 |
|
2 |
fun take n [] = [] |
|
3 |
| take n (x::xs) = (if n = 0 then [] else (x::(take (n - 1) xs))) |
|
4 |
||
5 |
fun drop n [] = [] |
|
6 |
| drop n (x::xs) = (if n = 0 then (x::xs) else drop (n-1) xs) |
|
7 |
||
8 |
fun remove n [] = [] |
|
9 |
| remove n (x::xs) = List.filter (not_equal n) (x::xs); |
|
10 |
||
11 |
fun remove_nth n [] = [] |
|
12 |
| remove_nth n (x::xs) = (take (n -1) (x::xs))@(drop n (x::xs)) |
|
13 |
||
14 |
fun get_nth n (x::xs) = hd (drop (n-1) (x::xs)) |
|
15 |
||
16 |
fun add_in_order (x:string) [] = [x] |
|
17 |
| add_in_order (x:string) ((y:string)::ys) = if (x < y) |
|
18 |
then |
|
19 |
(x::(y::ys)) |
|
20 |
else |
|
21 |
(y::(add_in_order x ys)) |
|
22 |
fun add_once x [] = [x] |
|
23 |
| add_once x (y::ys) = if (inlist x (y::ys)) then |
|
24 |
(y::ys) |
|
25 |
else |
|
26 |
add_in_order x (y::ys) |
|
27 |
||
28 |
fun thm_vars thm = map getindexstring (map fst (Drule.vars_of thm)); |
|
29 |
||
30 |
Goal "False ==> False"; |
|
31 |
by Auto_tac; |
|
32 |
qed "False_imp"; |
|
33 |
||
34 |
exception Reflex_equal; |
|
35 |
||
36 |
(********************************) |
|
37 |
(* Proofstep datatype *) |
|
38 |
(********************************) |
|
39 |
(* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3] *) |
|
40 |
||
41 |
datatype Side = Left |Right |
|
42 |
||
43 |
datatype Proofstep = ExtraAxiom |
|
44 |
|OrigAxiom |
|
45 |
| Axiom |
|
46 |
| Binary of (int * int) * (int * int) (* (clause1,lit1), (clause2, lit2) *) |
|
47 |
| MRR of (int * int) * (int * int) |
|
48 |
| Factor of (int * int * int) (* (clause,lit1, lit2) *) |
|
49 |
| Para of (int * int) * (int * int) |
|
50 |
| Rewrite of (int * int) * (int * int) |
|
51 |
| Obvious of (int * int) |
|
52 |
(*| Hyper of int list*) |
|
53 |
| Unusedstep of unit |
|
54 |
||
55 |
||
56 |
datatype Clausesimp = Binary_s of int * int |
|
57 |
| Factor_s of unit |
|
58 |
| Demod_s of (int * int) list |
|
59 |
| Hyper_s of int list |
|
60 |
| Unusedstep_s of unit |
|
61 |
||
62 |
||
63 |
||
64 |
datatype Step_label = T_info |
|
65 |
|P_info |
|
66 |
||
67 |
||
68 |
fun is_alpha_space_digit_or_neg ch = (ch = "~") orelse (is_alpha ch) orelse (is_digit ch) orelse ( ch = " ") |
|
69 |
||
70 |
||
71 |
||
72 |
fun lit_string_with_nums t = let val termstr = (Sign.string_of_term Mainsign) t |
|
73 |
val exp_term = explode termstr |
|
74 |
in |
|
75 |
implode(List.filter is_alpha_space_digit_or_neg exp_term) |
|
76 |
end |
|
77 |
||
78 |
||
79 |
(****************************************) |
|
80 |
(* Reconstruct an axiom resolution step *) |
|
81 |
(****************************************) |
|
82 |
||
83 |
fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = |
|
84 |
let val this_axiom =(assoc clausenum clauses) |
|
85 |
val (res, numlist, symlist, nsymlist) = (rearrange_clause this_axiom clause_strs allvars) |
|
86 |
val thmvars = thm_vars res |
|
87 |
in |
|
88 |
(res, (Axiom,clause_strs,thmvars ) ) |
|
89 |
end |
|
90 |
||
91 |
(****************************************) |
|
92 |
(* Reconstruct a binary resolution step *) |
|
93 |
(****************************************) |
|
94 |
||
95 |
(* numbers of clauses and literals*) (*vars*) (*list of current thms*) (* literal strings as parsed from spass *) |
|
96 |
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs |
|
97 |
= let |
|
98 |
val thm1 = select_literal (lit1 + 1) (assoc clause1 thml) |
|
99 |
val thm2 = assoc clause2 thml |
|
100 |
val res = thm1 RSN ((lit2 +1), thm2) |
|
101 |
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) |
|
102 |
val thmvars = thm_vars res |
|
103 |
in |
|
104 |
(res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) |
|
105 |
end |
|
106 |
||
107 |
||
108 |
||
109 |
(******************************************************) |
|
110 |
(* Reconstruct a matching replacement resolution step *) |
|
111 |
(******************************************************) |
|
112 |
||
113 |
||
114 |
fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs |
|
115 |
= let |
|
116 |
val thm1 = select_literal (lit1 + 1) (assoc clause1 thml) |
|
117 |
val thm2 = assoc clause2 thml |
|
118 |
val res = thm1 RSN ((lit2 +1), thm2) |
|
119 |
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) |
|
120 |
val thmvars = thm_vars res |
|
121 |
in |
|
122 |
(res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) |
|
123 |
end |
|
124 |
||
125 |
||
126 |
(*******************************************) |
|
127 |
(* Reconstruct a factoring resolution step *) |
|
128 |
(*******************************************) |
|
129 |
||
130 |
fun mksubstlist [] sublist = sublist |
|
131 |
|mksubstlist ((a,b)::rest) sublist = let val vartype = type_of b |
|
132 |
val avar = Var(a,vartype) |
|
133 |
val newlist = ((avar,b)::sublist) in |
|
134 |
mksubstlist rest newlist |
|
135 |
end; |
|
136 |
||
137 |
(* based on Tactic.distinct_subgoals_tac *) |
|
138 |
||
139 |
fun delete_assump_tac state lit = |
|
140 |
let val (frozth,thawfn) = freeze_thaw state |
|
141 |
val froz_prems = cprems_of frozth |
|
142 |
val assumed = implies_elim_list frozth (map assume froz_prems) |
|
143 |
val new_prems = remove_nth lit froz_prems |
|
144 |
val implied = implies_intr_list new_prems assumed |
|
145 |
in |
|
146 |
Seq.single (thawfn implied) |
|
147 |
end |
|
148 |
||
149 |
||
150 |
||
151 |
||
152 |
||
153 |
(*************************************) |
|
154 |
(* Reconstruct a factoring step *) |
|
155 |
(*************************************) |
|
156 |
||
157 |
fun follow_factor clause lit1 lit2 allvars thml clause_strs= |
|
158 |
let |
|
159 |
val th = assoc clause thml |
|
160 |
val prems = prems_of th |
|
161 |
val fac1 = get_nth (lit1+1) prems |
|
162 |
val fac2 = get_nth (lit2+1) prems |
|
163 |
val unif_env = unifiers (Mainsign,myenv, [(fac1, fac2)]) |
|
164 |
val newenv = getnewenv unif_env |
|
165 |
val envlist = alist_of newenv |
|
166 |
||
167 |
val newsubsts = mksubstlist envlist [] |
|
168 |
in |
|
169 |
if (is_Var (fst(hd(newsubsts)))) |
|
170 |
then |
|
171 |
let |
|
172 |
val str1 = lit_string_with_nums (fst (hd newsubsts)); |
|
173 |
val str2 = lit_string_with_nums (snd (hd newsubsts)); |
|
174 |
val facthm = read_instantiate [(str1,str2)] th; |
|
175 |
val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) |
|
176 |
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) |
|
177 |
val thmvars = thm_vars res' |
|
178 |
in |
|
179 |
(res',((Factor (clause, lit1, lit2)),clause_strs,thmvars)) |
|
180 |
end |
|
181 |
else |
|
182 |
let |
|
183 |
val str2 = lit_string_with_nums (fst (hd newsubsts)); |
|
184 |
val str1 = lit_string_with_nums (snd (hd newsubsts)); |
|
185 |
val facthm = read_instantiate [(str1,str2)] th; |
|
186 |
val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) |
|
187 |
val (res', numlist, symlist, nsymlist) = (rearrange_clause res clause_strs allvars) |
|
188 |
val thmvars = thm_vars res' |
|
189 |
in |
|
190 |
(res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) |
|
191 |
end |
|
192 |
end; |
|
193 |
||
194 |
||
195 |
||
196 |
Goal "[| [|Q |] ==> False; [|P|] ==> False; Q; P|] ==> False"; |
|
197 |
val prems = it; |
|
198 |
br (hd prems) 1; |
|
199 |
br (hd(tl(tl prems))) 1; |
|
200 |
qed "merge"; |
|
201 |
||
202 |
||
203 |
||
204 |
fun get_unif_comb t eqterm = if ((type_of t ) = (type_of eqterm)) |
|
205 |
then |
|
206 |
t |
|
207 |
else |
|
208 |
let val {Rand, Rator} = dest_comb t |
|
209 |
in |
|
210 |
get_unif_comb Rand eqterm |
|
211 |
end |
|
212 |
||
213 |
fun get_rhs_unif_lit t eqterm = if (can dest_eq t) |
|
214 |
then |
|
215 |
let val {lhs, rhs} = dest_eq( t) |
|
216 |
in |
|
217 |
rhs |
|
218 |
end |
|
219 |
else |
|
220 |
get_unif_comb t eqterm |
|
221 |
||
222 |
fun get_lhs_unif_lit t eqterm = if (can dest_eq t) |
|
223 |
then |
|
224 |
let val {lhs, rhs} = dest_eq( t) |
|
225 |
in |
|
226 |
lhs |
|
227 |
end |
|
228 |
else |
|
229 |
get_unif_comb t eqterm |
|
230 |
||
231 |
||
232 |
(*************************************) |
|
233 |
(* Reconstruct a paramodulation step *) |
|
234 |
(*************************************) |
|
235 |
||
236 |
val rev_subst = rotate_prems 1 subst; |
|
237 |
val rev_ssubst = rotate_prems 1 ssubst; |
|
238 |
||
239 |
||
240 |
(* have changed from negate_nead to negate_head. God knows if this will actually work *) |
|
241 |
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= |
|
242 |
let |
|
243 |
val th1 = assoc clause1 thml |
|
244 |
val th2 = assoc clause2 thml |
|
245 |
val eq_lit_th = select_literal (lit1+1) th1 |
|
246 |
val mod_lit_th = select_literal (lit2+1) th2 |
|
247 |
val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
248 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) |
|
249 |
val newth' =negate_head newth |
|
250 |
val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars |
|
251 |
handle Not_in_list => let |
|
252 |
val mod_lit_th' = mod_lit_th RS not_sym |
|
253 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst) |
|
254 |
val newth' =negate_head newth |
|
255 |
in |
|
256 |
(rearrange_clause newth' clause_strs allvars) |
|
257 |
end) |
|
258 |
val thmvars = thm_vars res |
|
259 |
in |
|
260 |
(res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) |
|
261 |
end |
|
262 |
||
263 |
(* |
|
264 |
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs= |
|
265 |
let |
|
266 |
val th1 = assoc clause1 thml |
|
267 |
val th2 = assoc clause2 thml |
|
268 |
val eq_lit_th = select_literal (lit1+1) th1 |
|
269 |
val mod_lit_th = select_literal (lit2+1) th2 |
|
270 |
val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
271 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) |
|
272 |
val newth' =negate_nead newth |
|
273 |
val (res, numlist, symlist, nsymlist) = (rearrange_clause newth' clause_strs allvars) |
|
274 |
val thmvars = thm_vars res |
|
275 |
in |
|
276 |
(res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) |
|
277 |
end |
|
278 |
||
279 |
*) |
|
280 |
||
281 |
||
282 |
(********************************) |
|
283 |
(* Reconstruct a rewriting step *) |
|
284 |
(********************************) |
|
285 |
||
286 |
(* |
|
287 |
||
288 |
val rev_subst = rotate_prems 1 subst; |
|
289 |
||
290 |
fun paramod_rule ((cl1, lit1), (cl2 , lit2)) = |
|
291 |
let val eq_lit_th = select_literal (lit1+1) cl1 |
|
292 |
val mod_lit_th = select_literal (lit2+1) cl2 |
|
293 |
val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
294 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 |
|
295 |
eqsubst) |
|
296 |
in negated_asm_of_head newth end; |
|
297 |
||
298 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 |
|
299 |
eqsubst) |
|
300 |
||
301 |
val mod_lit_th' = mod_lit_th RS not_sym |
|
302 |
||
303 |
*) |
|
304 |
||
305 |
||
306 |
fun delete_assumps 0 th = th |
|
307 |
| delete_assumps n th = let val th_prems = length (prems_of th) |
|
308 |
val th' = hd (Seq.list_of(delete_assump_tac th (th_prems -1))) |
|
309 |
in |
|
310 |
delete_assumps (n-1) th' |
|
311 |
end |
|
312 |
||
313 |
(* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *) |
|
314 |
(* changed negate_nead to negate_head here too*) |
|
315 |
(* clause1, lit1 is thing to rewrite with *) |
|
316 |
fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs= |
|
317 |
||
318 |
let val th1 = assoc clause1 thml |
|
319 |
val th2 = assoc clause2 thml |
|
320 |
val eq_lit_th = select_literal (lit1+1) th1 |
|
321 |
val mod_lit_th = select_literal (lit2+1) th2 |
|
322 |
val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
323 |
val eq_lit_prem_num = length (prems_of eq_lit_th) |
|
324 |
val sign = Sign.merge (sign_of_thm th1, sign_of_thm th2) |
|
325 |
val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 |
|
326 |
eqsubst) |
|
327 |
||
328 |
val newthm = negate_head newth |
|
329 |
val newthm' = delete_assumps eq_lit_prem_num newthm |
|
330 |
val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars) |
|
331 |
val thmvars = thm_vars res |
|
332 |
in |
|
333 |
(res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) |
|
334 |
end |
|
335 |
||
336 |
||
337 |
||
338 |
(*****************************************) |
|
339 |
(* Reconstruct an obvious reduction step *) |
|
340 |
(*****************************************) |
|
341 |
||
342 |
||
343 |
fun follow_obvious (clause1, lit1) allvars thml clause_strs= |
|
344 |
let val th1 = assoc clause1 thml |
|
345 |
val prems1 = prems_of th1 |
|
346 |
val newthm = refl RSN ((lit1+ 1), th1) |
|
347 |
handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1))) |
|
348 |
val (res, numlist, symlist, nsymlist) =(rearrange_clause newthm clause_strs allvars) |
|
349 |
val thmvars = thm_vars res |
|
350 |
in |
|
351 |
(res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) |
|
352 |
end |
|
353 |
||
354 |
(**************************************************************************************) |
|
355 |
(* reconstruct a single line of the res. proof - depending on what sort of proof step it was*) |
|
356 |
(**************************************************************************************) |
|
357 |
||
358 |
fun follow_proof clauses allvars clausenum thml (Axiom ) clause_strs |
|
359 |
= follow_axiom clauses allvars clausenum thml clause_strs |
|
360 |
||
361 |
| follow_proof clauses allvars clausenum thml (Binary (a, b)) clause_strs |
|
362 |
= follow_binary (a, b) allvars thml clause_strs |
|
363 |
||
364 |
| follow_proof clauses allvars clausenum thml (MRR (a, b)) clause_strs |
|
365 |
= follow_mrr (a, b) allvars thml clause_strs |
|
366 |
||
367 |
| follow_proof clauses allvars clausenum thml (Factor (a, b, c)) clause_strs |
|
368 |
= follow_factor a b c allvars thml clause_strs |
|
369 |
||
370 |
| follow_proof clauses allvars clausenum thml (Para (a, b)) clause_strs |
|
371 |
= follow_standard_para (a, b) allvars thml clause_strs |
|
372 |
||
373 |
| follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs |
|
374 |
= follow_rewrite (a,b) allvars thml clause_strs |
|
375 |
||
376 |
| follow_proof clauses allvars clausenum thml (Obvious (a,b)) clause_strs |
|
377 |
= follow_obvious (a,b) allvars thml clause_strs |
|
378 |
||
379 |
(*| follow_proof clauses clausenum thml (Hyper l) |
|
380 |
= follow_hyper l thml*) |
|
381 |
| follow_proof clauses allvars clausenum thml _ _ = |
|
382 |
raise ASSERTION "proof step not implemented" |
|
383 |
||
384 |
||
385 |
||
386 |
||
387 |
(**************************************************************************************) |
|
388 |
(* reconstruct a single line of the res. proof - at the moment do only inference steps*) |
|
389 |
(**************************************************************************************) |
|
390 |
||
391 |
fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons |
|
392 |
= let |
|
393 |
val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs |
|
394 |
val recon_step = (recon_fun) |
|
395 |
in |
|
396 |
(((clause_num, thm)::thml), ((clause_num,recon_step)::recons)) |
|
397 |
end |
|
398 |
||
399 |
(***************************************************************) |
|
400 |
(* follow through the res. proof, creating an Isabelle theorem *) |
|
401 |
(***************************************************************) |
|
402 |
||
403 |
||
404 |
||
405 |
(*fun is_proof_char ch = (case ch of |
|
406 |
||
407 |
"(" => true |
|
408 |
| ")" => true |
|
409 |
| ":" => true |
|
410 |
| "'" => true |
|
411 |
| "&" => true |
|
412 |
| "|" => true |
|
413 |
| "~" => true |
|
414 |
| "." => true |
|
415 |
|(is_alpha ) => true |
|
416 |
|(is_digit) => true |
|
417 |
| _ => false)*) |
|
418 |
||
419 |
fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ") |
|
420 |
||
421 |
fun proofstring x = let val exp = explode x |
|
422 |
in |
|
423 |
List.filter (is_proof_char ) exp |
|
424 |
end |
|
425 |
||
426 |
||
427 |
fun not_newline ch = not (ch = "\n"); |
|
428 |
||
429 |
fun concat_with_and [] str = str |
|
430 |
| concat_with_and (x::[]) str = str^"("^x^")" |
|
431 |
| concat_with_and (x::xs) str = (concat_with_and xs (str^"("^x^")"^" & ")) |
|
432 |
(* |
|
433 |
||
434 |
fun follow clauses [] allvars thml recons = |
|
435 |
let (* val _ = reset show_sorts*) |
|
436 |
val thmstring = concat_with_and (map string_of_thm (map snd thml)) "" |
|
437 |
val thmproofstring = proofstring ( thmstring) |
|
438 |
val no_returns =List.filter not_newline ( thmproofstring) |
|
439 |
val thmstr = implode no_returns |
|
15658
2edb384bf61f
watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley
parents:
15642
diff
changeset
|
440 |
val outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "thml_file"))) |
15642 | 441 |
val _ = TextIO.output(outfile, "thmstr is "^thmstr) |
442 |
val _ = TextIO.flushOut outfile; |
|
443 |
val _ = TextIO.closeOut outfile |
|
444 |
(*val _ = set show_sorts*) |
|
445 |
in |
|
446 |
((snd( hd thml)), recons) |
|
447 |
end |
|
448 |
| follow clauses (h::t) allvars thml recons |
|
449 |
= let |
|
450 |
val (thml', recons') = follow_line clauses allvars thml h recons |
|
451 |
val (thm, recons_list) = follow clauses t allvars thml' recons' |
|
452 |
||
453 |
||
454 |
in |
|
455 |
(thm,recons_list) |
|
456 |
end |
|
457 |
||
458 |
*) |
|
459 |
||
460 |
fun replace_clause_strs [] recons newrecons= (newrecons) |
|
461 |
| replace_clause_strs ((thmnum, thm)::thml) ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = |
|
462 |
let val new_clause_strs = get_meta_lits_bracket thm |
|
463 |
in |
|
464 |
replace_clause_strs thml recons ((clausenum,(step,new_clause_strs,thmvars))::newrecons) |
|
465 |
end |
|
466 |
||
467 |
||
468 |
fun follow clauses [] allvars thml recons = |
|
469 |
let |
|
470 |
val new_recons = replace_clause_strs thml recons [] |
|
471 |
in |
|
472 |
((snd( hd thml)), new_recons) |
|
473 |
end |
|
474 |
||
475 |
| follow clauses (h::t) allvars thml recons |
|
476 |
= let |
|
477 |
val (thml', recons') = follow_line clauses allvars thml h recons |
|
478 |
val (thm, recons_list) = follow clauses t allvars thml' recons' |
|
479 |
in |
|
480 |
(thm,recons_list) |
|
481 |
end |
|
482 |
||
483 |
||
484 |
||
485 |
(* Assume we have the cnf clauses as a list of (clauseno, clause) *) |
|
486 |
(* and the proof as a list of the proper datatype *) |
|
487 |
(* take the cnf clauses of the goal and the proof from the res. prover *) |
|
488 |
(* as a list of type Proofstep and return the thm goal ==> False *) |
|
489 |
||
490 |
fun first_pair (a,b,c) = (a,b); |
|
491 |
||
492 |
fun second_pair (a,b,c) = (b,c); |
|
493 |
||
494 |
fun one_of_three (a,b,c) = a; |
|
495 |
fun two_of_three (a,b,c) = b; |
|
496 |
fun three_of_three (a,b,c) = c; |
|
497 |
||
498 |
||
499 |
(* takes original axioms, proof_steps parsed from spass, variables *) |
|
500 |
||
501 |
fun translate_proof clauses proof allvars |
|
502 |
= let val (thm, recons) = follow clauses proof allvars [] [] |
|
503 |
in |
|
504 |
(thm, (recons)) |
|
505 |
end |
|
506 |
||
507 |
||
508 |
||
509 |
fun remove_tinfo [] = [] |
|
510 |
| remove_tinfo ( (clausenum, step, T_info, newstrs)::xs) = (clausenum, step , newstrs)::(remove_tinfo xs) |