don't generate TPTP THF 'Definition's, because they complicate reconstruction for AgsyHOL and Satallax

--- a/src/HOL/TPTP/atp_problem_import.ML	Sat Jul 12 11:31:22 2014 +0200
+++ b/src/HOL/TPTP/atp_problem_import.ML	Sat Jul 12 11:31:23 2014 +0200
@@ -62,11 +62,16 @@
   end
 
 
-(** Nitpick (alias Nitrox) **)
+(** Nitpick **)
 
 fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
   | aptrueprop f t = f t
 
+fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
+  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
+    (is_Const t orelse is_Free t) andalso not (exists_subterm (curry (op =) t) u)
+  | is_legitimate_tptp_def _ = false
+
 fun nitpick_tptp_file thy timeout file_name =
   let
     val (conjs, (defs, nondefs), ctxt) = read_tptp_file thy snd file_name
@@ -74,7 +79,7 @@
     val (defs, pseudo_defs) =
       defs |> map (ATP_Util.abs_extensionalize_term ctxt
                    #> aptrueprop (hol_open_form I))
-           |> List.partition (ATP_Util.is_legitimate_tptp_def
+           |> List.partition (is_legitimate_tptp_def
                               o perhaps (try HOLogic.dest_Trueprop)
                               o ATP_Util.unextensionalize_def)
     val nondefs = pseudo_defs @ nondefs

--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jul 12 11:31:22 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Jul 12 11:31:23 2014 +0200
@@ -1275,30 +1275,17 @@
     {name = name, stature = stature, role = role, iformula = iformula, atomic_types = atomic_Ts}
   end
 
-fun is_format_with_defs (THF _) = true
-  | is_format_with_defs _ = false
-
-fun make_fact ctxt format type_enc iff_for_eq ((name, stature as (_, status)), t) =
-  let
-    val role =
-      if is_format_with_defs format andalso status = Non_Rec_Def andalso
-         is_legitimate_tptp_def t then
-        Definition
-      else
-        Axiom
-  in
-    (case make_formula ctxt format type_enc iff_for_eq name stature role t of
-      formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
-      if s = tptp_true then NONE else SOME formula
-    | formula => SOME formula)
-  end
+fun make_fact ctxt format type_enc iff_for_eq ((name, stature), t) =
+  (case make_formula ctxt format type_enc iff_for_eq name stature Axiom t of
+    formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
+    if s = tptp_true then NONE else SOME formula
+  | formula => SOME formula)
 
 fun make_conjecture ctxt format type_enc =
   map (fn ((name, stature), (role, t)) =>
-    let
-      val role' = if role <> Conjecture andalso is_legitimate_tptp_def t then Definition else role
-      val t' = t |> role' = Conjecture ? s_not
-    in make_formula ctxt format type_enc true name stature role' t' end)
+    let val t' = t |> role = Conjecture ? s_not in
+      make_formula ctxt format type_enc true name stature role t'
+    end)
 
 (** Finite and infinite type inference **)
 

--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Jul 12 11:31:22 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sat Jul 12 11:31:23 2014 +0200
@@ -132,8 +132,7 @@
           Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
             (if null clss then @{sort type} else map class_of_atp_class clss))))
   end
-  | typ_of_atp_type ctxt (ty as AFun (a, tys)) =
-    (typ_of_atp_type ctxt a) --> (typ_of_atp_type ctxt tys)
+  | typ_of_atp_type ctxt (AFun (a, tys)) = typ_of_atp_type ctxt a --> typ_of_atp_type ctxt tys
 
 fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
 
