src/HOL/Tools/reconstruction.ML
author paulson
Fri Feb 04 18:35:46 2005 +0100 (2005-02-04)
changeset 15499 419dc5ffe8bc
parent 15495 50fde6f04e4c
child 15531 08c8dad8e399
permissions -rw-r--r--
clausification and proof reconstruction
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
let open Attrib
paulson@15151
    11
in
paulson@15151
    12
struct
paulson@15151
    13
paulson@15151
    14
(**************************************************************)
paulson@15151
    15
(* extra functions necessary for factoring and paramodulation *)
paulson@15151
    16
(**************************************************************)
paulson@15151
    17
paulson@15151
    18
fun mksubstlist [] sublist = sublist
paulson@15151
    19
  | mksubstlist ((a,b)::rest) sublist = 
paulson@15151
    20
      let val vartype = type_of b
paulson@15151
    21
          val avar = Var(a,vartype)
paulson@15151
    22
          val newlist = ((avar,b)::sublist) 
paulson@15151
    23
      in mksubstlist rest newlist end;
paulson@15151
    24
paulson@15151
    25
paulson@15151
    26
fun get_unif_comb t eqterm =
paulson@15151
    27
    if ((type_of t) = (type_of eqterm))
paulson@15151
    28
    then t
paulson@15151
    29
    else
paulson@15151
    30
        let val _ $ rand = t
paulson@15151
    31
        in get_unif_comb rand eqterm end;
paulson@15151
    32
paulson@15151
    33
fun get_unif_lit t eqterm =
paulson@15151
    34
    if (can HOLogic.dest_eq t)
paulson@15151
    35
    then
paulson@15151
    36
	let val (lhs,rhs) = HOLogic.dest_eq(HOLogic.dest_Trueprop eqterm)
paulson@15151
    37
	in lhs end
paulson@15151
    38
    else
paulson@15151
    39
	get_unif_comb t eqterm;
paulson@15151
    40
paulson@15151
    41
paulson@15151
    42
paulson@15151
    43
(**** attributes ****)
paulson@15151
    44
paulson@15151
    45
(** Binary resolution **)
paulson@15151
    46
paulson@15151
    47
fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
paulson@15151
    48
     select_literal (lit1 + 1) cl1
paulson@15151
    49
     RSN ((lit2 + 1), cl2);
paulson@15151
    50
paulson@15151
    51
fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
paulson@15151
    52
paulson@15384
    53
fun gen_binary thm = syntax
paulson@15151
    54
      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
paulson@15384
    55
val binary_global = gen_binary global_thm;
paulson@15384
    56
val binary_local = gen_binary local_thm;
paulson@15151
    57
paulson@15151
    58
(*I have not done the MRR rule because it seems to be identifical to 
paulson@15384
    59
binary*)
paulson@15151
    60
paulson@15151
    61
paulson@15151
    62
fun inst_single sign t1 t2 cl =
paulson@15151
    63
    let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
paulson@15151
    64
    in  hd (Seq.list_of(distinct_subgoals_tac
paulson@15151
    65
			    (cterm_instantiate [(ct1,ct2)] cl)))  
paulson@15151
    66
    end;
paulson@15151
    67
paulson@15151
    68
fun inst_subst sign substs cl =
paulson@15151
    69
    if (is_Var (fst(hd(substs))))
paulson@15151
    70
    then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
paulson@15151
    71
    else if (is_Var (snd(hd(substs))))
paulson@15151
    72
    then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
paulson@15151
    73
    else raise THM ("inst_subst", 0, [cl]);
paulson@15151
    74
paulson@15151
    75
(*Grabs the environment from the result of Unify.unifiers*)
paulson@15151
    76
fun getnewenv thisseq = fst (hd (Seq.list_of thisseq));
paulson@15151
    77
paulson@15151
    78
(** Factoring **)
paulson@15151
    79
paulson@15151
    80
fun factor_rule (cl, lit1, lit2) =
paulson@15151
    81
    let
paulson@15151
    82
       val prems = prems_of cl
paulson@15151
    83
       val fac1 = List.nth (prems,lit1)
paulson@15151
    84
       val fac2 = List.nth (prems,lit2)
paulson@15151
    85
       val sign = sign_of_thm cl
paulson@15151
    86
       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
paulson@15151
    87
       val newenv = getnewenv unif_env
paulson@15151
    88
       val envlist = Envir.alist_of newenv
paulson@15151
    89
     in
paulson@15151
    90
       inst_subst sign (mksubstlist envlist []) cl
paulson@15151
    91
    end;
paulson@15151
    92
paulson@15151
    93
fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
paulson@15151
    94
paulson@15384
    95
fun factor x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
paulson@15151
    96
paulson@15151
    97
paulson@15151
    98
(** Paramodulation **)
paulson@15151
    99
