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