@@ -253,7 +252,7 @@
           (case unprefix_and_unascii const_prefix s of
             SOME s' =>
             let
-              val ((s', s''), mangled_us) = s' |> unmangled_const |>> `invert_const
+              val ((s', _), mangled_us) = s' |> unmangled_const |>> `invert_const
               val num_ty_args = length us - the_default 0 (Symtab.lookup sym_tab s)
               val (type_us, term_us) = chop num_ty_args us |>> append mangled_us
               val term_ts = map (do_term NONE) term_us
@@ -475,25 +474,11 @@
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
 
-fun add_non_rec_defs facts =
-  fold (fn fact as (_, (_, status)) => status = Non_Rec_Def ? insert (op =) fact) facts
-
 val leo2_extcnf_equal_neg_rule = "extcnf_equal_neg"
-val leo2_unfold_def_rule = "unfold_def"
 
 fun add_fact ctxt facts ((_, ss), _, _, rule, deps) =
-  (if rule = leo2_extcnf_equal_neg_rule then
+  (if member (op =) [agsyhol_core_rule, leo2_extcnf_equal_neg_rule, satallax_core_rule] rule then
      insert (op =) (short_thm_name ctxt ext, (Global, General))
-   else if rule = leo2_unfold_def_rule then
-     (* LEO 1.3.3 does not record definitions properly, leading to missing dependencies in the TSTP
-        proof. Remove the next line once this is fixed. *)
-     add_non_rec_defs facts
-   else if rule = agsyhol_core_rule orelse rule = satallax_core_rule then
-     (fn [] =>
-         (* agsyHOL and Satallax don't include definitions in their unsatisfiable cores, so we
-            assume the worst and include them all here. *)
-         [(short_thm_name ctxt ext, (Global, General))] |> add_non_rec_defs facts
-       | facts => facts)
    else
      I)
   #> (if null deps then union (op =) (resolve_facts facts ss) else I)

--- a/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 12 11:31:22 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Sat Jul 12 11:31:23 2014 +0200
@@ -190,8 +190,6 @@
 
 (* Alt-Ergo *)
 
-val alt_ergo_tff1 = TFF Polymorphic
-
 val alt_ergo_config : atp_config =
   {exec = K (["WHY3_HOME"], ["why3"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
@@ -205,7 +203,7 @@
    prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
+     [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 
@@ -593,8 +591,6 @@
 
 (* Zipperposition*)
 
-val zipperposition_tff1 = TFF Polymorphic
-
 val zipperposition_config : atp_config =
   {exec = K (["ZIPPERPOSITION_HOME"], ["zipperposition"]),
    arguments = fn _ => fn _ => fn _ => fn timeout => fn file_name => fn _ =>
@@ -605,7 +601,7 @@
    prem_role = Hypothesis,
    best_slices = fn _ =>
      (* FUDGE *)
-     [(1.0, (((100, ""), alt_ergo_tff1, "poly_native", liftingN, false), ""))],
+     [(1.0, (((100, ""), TFF Polymorphic, "poly_native", liftingN, false), ""))],
    best_max_mono_iters = default_max_mono_iters,
    best_max_new_mono_instances = default_max_new_mono_instances}
 

--- a/src/HOL/Tools/ATP/atp_util.ML	Sat Jul 12 11:31:22 2014 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML	Sat Jul 12 11:31:23 2014 +0200
@@ -45,7 +45,6 @@
   val cong_extensionalize_term : theory -> term -> term
   val abs_extensionalize_term : Proof.context -> term -> term
   val unextensionalize_def : term -> term
-  val is_legitimate_tptp_def : term -> bool
   val transform_elim_prop : term -> term
   val specialize_type : theory -> (string * typ) -> term -> term
   val strip_subgoal : thm -> int -> Proof.context -> (string * typ) list * term list * term
@@ -382,12 +381,6 @@
      | _ => t)
   | _ => t
 
-fun is_legitimate_tptp_def (@{const Trueprop} $ t) = is_legitimate_tptp_def t
-  | is_legitimate_tptp_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
-    (is_Const t orelse is_Free t) andalso
-    not (exists_subterm (curry (op =) t) u)
-  | is_legitimate_tptp_def _ = false
-
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to "False". (Cf. "transform_elim_theorem" in