author | paulson |
Mon, 28 Aug 2006 18:18:31 +0200 | |
changeset 20423 | 593053389701 |
parent 20294 | a69cda724b5a |
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 |
|
16803 | 6 |
structure ReconTranslateProof = |
7 |
struct |
|
8 |
||
20294 | 9 |
fun thm_varnames thm = |
10 |
(Drule.fold_terms o Term.fold_aterms) |
|
11 |
(fn Var ((x, _), _) => insert (op =) x | _ => I) thm []; |
|
15642 | 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 |
||
16803 | 22 |
datatype Proofstep = ExtraAxiom |
16418 | 23 |
| OrigAxiom |
24 |
| VampInput |
|
15642 | 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) |
|
16357 | 30 |
| Super_l of (int * int) * (int * int) |
31 |
| Super_r of (int * int) * (int * int) |
|
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16433
diff
changeset
|
32 |
(*| Rewrite of (int * int) * (int * int) *) |
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16433
diff
changeset
|
33 |
| Rewrite of (int * int) list |
16357 | 34 |
| SortSimp of (int * int) * (int * int) |
35 |
| UnitConf of (int * int) * (int * int) |
|
15642 | 36 |
| Obvious of (int * int) |
16357 | 37 |
| AED of (int*int) |
38 |
| EqualRes of (int*int) |
|
39 |
| Condense of (int*int) |
|
15642 | 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 |
||
16061 | 56 |
fun is_alpha_space_digit_or_neg ch = |
57 |
(ch = "~") orelse (ReconOrderClauses.is_alpha ch) orelse |
|
58 |
(ReconOrderClauses.is_digit ch) orelse ( ch = " "); |
|
15642 | 59 |
|
19643
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
60 |
fun string_of_term (Const(s,_)) = s |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
61 |
| string_of_term (Free(s,_)) = s |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
62 |
| string_of_term (Var(ix,_)) = Term.string_of_vname ix |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
63 |
| string_of_term (Bound i) = string_of_int i |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
64 |
| string_of_term (Abs(x,_,t)) = "%" ^ x ^ ". " ^ string_of_term t |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
65 |
| string_of_term (s $ t) = |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
66 |
"(" ^ string_of_term s ^ " " ^ string_of_term t ^ ")" |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
67 |
|
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
68 |
(* FIXME string_of_term is quite unreliable here *) |
213e12ad2c03
added low-level string_of_term (back again from term.ML) -- should avoid this altogether;
wenzelm
parents:
17776
diff
changeset
|
69 |
fun lit_string_with_nums t = let val termstr = string_of_term t |
15642 | 70 |
val exp_term = explode termstr |
71 |
in |
|
72 |
implode(List.filter is_alpha_space_digit_or_neg exp_term) |
|
73 |
end |
|
74 |
||
15774 | 75 |
fun reconstruction_failed fname = error (fname ^ ": reconstruction failed") |
15642 | 76 |
|
15919
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15794
diff
changeset
|
77 |
(************************************************) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15794
diff
changeset
|
78 |
(* Reconstruct an axiom resolution step *) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15794
diff
changeset
|
79 |
(* clauses is a list of (clausenum,clause) pairs*) |
b30a35432f5a
Replaced reference to SPASS with general one - set SPASS_HOME in settings file.
quigley
parents:
15794
diff
changeset
|
80 |
(************************************************) |
15642 | 81 |
|
15774 | 82 |
fun follow_axiom clauses allvars (clausenum:int) thml clause_strs = |
17374 | 83 |
let val this_axiom = (the o AList.lookup (op =) clauses) clausenum |
16061 | 84 |
val (res, numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause this_axiom clause_strs allvars) |
20294 | 85 |
val thmvars = thm_varnames res |
16061 | 86 |
in |
87 |
(res, (Axiom,clause_strs,thmvars ) ) |
|
88 |
end |
|
89 |
handle Option => reconstruction_failed "follow_axiom" |
|
15642 | 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 *) |
|
16061 | 96 |
fun follow_binary ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = |
17374 | 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 |
|
16061 | 99 |
val res = thm1 RSN ((lit2 +1), thm2) |
100 |
val (res', numlist, symlist, nsymlist) = (ReconOrderClauses.rearrange_clause res clause_strs allvars) |
|
20294 | 101 |
val thmvars = thm_varnames res |
16061 | 102 |
in |
103 |
(res', ((Binary ((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars) ) |
|
104 |
end |
|
105 |
handle Option => reconstruction_failed "follow_binary" |
|
15642 | 106 |
|
107 |
||
108 |
||
109 |
(******************************************************) |
|
110 |
(* Reconstruct a matching replacement resolution step *) |
|
111 |
(******************************************************) |
|
112 |
||
113 |
||
16061 | 114 |
fun follow_mrr ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = |
17374 | 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 |
|
16061 | 117 |
val res = thm1 RSN ((lit2 +1), thm2) |
118 |
val (res', numlist, symlist, nsymlist) = |
|
119 |
(ReconOrderClauses.rearrange_clause res clause_strs allvars) |
|
20294 | 120 |
val thmvars = thm_varnames res |
16061 | 121 |
in |
122 |
(res', ((MRR ((clause1, lit1), (clause2 , lit2))) ,clause_strs,thmvars)) |
|
123 |
end |
|
124 |
handle Option => reconstruction_failed "follow_mrr" |
|
15642 | 125 |
|
126 |
||
127 |
(*******************************************) |
|
128 |
(* Reconstruct a factoring resolution step *) |
|
129 |
(*******************************************) |
|
130 |
||
131 |
fun mksubstlist [] sublist = sublist |
|
16061 | 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; |
|
15642 | 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) |
|
16061 | 146 |
val new_prems = ReconOrderClauses.remove_nth lit froz_prems |
15642 | 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 |
||
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
160 |
fun getnewenv seq = fst (fst (the (Seq.pull seq))); |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
161 |
|
15739
bb2acfed8212
yet more tidying up: removal of some references to Main
paulson
parents:
15736
diff
changeset
|
162 |
(*FIXME: share code with that in Tools/reconstruction.ML*) |
16061 | 163 |
fun follow_factor clause lit1 lit2 allvars thml clause_strs = |
164 |
let |
|
17374 | 165 |
val th = (the o AList.lookup (op =) thml) clause |
16061 | 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 |
|
20294 | 185 |
val thmvars = thm_varnames res' |
16061 | 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 |
|
20294 | 197 |
val thmvars = thm_varnames res' |
16061 | 198 |
in |
199 |
(res', ((Factor (clause, lit1, lit2)),clause_strs, thmvars)) |
|
200 |
end |
|
201 |
end |
|
202 |
handle Option => reconstruction_failed "follow_factor" |
|
15642 | 203 |
|
204 |
||
205 |
||
15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
206 |
fun get_unif_comb t eqterm = |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
207 |
if ((type_of t) = (type_of eqterm)) |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
208 |
then t |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
209 |
else |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
210 |
let val _ $ rand = t |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
211 |
in get_unif_comb rand eqterm end; |
15642 | 212 |
|
15684
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
213 |
fun get_unif_lit t eqterm = |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
214 |
if (can HOLogic.dest_eq t) |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
215 |
then |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
216 |
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
|
217 |
in lhs end |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
218 |
else |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
219 |
get_unif_comb t eqterm; |
5ec4d21889d6
Reconstruction code, now packaged to avoid name clashes
paulson
parents:
15658
diff
changeset
|
220 |
|
15642 | 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 |
||
16061 | 231 |
fun follow_standard_para ((clause1, lit1), (clause2 , lit2)) allvars thml clause_strs = |
232 |
let |
|
17374 | 233 |
val th1 = (the o AList.lookup (op =) thml) clause1 |
234 |
val th2 = (the o AList.lookup (op =) thml) clause2 |
|
16061 | 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) |
|
20294 | 249 |
val thmvars = thm_varnames res |
16061 | 250 |
in |
251 |
(res, ((Para((clause1, lit1), (clause2 , lit2))),clause_strs,thmvars)) |
|
252 |
end |
|
253 |
handle Option => reconstruction_failed "follow_standard_para" |
|
15642 | 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) |
|
15697 | 270 |
in Meson.negated_asm_of_head newth end; |
15642 | 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 *) |
|
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16433
diff
changeset
|
290 |
(*fun follow_rewrite ((clause1, lit1), (clause2, lit2)) allvars thml clause_strs = |
17374 | 291 |
let val th1 = (the o AList.lookup (op =) thml) clause1 |
292 |
val th2 = (the o AList.lookup (op =) thml) clause2 |
|
16061 | 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) |
|
16433 | 297 |
val sign = Theory.merge (sign_of_thm th1, sign_of_thm th2) |
16061 | 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 |
|
20294 | 303 |
val thmvars = thm_varnames res |
16061 | 304 |
in |
305 |
(res, ((Rewrite ((clause1, lit1), (clause2, lit2))),clause_strs,thmvars)) |
|
306 |
end |
|
307 |
handle Option => reconstruction_failed "follow_rewrite" |
|
15642 | 308 |
|
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16433
diff
changeset
|
309 |
*) |
15642 | 310 |
|
311 |
(*****************************************) |
|
312 |
(* Reconstruct an obvious reduction step *) |
|
313 |
(*****************************************) |
|
314 |
||
315 |
||
16061 | 316 |
fun follow_obvious (clause1, lit1) allvars thml clause_strs = |
17374 | 317 |
let val th1 = (the o AList.lookup (op =) thml) clause1 |
16061 | 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 |
|
20294 | 323 |
val thmvars = thm_varnames res |
16061 | 324 |
in |
325 |
(res, ((Obvious (clause1, lit1)),clause_strs,thmvars)) |
|
326 |
end |
|
327 |
handle Option => reconstruction_failed "follow_obvious" |
|
15642 | 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 |
||
16548
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16433
diff
changeset
|
348 |
(* | follow_proof clauses allvars clausenum thml (Rewrite (a,b)) clause_strs |
aa36ae6b955e
Temporarily removed Rewrite from the translation code so that parsing with work on lists of numbers.
quigley
parents:
16433
diff
changeset
|
349 |
= follow_rewrite (a,b) allvars thml clause_strs*) |
15642 | 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 _ _ = |
|
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
357 |
error "proof step not implemented" |
15642 | 358 |
|
359 |
||
360 |
||
361 |
||
362 |
(**************************************************************************************) |
|
363 |
(* reconstruct a single line of the res. proof - at the moment do only inference steps*) |
|
364 |
(**************************************************************************************) |
|
365 |
||
17488
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
366 |
fun follow_line clauses allvars thml (clause_num, proof_step, clause_strs) recons = |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
367 |
let |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
368 |
val (thm, recon_fun) = follow_proof clauses allvars clause_num thml proof_step clause_strs |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
369 |
in |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
370 |
((clause_num, thm)::thml, (clause_num,recon_fun)::recons) |
67376a311a2b
further simplification of the Isabelle-ATP linkup
paulson
parents:
17374
diff
changeset
|
371 |
end |
15642 | 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 |
||
16061 | 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 |
|
15642 | 392 |
|
393 |
||
394 |
fun follow clauses [] allvars thml recons = |
|
16061 | 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 |
|
15642 | 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 |
||
16803 | 421 |
end; |