thread original theorem along with CNF theorem, as a step toward killing the Skolem cache

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 22 14:48:46 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Tue Jun 22 16:23:29 2010 +0200
@@ -8,7 +8,8 @@
 
 signature ATP_MANAGER =
 sig
-  type name_pool = Sledgehammer_HOL_Clause.name_pool
+  type name_pool = Sledgehammer_FOL_Clause.name_pool
+  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
   type relevance_override = Sledgehammer_Fact_Filter.relevance_override
   type minimize_command = Sledgehammer_Proof_Reconstruct.minimize_command
   type params =
@@ -31,8 +32,8 @@
     {subgoal: int,
      goal: Proof.context * (thm list * thm),
      relevance_override: relevance_override,
-     axiom_clauses: (thm * (string * int)) list option,
-     filtered_clauses: (thm * (string * int)) list option}
+     axiom_clauses: cnf_thm list option,
+     filtered_clauses: cnf_thm list option}
   datatype failure =
     Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
     MalformedInput | MalformedOutput | UnknownError
@@ -46,7 +47,7 @@
      proof: string,
      internal_thm_names: string Vector.vector,
      conjecture_shape: int list list,
-     filtered_clauses: (thm * (string * int)) list}
+     filtered_clauses: cnf_thm list}
   type prover =
     params -> minimize_command -> Time.time -> problem -> prover_result
 
@@ -91,8 +92,8 @@
   {subgoal: int,
    goal: Proof.context * (thm list * thm),
    relevance_override: relevance_override,
-   axiom_clauses: (thm * (string * int)) list option,
-   filtered_clauses: (thm * (string * int)) list option};
+   axiom_clauses: cnf_thm list option,
+   filtered_clauses: cnf_thm list option}
 
 datatype failure =
   Unprovable | IncompleteUnprovable | TimedOut | OutOfResources | OldSpass |
@@ -108,7 +109,7 @@
    proof: string,
    internal_thm_names: string Vector.vector,
    conjecture_shape: int list list,
-   filtered_clauses: (thm * (string * int)) list};
+   filtered_clauses: cnf_thm list}
 
 type prover =
   params -> minimize_command -> Time.time -> problem -> prover_result

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 14:48:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Tue Jun 22 16:23:29 2010 +0200
@@ -5,11 +5,10 @@
 
 signature SLEDGEHAMMER_FACT_FILTER =
 sig
+  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
   type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   type arity_clause = Sledgehammer_FOL_Clause.arity_clause
-  type axiom_name = Sledgehammer_HOL_Clause.axiom_name
   type hol_clause = Sledgehammer_HOL_Clause.hol_clause
