Conversion to clause form now tolerates Boolean variables without looping.
Attribute "clausify" moved to res_axioms; rest of reconstruction.ML deleted

--- a/src/HOL/IsaMakefile	Tue Oct 24 12:02:53 2006 +0200
+++ b/src/HOL/IsaMakefile	Thu Oct 26 10:48:35 2006 +0200
@@ -110,7 +110,7 @@
   Tools/numeral_syntax.ML Tools/primrec_package.ML Tools/prop_logic.ML		\
   Tools/polyhash.ML \
   Tools/recdef_package.ML Tools/recfun_codegen.ML				\
-  Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML		\
+  Tools/record_package.ML Tools/refute.ML		\
   Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML			\
   Tools/res_clause.ML Tools/rewrite_hol_proof.ML	\
   Tools/sat_funcs.ML					\

--- a/src/HOL/Reconstruction.thy	Tue Oct 24 12:02:53 2006 +0200
+++ b/src/HOL/Reconstruction.thy	Thu Oct 26 10:48:35 2006 +0200
@@ -16,7 +16,6 @@
 	 ("Tools/res_hol_clause.ML")
 	 ("Tools/res_axioms.ML")
 	 ("Tools/res_atp.ML")
-	 ("Tools/reconstruction.ML")
 
 begin
 
@@ -72,13 +71,10 @@
 apply (simp add: COMBB_def) 
 done
 
-
 use "Tools/res_axioms.ML"
 use "Tools/res_hol_clause.ML"
 use "Tools/res_atp.ML"
-use "Tools/reconstruction.ML"
 
 setup ResAxioms.meson_method_setup
-setup Reconstruction.setup
 
 end

--- a/src/HOL/Tools/meson.ML	Tue Oct 24 12:02:53 2006 +0200
+++ b/src/HOL/Tools/meson.ML	Thu Oct 26 10:48:35 2006 +0200
@@ -312,9 +312,14 @@
 
 (**** Generation of contrapositives ****)
 
+fun is_left (Const ("Trueprop", _) $ 
+               (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
+  | is_left _ = false;
+               
 (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
-fun assoc_right th = assoc_right (th RS disj_assoc)
-	handle THM _ => th;
+fun assoc_right th = 
+  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
+  else th;
 
 (*Must check for negative literal first!*)
 val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
@@ -349,18 +354,25 @@
     exists_Const
       (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
       
-(*Raises an exception if any Vars in the theorem mention type bool; they
-  could cause make_horn to loop! Also rejects functions whose arguments are 
-  Booleans or other functions.*)
+(*Raises an exception if any Vars in the theorem mention type bool. 
+  Also rejects functions whose arguments are Booleans or other functions.*)
 fun is_fol_term t =
     not (exists (has_bool o fastype_of) (term_vars t)  orelse
 	 not (Term.is_first_order ["all","All","Ex"] t) orelse
 	 has_bool_arg_const t  orelse  
 	 has_meta_conn t);
 
+fun rigid t = not (is_Var (head_of t));
+
+fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
+  | ok4horn (Const ("Trueprop",_) $ t) = rigid t
+  | ok4horn _ = false;
+
 (*Create a meta-level Horn clause*)
-fun make_horn crules th = make_horn crules (tryres(th,crules))
-			  handle THM _ => th;
+fun make_horn crules th = 
+  if ok4horn (concl_of th) 
+  then make_horn crules (tryres(th,crules)) handle THM _ => th
+  else th;
 
 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   is a HOL disjunction.*)
@@ -434,11 +446,18 @@
 val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
                not_impD, not_iffD, not_allD, not_exD, not_notD];
 
-fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
+fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
+  | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
+  | ok4nnf _ = false;
+
+fun make_nnf1 th = 
+  if ok4nnf (concl_of th) 
+  then make_nnf1 (tryres(th, nnf_rls))
     handle THM _ =>
         forward_res make_nnf1
            (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
-    handle THM _ => th;
+    handle THM _ => th
+  else th;
 
 (*The simplification removes defined quantifiers and occurrences of True and False. 
   nnf_ss also includes the one-point simprocs,
@@ -455,7 +474,7 @@
 
 fun make_nnf th = case prems_of th of
     [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
-	     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
+	     |> simplify nnf_ss  
 	     |> make_nnf1
   | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
 
@@ -587,10 +606,8 @@
 
 (*Converting one clause*)
 fun make_meta_clause th = 
-  if is_fol_term (prop_of th) 
-  then negated_asm_of_head (make_horn resolution_clause_rules th)
-  else raise THM("make_meta_clause", 0, [th]);
-
+  negated_asm_of_head (make_horn resolution_clause_rules th);
+  
 fun make_meta_clauses ths =
     name_thms "MClause#"
       (distinct Drule.eq_thm_prop (map make_meta_clause ths));

--- 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

--- a/src/HOL/Tools/res_axioms.ML	Tue Oct 24 12:02:53 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 26 10:48:35 2006 +0200
@@ -590,9 +590,6 @@
 
 fun pairname th = (Thm.name_of_thm th, th);
 
-fun meta_cnf_axiom th =
-    map Meson.make_meta_clause (cnf_axiom (pairname th));
-
 (*Principally for debugging*)
 fun cnf_name s = 
   let val th = thm s
@@ -695,9 +692,16 @@
     [("meson", Method.thms_ctxt_args meson_meth,
       "MESON resolution proof procedure")];
 
+(** Attribute for converting a theorem into clauses **)
 
+fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th));
 
-(*** The Skolemization attribute ***)
+fun clausify_rule (th,i) = List.nth (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))));
+
+(** The Skolemization attribute **)
 
 fun conj2_rule (th1,th2) = conjI OF [th1,th2];
 
@@ -712,8 +716,9 @@
   | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
 
 val setup_attrs = Attrib.add_attributes
-  [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")];
-
+  [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
+   ("clausify", clausify, "conversion to clauses")];
+     
 val setup = clause_cache_setup #> setup_attrs;
 
 end;