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

     2.1 --- a/src/HOL/Reconstruction.thy	Tue Oct 24 12:02:53 2006 +0200
     2.2 +++ b/src/HOL/Reconstruction.thy	Thu Oct 26 10:48:35 2006 +0200
     2.3 @@ -16,7 +16,6 @@
     2.4  	 ("Tools/res_hol_clause.ML")
     2.5  	 ("Tools/res_axioms.ML")
     2.6  	 ("Tools/res_atp.ML")
     2.7 -	 ("Tools/reconstruction.ML")
     2.8  
     2.9  begin
    2.10  
    2.11 @@ -72,13 +71,10 @@
    2.12  apply (simp add: COMBB_def) 
    2.13  done
    2.14  
    2.15 -
    2.16  use "Tools/res_axioms.ML"
    2.17  use "Tools/res_hol_clause.ML"
    2.18  use "Tools/res_atp.ML"
    2.19 -use "Tools/reconstruction.ML"
    2.20  
    2.21  setup ResAxioms.meson_method_setup
    2.22 -setup Reconstruction.setup
    2.23  
    2.24  end

     3.1 --- a/src/HOL/Tools/meson.ML	Tue Oct 24 12:02:53 2006 +0200
     3.2 +++ b/src/HOL/Tools/meson.ML	Thu Oct 26 10:48:35 2006 +0200
     3.3 @@ -312,9 +312,14 @@
     3.4  
     3.5  (**** Generation of contrapositives ****)
     3.6  
     3.7 +fun is_left (Const ("Trueprop", _) $ 
     3.8 +               (Const ("op |", _) $ (Const ("op |", _) $ _ $ _) $ _)) = true
     3.9 +  | is_left _ = false;
    3.10 +               
    3.11  (*Associate disjuctions to right -- make leftmost disjunct a LITERAL*)
    3.12 -fun assoc_right th = assoc_right (th RS disj_assoc)
    3.13 -	handle THM _ => th;
    3.14 +fun assoc_right th = 
    3.15 +  if is_left (prop_of th) then assoc_right (th RS disj_assoc)
    3.16 +  else th;
    3.17  
    3.18  (*Must check for negative literal first!*)
    3.19  val clause_rules = [disj_assoc, make_neg_rule, make_pos_rule];
    3.20 @@ -349,18 +354,25 @@
    3.21      exists_Const
    3.22        (fn (c,T) => not(is_conn c) andalso exists (has_bool) (binder_types T));
    3.23        
    3.24 -(*Raises an exception if any Vars in the theorem mention type bool; they
    3.25 -  could cause make_horn to loop! Also rejects functions whose arguments are 
    3.26 -  Booleans or other functions.*)
    3.27 +(*Raises an exception if any Vars in the theorem mention type bool. 
    3.28 +  Also rejects functions whose arguments are Booleans or other functions.*)
    3.29  fun is_fol_term t =
    3.30      not (exists (has_bool o fastype_of) (term_vars t)  orelse
    3.31  	 not (Term.is_first_order ["all","All","Ex"] t) orelse
    3.32  	 has_bool_arg_const t  orelse  
    3.33  	 has_meta_conn t);
    3.34  
    3.35 +fun rigid t = not (is_Var (head_of t));
    3.36 +
    3.37 +fun ok4horn (Const ("Trueprop",_) $ (Const ("op |", _) $ t $ _)) = rigid t
    3.38 +  | ok4horn (Const ("Trueprop",_) $ t) = rigid t
    3.39 +  | ok4horn _ = false;
    3.40 +
    3.41  (*Create a meta-level Horn clause*)
    3.42 -fun make_horn crules th = make_horn crules (tryres(th,crules))
    3.43 -			  handle THM _ => th;
    3.44 +fun make_horn crules th = 
    3.45 +  if ok4horn (concl_of th) 
    3.46 +  then make_horn crules (tryres(th,crules)) handle THM _ => th
    3.47 +  else th;
    3.48  
    3.49  (*Generate Horn clauses for all contrapositives of a clause. The input, th,
    3.50    is a HOL disjunction.*)
    3.51 @@ -434,11 +446,18 @@
    3.52  val nnf_rls = [imp_to_disjD, iff_to_disjD, not_conjD, not_disjD,
    3.53                 not_impD, not_iffD, not_allD, not_exD, not_notD];
    3.54  
    3.55 -fun make_nnf1 th = make_nnf1 (tryres(th, nnf_rls))
    3.56 +fun ok4nnf (Const ("Trueprop",_) $ (Const ("Not", _) $ t)) = rigid t
    3.57 +  | ok4nnf (Const ("Trueprop",_) $ t) = rigid t
    3.58 +  | ok4nnf _ = false;
    3.59 +
    3.60 +fun make_nnf1 th = 
    3.61 +  if ok4nnf (concl_of th) 
    3.62 +  then make_nnf1 (tryres(th, nnf_rls))
    3.63      handle THM _ =>
    3.64          forward_res make_nnf1
    3.65             (tryres(th, [conj_forward,disj_forward,all_forward,ex_forward]))
    3.66 -    handle THM _ => th;
    3.67 +    handle THM _ => th
    3.68 +  else th;
    3.69  
    3.70  (*The simplification removes defined quantifiers and occurrences of True and False. 
    3.71    nnf_ss also includes the one-point simprocs,
    3.72 @@ -455,7 +474,7 @@
    3.73  
    3.74  fun make_nnf th = case prems_of th of
    3.75      [] => th |> rewrite_rule (map safe_mk_meta_eq nnf_simps)
    3.76 -	     |> simplify nnf_ss  (*But this doesn't simplify premises...*)
    3.77 +	     |> simplify nnf_ss  
    3.78  	     |> make_nnf1
    3.79    | _ => raise THM ("make_nnf: premises in argument", 0, [th]);
    3.80  
    3.81 @@ -587,10 +606,8 @@
    3.82  
    3.83  (*Converting one clause*)
    3.84  fun make_meta_clause th = 
    3.85 -  if is_fol_term (prop_of th) 
    3.86 -  then negated_asm_of_head (make_horn resolution_clause_rules th)
    3.87 -  else raise THM("make_meta_clause", 0, [th]);
    3.88 -
    3.89 +  negated_asm_of_head (make_horn resolution_clause_rules th);
    3.90 +  
    3.91  fun make_meta_clauses ths =
    3.92      name_thms "MClause#"
    3.93        (distinct Drule.eq_thm_prop (map make_meta_clause ths));

     4.1 --- a/src/HOL/Tools/reconstruction.ML	Tue Oct 24 12:02:53 2006 +0200
     4.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.3 @@ -1,120 +0,0 @@
     4.4 -(*  Title:      HOL/Reconstruction.thy
     4.5 -    ID: $Id$
     4.6 -    Author:     Lawrence C Paulson and Claire Quigley
     4.7 -    Copyright   2004  University of Cambridge
     4.8 -*)
     4.9 -
    4.10 -(*Attributes for reconstructing external resolution proofs*)
    4.11 -
    4.12 -structure Reconstruction =
    4.13 -struct
    4.14 -
    4.15 -(**** attributes ****)
    4.16 -
    4.17 -(** Binary resolution **)
    4.18 -
    4.19 -fun binary_rule ((cl1, lit1), (cl2 , lit2)) =
    4.20 -     select_literal (lit1 + 1) cl1
    4.21 -     RSN ((lit2 + 1), cl2);
    4.22 -
    4.23 -val binary = Attrib.syntax
    4.24 -  (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    4.25 -    >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => binary_rule ((A, i), (B, j)))));
    4.26 -
    4.27 -
    4.28 -(** Factoring **)
    4.29 -
    4.30 -(*NB this code did not work at all before 29/6/2006. Even now its behaviour may
    4.31 -  not be as expected. It unifies the designated literals
    4.32 -  and then deletes ALL duplicates of literals (not just those designated)*)
    4.33 -
    4.34 -fun mksubstlist [] sublist = sublist
    4.35 -  | mksubstlist ((a, (T, b)) :: rest) sublist =
    4.36 -      mksubstlist rest ((Var(a,T), b)::sublist);
    4.37 -
    4.38 -fun reorient (x,y) = 
    4.39 -      if is_Var x then (x,y)
    4.40 -      else if is_Var y then (y,x)
    4.41 -      else error "Reconstruction.reorient: neither term is a Var";
    4.42 -
    4.43 -fun inst_subst sign subst cl =
    4.44 -  let val subst' = map (pairself (cterm_of sign) o reorient) subst
    4.45 -  in 
    4.46 -      Seq.hd(distinct_subgoals_tac (cterm_instantiate subst' cl))
    4.47 -  end;
    4.48 -
    4.49 -fun getnewenv seq = fst (fst (the (Seq.pull seq)));
    4.50 -
    4.51 -fun factor_rule (cl, lit1, lit2) =
    4.52 -    let
    4.53 -       val prems = prems_of cl
    4.54 -       val fac1 = List.nth (prems,lit1)
    4.55 -       val fac2 = List.nth (prems,lit2)
    4.56 -       val sign = sign_of_thm cl
    4.57 -       val unif_env = Unify.unifiers (sign, Envir.empty 0, [(fac1, fac2)])
    4.58 -       val newenv = getnewenv unif_env
    4.59 -       val envlist = Envir.alist_of newenv
    4.60 -     in
    4.61 -       inst_subst sign (mksubstlist envlist []) cl
    4.62 -    end;
    4.63 -
    4.64 -val factor = Attrib.syntax (Scan.lift (Args.nat -- Args.nat)
    4.65 -  >> (fn (i, j) => Thm.rule_attribute (fn _ => fn A => factor_rule (A, i, j))));
    4.66 -
    4.67 -
    4.68 -(** Paramodulation **)
    4.69 -
    4.70 -(*subst with premises exchanged: that way, side literals of the equality will appear
    4.71 -  as the second to last premises of the result.*)
    4.72 -val rev_subst = rotate_prems 1 subst;
    4.73 -
    4.74 -fun paramod_rule ((cl1, lit1), (cl2, lit2)) =
    4.75 -    let  val eq_lit_th = select_literal (lit1+1) cl1
    4.76 -         val mod_lit_th = select_literal (lit2+1) cl2
    4.77 -         val eqsubst = eq_lit_th RSN (2,rev_subst)
    4.78 -         val newth = Seq.hd (biresolution false [(false, mod_lit_th)] 1 eqsubst)
    4.79 -         val newth' = Seq.hd (flexflex_rule newth)
    4.80 -    in Meson.negated_asm_of_head newth' end;
    4.81 -
    4.82 -
    4.83 -val paramod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
    4.84 -  >> (fn ((i, B), j) => Thm.rule_attribute (fn _ => fn A => paramod_rule ((A, i), (B, j)))));
    4.85 -
    4.86 -
    4.87 -(** Demodulation: rewriting of a single literal (Non-Unit Rewriting, SPASS) **)
    4.88 -
    4.89 -fun demod_rule ctxt ((cl1, lit1), (cl2 , lit2)) =
    4.90 -    let  val eq_lit_th = select_literal (lit1+1) cl1
    4.91 -         val mod_lit_th = select_literal (lit2+1) cl2
    4.92 -         val ((_, [fmod_th]), ctxt') = Variable.import true [mod_lit_th] ctxt
    4.93 -         val eqsubst = eq_lit_th RSN (2,rev_subst)
    4.94 -         val newth =
    4.95 -           Seq.hd (biresolution false [(false, fmod_th)] 1 eqsubst)
    4.96 -           |> singleton (Variable.export ctxt' ctxt)
    4.97 -    in Meson.negated_asm_of_head newth end;
    4.98 -
    4.99 -val demod = Attrib.syntax (Scan.lift Args.nat -- Attrib.thm -- Scan.lift Args.nat
   4.100 -  >> (fn ((i, B), j) => Thm.rule_attribute (fn context => fn A =>
   4.101 -      demod_rule (Context.proof_of context) ((A, i), (B, j)))));
   4.102 -
   4.103 -
   4.104 -(** Conversion of a theorem into clauses **)
   4.105 -
   4.106 -(*For efficiency, we rely upon memo-izing in ResAxioms.*)
   4.107 -fun clausify_rule (th,i) = List.nth (ResAxioms.meta_cnf_axiom th, i)
   4.108 -
   4.109 -val clausify = Attrib.syntax (Scan.lift Args.nat
   4.110 -  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
   4.111 -
   4.112 -
   4.113 -(** theory setup **)
   4.114 -
   4.115 -val setup =
   4.116 -  Attrib.add_attributes
   4.117 -    [("binary", binary, "binary resolution"),
   4.118 -     ("paramod", paramod, "paramodulation"),
   4.119 -     ("demod", demod, "demodulation"),
   4.120 -     ("factor", factor, "factoring"),
   4.121 -     ("clausify", clausify, "conversion to clauses")];
   4.122 -
   4.123 -end

     5.1 --- a/src/HOL/Tools/res_axioms.ML	Tue Oct 24 12:02:53 2006 +0200
     5.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Oct 26 10:48:35 2006 +0200
     5.3 @@ -590,9 +590,6 @@
     5.4  
     5.5  fun pairname th = (Thm.name_of_thm th, th);
     5.6  
     5.7 -fun meta_cnf_axiom th =
     5.8 -    map Meson.make_meta_clause (cnf_axiom (pairname th));
     5.9 -
    5.10  (*Principally for debugging*)
    5.11  fun cnf_name s = 
    5.12    let val th = thm s
    5.13 @@ -695,9 +692,16 @@
    5.14      [("meson", Method.thms_ctxt_args meson_meth,
    5.15        "MESON resolution proof procedure")];
    5.16  
    5.17 +(** Attribute for converting a theorem into clauses **)
    5.18  
    5.19 +fun meta_cnf_axiom th = map Meson.make_meta_clause (cnf_axiom (pairname th));
    5.20  
    5.21 -(*** The Skolemization attribute ***)
    5.22 +fun clausify_rule (th,i) = List.nth (meta_cnf_axiom th, i)
    5.23 +
    5.24 +val clausify = Attrib.syntax (Scan.lift Args.nat
    5.25 +  >> (fn i => Thm.rule_attribute (fn _ => fn th => clausify_rule (th, i))));
    5.26 +
    5.27 +(** The Skolemization attribute **)
    5.28  
    5.29  fun conj2_rule (th1,th2) = conjI OF [th1,th2];
    5.30  
    5.31 @@ -712,8 +716,9 @@
    5.32    | skolem_attr (context, th) = (context, conj_rule (skolem_use_cache_thm th));
    5.33  
    5.34  val setup_attrs = Attrib.add_attributes
    5.35 -  [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem")];
    5.36 -
    5.37 +  [("skolem", Attrib.no_args skolem_attr, "skolemization of a theorem"),
    5.38 +   ("clausify", clausify, "conversion to clauses")];
    5.39 +     
    5.40  val setup = clause_cache_setup #> setup_attrs;
    5.41  
    5.42  end;