src/HOL/Tools/ATP/atp_problem.ML

     AQuant of quantifier * 'a list * ('a, 'b) formula |
     AConn of connective * ('a, 'b) formula list |
     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
   val is_atp_variable : string -> bool
   val tptp_strings_for_atp_problem :

   AQuant of quantifier * 'a list * ('a, 'b) formula |
   AConn of connective * ('a, 'b) formula list |
   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 = "!"
   | string_for_quantifier AExists = "?"
 fun string_for_connective ANot = "~"

     "(" ^ space_implode (" " ^ string_for_connective c ^ " ")
                         (map string_for_formula phis) ^ ")"
   | 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
         (Conjecture, AConn (ANot, [phi]))
       else
         (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\
   \% " ^ timestamp () ^ "\n" ::
   maps (fn (_, []) => []

     pool_map nice_name xs ##>> nice_formula phi
     #>> (fn (xs, phi) => AQuant (q, xs, phi))
   | 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
 fun nice_atp_problem readable_names problem =
   nice_problem problem (empty_name_pool readable_names)