163 |
161 |
164 |
162 |
165 (*************************************) |
163 (*************************************) |
166 (* Reconstruct a factoring step *) |
164 (* Reconstruct a factoring step *) |
167 (*************************************) |
165 (*************************************) |
|
166 |
|
167 fun getnewenv seq = fst (fst (the (Seq.pull seq))); |
168 |
168 |
169 (*FIXME: share code with that in Tools/reconstruction.ML*) |
169 (*FIXME: share code with that in Tools/reconstruction.ML*) |
170 fun follow_factor clause lit1 lit2 allvars thml clause_strs = |
170 fun follow_factor clause lit1 lit2 allvars thml clause_strs = |
171 let |
171 let |
172 val th = (the o AList.lookup (op =) thml) clause |
172 val th = (the o AList.lookup (op =) thml) clause |
359 = follow_obvious (a,b) allvars thml clause_strs |
359 = follow_obvious (a,b) allvars thml clause_strs |
360 |
360 |
361 (*| follow_proof clauses clausenum thml (Hyper l) |
361 (*| follow_proof clauses clausenum thml (Hyper l) |
362 = follow_hyper l thml*) |
362 = follow_hyper l thml*) |
363 | follow_proof clauses allvars clausenum thml _ _ = |
363 | follow_proof clauses allvars clausenum thml _ _ = |
364 raise ASSERTION "proof step not implemented" |
364 error "proof step not implemented" |
365 |
365 |
366 |
366 |
367 |
367 |
368 |
368 |
369 (**************************************************************************************) |
369 (**************************************************************************************) |
370 (* reconstruct a single line of the res. proof - at the moment do only inference steps*) |
370 (* reconstruct a single line of the res. proof - at the moment do only inference steps*) |
371 (**************************************************************************************) |
371 (**************************************************************************************) |
372 |
372 |
373 fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons |
373 fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons = |
374 = let |
374 let |
375 val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs |
375 val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs |
376 val recon_step = (recon_fun) |
376 in |
377 in |
377 ((clause_num, thm)::thml, (clause_num,recon_fun)::recons) |
378 (((clause_num, thm)::thml), ((clause_num,recon_step)::recons)) |
378 end |
379 end |
|
380 |
379 |
381 (***************************************************************) |
380 (***************************************************************) |
382 (* follow through the res. proof, creating an Isabelle theorem *) |
381 (* follow through the res. proof, creating an Isabelle theorem *) |
383 (***************************************************************) |
382 (***************************************************************) |
384 |
383 |