6 |
6 |
7 (*Attributes for reconstructing external resolution proofs*) |
7 (*Attributes for reconstructing external resolution proofs*) |
8 |
8 |
9 structure Reconstruction = |
9 structure Reconstruction = |
10 struct |
10 struct |
11 |
|
12 (**************************************************************) |
|
13 (* extra functions necessary for factoring and paramodulation *) |
|
14 (**************************************************************) |
|
15 |
|
16 fun mksubstlist [] sublist = sublist |
|
17 | mksubstlist ((a, (_, b)) :: rest) sublist = |
|
18 let val vartype = type_of b |
|
19 val avar = Var(a,vartype) |
|
20 val newlist = ((avar,b)::sublist) |
|
21 in mksubstlist rest newlist end; |
|
22 |
|
23 |
11 |
24 (**** attributes ****) |
12 (**** attributes ****) |
25 |
13 |
26 (** Binary resolution **) |
14 (** Binary resolution **) |
27 |
15 |
32 val binary = Attrib.syntax |
20 val binary = Attrib.syntax |
33 (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
21 (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
34 >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); |
22 >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); |
35 |
23 |
36 |
24 |
37 fun inst_single sign t1 t2 cl = |
25 (** Factoring **) |
38 let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2 |
|
39 in hd (Seq.list_of(distinct_subgoals_tac |
|
40 (cterm_instantiate [(ct1,ct2)] cl))) |
|
41 end; |
|
42 |
26 |
43 fun inst_subst sign substs cl = |
27 (*NB this code did not work at all before 29/6/2006. Even now its behaviour may |
44 if (is_Var (fst(hd(substs)))) |
28 not be as expected. It unifies the designated literals |
45 then inst_single sign (fst (hd substs)) (snd (hd substs)) cl |
29 and then deletes ALL duplicates of literals (not just those designated)*) |
46 else if (is_Var (snd(hd(substs)))) |
|
47 then inst_single sign (snd (hd substs)) (fst (hd substs)) cl |
|
48 else raise THM ("inst_subst", 0, [cl]); |
|
49 |
30 |
|
31 fun mksubstlist [] sublist = sublist |
|
32 | mksubstlist ((a, (T, b)) :: rest) sublist = |
|
33 mksubstlist rest ((Var(a,T), b)::sublist); |
50 |
34 |
51 (** Factoring **) |
35 fun reorient (x,y) = |
|
36 if is_Var x then (x,y) |
|
37 else if is_Var y then (y,x) |
|
38 else error "Reconstruction.reorient: neither term is a Var"; |
|
39 |
|
40 fun inst_subst sign subst cl = |
|
41 let val subst' = map (pairself (cterm_of sign) o reorient) subst |
|
42 in |
|
43 Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl)) |
|
44 end; |
52 |
45 |
53 fun factor_rule (cl, lit1, lit2) = |
46 fun factor_rule (cl, lit1, lit2) = |
54 let |
47 let |
55 val prems = prems_of cl |
48 val prems = prems_of cl |
56 val fac1 = List.nth (prems,lit1) |
49 val fac1 = List.nth (prems,lit1) |