extended ATP problem syntax to support other applications than Sledgehammer, e.g. experiments with ATPs

--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Feb 17 12:14:47 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Fri Feb 18 12:32:55 2011 +0100
@@ -16,8 +16,9 @@
     AAtom of 'b
   type 'a uniform_formula = ('a, 'a fo_term) formula
 
-  datatype kind = Axiom | Hypothesis | Conjecture
-  datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+  datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
+  datatype 'a problem_line =
+    Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option
   type 'a problem = (string * 'a problem_line list) list
 
   val timestamp : unit -> string
@@ -44,19 +45,25 @@
   AAtom of 'b
 type 'a uniform_formula = ('a, 'a fo_term) formula
 
-datatype kind = Axiom | Hypothesis | Conjecture
-datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
+datatype 'a problem_line =
+  Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option
 type 'a problem = (string * 'a problem_line list) list
 
 val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
 
 fun string_for_kind Axiom = "axiom"
+  | string_for_kind Definition = "definition"
+  | string_for_kind Lemma = "lemma"
   | string_for_kind Hypothesis = "hypothesis"
   | string_for_kind Conjecture = "conjecture"
 
 fun string_for_term (ATerm (s, [])) = s
   | string_for_term (ATerm ("equal", ts)) =
     space_implode " = " (map string_for_term ts)
+  | string_for_term (ATerm ("[]", ts)) =
+    (* used for lists in the optional "source" field of a derivation *)
+    "[" ^ commas (map string_for_term ts) ^ "]"
   | string_for_term (ATerm (s, ts)) =
     s ^ "(" ^ commas (map string_for_term ts) ^ ")"
 fun string_for_quantifier AForall = "!"
@@ -81,7 +88,7 @@
   | string_for_formula (AAtom tm) = string_for_term tm
 
 fun string_for_problem_line use_conjecture_for_hypotheses
-                            (Fof (ident, kind, phi)) =
+                            (Fof (ident, kind, phi, source)) =
   let
     val (kind, phi) =
       if kind = Hypothesis andalso use_conjecture_for_hypotheses then
@@ -90,7 +97,10 @@
         (kind, phi)
   in
     "fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n    (" ^
-    string_for_formula phi ^ ")).\n"
+    string_for_formula phi ^ ")" ^
+    (case source of
+       SOME tm => ", " ^ string_for_term tm
+     | NONE => "") ^ ").\n"
   end
 fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
   "% This file was generated by Isabelle (most likely Sledgehammer)\n\
@@ -160,8 +170,8 @@
   | nice_formula (AConn (c, phis)) =
     pool_map nice_formula phis #>> curry AConn c
   | nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Fof (ident, kind, phi)) =
-  nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
+fun nice_problem_line (Fof (ident, kind, phi, source)) =
+  nice_formula phi #>> (fn phi => Fof (ident, kind, phi, source))
 fun nice_problem problem =
   pool_map (fn (heading, lines) =>
                pool_map nice_problem_line lines #>> pair heading) problem

--- a/src/HOL/Tools/ATP/atp_systems.ML	Thu Feb 17 12:14:47 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Fri Feb 18 12:32:55 2011 +0100
@@ -109,10 +109,10 @@
 datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
 
 val e_weight_method = Unsynchronized.ref E_Fun_Weight
-val e_default_fun_weight = Unsynchronized.ref 0.5
+val e_default_fun_weight = Unsynchronized.ref 20.0 (* ### *)
 val e_fun_weight_base = Unsynchronized.ref 0.0
 val e_fun_weight_factor = Unsynchronized.ref 40.0
-val e_default_sym_offs_weight = Unsynchronized.ref 0.0
+val e_default_sym_offs_weight = Unsynchronized.ref 1.0 (* ### *)
 val e_sym_offs_weight_base = Unsynchronized.ref ~30.0
 val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0
 
@@ -138,8 +138,8 @@
     \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
     \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^
     "(SimulateSOS, " ^
-    scaled_e_weight (e_weight_method_case (!e_default_fun_weight)
-                                          (!e_default_sym_offs_weight)) ^
+    (e_weight_method_case (!e_default_fun_weight) (!e_default_sym_offs_weight)
+     |> Real.ceil |> signed_string_of_int) ^
     ",20,1.5,1.5,1" ^
     (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w)
                 |> implode) ^

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu Feb 17 12:14:47 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Fri Feb 18 12:32:55 2011 +0100
@@ -294,7 +294,7 @@
        in
          [Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
                AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
-               |> explicit_forall ? close_universally)]
+               |> explicit_forall ? close_universally, NONE)]
        end
      else
        [])
@@ -440,14 +440,15 @@
            (formula_for_combformula ctxt type_sys combformula)
 
 fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
-  Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula)
+  Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula,
+       NONE)
 
 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
                                                        superclass, ...}) =
   let val ty_arg = ATerm (("T", "T"), []) in
     Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
-                           AAtom (ATerm (superclass, [ty_arg]))]))
+                           AAtom (ATerm (superclass, [ty_arg]))]), NONE)
   end
 
 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
@@ -461,12 +462,12 @@
        mk_ahorn (map (formula_for_fo_literal o apfst not
                       o fo_literal_for_arity_literal) premLits)
                 (formula_for_fo_literal
-                     (fo_literal_for_arity_literal conclLit)))
+                     (fo_literal_for_arity_literal conclLit)), NONE)
 
 fun problem_line_for_conjecture ctxt type_sys
         ({name, kind, combformula, ...} : translated_formula) =
   Fof (conjecture_prefix ^ name, kind,
-       formula_for_combformula ctxt type_sys combformula)
+       formula_for_combformula ctxt type_sys combformula, NONE)
 
 fun free_type_literals_for_conjecture type_sys
         ({ctypes_sorts, ...} : translated_formula) =
@@ -474,7 +475,8 @@
                |> map fo_literal_for_type_literal
 
 fun problem_line_for_free_type j lit =
-  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
+  Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit,
+       NONE)
 fun problem_lines_for_free_types type_sys conjs =
   let
     val litss = map (free_type_literals_for_conjecture type_sys) conjs
@@ -502,7 +504,7 @@
   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   | consider_formula (AAtom tm) = consider_term true tm
 
-fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
+fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi
 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
 
 (* needed for helper facts if the problem otherwise does not involve equality *)
@@ -593,8 +595,9 @@
   in aux #> explicit_forall ? close_universally end
 
 fun repair_problem_line thy explicit_forall type_sys const_tab
-                        (Fof (ident, kind, phi)) =
-  Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi)
+                        (Fof (ident, kind, phi, source)) =
+  Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi,
+       source)
 fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
 
 fun dest_Fof (Fof z) = z
@@ -654,7 +657,7 @@
 fun add_term_weights weight (ATerm (s, tms)) =
   (not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
   #> fold (add_term_weights weight) tms
-fun add_problem_line_weights weight (Fof (_, _, phi)) =
+fun add_problem_line_weights weight (Fof (_, _, phi, _)) =
   fold_formula (add_term_weights weight) phi
 
 fun add_conjectures_weights [] = I