src/HOL/Tools/reconstruction.ML
author haftmann
Wed Jun 07 16:55:39 2006 +0200 (2006-06-07)
changeset 19818 5c5c1208a3fa
parent 18729 216e31270509
child 19963 806eaa2a2a5e
permissions -rw-r--r--
adding case theorems for code generator
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
(**************************************************************)
paulson@15151
    13
(* extra functions necessary for factoring and paramodulation *)
paulson@15151
    14
(**************************************************************)
paulson@15151
    15
paulson@15151
    16
fun mksubstlist [] sublist = sublist
wenzelm@18729
    17
  | mksubstlist ((a, (_, b)) :: rest) sublist =
paulson@15151
    18
      let val vartype = type_of b
paulson@15151
    19
          val avar = Var(a,vartype)
wenzelm@18729
    20
          val newlist = ((avar,b)::sublist)
paulson@15151
    21
      in mksubstlist rest newlist end;
paulson@15151
    22
paulson@15151
    23
paulson@15151
    24
(**** attributes ****)
paulson@15151
    25
paulson@15151
    26
(** Binary resolution **)
paulson@15151
    27
paulson@15151
    28
fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
paulson@15151
    29
     select_literal (lit1 + 1) cl1
paulson@15151
    30
     RSN ((lit2 + 1), cl2);
paulson@15151
    31
wenzelm@18729
    32
val binary = Attrib.syntax
wenzelm@18729
    33
  (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
wenzelm@18729
    34
    >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
paulson@15151
    35
paulson@15151
    36
paulson@15151
    37
fun inst_single sign t1 t2 cl =
paulson@15151
    38
    let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
paulson@15151
    39
    in  hd (Seq.list_of(distinct_subgoals_tac
wenzelm@18729
    40
                            (cterm_instantiate [(ct1,ct2)] cl)))
paulson@15151
    41
    end;
paulson@15151
    42
paulson@15151
    43
fun inst_subst sign substs cl =
paulson@15151
    44
    if (is_Var (fst(hd(substs))))
paulson@15151
    45
    then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
paulson@15151
    46
    else if (is_Var (snd(hd(substs))))
paulson@15151
    47
    then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
paulson@15151
    48
    else raise THM ("inst_subst", 0, [cl]);
paulson@15151
    49
paulson@15151
    50
paulson@15151
    51
(** Factoring **)
paulson@15151
    52
paulson@15151
    53
fun factor_rule (cl, lit1, lit2) =
paulson@15151
    54
    let
paulson@15151
    55
       val prems = prems_of cl
paulson@15151
    56
       val fac1 = List.nth (prems,lit1)
paulson@15151
    57
       val fac2 = List.nth (prems,lit2)
paulson@15151
    58
       val sign = sign_of_thm cl
paulson@15151
    59
       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
paulson@17488
    60
       val newenv = ReconTranslateProof.getnewenv unif_env
paulson@15151
    61
       val envlist = Envir.alist_of newenv
paulson@15151
    62
     in
paulson@15151
    63
       inst_subst sign (mksubstlist envlist []) cl
paulson@15151
    64
    end;
paulson@15151
    65
wenzelm@18729
    66
val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
wenzelm@18729
    67
  >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
paulson@15151
    68
paulson@15151
    69
paulson@15151
    70
(** Paramodulation **)
paulson@15151
    71
paulson@15449
    72
(*subst with premises exchanged: that way, side literals of the equality will appear
paulson@15449
    73
  as the second to last premises of the result.*)
paulson@15449
    74
val rev_subst = rotate_prems 1 subst;
paulson@15449
    75
paulson@15499
    76
fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
paulson@15449
    77
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15449
    78
         val mod_lit_th = select_literal (lit2+1) cl2
paulson@15449
    79
         val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@15449
    80
         val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
paulson@15499
    81
         val newth' = Seq.hd (flexflex_rule newth)
paulson@15579
    82
    in Meson.negated_asm_of_head newth' end;
paulson@15151
    83
paulson@15151
    84
wenzelm@18729
    85
val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
wenzelm@18729
    86
  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
paulson@15151
    87
paulson@15151
    88
paulson@15449
    89
(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
paulson@15151
    90
wenzelm@18729
    91
fun demod_rule ((cl1, lit1), (cl2 , lit2)) =
paulson@15151
    92
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15449
    93
         val mod_lit_th = select_literal (lit2+1) cl2
wenzelm@18729
    94
         val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
paulson@15449
    95
         val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@15495
    96
         val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
paulson@15499
    97
         val offset = #maxidx(rep_thm newth) + 1
wenzelm@18729
    98
                          (*ensures "renaming apart" even when Vars are frozen*)
paulson@15579
    99
    in Meson.negated_asm_of_head (thaw offset newth) end;
paulson@15151
   100
wenzelm@18729
   101
val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
wenzelm@18729
   102
  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j)))));
paulson@15151
   103
paulson@15151
   104
paulson@15359
   105
(** Conversion of a theorem into clauses **)
paulson@15359
   106
paulson@15955
   107
(*For efficiency, we rely upon memo-izing in ResAxioms.*)
paulson@15955
   108
fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
paulson@15466
   109
wenzelm@18729
   110
val clausify = Attrib.syntax (Scan.lift Args.nat
wenzelm@18729
   111
  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
paulson@15359
   112
paulson@15359
   113
paulson@15151
   114
(** theory setup **)
paulson@15151
   115
paulson@15151
   116
val setup =
wenzelm@18708
   117
  Attrib.add_attributes
wenzelm@18729
   118
    [("binary", binary, "binary resolution"),
wenzelm@18729
   119
     ("paramod", paramod, "paramodulation"),
wenzelm@18729
   120
     ("demod", demod, "demodulation"),
wenzelm@18729
   121
     ("factor", factor, "factoring"),
wenzelm@18729
   122
     ("clausify", clausify, "conversion to clauses")];
paulson@15151
   123
paulson@15151
   124
end