src/HOL/Tools/reconstruction.ML
author paulson
Fri Oct 20 11:04:15 2006 +0200 (2006-10-20 ago)
changeset 21070 0a898140fea2
parent 20762 a7a5157c5e75
permissions -rw-r--r--
Added more debugging info
     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