src/HOL/Tools/reconstruction.ML
 author wenzelm Thu Aug 03 17:30:36 2006 +0200 (2006-08-03) changeset 20328 5b240a4216b0 parent 20258 4fe3c0911907 child 20762 a7a5157c5e75 permissions -rw-r--r--
RuleInsts.bires_inst_tac;
1 (*  Title:      HOL/Reconstruction.thy
2     ID: \$Id\$
3     Author:     Lawrence C Paulson and Claire Quigley
4     Copyright   2004  University of Cambridge
5 *)
7 (*Attributes for reconstructing external resolution proofs*)
9 structure Reconstruction =
10 struct
12 (**** attributes ****)
14 (** Binary resolution **)
16 fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
17      select_literal (lit1 + 1) cl1
18      RSN ((lit2 + 1), cl2);
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)))));
25 (** Factoring **)
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)*)
31 fun mksubstlist [] sublist = sublist
32   | mksubstlist ((a, (T, b)) :: rest) sublist =
33       mksubstlist rest ((Var(a,T), b)::sublist);
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";
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;
46 fun factor_rule (cl, lit1, lit2) =
47     let
48        val prems = prems_of cl
49        val fac1 = List.nth (prems,lit1)
50        val fac2 = List.nth (prems,lit2)
51        val sign = sign_of_thm cl
52        val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
53        val newenv = ReconTranslateProof.getnewenv unif_env
54        val envlist = Envir.alist_of newenv
55      in
56        inst_subst sign (mksubstlist envlist []) cl
57     end;
59 val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
60   >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
63 (** Paramodulation **)
65 (*subst with premises exchanged: that way, side literals of the equality will appear
66   as the second to last premises of the result.*)
67 val rev_subst = rotate_prems 1 subst;
69 fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
70     let  val eq_lit_th = select_literal (lit1+1) cl1
71          val mod_lit_th = select_literal (lit2+1) cl2
72          val eqsubst = eq_lit_th RSN (2,rev_subst)
73          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
74          val newth' = Seq.hd (flexflex_rule newth)
78 val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
79   >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
82 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
84 fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) =
85     let  val eq_lit_th = select_literal (lit1+1) cl1
86          val mod_lit_th = select_literal (lit2+1) cl2
87          val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt
88          val eqsubst = eq_lit_th RSN (2,rev_subst)
89          val newth =
90            Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst)
91            |> singleton (Variable.export ctxt' ctxt)
94 val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
95   >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A =>
96       demod_rule (Context.proof_of context) ((A, i), (B, j)))));
99 (** Conversion of a theorem into clauses **)
101 (*For efficiency, we rely upon memo-izing in ResAxioms.*)
102 fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
104 val clausify = Attrib.syntax (Scan.lift Args.nat
105   >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
108 (** theory setup **)
110 val setup =