1 (* Title: HOL/Reconstruction.thy
3 Author: Lawrence C Paulson and Claire Quigley
4 Copyright 2004 University of Cambridge
7 (*Attributes for reconstructing external resolution proofs*)
9 structure Reconstruction =
12 (**************************************************************)
13 (* extra functions necessary for factoring and paramodulation *)
14 (**************************************************************)
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;
24 (**** attributes ****)
26 (** Binary resolution **)
28 fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
29 select_literal (lit1 + 1) cl1
30 RSN ((lit2 + 1), cl2);
32 val binary = Attrib.syntax
33 (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)))));
37 fun inst_single sign t1 t2 cl =
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)))
43 fun inst_subst sign substs cl =
44 if (is_Var (fst(hd(substs))))
45 then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
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]);
53 fun factor_rule (cl, lit1, lit2) =
55 val prems = prems_of cl
56 val fac1 = List.nth (prems,lit1)
57 val fac2 = List.nth (prems,lit2)
58 val sign = sign_of_thm cl
59 val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
60 val newenv = ReconTranslateProof.getnewenv unif_env
61 val envlist = Envir.alist_of newenv
63 inst_subst sign (mksubstlist envlist []) cl
66 val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
67 >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
70 (** Paramodulation **)
72 (*subst with premises exchanged: that way, side literals of the equality will appear
73 as the second to last premises of the result.*)
74 val rev_subst = rotate_prems 1 subst;
76 fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
77 let val eq_lit_th = select_literal (lit1+1) cl1
78 val mod_lit_th = select_literal (lit2+1) cl2
79 val eqsubst = eq_lit_th RSN (2,rev_subst)
80 val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
81 val newth' = Seq.hd (flexflex_rule newth)
82 in Meson.negated_asm_of_head newth' end;
85 val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
86 >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
89 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
91 fun demod_rule ((cl1, lit1), (cl2 , lit2)) =
92 let val eq_lit_th = select_literal (lit1+1) cl1
93 val mod_lit_th = select_literal (lit2+1) cl2
94 val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
95 val eqsubst = eq_lit_th RSN (2,rev_subst)
96 val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
97 val offset = #maxidx(rep_thm newth) + 1
98 (*ensures "renaming apart" even when Vars are frozen*)
99 in Meson.negated_asm_of_head (thaw offset newth) end;
101 val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
102 >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j)))));
105 (** Conversion of a theorem into clauses **)
107 (*For efficiency, we rely upon memo-izing in ResAxioms.*)
108 fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
110 val clausify = Attrib.syntax (Scan.lift Args.nat
111 >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
117 Attrib.add_attributes
118 [("binary", binary, "binary resolution"),
119 ("paramod", paramod, "paramodulation"),
120 ("demod", demod, "demodulation"),
121 ("factor", factor, "factoring"),
122 ("clausify", clausify, "conversion to clauses")];