src/HOL/Tools/reconstruction.ML
author haftmann
Fri Feb 10 09:09:07 2006 +0100 (2006-02-10)
changeset 19008 14c1b2f5dda4
parent 18729 216e31270509
child 19963 806eaa2a2a5e
permissions -rw-r--r--
improved code generator devarification
     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 (**************************************************************)
    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 
    24 (**** attributes ****)
    25 
    26 (** Binary resolution **)
    27 
    28 fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
    29      select_literal (lit1 + 1) cl1
    30      RSN ((lit2 + 1), cl2);
    31 
    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)))));
    35 
    36 
    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)))
    41     end;
    42 
    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]);
    49 
    50 
    51 (** Factoring **)
    52 
    53 fun factor_rule (cl, lit1, lit2) =
    54     let
    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
    62      in
    63        inst_subst sign (mksubstlist envlist []) cl
    64     end;
    65 
    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))));
    68 
    69 
    70 (** Paramodulation **)
    71 
    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;
    75 
    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;
    83 
    84 
    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)))));
    87 
    88 
    89 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
    90 
    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;
   100 
   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)))));
   103 
   104 
   105 (** Conversion of a theorem into clauses **)
   106 
   107 (*For efficiency, we rely upon memo-izing in ResAxioms.*)
   108 fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
   109 
   110 val clausify = Attrib.syntax (Scan.lift Args.nat
   111   >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   112 
   113 
   114 (** theory setup **)
   115 
   116 val setup =
   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")];
   123 
   124 end