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;
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@15151
    46
fun factor_rule (cl, lit1, lit2) =
paulson@15151
    47
    let
paulson@15151
    48
       val prems = prems_of cl
paulson@15151
    49
       val fac1 = List.nth (prems,lit1)
paulson@15151
    50
       val fac2 = List.nth (prems,lit2)
paulson@15151
    51
       val sign = sign_of_thm cl
paulson@15151
    52
       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
paulson@17488
    53
       val newenv = ReconTranslateProof.getnewenv unif_env
paulson@15151
    54
       val envlist = Envir.alist_of newenv
paulson@15151
    55
     in
paulson@15151
    56
       inst_subst sign (mksubstlist envlist []) cl
paulson@15151
    57
    end;
paulson@15151
    58
wenzelm@18729
    59
val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
wenzelm@18729
    60
  >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
paulson@15151
    61
paulson@15151
    62
paulson@15151
    63
(** Paramodulation **)
paulson@15151
    64
paulson@15449
    65
(*subst with premises exchanged: that way, side literals of the equality will appear
paulson@15449
    66
  as the second to last premises of the result.*)
paulson@15449
    67
val rev_subst = rotate_prems 1 subst;
paulson@15449
    68
paulson@15499
    69
fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
paulson@15449
    70
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15449
    71
         val mod_lit_th = select_literal (lit2+1) cl2
paulson@15449
    72
         val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@15449
    73
         val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
paulson@15499
    74
         val newth' = Seq.hd (flexflex_rule newth)
paulson@15579
    75
    in Meson.negated_asm_of_head newth' end;
paulson@15151
    76
paulson@15151
    77
wenzelm@18729
    78
val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
wenzelm@18729
    79
  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
paulson@15151
    80
paulson@15151
    81
paulson@15449
    82
(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
paulson@15151
    83
wenzelm@20258
    84
fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) =
paulson@15151
    85
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15449
    86
         val mod_lit_th = select_literal (lit2+1) cl2
wenzelm@20258
    87
         val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt
paulson@15449
    88
         val eqsubst = eq_lit_th RSN (2,rev_subst)
wenzelm@20258
    89
         val newth =
wenzelm@20258
    90
           Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst)
wenzelm@20258
    91
           |> singleton (Variable.export ctxt' ctxt)
wenzelm@20258
    92
    in Meson.negated_asm_of_head newth end;
paulson@15151
    93
wenzelm@18729
    94
val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
wenzelm@20258
    95
  >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A =>
wenzelm@20258
    96
      demod_rule (Context.proof_of context) ((A, i), (B, j)))));
paulson@15151
    97
paulson@15151
    98
paulson@15359
    99
(** Conversion of a theorem into clauses **)
paulson@15359
   100
paulson@15955
   101
(*For efficiency, we rely upon memo-izing in ResAxioms.*)
paulson@15955
   102
fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
paulson@15466
   103
wenzelm@18729
   104
val clausify = Attrib.syntax (Scan.lift Args.nat
wenzelm@18729
   105
  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
paulson@15359
   106
paulson@15359
   107
paulson@15151
   108
(** theory setup **)
paulson@15151
   109
paulson@15151
   110
val setup =
wenzelm@18708
   111
  Attrib.add_attributes
wenzelm@18729
   112
    [("binary", binary, "binary resolution"),
wenzelm@18729
   113
     ("paramod", paramod, "paramodulation"),
wenzelm@18729
   114
     ("demod", demod, "demodulation"),
wenzelm@18729
   115
     ("factor", factor, "factoring"),
wenzelm@18729
   116
     ("clausify", clausify, "conversion to clauses")];
paulson@15151
   117
paulson@15151
   118
end