paulson@15449
   100
(*subst with premises exchanged: that way, side literals of the equality will appear
paulson@15449
   101
  as the second to last premises of the result.*)
paulson@15449
   102
val rev_subst = rotate_prems 1 subst;
paulson@15449
   103
paulson@15499
   104
fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
paulson@15449
   105
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15449
   106
         val mod_lit_th = select_literal (lit2+1) cl2
paulson@15449
   107
         val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@15449
   108
         val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
paulson@15499
   109
         val newth' = Seq.hd (flexflex_rule newth)
paulson@15499
   110
    in negated_asm_of_head newth' end;
paulson@15151
   111
paulson@15151
   112
paulson@15151
   113
fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
paulson@15151
   114
paulson@15384
   115
fun gen_paramod thm = syntax
paulson@15151
   116
      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
paulson@15384
   117
val paramod_global = gen_paramod global_thm;
paulson@15384
   118
val paramod_local = gen_paramod local_thm;
paulson@15151
   119
paulson@15151
   120
paulson@15449
   121
(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
paulson@15151
   122
paulson@15449
   123
fun demod_rule ((cl1, lit1), (cl2 , lit2)) = 
paulson@15151
   124
    let  val eq_lit_th = select_literal (lit1+1) cl1
paulson@15449
   125
         val mod_lit_th = select_literal (lit2+1) cl2
paulson@15495
   126
	 val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
paulson@15449
   127
         val eqsubst = eq_lit_th RSN (2,rev_subst)
paulson@15495
   128
         val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
paulson@15499
   129
         val offset = #maxidx(rep_thm newth) + 1
paulson@15499
   130
	                  (*ensures "renaming apart" even when Vars are frozen*)
paulson@15499
   131
    in negated_asm_of_head (thaw offset newth) end;
paulson@15151
   132
paulson@15449
   133
fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j)));
paulson@15151
   134
paulson@15449
   135
fun gen_demod thm = syntax
paulson@15449
   136
      ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> demod_syntax);
paulson@15384
   137
val demod_global = gen_demod global_thm;
paulson@15384
   138
val demod_local = gen_demod local_thm;
paulson@15151
   139
paulson@15151
   140
paulson@15359
   141
(** Conversion of a theorem into clauses **)
paulson@15359
   142
paulson@15466
   143
local
paulson@15466
   144
paulson@15466
   145
  (*Cache for clauses: could be a hash table if we provided them.*)
paulson@15466
   146
  val cc = ref (Symtab.empty : (thm * thm list) Symtab.table)
paulson@15466
   147
paulson@15466
   148
  fun memo_cnf th =
paulson@15466
   149
    case Thm.name_of_thm th of
paulson@15499
   150
        "" => ResAxioms.meta_cnf_axiom th (*no name, so can't cache*)
paulson@15466
   151
      | s  => case Symtab.lookup (!cc,s) of
paulson@15466
   152
      	        None => 
paulson@15499
   153
      	        	let val cls = ResAxioms.meta_cnf_axiom th
paulson@15466
   154
      	        	in  cc := Symtab.update ((s, (th,cls)), !cc); cls
paulson@15466
   155
      	        	end
paulson@15466
   156
      	      | Some(th',cls) =>
paulson@15466
   157
      	      	    if eq_thm(th,th') then cls
paulson@15466
   158
      	      	    else (*New theorem stored under the same name? Possible??*)
paulson@15499
   159
      	      	      let val cls = ResAxioms.meta_cnf_axiom th
paulson@15466
   160
      	        	  in  cc := Symtab.update ((s, (th,cls)), !cc); cls
paulson@15466
   161
      	        	  end;
paulson@15466
   162
paulson@15466
   163
in
paulson@15499
   164
fun clausify_rule (A,i) = List.nth (memo_cnf A,i)
paulson@15466
   165
end;
paulson@15359
   166
paulson@15359
   167
fun clausify_syntax i (x, A) = (x, clausify_rule (A,i));
paulson@15359
   168
paulson@15384
   169
fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
paulson@15359
   170
paulson@15359
   171
paulson@15151
   172
(** theory setup **)
paulson@15151
   173
paulson@15151
   174
val setup =
paulson@15151
   175
  [Attrib.add_attributes
paulson@15384
   176
     [("binary", (binary_global, binary_local), "binary resolution"),
paulson@15384
   177
      ("paramod", (paramod_global, paramod_local), "paramodulation"),
paulson@15384
   178
      ("demod", (demod_global, demod_local), "demodulation"),
paulson@15384
   179
      ("factor", (factor, factor), "factoring"),
paulson@15384
   180
      ("clausify", (clausify, clausify), "conversion to clauses")]];
paulson@15151
   181
paulson@15151
   182
end
paulson@15151
   183
end
paulson@15151
   184
paulson@15151
   185