src/HOL/Tools/reconstruction.ML
author paulson
Mon Sep 19 18:30:22 2005 +0200 (2005-09-19 ago)
changeset 17488 67376a311a2b
parent 15955 87cf2ce8ede8
child 18708 4b3dadb4fe33
permissions -rw-r--r--
further simplification of the Isabelle-ATP linkup
     1 (*  Title:      HOL/Reconstruction.thy
     2     ID: $Id$
     3     Author:     Lawrence C Paulson and Claire Quigley
     4     Copyright   2004  University of Cambridge
     5 *)
     6 
     7 (*Attributes for reconstructing external resolution proofs*)
     8 
     9 structure Reconstruction =
    10 let open Attrib
    11 in
    12 struct
    13 
    14 (**************************************************************)
    15 (* extra functions necessary for factoring and paramodulation *)
    16 (**************************************************************)
    17 
    18 fun mksubstlist [] sublist = sublist
    19   | mksubstlist ((a, (_, b)) :: rest) sublist = 
    20       let val vartype = type_of b
    21           val avar = Var(a,vartype)
    22           val newlist = ((avar,b)::sublist) 
    23       in mksubstlist rest newlist end;
    24 
    25 
    26 (**** attributes ****)
    27 
    28 (** Binary resolution **)
    29 
    30 fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
    31      select_literal (lit1 + 1) cl1
    32      RSN ((lit2 + 1), cl2);
    33 
    34 fun binary_syntax ((i, B), j) (x, A) = (x, binary_rule ((A,i), (B,j)));
    35 
    36 fun gen_binary thm = syntax
    37       ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> binary_syntax);
    38 val binary_global = gen_binary global_thm;
    39 val binary_local = gen_binary local_thm;
    40 
    41 (*I have not done the MRR rule because it seems to be identifical to 
    42 binary*)
    43 
    44 
    45 fun inst_single sign t1 t2 cl =
    46     let val ct1 = cterm_of sign t1 and ct2 = cterm_of sign t2
    47     in  hd (Seq.list_of(distinct_subgoals_tac
    48 			    (cterm_instantiate [(ct1,ct2)] cl)))  
    49     end;
    50 
    51 fun inst_subst sign substs cl =
    52     if (is_Var (fst(hd(substs))))
    53     then inst_single sign (fst (hd substs)) (snd (hd substs)) cl
    54     else if (is_Var (snd(hd(substs))))
    55     then inst_single sign (snd (hd substs)) (fst (hd substs)) cl
    56     else raise THM ("inst_subst", 0, [cl]);
    57 
    58 
    59 (** Factoring **)
    60 
    61 fun factor_rule (cl, lit1, lit2) =
    62     let
    63        val prems = prems_of cl
    64        val fac1 = List.nth (prems,lit1)
    65        val fac2 = List.nth (prems,lit2)
    66        val sign = sign_of_thm cl
    67        val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
    68        val newenv = ReconTranslateProof.getnewenv unif_env
    69        val envlist = Envir.alist_of newenv
    70      in
    71        inst_subst sign (mksubstlist envlist []) cl
    72     end;
    73 
    74 fun factor_syntax (i, j) (x, A) = (x, factor_rule (A,i,j));
    75 
    76 fun factor x = syntax ((Scan.lift (Args.nat -- Args.nat)) >> factor_syntax) x;
    77 
    78 
    79 (** Paramodulation **)
    80 
    81 (*subst with premises exchanged: that way, side literals of the equality will appear
    82   as the second to last premises of the result.*)
    83 val rev_subst = rotate_prems 1 subst;
    84 
    85 fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
    86     let  val eq_lit_th = select_literal (lit1+1) cl1
    87          val mod_lit_th = select_literal (lit2+1) cl2
    88          val eqsubst = eq_lit_th RSN (2,rev_subst)
    89          val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
    90          val newth' = Seq.hd (flexflex_rule newth)
    91     in Meson.negated_asm_of_head newth' end;
    92 
    93 
    94 fun paramod_syntax ((i, B), j) (x, A) = (x, paramod_rule ((A,i), (B,j)));
    95 
    96 fun gen_paramod thm = syntax
    97       ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> paramod_syntax);
    98 val paramod_global = gen_paramod global_thm;
    99 val paramod_local = gen_paramod local_thm;
   100 
   101 
   102 (** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
   103 
   104 fun demod_rule ((cl1, lit1), (cl2 , lit2)) = 
   105     let  val eq_lit_th = select_literal (lit1+1) cl1
   106          val mod_lit_th = select_literal (lit2+1) cl2
   107 	 val (fmod_th,thaw) = Drule.freeze_thaw_robust mod_lit_th
   108          val eqsubst = eq_lit_th RSN (2,rev_subst)
   109          val newth = Seq.hd(biresolution false [(false, fmod_th)] 1 eqsubst)
   110          val offset = #maxidx(rep_thm newth) + 1
   111 	                  (*ensures "renaming apart" even when Vars are frozen*)
   112     in Meson.negated_asm_of_head (thaw offset newth) end;
   113 
   114 fun demod_syntax ((i, B), j) (x, A) = (x, demod_rule ((A,i), (B,j)));
   115 
   116 fun gen_demod thm = syntax
   117       ((Scan.lift Args.nat -- thm -- Scan.lift Args.nat) >> demod_syntax);
   118 val demod_global = gen_demod global_thm;
   119 val demod_local = gen_demod local_thm;
   120 
   121 
   122 (** Conversion of a theorem into clauses **)
   123 
   124 (*For efficiency, we rely upon memo-izing in ResAxioms.*)
   125 fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
   126 
   127 fun clausify_syntax i (x, th) = (x, clausify_rule (th,i));
   128 
   129 fun clausify x = syntax ((Scan.lift Args.nat) >> clausify_syntax) x;
   130 
   131 
   132 (** theory setup **)
   133 
   134 val setup =
   135   [Attrib.add_attributes
   136      [("binary", (binary_global, binary_local), "binary resolution"),
   137       ("paramod", (paramod_global, paramod_local), "paramodulation"),
   138       ("demod", (demod_global, demod_local), "demodulation"),
   139       ("factor", (factor, factor), "factoring"),
   140       ("clausify", (clausify, clausify), "conversion to clauses")]];
   141 
   142 end
   143 end
   144 
   145