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