src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
author blanchet
Thu Aug 26 10:42:06 2010 +0200 (2010-08-26)
changeset 38752 6628adcae4a7
parent 38748 69fea359d3f8
child 38786 e46e7a9cb622
child 38818 61cf050f8b2e
permissions -rw-r--r--
consider "locality" when assigning weights to facts
     1 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_translate.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Translation of HOL to FOL.
     7 *)
     8 
     9 signature SLEDGEHAMMER_TRANSLATE =
    10 sig
    11   type 'a problem = 'a ATP_Problem.problem
    12 
    13   val axiom_prefix : string
    14   val conjecture_prefix : string
    15   val helper_prefix : string
    16   val class_rel_clause_prefix : string
    17   val arity_clause_prefix : string
    18   val tfrees_name : string
    19   val prepare_problem :
    20     Proof.context -> bool -> bool -> bool -> bool -> term list -> term
    21     -> ((string * 'a) * thm) list
    22     -> string problem * string Symtab.table * int * (string * 'a) vector
    23 end;
    24 
    25 structure Sledgehammer_Translate : SLEDGEHAMMER_TRANSLATE =
    26 struct
    27 
    28 open ATP_Problem
    29 open Metis_Clauses
    30 open Sledgehammer_Util
    31 
    32 val axiom_prefix = "ax_"
    33 val conjecture_prefix = "conj_"
    34 val helper_prefix = "help_"
    35 val class_rel_clause_prefix = "clrel_";
    36 val arity_clause_prefix = "arity_"
    37 val tfrees_name = "tfrees"
    38 
    39 (* Freshness almost guaranteed! *)
    40 val sledgehammer_weak_prefix = "Sledgehammer:"
    41 
    42 type fol_formula =
    43   {name: string,
    44    kind: kind,
    45    combformula: (name, combterm) formula,
    46    ctypes_sorts: typ list}
    47 
    48 fun mk_anot phi = AConn (ANot, [phi])
    49 fun mk_aconn c phi1 phi2 = AConn (c, [phi1, phi2])
    50 fun mk_ahorn [] phi = phi
    51   | mk_ahorn (phi :: phis) psi =
    52     AConn (AImplies, [fold (mk_aconn AAnd) phis phi, psi])
    53 
    54 fun combformula_for_prop thy =
    55   let
    56     val do_term = combterm_from_term thy
    57     fun do_quant bs q s T t' =
    58       let val s = Name.variant (map fst bs) s in
    59         do_formula ((s, T) :: bs) t'
    60         #>> (fn phi => AQuant (q, [`make_bound_var s], phi))
    61       end
    62     and do_conn bs c t1 t2 =
    63       do_formula bs t1 ##>> do_formula bs t2
    64       #>> (fn (phi1, phi2) => AConn (c, [phi1, phi2]))
    65     and do_formula bs t =
    66       case t of
    67         @{const Not} $ t1 =>
    68         do_formula bs t1 #>> (fn phi => AConn (ANot, [phi]))
    69       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
    70         do_quant bs AForall s T t'
    71       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
    72         do_quant bs AExists s T t'
    73       | @{const "op &"} $ t1 $ t2 => do_conn bs AAnd t1 t2
    74       | @{const "op |"} $ t1 $ t2 => do_conn bs AOr t1 t2
    75       | @{const "op -->"} $ t1 $ t2 => do_conn bs AImplies t1 t2
    76       | Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
    77         do_conn bs AIff t1 t2
    78       | _ => (fn ts => do_term bs (Envir.eta_contract t)
    79                        |>> AAtom ||> union (op =) ts)
    80   in do_formula [] end
    81 
    82 val presimplify_term = prop_of o Meson.presimplify oo Skip_Proof.make_thm
    83 
    84 fun concealed_bound_name j = sledgehammer_weak_prefix ^ Int.toString j
    85 fun conceal_bounds Ts t =
    86   subst_bounds (map (Free o apfst concealed_bound_name)
    87                     (0 upto length Ts - 1 ~~ Ts), t)
    88 fun reveal_bounds Ts =
    89   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
    90                     (0 upto length Ts - 1 ~~ Ts))
    91 
    92 (* Removes the lambdas from an equation of the form "t = (%x. u)".
    93    (Cf. "extensionalize_theorem" in "Clausifier".) *)
    94 fun extensionalize_term t =
    95   let
    96     fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
    97       | aux j (t as Const (s, Type (_, [Type (_, [_, T']),
    98                                         Type (_, [_, res_T])]))
    99                     $ t2 $ Abs (var_s, var_T, t')) =
   100         if s = @{const_name "op ="} orelse s = @{const_name "=="} then
   101           let val var_t = Var ((var_s, j), var_T) in
   102             Const (s, T' --> T' --> res_T)
   103               $ betapply (t2, var_t) $ subst_bound (var_t, t')
   104             |> aux (j + 1)
   105           end
   106         else
   107           t
   108       | aux _ t = t
   109   in aux (maxidx_of_term t + 1) t end
   110 
   111 fun introduce_combinators_in_term ctxt kind t =
   112   let val thy = ProofContext.theory_of ctxt in
   113     if Meson.is_fol_term thy t then
   114       t
   115     else
   116       let
   117         fun aux Ts t =
   118           case t of
   119             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   120           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   121             t0 $ Abs (s, T, aux (T :: Ts) t')
   122           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   123             aux Ts (t0 $ eta_expand Ts t1 1)
   124           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   125             t0 $ Abs (s, T, aux (T :: Ts) t')
   126           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   127             aux Ts (t0 $ eta_expand Ts t1 1)
   128           | (t0 as @{const "op &"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   129           | (t0 as @{const "op |"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   130           | (t0 as @{const "op -->"}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   131           | (t0 as Const (@{const_name "op ="}, Type (_, [@{typ bool}, _])))
   132               $ t1 $ t2 =>
   133             t0 $ aux Ts t1 $ aux Ts t2
   134           | _ => if not (exists_subterm (fn Abs _ => true | _ => false) t) then
   135                    t
   136                  else
   137                    t |> conceal_bounds Ts
   138                      |> Envir.eta_contract
   139                      |> cterm_of thy
   140                      |> Clausifier.introduce_combinators_in_cterm
   141                      |> prop_of |> Logic.dest_equals |> snd
   142                      |> reveal_bounds Ts
   143         val ([t], ctxt') = Variable.import_terms true [t] ctxt
   144       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   145       handle THM _ =>
   146              (* A type variable of sort "{}" will make abstraction fail. *)
   147              if kind = Conjecture then HOLogic.false_const
   148              else HOLogic.true_const
   149   end
   150 
   151 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   152    same in Sledgehammer to prevent the discovery of unreplable proofs. *)
   153 fun freeze_term t =
   154   let
   155     fun aux (t $ u) = aux t $ aux u
   156       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
   157       | aux (Var ((s, i), T)) =
   158         Free (sledgehammer_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
   159       | aux t = t
   160   in t |> exists_subterm is_Var t ? aux end
   161 
   162 (* "Object_Logic.atomize_term" isn't as powerful as it could be; for example,
   163     it leaves metaequalities over "prop"s alone. *)
   164 val atomize_term =
   165   let
   166     fun aux (@{const Trueprop} $ t1) = t1
   167       | aux (Const (@{const_name all}, _) $ Abs (s, T, t')) =
   168         HOLogic.all_const T $ Abs (s, T, aux t')
   169       | aux (@{const "==>"} $ t1 $ t2) = HOLogic.mk_imp (pairself aux (t1, t2))
   170       | aux (Const (@{const_name "=="}, Type (_, [@{typ prop}, _])) $ t1 $ t2) =
   171         HOLogic.eq_const HOLogic.boolT $ aux t1 $ aux t2
   172       | aux (Const (@{const_name "=="}, Type (_, [T, _])) $ t1 $ t2) =
   173         HOLogic.eq_const T $ t1 $ t2
   174       | aux _ = raise Fail "aux"
   175   in perhaps (try aux) end
   176 
   177 (* making axiom and conjecture formulas *)
   178 fun make_formula ctxt presimp name kind t =
   179   let
   180     val thy = ProofContext.theory_of ctxt
   181     val t = t |> Envir.beta_eta_contract
   182               |> transform_elim_term
   183               |> atomize_term
   184     val need_trueprop = (fastype_of t = HOLogic.boolT)
   185     val t = t |> need_trueprop ? HOLogic.mk_Trueprop
   186               |> extensionalize_term
   187               |> presimp ? presimplify_term thy
   188               |> perhaps (try (HOLogic.dest_Trueprop))
   189               |> introduce_combinators_in_term ctxt kind
   190               |> kind <> Axiom ? freeze_term
   191     val (combformula, ctypes_sorts) = combformula_for_prop thy t []
   192   in
   193     {name = name, combformula = combformula, kind = kind,
   194      ctypes_sorts = ctypes_sorts}
   195   end
   196 
   197 fun make_axiom ctxt presimp ((name, loc), th) =
   198   case make_formula ctxt presimp name Axiom (prop_of th) of
   199     {combformula = AAtom (CombConst (("c_True", _), _, _)), ...} => NONE
   200   | formula => SOME ((name, loc), formula)
   201 fun make_conjecture ctxt ts =
   202   let val last = length ts - 1 in
   203     map2 (fn j => make_formula ctxt true (Int.toString j)
   204                                (if j = last then Conjecture else Hypothesis))
   205          (0 upto last) ts
   206   end
   207 
   208 (** Helper facts **)
   209 
   210 fun count_combterm (CombConst ((s, _), _, _)) =
   211     Symtab.map_entry s (Integer.add 1)
   212   | count_combterm (CombVar _) = I
   213   | count_combterm (CombApp (t1, t2)) = fold count_combterm [t1, t2]
   214 fun count_combformula (AQuant (_, _, phi)) = count_combformula phi
   215   | count_combformula (AConn (_, phis)) = fold count_combformula phis
   216   | count_combformula (AAtom tm) = count_combterm tm
   217 fun count_fol_formula ({combformula, ...} : fol_formula) =
   218   count_combformula combformula
   219 
   220 val optional_helpers =
   221   [(["c_COMBI", "c_COMBK"], @{thms COMBI_def COMBK_def}),
   222    (["c_COMBB", "c_COMBC"], @{thms COMBB_def COMBC_def}),
   223    (["c_COMBS"], @{thms COMBS_def})]
   224 val optional_typed_helpers =
   225   [(["c_True", "c_False", "c_If"], @{thms True_or_False}),
   226    (["c_If"], @{thms if_True if_False})]
   227 val mandatory_helpers = @{thms fequal_def}
   228 
   229 val init_counters =
   230   [optional_helpers, optional_typed_helpers] |> maps (maps fst)
   231   |> sort_distinct string_ord |> map (rpair 0) |> Symtab.make
   232 
   233 fun get_helper_facts ctxt is_FO full_types conjectures axioms =
   234   let
   235     val ct = fold (fold count_fol_formula) [conjectures, axioms] init_counters
   236     fun is_needed c = the (Symtab.lookup ct c) > 0
   237     fun baptize th = ((Thm.get_name_hint th, false), th)
   238   in
   239     (optional_helpers
   240      |> full_types ? append optional_typed_helpers
   241      |> maps (fn (ss, ths) =>
   242                  if exists is_needed ss then map baptize ths else [])) @
   243     (if is_FO then [] else map baptize mandatory_helpers)
   244     |> map_filter (Option.map snd o make_axiom ctxt false)
   245   end
   246 
   247 fun prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs =
   248   let
   249     val thy = ProofContext.theory_of ctxt
   250     val axiom_ts = map (prop_of o snd) axiom_pairs
   251     val hyp_ts =
   252       if null hyp_ts then
   253         []
   254       else
   255         (* Remove existing axioms from the conjecture, as this can dramatically
   256            boost an ATP's performance (for some reason). *)
   257         let
   258           val axiom_table = fold (Termtab.update o rpair ()) axiom_ts
   259                                  Termtab.empty
   260         in hyp_ts |> filter_out (Termtab.defined axiom_table) end
   261     val goal_t = Logic.list_implies (hyp_ts, concl_t)
   262     val is_FO = Meson.is_fol_term thy goal_t
   263     val subs = tfree_classes_of_terms [goal_t]
   264     val supers = tvar_classes_of_terms axiom_ts
   265     val tycons = type_consts_of_terms thy (goal_t :: axiom_ts)
   266     (* TFrees in the conjecture; TVars in the axioms *)
   267     val conjectures = make_conjecture ctxt (hyp_ts @ [concl_t])
   268     val (axiom_names, axioms) =
   269       ListPair.unzip (map_filter (make_axiom ctxt true) axiom_pairs)
   270     val helper_facts = get_helper_facts ctxt is_FO full_types conjectures axioms
   271     val (supers', arity_clauses) = make_arity_clauses thy tycons supers
   272     val class_rel_clauses = make_class_rel_clauses thy subs supers'
   273   in
   274     (Vector.fromList axiom_names,
   275      (conjectures, axioms, helper_facts, class_rel_clauses, arity_clauses))
   276   end
   277 
   278 fun wrap_type ty t = ATerm ((type_wrapper_name, type_wrapper_name), [ty, t])
   279 
   280 fun fo_term_for_combtyp (CombTVar name) = ATerm (name, [])
   281   | fo_term_for_combtyp (CombTFree name) = ATerm (name, [])
   282   | fo_term_for_combtyp (CombType (name, tys)) =
   283     ATerm (name, map fo_term_for_combtyp tys)
   284 
   285 fun fo_literal_for_type_literal (TyLitVar (class, name)) =
   286     (true, ATerm (class, [ATerm (name, [])]))
   287   | fo_literal_for_type_literal (TyLitFree (class, name)) =
   288     (true, ATerm (class, [ATerm (name, [])]))
   289 
   290 fun formula_for_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
   291 
   292 fun fo_term_for_combterm full_types =
   293   let
   294     fun aux top_level u =
   295       let
   296         val (head, args) = strip_combterm_comb u
   297         val (x, ty_args) =
   298           case head of
   299             CombConst (name as (s, s'), _, ty_args) =>
   300             let val ty_args = if full_types then [] else ty_args in
   301               if s = "equal" then
   302                 if top_level andalso length args = 2 then (name, [])
   303                 else (("c_fequal", @{const_name fequal}), ty_args)
   304               else if top_level then
   305                 case s of
   306                   "c_False" => (("$false", s'), [])
   307                 | "c_True" => (("$true", s'), [])
   308                 | _ => (name, ty_args)
   309               else
   310                 (name, ty_args)
   311             end
   312           | CombVar (name, _) => (name, [])
   313           | CombApp _ => raise Fail "impossible \"CombApp\""
   314         val t = ATerm (x, map fo_term_for_combtyp ty_args @
   315                           map (aux false) args)
   316     in
   317       if full_types then wrap_type (fo_term_for_combtyp (combtyp_of u)) t else t
   318     end
   319   in aux true end
   320 
   321 fun formula_for_combformula full_types =
   322   let
   323     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   324       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   325       | aux (AAtom tm) = AAtom (fo_term_for_combterm full_types tm)
   326   in aux end
   327 
   328 fun formula_for_axiom full_types
   329                       ({combformula, ctypes_sorts, ...} : fol_formula) =
   330   mk_ahorn (map (formula_for_fo_literal o fo_literal_for_type_literal)
   331                 (type_literals_for_types ctypes_sorts))
   332            (formula_for_combformula full_types combformula)
   333 
   334 fun problem_line_for_fact prefix full_types (formula as {name, kind, ...}) =
   335   Fof (prefix ^ ascii_of name, kind, formula_for_axiom full_types formula)
   336 
   337 fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
   338                                                        superclass, ...}) =
   339   let val ty_arg = ATerm (("T", "T"), []) in
   340     Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
   341          AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
   342                            AAtom (ATerm (superclass, [ty_arg]))]))
   343   end
   344 
   345 fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
   346     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
   347   | fo_literal_for_arity_literal (TVarLit (c, sort)) =
   348     (false, ATerm (c, [ATerm (sort, [])]))
   349 
   350 fun problem_line_for_arity_clause (ArityClause {name, conclLit, premLits,
   351                                                 ...}) =
   352   Fof (arity_clause_prefix ^ ascii_of name, Axiom,
   353        mk_ahorn (map (formula_for_fo_literal o apfst not
   354                       o fo_literal_for_arity_literal) premLits)
   355                 (formula_for_fo_literal
   356                      (fo_literal_for_arity_literal conclLit)))
   357 
   358 fun problem_line_for_conjecture full_types
   359                                 ({name, kind, combformula, ...} : fol_formula) =
   360   Fof (conjecture_prefix ^ name, kind,
   361        formula_for_combformula full_types combformula)
   362 
   363 fun free_type_literals_for_conjecture ({ctypes_sorts, ...} : fol_formula) =
   364   map fo_literal_for_type_literal (type_literals_for_types ctypes_sorts)
   365 
   366 fun problem_line_for_free_type lit =
   367   Fof (tfrees_name, Hypothesis, formula_for_fo_literal lit)
   368 fun problem_lines_for_free_types conjectures =
   369   let
   370     val litss = map free_type_literals_for_conjecture conjectures
   371     val lits = fold (union (op =)) litss []
   372   in map problem_line_for_free_type lits end
   373 
   374 (** "hBOOL" and "hAPP" **)
   375 
   376 type const_info = {min_arity: int, max_arity: int, sub_level: bool}
   377 
   378 fun consider_term top_level (ATerm ((s, _), ts)) =
   379   (if is_tptp_variable s then
   380      I
   381    else
   382      let val n = length ts in
   383        Symtab.map_default
   384            (s, {min_arity = n, max_arity = 0, sub_level = false})
   385            (fn {min_arity, max_arity, sub_level} =>
   386                {min_arity = Int.min (n, min_arity),
   387                 max_arity = Int.max (n, max_arity),
   388                 sub_level = sub_level orelse not top_level})
   389      end)
   390   #> fold (consider_term (top_level andalso s = type_wrapper_name)) ts
   391 fun consider_formula (AQuant (_, _, phi)) = consider_formula phi
   392   | consider_formula (AConn (_, phis)) = fold consider_formula phis
   393   | consider_formula (AAtom tm) = consider_term true tm
   394 
   395 fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
   396 fun consider_problem problem = fold (fold consider_problem_line o snd) problem
   397 
   398 fun const_table_for_problem explicit_apply problem =
   399   if explicit_apply then NONE
   400   else SOME (Symtab.empty |> consider_problem problem)
   401 
   402 fun min_arity_of thy full_types NONE s =
   403     (if s = "equal" orelse s = type_wrapper_name orelse
   404         String.isPrefix type_const_prefix s orelse
   405         String.isPrefix class_prefix s then
   406        16383 (* large number *)
   407      else if full_types then
   408        0
   409      else case strip_prefix_and_unascii const_prefix s of
   410        SOME s' => num_type_args thy (invert_const s')
   411      | NONE => 0)
   412   | min_arity_of _ _ (SOME the_const_tab) s =
   413     case Symtab.lookup the_const_tab s of
   414       SOME ({min_arity, ...} : const_info) => min_arity
   415     | NONE => 0
   416 
   417 fun full_type_of (ATerm ((s, _), [ty, _])) =
   418     if s = type_wrapper_name then ty else raise Fail "expected type wrapper"
   419   | full_type_of _ = raise Fail "expected type wrapper"
   420 
   421 fun list_hAPP_rev _ t1 [] = t1
   422   | list_hAPP_rev NONE t1 (t2 :: ts2) =
   423     ATerm (`I "hAPP", [list_hAPP_rev NONE t1 ts2, t2])
   424   | list_hAPP_rev (SOME ty) t1 (t2 :: ts2) =
   425     let val ty' = ATerm (`make_fixed_type_const @{type_name fun},
   426                          [full_type_of t2, ty]) in
   427       ATerm (`I "hAPP", [wrap_type ty' (list_hAPP_rev (SOME ty') t1 ts2), t2])
   428     end
   429 
   430 fun repair_applications_in_term thy full_types const_tab =
   431   let
   432     fun aux opt_ty (ATerm (name as (s, _), ts)) =
   433       if s = type_wrapper_name then
   434         case ts of
   435           [t1, t2] => ATerm (name, [aux NONE t1, aux (SOME t1) t2])
   436         | _ => raise Fail "malformed type wrapper"
   437       else
   438         let
   439           val ts = map (aux NONE) ts
   440           val (ts1, ts2) = chop (min_arity_of thy full_types const_tab s) ts
   441         in list_hAPP_rev opt_ty (ATerm (name, ts1)) (rev ts2) end
   442   in aux NONE end
   443 
   444 fun boolify t = ATerm (`I "hBOOL", [t])
   445 
   446 (* True if the constant ever appears outside of the top-level position in
   447    literals, or if it appears with different arities (e.g., because of different
   448    type instantiations). If false, the constant always receives all of its
   449    arguments and is used as a predicate. *)
   450 fun is_predicate NONE s =
   451     s = "equal" orelse s = "$false" orelse s = "$true" orelse
   452     String.isPrefix type_const_prefix s orelse String.isPrefix class_prefix s
   453   | is_predicate (SOME the_const_tab) s =
   454     case Symtab.lookup the_const_tab s of
   455       SOME {min_arity, max_arity, sub_level} =>
   456       not sub_level andalso min_arity = max_arity
   457     | NONE => false
   458 
   459 fun repair_predicates_in_term const_tab (t as ATerm ((s, _), ts)) =
   460   if s = type_wrapper_name then
   461     case ts of
   462       [_, t' as ATerm ((s', _), _)] =>
   463       if is_predicate const_tab s' then t' else boolify t
   464     | _ => raise Fail "malformed type wrapper"
   465   else
   466     t |> not (is_predicate const_tab s) ? boolify
   467 
   468 fun close_universally phi =
   469   let
   470     fun term_vars bounds (ATerm (name as (s, _), tms)) =
   471         (is_tptp_variable s andalso not (member (op =) bounds name))
   472           ? insert (op =) name
   473         #> fold (term_vars bounds) tms
   474     fun formula_vars bounds (AQuant (_, xs, phi)) =
   475         formula_vars (xs @ bounds) phi
   476       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   477       | formula_vars bounds (AAtom tm) = term_vars bounds tm
   478   in
   479     case formula_vars [] phi [] of [] => phi | xs => AQuant (AForall, xs, phi)
   480   end
   481 
   482 fun repair_formula thy explicit_forall full_types const_tab =
   483   let
   484     fun aux (AQuant (q, xs, phi)) = AQuant (q, xs, aux phi)
   485       | aux (AConn (c, phis)) = AConn (c, map aux phis)
   486       | aux (AAtom tm) =
   487         AAtom (tm |> repair_applications_in_term thy full_types const_tab
   488                   |> repair_predicates_in_term const_tab)
   489   in aux #> explicit_forall ? close_universally end
   490 
   491 fun repair_problem_line thy explicit_forall full_types const_tab
   492                         (Fof (ident, kind, phi)) =
   493   Fof (ident, kind, repair_formula thy explicit_forall full_types const_tab phi)
   494 fun repair_problem_with_const_table thy =
   495   map o apsnd o map ooo repair_problem_line thy
   496 
   497 fun repair_problem thy explicit_forall full_types explicit_apply problem =
   498   repair_problem_with_const_table thy explicit_forall full_types
   499       (const_table_for_problem explicit_apply problem) problem
   500 
   501 fun prepare_problem ctxt readable_names explicit_forall full_types
   502                     explicit_apply hyp_ts concl_t axiom_pairs =
   503   let
   504     val thy = ProofContext.theory_of ctxt
   505     val (axiom_names, (conjectures, axioms, helper_facts, class_rel_clauses,
   506                        arity_clauses)) =
   507       prepare_formulas ctxt full_types hyp_ts concl_t axiom_pairs
   508     val axiom_lines = map (problem_line_for_fact axiom_prefix full_types) axioms
   509     val helper_lines =
   510       map (problem_line_for_fact helper_prefix full_types) helper_facts
   511     val conjecture_lines =
   512       map (problem_line_for_conjecture full_types) conjectures
   513     val tfree_lines = problem_lines_for_free_types conjectures
   514     val class_rel_lines =
   515       map problem_line_for_class_rel_clause class_rel_clauses
   516     val arity_lines = map problem_line_for_arity_clause arity_clauses
   517     (* Reordering these might or might not confuse the proof reconstruction
   518        code or the SPASS Flotter hack. *)
   519     val problem =
   520       [("Relevant facts", axiom_lines),
   521        ("Class relationships", class_rel_lines),
   522        ("Arity declarations", arity_lines),
   523        ("Helper facts", helper_lines),
   524        ("Conjectures", conjecture_lines),
   525        ("Type variables", tfree_lines)]
   526       |> repair_problem thy explicit_forall full_types explicit_apply
   527     val (problem, pool) = nice_tptp_problem readable_names problem
   528     val conjecture_offset =
   529       length axiom_lines + length class_rel_lines + length arity_lines
   530       + length helper_lines
   531   in
   532     (problem,
   533      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
   534      conjecture_offset, axiom_names)
   535   end
   536 
   537 end;