1 (* ID: $Id$ |
|
2 Author: Claire Quigley |
|
3 Copyright 2004 University of Cambridge |
|
4 *) |
|
5 |
|
6 structure ReconTranslateProof = |
|
7 struct |
|
8 |
|
9 fun thm_varnames thm = |
|
10 (Drule.fold_terms o Term.fold_aterms) |
|
11 (fn Var ((x, _), _) => insert (op =) x | _ => I) thm []; |
|
12 |
|
13 exception Reflex_equal; |
|
14 |
|
15 (********************************) |
|
16 (* Proofstep datatype *) |
|
17 (********************************) |
|
18 (* Assume rewrite steps have only two clauses in them just now, but lcl109-5 has Rew[5,3,5,3] *) |
|
19 |
|
20 datatype Side = Left |Right |
|
21 |
|
22 datatype Proofstep = ExtraAxiom |
|
23 | OrigAxiom |
|
24 | VampInput |
|
25 | Axiom |
|
26 | Binary of (int * int) * (int * int) (* (clause1,lit1), (clause2, lit2) *) |
|
27 | MRR of (int * int) * (int * int) |
|
28 | Factor of (int * int * int) (* (clause,lit1, lit2) *) |
|
29 | Para of (int * int) * (int * int) |
|
30 | Super_l of (int * int) * (int * int) |
|
31 | Super_r of (int * int) * (int * int) |
|
32 (*| Rewrite of (int * int) * (int * int) *) |
|
33 | Rewrite of (int * int) list |
|
34 | SortSimp of (int * int) * (int * int) |
|
35 | UnitConf of (int * int) * (int * int) |
|
36 | Obvious of (int * int) |
|
37 | AED of (int*int) |
|
38 | EqualRes of (int*int) |
|
39 | Condense of (int*int) |
|
40 (*| Hyper of int list*) |
|
41 | Unusedstep of unit |
|
42 |
|
43 |
|
44 datatype Clausesimp = Binary_s of int * int |
|
45 | Factor_s of unit |
|
46 | Demod_s of (int * int) list |
|
47 | Hyper_s of int list |
|
48 | Unusedstep_s of unit |
|
49 |
|
50 |
|
51 |
|
52 datatype Step_label = T_info |
|
53 |P_info |
|
54 |
|
55 |
|
56 fun is_alpha_space_digit_or_neg ch = |
|
57 (ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse |
|
58 (ReconOrderClauses.is_digit ch) orelse ( ch = " "); |
|
59 |
|
60 fun string_of_term (Const(s,_)) = s |
|
61 | string_of_term (Free(s,_)) = s |
|
62 | string_of_term (Var(ix,_)) = Term.string_of_vname ix |
|
63 | string_of_term (Bound i) = string_of_int i |
|
64 | string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t |
|
65 | string_of_term (s $ t) = |
|
66 "(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" |
|
67 |
|
68 (* FIXME string_of_term is quite unreliable here *) |
|
69 fun lit_string_with_nums t = let val termstr = string_of_term t |
|
70 val exp_term = explode termstr |
|
71 in |
|
72 implode(List.filter is_alpha_space_digit_or_neg exp_term) |
|
73 end |
|
74 |
|
75 fun reconstruction_failed fname = error (fname ^ ": reconstruction failed") |
|
76 |
|
77 (************************************************) |
|
78 (* Reconstruct an axiom resolution step *) |
|
79 (* clauses is a list of (clausenum,clause) pairs*) |
|
80 (************************************************) |
|
81 |
|
82 fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = |
|
83 let val this_axiom = (the o AList.lookup (op =) clauses) clausenum |
|
84 val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars) |
|
85 val thmvars = thm_varnames res |
|
86 in |
|
87 (res, (Axiom,clause_strs,thmvars ) ) |
|
88 end |
|
89 handle Option => reconstruction_failed "follow_axiom" |
|
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 val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1) |
|
98 val thm2 = (the o AList.lookup (op =) thml) clause2 |
|
99 val res = thm1 RSN ((lit2 +1), thm2) |
|
100 val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars) |
|
101 val thmvars = thm_varnames res |
|
102 in |
|
103 (res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) |
|
104 end |
|
105 handle Option => reconstruction_failed "follow_binary" |
|
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 val thm1 = select_literal (lit1 + 1) ((the o AList.lookup (op =) thml) clause1) |
|
116 val thm2 = (the o AList.lookup (op =) thml) clause2 |
|
117 val res = thm1 RSN ((lit2 +1), thm2) |
|
118 val (res', numlist, symlist, nsymlist) = |
|
119 (ReconOrderClauses.rearrange_clause res clause_strs allvars) |
|
120 val thmvars = thm_varnames res |
|
121 in |
|
122 (res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) |
|
123 end |
|
124 handle Option => reconstruction_failed "follow_mrr" |
|
125 |
|
126 |
|
127 (*******************************************) |
|
128 (* Reconstruct a factoring resolution step *) |
|
129 (*******************************************) |
|
130 |
|
131 fun mksubstlist [] sublist = sublist |
|
132 |mksubstlist ((a, (_, b)) :: rest) sublist = |
|
133 let val vartype = type_of b |
|
134 val avar = Var(a,vartype) |
|
135 val newlist = ((avar,b)::sublist) |
|
136 in |
|
137 mksubstlist rest newlist |
|
138 end; |
|
139 |
|
140 (* based on Tactic.distinct_subgoals_tac *) |
|
141 |
|
142 fun delete_assump_tac state lit = |
|
143 let val (frozth,thawfn) = freeze_thaw state |
|
144 val froz_prems = cprems_of frozth |
|
145 val assumed = implies_elim_list frozth (map assume froz_prems) |
|
146 val new_prems = ReconOrderClauses.remove_nth lit froz_prems |
|
147 val implied = implies_intr_list new_prems assumed |
|
148 in |
|
149 Seq.single (thawfn implied) |
|
150 end |
|
151 |
|
152 |
|
153 |
|
154 |
|
155 |
|
156 (*************************************) |
|
157 (* Reconstruct a factoring step *) |
|
158 (*************************************) |
|
159 |
|
160 fun getnewenv seq = fst (fst (the (Seq.pull seq))); |
|
161 |
|
162 (*FIXME: share code with that in Tools/reconstruction.ML*) |
|
163 fun follow_factor clause lit1 lit2 allvars thml clause_strs = |
|
164 let |
|
165 val th = (the o AList.lookup (op =) thml) clause |
|
166 val prems = prems_of th |
|
167 val sign = sign_of_thm th |
|
168 val fac1 = ReconOrderClauses.get_nth (lit1+1) prems |
|
169 val fac2 = ReconOrderClauses.get_nth (lit2+1) prems |
|
170 val unif_env = Unify.unifiers (sign,Envir.empty 0, [(fac1, fac2)]) |
|
171 val newenv = getnewenv unif_env |
|
172 val envlist = Envir.alist_of newenv |
|
173 |
|
174 val (t1,t2)::_ = mksubstlist envlist [] |
|
175 in |
|
176 if (is_Var t1) |
|
177 then |
|
178 let |
|
179 val str1 = lit_string_with_nums t1; |
|
180 val str2 = lit_string_with_nums t2; |
|
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) = |
|
184 ReconOrderClauses.rearrange_clause res clause_strs allvars |
|
185 val thmvars = thm_varnames res' |
|
186 in |
|
187 (res',((Factor (clause, lit1, lit2)),clause_strs,thmvars)) |
|
188 end |
|
189 else |
|
190 let |
|
191 val str2 = lit_string_with_nums t1; |
|
192 val str1 = lit_string_with_nums t2; |
|
193 val facthm = read_instantiate [(str1,str2)] th; |
|
194 val res = hd (Seq.list_of(delete_assump_tac facthm (lit1 + 1))) |
|
195 val (res', numlist, symlist, nsymlist) = |
|
196 ReconOrderClauses.rearrange_clause res clause_strs allvars |
|
197 val thmvars = thm_varnames res' |
|
198 in |
|
199 (res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) |
|
200 end |
|
201 end |
|
202 handle Option => reconstruction_failed "follow_factor" |
|
203 |
|
204 |
|
205 |
|
206 fun get_unif_comb t eqterm = |
|
207 if ((type_of t) = (type_of eqterm)) |
|
208 then t |
|
209 else |
|
210 let val _ $ rand = t |
|
211 in get_unif_comb rand eqterm end; |
|
212 |
|
213 fun get_unif_lit t eqterm = |
|
214 if (can HOLogic.dest_eq t) |
|
215 then |
|
216 let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm) |
|
217 in lhs end |
|
218 else |
|
219 get_unif_comb t eqterm; |
|
220 |
|
221 |
|
222 |
|
223 (*************************************) |
|
224 (* Reconstruct a paramodulation step *) |
|
225 (*************************************) |
|
226 |
|
227 val rev_subst = rotate_prems 1 subst; |
|
228 val rev_ssubst = rotate_prems 1 ssubst; |
|
229 |
|
230 |
|
231 fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = |
|
232 let |
|
233 val th1 = (the o AList.lookup (op =) thml) clause1 |
|
234 val th2 = (the o AList.lookup (op =) thml) clause2 |
|
235 val eq_lit_th = select_literal (lit1+1) th1 |
|
236 val mod_lit_th = select_literal (lit2+1) th2 |
|
237 val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
238 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) |
|
239 val newth' =negate_head newth |
|
240 val (res, numlist, symlist, nsymlist) = |
|
241 (ReconOrderClauses.rearrange_clause newth' clause_strs allvars |
|
242 handle Not_in_list => |
|
243 let val mod_lit_th' = mod_lit_th RS not_sym |
|
244 val newth = Seq.hd (biresolution false [(false, mod_lit_th')] 1 eqsubst) |
|
245 val newth' =negate_head newth |
|
246 in |
|
247 ReconOrderClauses.rearrange_clause newth' clause_strs allvars |
|
248 end) |
|
249 val thmvars = thm_varnames res |
|
250 in |
|
251 (res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) |
|
252 end |
|
253 handle Option => reconstruction_failed "follow_standard_para" |
|
254 |
|
255 |
|
256 (********************************) |
|
257 (* Reconstruct a rewriting step *) |
|
258 (********************************) |
|
259 |
|
260 (* |
|
261 |
|
262 val rev_subst = rotate_prems 1 subst; |
|
263 |
|
264 fun paramod_rule ((cl1, lit1), (cl2 , lit2)) = |
|
265 let val eq_lit_th = select_literal (lit1+1) cl1 |
|
266 val mod_lit_th = select_literal (lit2+1) cl2 |
|
267 val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
268 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 |
|
269 eqsubst) |
|
270 in Meson.negated_asm_of_head newth end; |
|
271 |
|
272 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 |
|
273 eqsubst) |
|
274 |
|
275 val mod_lit_th' = mod_lit_th RS not_sym |
|
276 |
|
277 *) |
|
278 |
|
279 |
|
280 fun delete_assumps 0 th = th |
|
281 | delete_assumps n th = let val th_prems = length (prems_of th) |
|
282 val th' = hd (Seq.list_of(delete_assump_tac th (th_prems -1))) |
|
283 in |
|
284 delete_assumps (n-1) th' |
|
285 end |
|
286 |
|
287 (* extra conditions from the equality turn up as 2nd to last literals of result. Need to delete them *) |
|
288 (* changed negate_nead to negate_head here too*) |
|
289 (* clause1, lit1 is thing to rewrite with *) |
|
290 (*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = |
|
291 let val th1 = (the o AList.lookup (op =) thml) clause1 |
|
292 val th2 = (the o AList.lookup (op =) thml) clause2 |
|
293 val eq_lit_th = select_literal (lit1+1) th1 |
|
294 val mod_lit_th = select_literal (lit2+1) th2 |
|
295 val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
296 val eq_lit_prem_num = length (prems_of eq_lit_th) |
|
297 val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2) |
|
298 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) |
|
299 val newthm = negate_head newth |
|
300 val newthm' = delete_assumps eq_lit_prem_num newthm |
|
301 val (res, numlist, symlist, nsymlist) = |
|
302 ReconOrderClauses.rearrange_clause newthm clause_strs allvars |
|
303 val thmvars = thm_varnames res |
|
304 in |
|
305 (res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) |
|
306 end |
|
307 handle Option => reconstruction_failed "follow_rewrite" |
|
308 |
|
309 *) |
|
310 |
|
311 (*****************************************) |
|
312 (* Reconstruct an obvious reduction step *) |
|
313 (*****************************************) |
|
314 |
|
315 |
|
316 fun follow_obvious (clause1, lit1) allvars thml clause_strs = |
|
317 let val th1 = (the o AList.lookup (op =) thml) clause1 |
|
318 val prems1 = prems_of th1 |
|
319 val newthm = refl RSN ((lit1+ 1), th1) |
|
320 handle THM _ => hd (Seq.list_of(delete_assump_tac th1 (lit1 + 1))) |
|
321 val (res, numlist, symlist, nsymlist) = |
|
322 ReconOrderClauses.rearrange_clause newthm clause_strs allvars |
|
323 val thmvars = thm_varnames res |
|
324 in |
|
325 (res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) |
|
326 end |
|
327 handle Option => reconstruction_failed "follow_obvious" |
|
328 |
|
329 (**************************************************************************************) |
|
330 (* reconstruct a single line of the res. proof - depending on what sort of proof step it was*) |
|
331 (**************************************************************************************) |
|
332 |
|
333 fun follow_proof clauses allvars clausenum thml (Axiom ) clause_strs |
|
334 = follow_axiom clauses allvars clausenum thml clause_strs |
|
335 |
|
336 | follow_proof clauses allvars clausenum thml (Binary (a, b)) clause_strs |
|
337 = follow_binary (a, b) allvars thml clause_strs |
|
338 |
|
339 | follow_proof clauses allvars clausenum thml (MRR (a, b)) clause_strs |
|
340 = follow_mrr (a, b) allvars thml clause_strs |
|
341 |
|
342 | follow_proof clauses allvars clausenum thml (Factor (a, b, c)) clause_strs |
|
343 = follow_factor a b c allvars thml clause_strs |
|
344 |
|
345 | follow_proof clauses allvars clausenum thml (Para (a, b)) clause_strs |
|
346 = follow_standard_para (a, b) allvars thml clause_strs |
|
347 |
|
348 (* | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs |
|
349 = follow_rewrite (a,b) allvars thml clause_strs*) |
|
350 |
|
351 | follow_proof clauses allvars clausenum thml (Obvious (a,b)) clause_strs |
|
352 = follow_obvious (a,b) allvars thml clause_strs |
|
353 |
|
354 (*| follow_proof clauses clausenum thml (Hyper l) |
|
355 = follow_hyper l thml*) |
|
356 | follow_proof clauses allvars clausenum thml _ _ = |
|
357 error "proof step not implemented" |
|
358 |
|
359 |
|
360 |
|
361 |
|
362 (**************************************************************************************) |
|
363 (* reconstruct a single line of the res. proof - at the moment do only inference steps*) |
|
364 (**************************************************************************************) |
|
365 |
|
366 fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons = |
|
367 let |
|
368 val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs |
|
369 in |
|
370 ((clause_num, thm)::thml, (clause_num,recon_fun)::recons) |
|
371 end |
|
372 |
|
373 (***************************************************************) |
|
374 (* follow through the res. proof, creating an Isabelle theorem *) |
|
375 (***************************************************************) |
|
376 |
|
377 fun is_proof_char ch = ((33 <= (ord ch)) andalso ((ord ch ) <= 126)) orelse (ch = " ") |
|
378 |
|
379 fun proofstring x = let val exp = explode x |
|
380 in |
|
381 List.filter (is_proof_char ) exp |
|
382 end |
|
383 |
|
384 fun replace_clause_strs [] recons newrecons = (newrecons) |
|
385 | replace_clause_strs ((thmnum, thm)::thml) |
|
386 ((clausenum,(step,clause_strs,thmvars))::recons) newrecons = |
|
387 let val new_clause_strs = ReconOrderClauses.get_meta_lits_bracket thm |
|
388 in |
|
389 replace_clause_strs thml recons |
|
390 ((clausenum,(step,new_clause_strs,thmvars))::newrecons) |
|
391 end |
|
392 |
|
393 |
|
394 fun follow clauses [] allvars thml recons = |
|
395 let |
|
396 val new_recons = replace_clause_strs thml recons [] |
|
397 in |
|
398 (#2(hd thml), new_recons) |
|
399 end |
|
400 | follow clauses (h::t) allvars thml recons = |
|
401 let |
|
402 val (thml', recons') = follow_line clauses allvars thml h recons |
|
403 val (thm, recons_list) = follow clauses t allvars thml' recons' |
|
404 in |
|
405 (thm,recons_list) |
|
406 end |
|
407 |
|
408 (* Assume we have the cnf clauses as a list of (clauseno, clause) *) |
|
409 (* and the proof as a list of the proper datatype *) |
|
410 (* take the cnf clauses of the goal and the proof from the res. prover *) |
|
411 (* as a list of type Proofstep and return the thm goal ==> False *) |
|
412 |
|
413 (* takes original axioms, proof_steps parsed from spass, variables *) |
|
414 |
|
415 fun translate_proof clauses proof allvars |
|
416 = let val (thm, recons) = follow clauses proof allvars [] [] |
|
417 in |
|
418 (thm, (recons)) |
|
419 end |
|
420 |
|
421 end; |
|