1 (* Title: HOL/Reconstruction.thy |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson and Claire Quigley |
|
4 Copyright 2004 University of Cambridge |
|
5 *) |
|
6 |
|
7 (*Attributes for reconstructing external resolution proofs*) |
|
8 |
|
9 structure Reconstruction = |
|
10 struct |
|
11 |
|
12 (**** attributes ****) |
|
13 |
|
14 (** Binary resolution **) |
|
15 |
|
16 fun binary_rule ((cl1, lit1), (cl2 , lit2)) = |
|
17 select_literal (lit1 + 1) cl1 |
|
18 RSN ((lit2 + 1), cl2); |
|
19 |
|
20 val binary = Attrib.syntax |
|
21 (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
|
22 >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j))))); |
|
23 |
|
24 |
|
25 (** Factoring **) |
|
26 |
|
27 (*NB this code did not work at all before 29/6/2006. Even now its behaviour may |
|
28 not be as expected. It unifies the designated literals |
|
29 and then deletes ALL duplicates of literals (not just those designated)*) |
|
30 |
|
31 fun mksubstlist [] sublist = sublist |
|
32 | mksubstlist ((a, (T, b)) :: rest) sublist = |
|
33 mksubstlist rest ((Var(a,T), b)::sublist); |
|
34 |
|
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; |
|
45 |
|
46 fun getnewenv seq = fst (fst (the (Seq.pull seq))); |
|
47 |
|
48 fun factor_rule (cl, lit1, lit2) = |
|
49 let |
|
50 val prems = prems_of cl |
|
51 val fac1 = List.nth (prems,lit1) |
|
52 val fac2 = List.nth (prems,lit2) |
|
53 val sign = sign_of_thm cl |
|
54 val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)]) |
|
55 val newenv = getnewenv unif_env |
|
56 val envlist = Envir.alist_of newenv |
|
57 in |
|
58 inst_subst sign (mksubstlist envlist []) cl |
|
59 end; |
|
60 |
|
61 val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat) |
|
62 >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j)))); |
|
63 |
|
64 |
|
65 (** Paramodulation **) |
|
66 |
|
67 (*subst with premises exchanged: that way, side literals of the equality will appear |
|
68 as the second to last premises of the result.*) |
|
69 val rev_subst = rotate_prems 1 subst; |
|
70 |
|
71 fun paramod_rule ((cl1, lit1), (cl2, lit2)) = |
|
72 let val eq_lit_th = select_literal (lit1+1) cl1 |
|
73 val mod_lit_th = select_literal (lit2+1) cl2 |
|
74 val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
75 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst) |
|
76 val newth' = Seq.hd (flexflex_rule newth) |
|
77 in Meson.negated_asm_of_head newth' end; |
|
78 |
|
79 |
|
80 val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
|
81 >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j))))); |
|
82 |
|
83 |
|
84 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **) |
|
85 |
|
86 fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) = |
|
87 let val eq_lit_th = select_literal (lit1+1) cl1 |
|
88 val mod_lit_th = select_literal (lit2+1) cl2 |
|
89 val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt |
|
90 val eqsubst = eq_lit_th RSN (2,rev_subst) |
|
91 val newth = |
|
92 Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst) |
|
93 |> singleton (Variable.export ctxt' ctxt) |
|
94 in Meson.negated_asm_of_head newth end; |
|
95 |
|
96 val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat |
|
97 >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A => |
|
98 demod_rule (Context.proof_of context) ((A, i), (B, j))))); |
|
99 |
|
100 |
|
101 (** Conversion of a theorem into clauses **) |
|
102 |
|
103 (*For efficiency, we rely upon memo-izing in ResAxioms.*) |
|
104 fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i) |
|
105 |
|
106 val clausify = Attrib.syntax (Scan.lift Args.nat |
|
107 >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i)))); |
|
108 |
|
109 |
|
110 (** theory setup **) |
|
111 |
|
112 val setup = |
|
113 Attrib.add_attributes |
|
114 [("binary", binary, "binary resolution"), |
|
115 ("paramod", paramod, "paramodulation"), |
|
116 ("demod", demod, "demodulation"), |
|
117 ("factor", factor, "factoring"), |
|
118 ("clausify", clausify, "conversion to clauses")]; |
|
119 |
|
120 end |
|