src/HOL/Tools/reconstruction.ML
author paulson
Thu, 29 Jun 2006 18:10:59 +0200
changeset 19963 806eaa2a2a5e
parent 18729 216e31270509
child 20258 4fe3c0911907
permissions -rw-r--r--
fixed the "factor" method
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Reconstruction.thy
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     2
    ID: $Id$
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson and Claire Quigley
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     4
    Copyright   2004  University of Cambridge
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     5
*)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     6
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     7
(*Attributes for reconstructing external resolution proofs*)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     8
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
     9
structure Reconstruction =
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    10
struct
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    11
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    12
(**** attributes ****)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    13
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    14
(** Binary resolution **)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    15
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    16
fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    17
     select_literal (lit1 + 1) cl1
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    18
     RSN ((lit2 + 1), cl2);
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    19
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    20
val binary = Attrib.syntax
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    21
  (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    22
    >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    23
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    24
19963
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    25
(** Factoring **)
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    26
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    27
(*NB this code did not work at all before 29/6/2006. Even now its behaviour may
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    28
  not be as expected. It unifies the designated literals
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    29
  and then deletes ALL duplicates of literals (not just those designated)*)
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    30
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    31
fun mksubstlist [] sublist = sublist
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    32
  | mksubstlist ((a, (T, b)) :: rest) sublist =
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    33
      mksubstlist rest ((Var(a,T), b)::sublist);
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    34
19963
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    35
fun reorient (x,y) = 
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    36
      if is_Var x then (x,y)
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    37
      else if is_Var y then (y,x)
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    38
      else error "Reconstruction.reorient: neither term is a Var";
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    39
19963
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    40
fun inst_subst sign subst cl =
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    41
  let val subst' = map (pairself (cterm_of sign) o reorient) subst
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    42
  in 
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    43
      Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
806eaa2a2a5e fixed the "factor" method
paulson
parents: 18729
diff changeset
    44
  end;
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    45
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    46
fun factor_rule (cl, lit1, lit2) =
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    47
    let
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    48
       val prems = prems_of cl
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    49
       val fac1 = List.nth (prems,lit1)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    50
       val fac2 = List.nth (prems,lit2)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    51
       val sign = sign_of_thm cl
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    52
       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
17488
67376a311a2b further simplification of the Isabelle-ATP linkup
paulson
parents: 15955
diff changeset
    53
       val newenv = ReconTranslateProof.getnewenv unif_env
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    54
       val envlist = Envir.alist_of newenv
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    55
     in
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    56
       inst_subst sign (mksubstlist envlist []) cl
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    57
    end;
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    58
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    59
val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    60
  >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    61
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    62
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    63
(** Paramodulation **)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    64
15449
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    65
(*subst with premises exchanged: that way, side literals of the equality will appear
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    66
  as the second to last premises of the result.*)
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    67
val rev_subst = rotate_prems 1 subst;
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    68
15499
419dc5ffe8bc clausification and proof reconstruction
paulson
parents: 15495
diff changeset
    69
fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
15449
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    70
    let  val eq_lit_th = select_literal (lit1+1) cl1
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    71
         val mod_lit_th = select_literal (lit2+1) cl2
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    72
         val eqsubst = eq_lit_th RSN (2,rev_subst)
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    73
         val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
15499
419dc5ffe8bc clausification and proof reconstruction
paulson
parents: 15495
diff changeset
    74
         val newth' = Seq.hd (flexflex_rule newth)
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15531
diff changeset
    75
    in Meson.negated_asm_of_head newth' end;
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    76
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    77
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    78
val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    79
  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    80
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    81
15449
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    82
(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    83
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    84
fun demod_rule ((cl1, lit1), (cl2 , lit2)) =
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    85
    let  val eq_lit_th = select_literal (lit1+1) cl1
15449
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    86
         val mod_lit_th = select_literal (lit2+1) cl2
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    87
         val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
15449
a27c81bd838d fixed the treatment of demodulation and paramodulation
paulson
parents: 15384
diff changeset
    88
         val eqsubst = eq_lit_th RSN (2,rev_subst)
15495
50fde6f04e4c new treatment of demodulation in proof reconstruction
paulson
parents: 15466
diff changeset
    89
         val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
15499
419dc5ffe8bc clausification and proof reconstruction
paulson
parents: 15495
diff changeset
    90
         val offset = #maxidx(rep_thm newth) + 1
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    91
                          (*ensures "renaming apart" even when Vars are frozen*)
15579
32bee18c675f Tools/meson.ML: signature, structure and "open" rather than "local"
paulson
parents: 15531
diff changeset
    92
    in Meson.negated_asm_of_head (thaw offset newth) end;
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    93
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    94
val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
    95
  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => demod_rule ((A, i), (B, j)))));
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    96
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
    97
15359
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents: 15151
diff changeset
    98
(** Conversion of a theorem into clauses **)
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents: 15151
diff changeset
    99
15955
87cf2ce8ede8 memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents: 15794
diff changeset
   100
(*For efficiency, we rely upon memo-izing in ResAxioms.*)
87cf2ce8ede8 memoization of ResAxioms.cnf_axiom rather than of Reconstruction.clausify_rule
paulson
parents: 15794
diff changeset
   101
fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
15466
dce7827f8d75 implemented cache for conversion to clauses
paulson
parents: 15449
diff changeset
   102
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   103
val clausify = Attrib.syntax (Scan.lift Args.nat
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   104
  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
15359
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents: 15151
diff changeset
   105
8bad1f42fec0 new CLAUSIFY attribute for proof reconstruction with lemmas
paulson
parents: 15151
diff changeset
   106
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
   107
(** theory setup **)
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
   108
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
   109
val setup =
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 17488
diff changeset
   110
  Attrib.add_attributes
18729
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   111
    [("binary", binary, "binary resolution"),
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   112
     ("paramod", paramod, "paramodulation"),
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   113
     ("demod", demod, "demodulation"),
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   114
     ("factor", factor, "factoring"),
216e31270509 simplified type attribute;
wenzelm
parents: 18708
diff changeset
   115
     ("clausify", clausify, "conversion to clauses")];
15151
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
   116
429666b09783 proof reconstruction for external ATPs
paulson
parents:
diff changeset
   117
end