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