-  type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
 
   type relevance_override =
     {add: Facts.ref list,
@@ -24,14 +23,12 @@
   val is_quasi_fol_term : theory -> term -> bool
   val relevant_facts :
     bool -> bool -> real -> real -> bool -> int -> bool -> relevance_override
-    -> Proof.context * (thm list * 'a) -> thm list
-    -> (thm * (string * int)) list
+    -> Proof.context * (thm list * 'a) -> thm list -> cnf_thm list
   val prepare_clauses :
-    bool -> thm list -> (thm * (axiom_name * hol_clause_id)) list
-    -> (thm * (axiom_name * hol_clause_id)) list -> theory
-    -> axiom_name vector
-       * (hol_clause list * hol_clause list * hol_clause list *
-          hol_clause list * classrel_clause list * arity_clause list)
+    bool -> thm list -> cnf_thm list -> cnf_thm list -> theory
+    -> string vector
+       * (hol_clause list * hol_clause list * hol_clause list
+          * hol_clause list * classrel_clause list * arity_clause list)
 end;
 
 structure Sledgehammer_Fact_Filter : SLEDGEHAMMER_FACT_FILTER =
@@ -234,13 +231,13 @@
         | _ => false
     end;
 
-type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
+type annotated_clause = cnf_thm * ((string * const_typ list) list)
        
 (*For a reverse sort, putting the largest values first.*)
-fun compare_pairs ((_,w1),(_,w2)) = Real.compare (w2,w1);
+fun compare_pairs ((_, w1), (_, w2)) = Real.compare (w2, w1)
 
 (*Limit the number of new clauses, to prevent runaway acceptance.*)
-fun take_best max_new (newpairs : (annotd_cls*real) list) =
+fun take_best max_new (newpairs : (annotated_clause * real) list) =
   let val nnew = length newpairs
   in
     if nnew <= max_new then (map #1 newpairs, [])
@@ -252,7 +249,7 @@
                        ", exceeds the limit of " ^ Int.toString (max_new)));
         trace_msg (fn () => ("Effective pass mark: " ^ Real.toString (#2 (List.last accepted))));
         trace_msg (fn () => "Actually passed: " ^
-          space_implode ", " (map (fn (((_,(name,_)),_),_) => name) accepted));
+          space_implode ", " (map (fn (((_,((name,_), _)),_),_) => name) accepted));
 
         (map #1 accepted, map #1 (List.drop (cls, max_new)))
       end
@@ -286,7 +283,8 @@
                   (more_rejects @ rejects)
             end
           | relevant (newrels, rejects)
-                     ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+                     ((ax as (clsthm as (thm, ((name, n), _)), consts_typs)) ::
+                      axs) =
             let
               val weight = if member Thm.eq_thm add_thms thm then 1.0
                            else if member Thm.eq_thm del_thms thm then 0.0
@@ -309,7 +307,7 @@
         
 fun relevance_filter ctxt relevance_threshold relevance_convergence
                      defs_relevant max_new theory_relevant relevance_override
-                     thy axioms goals = 
+                     thy (axioms : cnf_thm list) goals = 
   if relevance_threshold > 0.0 then
     let
       val const_tab = List.foldl (count_axiom_consts theory_relevant thy)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 14:48:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Tue Jun 22 16:23:29 2010 +0200
@@ -7,6 +7,7 @@
 
 signature SLEDGEHAMMER_FACT_PREPROCESSOR =
 sig
+  type cnf_thm = thm * ((string * int) * thm)
   val chained_prefix: string
   val trace: bool Unsynchronized.ref
   val trace_msg: (unit -> string) -> unit
@@ -18,8 +19,7 @@
   val multi_base_blacklist: string list
   val is_theorem_bad_for_atps: thm -> bool
   val type_has_topsort: typ -> bool
-  val cnf_rules_pairs:
-    theory -> (string * thm) list -> (thm * (string * int)) list
+  val cnf_rules_pairs : theory -> (string * thm) list -> cnf_thm list
   val saturate_skolem_cache: theory -> theory option
   val auto_saturate_skolem_cache: bool Unsynchronized.ref
     (* for emergency use where the Skolem cache causes problems *)
@@ -35,6 +35,8 @@
 
 open Sledgehammer_FOL_Clause
 
+type cnf_thm = thm * ((string * int) * thm)
+
 (* Used to label theorems chained into the goal. *)
 val chained_prefix = "Sledgehammer.chained_"
 
@@ -153,10 +155,11 @@
           val cT = Ts ---> T (* FIXME: use "skolem_type_and_args" *)
           val id = skolem_name s (Unsynchronized.inc skolem_count) s'
           val c = Free (id, cT)
-          val rhs = list_abs_free (map dest_Free args,
-                                   HOLogic.choice_const T $ body)
-                    |> inline ? mk_skolem_id
-                (*Forms a lambda-abstraction over the formal parameters*)
+          (* Forms a lambda-abstraction over the formal parameters *)
+          val rhs =
+            list_abs_free (map dest_Free args,
+                           HOLogic.choice_const T $ body)
+            |> inline ? mk_skolem_id
           val def = Logic.mk_equals (c, rhs)
           val comb = list_comb (if inline then rhs else c, args)
         in dec_sko (subst_bound (comb, p)) (def :: defs) end
@@ -446,20 +449,20 @@
 
 (**** Translate a set of theorems into CNF ****)
 
-fun pair_name_cls _ (_, []) = []
-  | pair_name_cls k (n, cls::clss) = (cls, (n,k)) :: pair_name_cls (k+1) (n, clss)
-
 (*The combination of rev and tail recursion preserves the original order*)
 fun cnf_rules_pairs thy =
   let
-    fun aux pairs [] = pairs
-      | aux pairs ((name, th) :: ths) =
+    fun do_one _ [] = []
+      | do_one ((name, k), th) (cls :: clss) =
+        (cls, ((name, k), th)) :: do_one ((name, k + 1), th) clss
+    fun do_all pairs [] = pairs
+      | do_all pairs ((name, th) :: ths) =
         let
-          val new_pairs = pair_name_cls 0 (name, cnf_axiom thy th)
+          val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
                           handle THM _ => [] |
                                  CLAUSE _ => []
-        in aux (new_pairs @ pairs) ths end
-  in aux [] o rev end
+        in do_all (new_pairs @ pairs) ths end
+  in do_all [] o rev end
 
 
 (**** Convert all facts of the theory into FOL or HOL clauses ****)

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 14:48:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML	Tue Jun 22 16:23:29 2010 +0200
@@ -37,7 +37,6 @@
   val pool_map : ('a -> 'b -> 'c * 'b) -> 'a list -> 'b -> 'c list * 'b
   val nice_name : name -> name_pool option -> string * name_pool option
   datatype kind = Axiom | Conjecture
-  type axiom_name = string
   datatype fol_type =
     TyVar of name |
     TyFree of name |
@@ -53,9 +52,9 @@
       TConsLit of class * string * string list
     | TVarLit of class * string
   datatype arity_clause = ArityClause of
-   {axiom_name: axiom_name, conclLit: arLit, premLits: arLit list}
+   {axiom_name: string, conclLit: arLit, premLits: arLit list}
   datatype classrel_clause = ClassrelClause of
-   {axiom_name: axiom_name, subclass: class, superclass: class}
+   {axiom_name: string, subclass: class, superclass: class}
   val make_classrel_clauses: theory -> class list -> class list -> classrel_clause list
   val make_arity_clauses: theory -> string list -> class list -> class list * arity_clause list
   val tptp_sign: bool -> string -> string
@@ -259,8 +258,6 @@
 
 datatype kind = Axiom | Conjecture;
 
-type axiom_name = string;
-
 (**** Isabelle FOL clauses ****)
 
 datatype fol_type =
@@ -308,9 +305,7 @@
                | TVarLit of class * string;
 
 datatype arity_clause =
-         ArityClause of {axiom_name: axiom_name,
-                         conclLit: arLit,
-                         premLits: arLit list};
+  ArityClause of {axiom_name: string, conclLit: arLit, premLits: arLit list}
 
 
 fun gen_TVars 0 = []
@@ -334,9 +329,7 @@
 (**** Isabelle class relations ****)
 
 datatype classrel_clause =
-         ClassrelClause of {axiom_name: axiom_name,
-                            subclass: class,
-                            superclass: class};
+  ClassrelClause of {axiom_name: string, subclass: class, superclass: class}
 
 (*Generate all pairs (sub,super) such that sub is a proper subclass of super in theory thy.*)
 fun class_pairs _ [] _ = []
@@ -437,7 +430,8 @@
   let val tvar = "(T)"
   in  tptp_clause [tptp_sign false (sub^tvar), tptp_sign true (sup^tvar)]  end;
 
-fun tptp_classrel_clause (ClassrelClause {axiom_name,subclass,superclass,...}) =
+fun tptp_classrel_clause (ClassrelClause {axiom_name, subclass, superclass,
+                                          ...}) =
   tptp_cnf axiom_name "axiom" (tptp_classrelLits subclass superclass)
 
 end;

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 14:48:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Tue Jun 22 16:23:29 2010 +0200
@@ -7,15 +7,14 @@
 
 signature SLEDGEHAMMER_HOL_CLAUSE =
 sig
+  type cnf_thm = Sledgehammer_Fact_Preprocessor.cnf_thm
   type name = Sledgehammer_FOL_Clause.name
   type name_pool = Sledgehammer_FOL_Clause.name_pool
   type kind = Sledgehammer_FOL_Clause.kind
   type fol_type = Sledgehammer_FOL_Clause.fol_type
   type classrel_clause = Sledgehammer_FOL_Clause.classrel_clause
   type arity_clause = Sledgehammer_FOL_Clause.arity_clause
-  type axiom_name = string
   type polarity = bool
-  type hol_clause_id = int
 
   datatype combterm =
     CombConst of name * fol_type * fol_type list (* Const and Free *) |
@@ -23,8 +22,8 @@
     CombApp of combterm * combterm
   datatype literal = Literal of polarity * combterm
   datatype hol_clause =
-    HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
-                  kind: kind, literals: literal list, ctypes_sorts: typ list}
+    HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+                  literals: literal list, ctypes_sorts: typ list}
 
   val type_of_combterm : combterm -> fol_type
   val strip_combterm_comb : combterm -> combterm * combterm list
@@ -33,13 +32,10 @@
     int -> (string * term) list -> term -> (string * term) list * term
   exception TRIVIAL
   val make_conjecture_clauses : theory -> thm list -> hol_clause list
-  val make_axiom_clauses :
-    theory -> (thm * (axiom_name * hol_clause_id)) list
-    -> (axiom_name * hol_clause) list
+  val make_axiom_clauses : theory -> cnf_thm list -> (string * hol_clause) list
   val type_wrapper_name : string
   val get_helper_clauses :
-    theory -> bool -> bool -> hol_clause list
-    -> (thm * (axiom_name * hol_clause_id)) list -> hol_clause list
+    theory -> bool -> bool -> hol_clause list -> cnf_thm list -> hol_clause list
   val write_tptp_file : bool -> bool -> bool -> Path.T ->
     hol_clause list * hol_clause list * hol_clause list * hol_clause list *
     classrel_clause list * arity_clause list -> name_pool option * int
@@ -65,9 +61,7 @@
 (* data types for typed combinator expressions        *)
 (******************************************************)
 
-type axiom_name = string;
-type polarity = bool;
-type hol_clause_id = int;
+type polarity = bool
 
 datatype combterm =
   CombConst of name * fol_type * fol_type list (* Const and Free *) |
@@ -77,8 +71,8 @@
 datatype literal = Literal of polarity * combterm;
 
 datatype hol_clause =
-  HOLClause of {clause_id: hol_clause_id, axiom_name: axiom_name, th: thm,
-                kind: kind, literals: literal list, ctypes_sorts: typ list};
+  HOLClause of {clause_id: int, axiom_name: string, th: thm, kind: kind,
+                literals: literal list, ctypes_sorts: typ list}
 
 
 (*********************************************************************)
@@ -212,7 +206,7 @@
                   kind = kind, literals = lits, ctypes_sorts = ctypes_sorts})
   end
 
-fun add_axiom_clause thy (th, (name, id)) (skolem_somes, clss) =
+fun add_axiom_clause thy (th, ((name, id), _ : thm)) (skolem_somes, clss) =
   let
     val (skolem_somes, cls) = make_clause thy (id, name, Axiom, th) skolem_somes
   in (skolem_somes, clss |> not (isTaut cls) ? cons (name, cls)) end
@@ -364,7 +358,7 @@
 
 fun count_clause (HOLClause {literals, ...}) = fold count_literal literals
 
-val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, (name, 0)))
+val raw_cnf_rules_pairs = map (fn (name, thm) => (thm, ((name, 0), thm)))
 fun cnf_helper_thms thy raw =
   map (`Thm.get_name_hint)
   #> (if raw then raw_cnf_rules_pairs else cnf_rules_pairs thy)