--- a/src/HOL/Tools/reconstruction.ML Tue Oct 24 12:02:53 2006 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,120 +0,0 @@
-(* Title: HOL/Reconstruction.thy
- ID: $Id$
- Author: Lawrence C Paulson and Claire Quigley
- Copyright 2004 University of Cambridge
-*)
-
-(*Attributes for reconstructing external resolution proofs*)
-
-structure Reconstruction =
-struct
-
-(**** attributes ****)
-
-(** Binary resolution **)
-
-fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
- select_literal (lit1 + 1) cl1
- RSN ((lit2 + 1), cl2);
-
-val binary = Attrib.syntax
- (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
- >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
-
-
-(** Factoring **)
-
-(*NB this code did not work at all before 29/6/2006. Even now its behaviour may
- not be as expected. It unifies the designated literals
- and then deletes ALL duplicates of literals (not just those designated)*)
-
-fun mksubstlist [] sublist = sublist
- | mksubstlist ((a, (T, b)) :: rest) sublist =
- mksubstlist rest ((Var(a,T), b)::sublist);
-
-fun reorient (x,y) =
- if is_Var x then (x,y)
- else if is_Var y then (y,x)
- else error "Reconstruction.reorient: neither term is a Var";
-
-fun inst_subst sign subst cl =
- let val subst' = map (pairself (cterm_of sign) o reorient) subst
- in
- Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
- end;
-
-fun getnewenv seq = fst (fst (the (Seq.pull seq)));
-
-fun factor_rule (cl, lit1, lit2) =
- let
- val prems = prems_of cl
- val fac1 = List.nth (prems,lit1)
- val fac2 = List.nth (prems,lit2)
- val sign = sign_of_thm cl
- val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
- val newenv = getnewenv unif_env
- val envlist = Envir.alist_of newenv
- in
- inst_subst sign (mksubstlist envlist []) cl
- end;
-
-val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
- >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
-
-
-(** Paramodulation **)
-
-(*subst with premises exchanged: that way, side literals of the equality will appear
- as the second to last premises of the result.*)
-val rev_subst = rotate_prems 1 subst;
-
-fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
- let val eq_lit_th = select_literal (lit1+1) cl1
- val mod_lit_th = select_literal (lit2+1) cl2
- val eqsubst = eq_lit_th RSN (2,rev_subst)
- val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
- val newth' = Seq.hd (flexflex_rule newth)
- in Meson.negated_asm_of_head newth' end;
-
-
-val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
- >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
-
-
-(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
-
-fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) =
- let val eq_lit_th = select_literal (lit1+1) cl1
- val mod_lit_th = select_literal (lit2+1) cl2
- val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt
- val eqsubst = eq_lit_th RSN (2,rev_subst)
- val newth =
- Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst)
- |> singleton (Variable.export ctxt' ctxt)
- in Meson.negated_asm_of_head newth end;
-
-val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
- >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A =>
- demod_rule (Context.proof_of context) ((A, i), (B, j)))));
-
-
-(** Conversion of a theorem into clauses **)
-
-(*For efficiency, we rely upon memo-izing in ResAxioms.*)
-fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
-
-val clausify = Attrib.syntax (Scan.lift Args.nat
- >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
-
-
-(** theory setup **)
-
-val setup =
- Attrib.add_attributes
- [("binary", binary, "binary resolution"),
- ("paramod", paramod, "paramodulation"),
- ("demod", demod, "demodulation"),
- ("factor", factor, "factoring"),
- ("clausify", clausify, "conversion to clauses")];
-
-end