src/HOL/Tools/ATP/atp_translate.ML

tuning

(*  Title:      HOL/Tools/ATP/atp_translate.ML
    Author:     Fabian Immler, TU Muenchen
    Author:     Makarius
    Author:     Jasmin Blanchette, TU Muenchen

Translation of HOL to FOL for Metis and Sledgehammer.
*)

signature ATP_TRANSLATE =
sig
  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
  type connective = ATP_Problem.connective
  type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
  type tptp_format = ATP_Problem.tptp_format
  type formula_kind = ATP_Problem.formula_kind
  type 'a problem = 'a ATP_Problem.problem

  datatype locality =
    General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained

  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
  datatype soundness = Sound_Modulo_Infiniteness | Sound
  datatype heaviness = Heavy | Ann_Light | Arg_Light
  datatype type_level =
    All_Types |
    Noninf_Nonmono_Types of soundness * heaviness |
    Fin_Nonmono_Types of heaviness |
    Const_Arg_Types |
    No_Types
  type type_enc

  val type_tag_idempotence : bool Config.T
  val type_tag_arguments : bool Config.T
  val no_lambdasN : string
  val concealedN : string
  val liftingN : string
  val combinatorsN : string
  val hybridN : string
  val lambdasN : string
  val smartN : string
  val schematic_var_prefix : string
  val fixed_var_prefix : string
  val tvar_prefix : string
  val tfree_prefix : string
  val const_prefix : string
  val type_const_prefix : string
  val class_prefix : string
  val polymorphic_free_prefix : string
  val skolem_const_prefix : string
  val old_skolem_const_prefix : string
  val new_skolem_const_prefix : string
  val type_decl_prefix : string
  val sym_decl_prefix : string
  val guards_sym_formula_prefix : string
  val tags_sym_formula_prefix : string
  val fact_prefix : string
  val conjecture_prefix : string
  val helper_prefix : string
  val class_rel_clause_prefix : string
  val arity_clause_prefix : string
  val tfree_clause_prefix : string
  val typed_helper_suffix : string
  val untyped_helper_suffix : string
  val type_tag_idempotence_helper_name : string
  val predicator_name : string
  val app_op_name : string
  val type_guard_name : string
  val type_tag_name : string
  val simple_type_prefix : string
  val prefixed_predicator_name : string
  val prefixed_app_op_name : string
  val prefixed_type_tag_name : string
  val ascii_of : string -> string
  val unascii_of : string -> string
  val strip_prefix_and_unascii : string -> string -> string option
  val proxy_table : (string * (string * (thm * (string * string)))) list
  val proxify_const : string -> (string * string) option
  val invert_const : string -> string
  val unproxify_const : string -> string
  val new_skolem_var_name_from_const : string -> string
  val atp_irrelevant_consts : string list
  val atp_schematic_consts_of : term -> typ list Symtab.table
  val is_type_enc_higher_order : type_enc -> bool
  val polymorphism_of_type_enc : type_enc -> polymorphism
  val level_of_type_enc : type_enc -> type_level
  val is_type_enc_quasi_sound : type_enc -> bool
  val is_type_enc_fairly_sound : type_enc -> bool
  val type_enc_from_string : soundness -> string -> type_enc
  val adjust_type_enc : tptp_format -> type_enc -> type_enc
  val mk_aconns :
    connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
  val unmangled_const : string -> string * (string, 'b) ho_term list
  val unmangled_const_name : string -> string
  val helper_table : ((string * bool) * thm list) list
  val factsN : string
  val prepare_atp_problem :
    Proof.context -> tptp_format -> formula_kind -> formula_kind -> type_enc
    -> bool -> string -> bool -> bool -> term list -> term
    -> ((string * locality) * term) list
    -> string problem * string Symtab.table * int * int
       * (string * locality) list vector * int list * int Symtab.table
  val atp_problem_weights : string problem -> (string * real) list
end;

structure ATP_Translate : ATP_TRANSLATE =
struct

open ATP_Util
open ATP_Problem

type name = string * string

val type_tag_idempotence =
  Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K false)
val type_tag_arguments =
  Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K false)

val no_lambdasN = "no_lambdas"
val concealedN = "concealed"
val liftingN = "lifting"
val combinatorsN = "combinators"
val hybridN = "hybrid"
val lambdasN = "lambdas"
val smartN = "smart"

val generate_info = false (* experimental *)

fun isabelle_info s =
  if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
  else NONE

val introN = "intro"
val elimN = "elim"
val simpN = "simp"

(* TFF1 is still in development, and it is still unclear whether symbols will be
   allowed to have types like "$tType > $o" (i.e., "![A : $tType] : $o"), with
   "dummy" type variables. *)
val avoid_first_order_dummy_type_vars = true

val bound_var_prefix = "B_"
val all_bound_var_prefix = "BA_"
val exist_bound_var_prefix = "BE_"
val schematic_var_prefix = "V_"
val fixed_var_prefix = "v_"
val tvar_prefix = "T_"
val tfree_prefix = "t_"
val const_prefix = "c_"
val type_const_prefix = "tc_"
val simple_type_prefix = "s_"
val class_prefix = "cl_"

val polymorphic_free_prefix = "poly_free"

val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
val old_skolem_const_prefix = skolem_const_prefix ^ "o"
val new_skolem_const_prefix = skolem_const_prefix ^ "n"

val type_decl_prefix = "ty_"
val sym_decl_prefix = "sy_"
val guards_sym_formula_prefix = "gsy_"
val tags_sym_formula_prefix = "tsy_"
val fact_prefix = "fact_"
val conjecture_prefix = "conj_"
val helper_prefix = "help_"
val class_rel_clause_prefix = "clar_"
val arity_clause_prefix = "arity_"
val tfree_clause_prefix = "tfree_"

val lambda_fact_prefix = "ATP.lambda_"
val typed_helper_suffix = "_T"
val untyped_helper_suffix = "_U"
val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"

val predicator_name = "pp"
val app_op_name = "aa"
val type_guard_name = "gg"
val type_tag_name = "tt"

val prefixed_predicator_name = const_prefix ^ predicator_name
val prefixed_app_op_name = const_prefix ^ app_op_name
val prefixed_type_tag_name = const_prefix ^ type_tag_name

(* Freshness almost guaranteed! *)
val atp_weak_prefix = "ATP:"

(*Escaping of special characters.
  Alphanumeric characters are left unchanged.
  The character _ goes to __
  Characters in the range ASCII space to / go to _A to _P, respectively.
  Other characters go to _nnn where nnn is the decimal ASCII code.*)
val upper_a_minus_space = Char.ord #"A" - Char.ord #" "

fun stringN_of_int 0 _ = ""
  | stringN_of_int k n =
    stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)

fun ascii_of_char c =
  if Char.isAlphaNum c then
    String.str c
  else if c = #"_" then
    "__"
  else if #" " <= c andalso c <= #"/" then
    "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
  else
    (* fixed width, in case more digits follow *)
    "_" ^ stringN_of_int 3 (Char.ord c)

val ascii_of = String.translate ascii_of_char

(** Remove ASCII armoring from names in proof files **)

(* We don't raise error exceptions because this code can run inside a worker
   thread. Also, the errors are impossible. *)
val unascii_of =
  let
    fun un rcs [] = String.implode(rev rcs)
      | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
        (* Three types of _ escapes: __, _A to _P, _nnn *)
      | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
      | un rcs (#"_" :: c :: cs) =
        if #"A" <= c andalso c<= #"P" then
          (* translation of #" " to #"/" *)
          un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
        else
          let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
            case Int.fromString (String.implode digits) of
              SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
            | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
          end
      | un rcs (c :: cs) = un (c :: rcs) cs
  in un [] o String.explode end

(* If string s has the prefix s1, return the result of deleting it,
   un-ASCII'd. *)
fun strip_prefix_and_unascii s1 s =
  if String.isPrefix s1 s then
    SOME (unascii_of (String.extract (s, size s1, NONE)))
  else
    NONE

val proxy_table =
  [("c_False", (@{const_name False}, (@{thm fFalse_def},
       ("fFalse", @{const_name ATP.fFalse})))),
   ("c_True", (@{const_name True}, (@{thm fTrue_def},
       ("fTrue", @{const_name ATP.fTrue})))),
   ("c_Not", (@{const_name Not}, (@{thm fNot_def},
       ("fNot", @{const_name ATP.fNot})))),
   ("c_conj", (@{const_name conj}, (@{thm fconj_def},
       ("fconj", @{const_name ATP.fconj})))),
   ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
       ("fdisj", @{const_name ATP.fdisj})))),
   ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
       ("fimplies", @{const_name ATP.fimplies})))),
   ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
       ("fequal", @{const_name ATP.fequal})))),
   ("c_All", (@{const_name All}, (@{thm fAll_def},
       ("fAll", @{const_name ATP.fAll})))),
   ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
       ("fEx", @{const_name ATP.fEx}))))]

val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)

(* Readable names for the more common symbolic functions. Do not mess with the
   table unless you know what you are doing. *)
val const_trans_table =
  [(@{type_name Product_Type.prod}, "prod"),
   (@{type_name Sum_Type.sum}, "sum"),
   (@{const_name False}, "False"),
   (@{const_name True}, "True"),
   (@{const_name Not}, "Not"),
   (@{const_name conj}, "conj"),
   (@{const_name disj}, "disj"),
   (@{const_name implies}, "implies"),
   (@{const_name HOL.eq}, "equal"),
   (@{const_name All}, "All"),
   (@{const_name Ex}, "Ex"),
   (@{const_name If}, "If"),
   (@{const_name Set.member}, "member"),
   (@{const_name Meson.COMBI}, "COMBI"),
   (@{const_name Meson.COMBK}, "COMBK"),
   (@{const_name Meson.COMBB}, "COMBB"),
   (@{const_name Meson.COMBC}, "COMBC"),
   (@{const_name Meson.COMBS}, "COMBS")]
  |> Symtab.make
  |> fold (Symtab.update o swap o snd o snd o snd) proxy_table

(* Invert the table of translations between Isabelle and ATPs. *)
val const_trans_table_inv =
  const_trans_table |> Symtab.dest |> map swap |> Symtab.make
val const_trans_table_unprox =
  Symtab.empty
  |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table

val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)

fun lookup_const c =
  case Symtab.lookup const_trans_table c of
    SOME c' => c'
  | NONE => ascii_of c

fun ascii_of_indexname (v, 0) = ascii_of v
  | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i

fun make_bound_var x = bound_var_prefix ^ ascii_of x
fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
fun make_fixed_var x = fixed_var_prefix ^ ascii_of x

fun make_schematic_type_var (x, i) =
  tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))

(* "HOL.eq" and Choice are mapped to the ATP's equivalents *)
local
  val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
  fun default c = const_prefix ^ lookup_const c
in
  fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
    | make_fixed_const (SOME (THF (_, _, THF_With_Choice))) c =
      if c = choice_const then tptp_choice else default c
    | make_fixed_const _ c = default c
end

fun make_fixed_type_const c = type_const_prefix ^ lookup_const c

fun make_type_class clas = class_prefix ^ ascii_of clas

fun new_skolem_var_name_from_const s =
  let val ss = s |> space_explode Long_Name.separator in
    nth ss (length ss - 2)
  end

(* These are either simplified away by "Meson.presimplify" (most of the time) or
   handled specially via "fFalse", "fTrue", ..., "fequal". *)
val atp_irrelevant_consts =
  [@{const_name False}, @{const_name True}, @{const_name Not},
   @{const_name conj}, @{const_name disj}, @{const_name implies},
   @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]

val atp_monomorph_bad_consts =
  atp_irrelevant_consts @
  (* These are ignored anyway by the relevance filter (unless they appear in
     higher-order places) but not by the monomorphizer. *)
  [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
   @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]

fun add_schematic_const (x as (_, T)) =
  Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
val add_schematic_consts_of =
  Term.fold_aterms (fn Const (x as (s, _)) =>
                       not (member (op =) atp_monomorph_bad_consts s)
                       ? add_schematic_const x
                      | _ => I)
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty

(** Definitions and functions for FOL clauses and formulas for TPTP **)

(** Isabelle arities **)

type arity_atom = name * name * name list

val type_class = the_single @{sort type}

type arity_clause =
  {name : string,
   prem_atoms : arity_atom list,
   concl_atom : arity_atom}

fun add_prem_atom tvar =
  fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))

(* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
fun make_axiom_arity_clause (tcons, name, (cls, args)) =
  let
    val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
    val tvars_srts = ListPair.zip (tvars, args)
  in
    {name = name,
     prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
     concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
                   tvars ~~ tvars)}
  end

fun arity_clause _ _ (_, []) = []
  | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
    arity_clause seen n (tcons, ars)
  | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
    if member (op =) seen class then
      (* multiple arities for the same (tycon, class) pair *)
      make_axiom_arity_clause (tcons,
          lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
          ar) ::
      arity_clause seen (n + 1) (tcons, ars)
    else
      make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
                               ascii_of class, ar) ::
      arity_clause (class :: seen) n (tcons, ars)

fun multi_arity_clause [] = []
  | multi_arity_clause ((tcons, ars) :: tc_arlists) =
    arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists

(* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
   theory thy provided its arguments have the corresponding sorts. *)
fun type_class_pairs thy tycons classes =
  let
    val alg = Sign.classes_of thy
    fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
    fun add_class tycon class =
      cons (class, domain_sorts tycon class)
      handle Sorts.CLASS_ERROR _ => I
    fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
  in map try_classes tycons end

(*Proving one (tycon, class) membership may require proving others, so iterate.*)
fun iter_type_class_pairs _ _ [] = ([], [])
  | iter_type_class_pairs thy tycons classes =
      let
        fun maybe_insert_class s =
          (s <> type_class andalso not (member (op =) classes s))
          ? insert (op =) s
        val cpairs = type_class_pairs thy tycons classes
        val newclasses =
          [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
        val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
      in (classes' @ classes, union (op =) cpairs' cpairs) end

fun make_arity_clauses thy tycons =
  iter_type_class_pairs thy tycons ##> multi_arity_clause


(** Isabelle class relations **)

type class_rel_clause =
  {name : string,
   subclass : name,
   superclass : name}

(* Generate all pairs (sub, super) such that sub is a proper subclass of super
   in theory "thy". *)
fun class_pairs _ [] _ = []
  | class_pairs thy subs supers =
      let
        val class_less = Sorts.class_less (Sign.classes_of thy)
        fun add_super sub super = class_less (sub, super) ? cons (sub, super)
        fun add_supers sub = fold (add_super sub) supers
      in fold add_supers subs [] end

fun make_class_rel_clause (sub, super) =
  {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
   superclass = `make_type_class super}

fun make_class_rel_clauses thy subs supers =
  map make_class_rel_clause (class_pairs thy subs supers)

(* intermediate terms *)
datatype iterm =
  IConst of name * typ * typ list |
  IVar of name * typ |
  IApp of iterm * iterm |
  IAbs of (name * typ) * iterm

fun ityp_of (IConst (_, T, _)) = T
  | ityp_of (IVar (_, T)) = T
  | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
  | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm

(*gets the head of a combinator application, along with the list of arguments*)
fun strip_iterm_comb u =
  let
    fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
      | stripc x = x
  in stripc (u, []) end

fun atyps_of T = fold_atyps (insert (op =)) T []

fun new_skolem_const_name s num_T_args =
  [new_skolem_const_prefix, s, string_of_int num_T_args]
  |> space_implode Long_Name.separator

fun robust_const_type thy s =
  if s = app_op_name then Logic.varifyT_global @{typ "('a => 'b) => 'a => 'b"}
  else s |> Sign.the_const_type thy

(* This function only makes sense if "T" is as general as possible. *)
fun robust_const_typargs thy (s, T) =
  (s, T) |> Sign.const_typargs thy
  handle TYPE _ => [] |> Term.add_tvarsT T |> rev |> map TVar

(* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
   Also accumulates sort infomation. *)
fun iterm_from_term thy format bs (P $ Q) =
    let
      val (P', P_atomics_Ts) = iterm_from_term thy format bs P
      val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
    in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
  | iterm_from_term thy format _ (Const (c, T)) =
    (IConst (`(make_fixed_const (SOME format)) c, T,
             robust_const_typargs thy (c, T)),
     atyps_of T)
  | iterm_from_term _ _ _ (Free (s, T)) =
    (IConst (`make_fixed_var s, T,
             if String.isPrefix polymorphic_free_prefix s then [T] else []),
     atyps_of T)
  | iterm_from_term _ format _ (Var (v as (s, _), T)) =
    (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
       let
         val Ts = T |> strip_type |> swap |> op ::
         val s' = new_skolem_const_name s (length Ts)
       in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
     else
       IVar ((make_schematic_var v, s), T), atyps_of T)
  | iterm_from_term _ _ bs (Bound j) =
    nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
  | iterm_from_term thy format bs (Abs (s, T, t)) =
    let
      fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
      val s = vary s
      val name = `make_bound_var s
      val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
    in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end

datatype locality =
  General | Helper | Induction | Intro | Elim | Simp | Local | Assum | Chained

datatype order = First_Order | Higher_Order
datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
datatype soundness = Sound_Modulo_Infiniteness | Sound
datatype heaviness = Heavy | Ann_Light | Arg_Light
datatype type_level =
  All_Types |
  Noninf_Nonmono_Types of soundness * heaviness |
  Fin_Nonmono_Types of heaviness |
  Const_Arg_Types |
  No_Types

datatype type_enc =
  Simple_Types of order * polymorphism * type_level |
  Guards of polymorphism * type_level |
  Tags of polymorphism * type_level

fun is_type_enc_higher_order (Simple_Types (Higher_Order, _, _)) = true
  | is_type_enc_higher_order _ = false

fun polymorphism_of_type_enc (Simple_Types (_, poly, _)) = poly
  | polymorphism_of_type_enc (Guards (poly, _)) = poly
  | polymorphism_of_type_enc (Tags (poly, _)) = poly

fun level_of_type_enc (Simple_Types (_, _, level)) = level
  | level_of_type_enc (Guards (_, level)) = level
  | level_of_type_enc (Tags (_, level)) = level

fun heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
  | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
  | heaviness_of_level _ = Heavy

fun is_type_level_quasi_sound All_Types = true
  | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
  | is_type_level_quasi_sound _ = false
val is_type_enc_quasi_sound = is_type_level_quasi_sound o level_of_type_enc

fun is_type_level_fairly_sound (Fin_Nonmono_Types _) = true
  | is_type_level_fairly_sound level = is_type_level_quasi_sound level
val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc

fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
  | is_type_level_monotonicity_based (Fin_Nonmono_Types _) = true
  | is_type_level_monotonicity_based _ = false

fun try_unsuffixes ss s =
  fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE

val queries = ["?", "_query"]
val bangs = ["!", "_bang"]

fun type_enc_from_string soundness s =
  (case try (unprefix "poly_") s of
     SOME s => (SOME Polymorphic, s)
   | NONE =>
     case try (unprefix "raw_mono_") s of
       SOME s => (SOME Raw_Monomorphic, s)
     | NONE =>
       case try (unprefix "mono_") s of
         SOME s => (SOME Mangled_Monomorphic, s)
       | NONE => (NONE, s))
  ||> (fn s =>
          (* "_query" and "_bang" are for the ASCII-challenged Metis and
             Mirabelle. *)
          case try_unsuffixes queries s of
            SOME s =>
            (case try_unsuffixes queries s of
               SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s)
             | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s))
          | NONE =>
            case try_unsuffixes bangs s of
              SOME s =>
              (case try_unsuffixes bangs s of
                 SOME s => (Fin_Nonmono_Types Ann_Light, s)
               | NONE => (Fin_Nonmono_Types Heavy, s))
            | NONE => (All_Types, s))
  |> (fn (poly, (level, core)) =>
         case (core, (poly, level)) of
           ("simple", (SOME poly, _)) =>
           (case (poly, level) of
              (Polymorphic, All_Types) =>
              Simple_Types (First_Order, Polymorphic, All_Types)
            | (Mangled_Monomorphic, _) =>
              if heaviness_of_level level = Heavy then
                Simple_Types (First_Order, Mangled_Monomorphic, level)
              else
                raise Same.SAME
            | _ => raise Same.SAME)
         | ("simple_higher", (SOME poly, _)) =>
           (case (poly, level) of
              (Polymorphic, All_Types) =>
              Simple_Types (Higher_Order, Polymorphic, All_Types)
            | (_, Noninf_Nonmono_Types _) => raise Same.SAME
            | (Mangled_Monomorphic, _) =>
              if heaviness_of_level level = Heavy then
                Simple_Types (Higher_Order, Mangled_Monomorphic, level)
              else
                raise Same.SAME
            | _ => raise Same.SAME)
         | ("guards", (SOME poly, _)) => Guards (poly, level)
         | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
         | ("tags", (SOME poly, _)) => Tags (poly, level)
         | ("args", (SOME poly, All_Types (* naja *))) =>
           Guards (poly, Const_Arg_Types)
         | ("erased", (NONE, All_Types (* naja *))) =>
           Guards (Polymorphic, No_Types)
         | _ => raise Same.SAME)
  handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")

fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
                    (Simple_Types (order, _, level)) =
    Simple_Types (order, Mangled_Monomorphic, level)
  | adjust_type_enc (THF _) type_enc = type_enc
  | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
    Simple_Types (First_Order, Mangled_Monomorphic, level)
  | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
    Simple_Types (First_Order, poly, level)
  | adjust_type_enc format (Simple_Types (_, poly, level)) =
    adjust_type_enc format (Guards (poly, level))
  | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
    (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
  | adjust_type_enc _ type_enc = type_enc

fun lift_lambdas ctxt type_enc =
  map (close_form o Envir.eta_contract) #> rpair ctxt
  #-> Lambda_Lifting.lift_lambdas
          (if polymorphism_of_type_enc type_enc = Polymorphic then
             SOME polymorphic_free_prefix
           else
             NONE)
          Lambda_Lifting.is_quantifier
  #> fst

fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
    intentionalize_def t
  | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
    let
      fun lam T t = Abs (Name.uu, T, t)
      val (head, args) = strip_comb t ||> rev
      val head_T = fastype_of head
      val n = length args
      val arg_Ts = head_T |> binder_types |> take n |> rev
      val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
    in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
  | intentionalize_def t = t

type translated_formula =
  {name : string,
   locality : locality,
   kind : formula_kind,
   iformula : (name, typ, iterm) formula,
   atomic_types : typ list}

fun update_iformula f ({name, locality, kind, iformula, atomic_types}
                       : translated_formula) =
  {name = name, locality = locality, kind = kind, iformula = f iformula,
   atomic_types = atomic_types} : translated_formula

fun fact_lift f ({iformula, ...} : translated_formula) = f iformula

fun insert_type ctxt get_T x xs =
  let val T = get_T x in
    if exists (type_instance ctxt T o get_T) xs then xs
    else x :: filter_out (type_generalization ctxt T o get_T) xs
  end

(* The Booleans indicate whether all type arguments should be kept. *)
datatype type_arg_policy =
  Explicit_Type_Args of bool |
  Mangled_Type_Args |
  No_Type_Args

fun should_drop_arg_type_args (Simple_Types _) = false
  | should_drop_arg_type_args type_enc =
    level_of_type_enc type_enc = All_Types

fun type_arg_policy type_enc s =
  let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
    if s = type_tag_name then
      if mangled then Mangled_Type_Args else Explicit_Type_Args false
    else case type_enc of
      Tags (_, All_Types) => No_Type_Args
    | _ =>
      let val level = level_of_type_enc type_enc in
        if level = No_Types orelse s = @{const_name HOL.eq} orelse
           (s = app_op_name andalso level = Const_Arg_Types) then
          No_Type_Args
        else if mangled then
          Mangled_Type_Args
        else
          Explicit_Type_Args (should_drop_arg_type_args type_enc)
      end
  end

(* Make atoms for sorted type variables. *)
fun generic_add_sorts_on_type (_, []) = I
  | generic_add_sorts_on_type ((x, i), s :: ss) =
    generic_add_sorts_on_type ((x, i), ss)
    #> (if s = the_single @{sort HOL.type} then
          I
        else if i = ~1 then
          insert (op =) (`make_type_class s, `make_fixed_type_var x)
        else
          insert (op =) (`make_type_class s,
                         (make_schematic_type_var (x, i), x)))
fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
  | add_sorts_on_tfree _ = I
fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
  | add_sorts_on_tvar _ = I

val tvar_a_str = "'a"
val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
val itself_name = `make_fixed_type_const @{type_name itself}
val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
val tvar_a_atype = AType (tvar_a_name, [])
val a_itself_atype = AType (itself_name, [tvar_a_atype])

fun type_class_formula type_enc class arg =
  AAtom (ATerm (class, arg ::
      (case type_enc of
         Simple_Types (First_Order, Polymorphic, _) =>
         if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
         else []
       | _ => [])))
fun formulas_for_types type_enc add_sorts_on_typ Ts =
  [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
     |> map (fn (class, name) =>
                type_class_formula type_enc class (ATerm (name, [])))

fun mk_aconns c phis =
  let val (phis', phi') = split_last phis in
    fold_rev (mk_aconn c) phis' phi'
  end
fun mk_ahorn [] phi = phi
  | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
fun mk_aquant _ [] phi = phi
  | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
    if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
  | mk_aquant q xs phi = AQuant (q, xs, phi)

fun close_universally atom_vars phi =
  let
    fun formula_vars bounds (AQuant (_, xs, phi)) =
        formula_vars (map fst xs @ bounds) phi
      | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
      | formula_vars bounds (AAtom tm) =
        union (op =) (atom_vars tm []
                      |> filter_out (member (op =) bounds o fst))
  in mk_aquant AForall (formula_vars [] phi []) phi end

fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
  | iterm_vars (IConst _) = I
  | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
  | iterm_vars (IAbs (_, tm)) = iterm_vars tm
fun close_iformula_universally phi = close_universally iterm_vars phi

fun term_vars type_enc =
  let
    fun vars bounds (ATerm (name as (s, _), tms)) =
        (if is_tptp_variable s andalso not (member (op =) bounds name) then
           (case type_enc of
              Simple_Types (_, Polymorphic, _) =>
              if String.isPrefix tvar_prefix s then SOME atype_of_types
              else NONE
            | _ => NONE)
           |> pair name |> insert (op =)
         else
           I)
        #> fold (vars bounds) tms
      | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm
  in vars end
fun close_formula_universally type_enc =
  close_universally (term_vars type_enc [])

val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
val fused_infinite_type = Type (fused_infinite_type_name, [])

fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)

fun ho_term_from_typ format type_enc =
  let
    fun term (Type (s, Ts)) =
      ATerm (case (is_type_enc_higher_order type_enc, s) of
               (true, @{type_name bool}) => `I tptp_bool_type
             | (true, @{type_name fun}) => `I tptp_fun_type
             | _ => if s = fused_infinite_type_name andalso
                       is_format_typed format then
                      `I tptp_individual_type
                    else
                      `make_fixed_type_const s,
             map term Ts)
    | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
    | term (TVar (x, _)) = ATerm (tvar_name x, [])
  in term end

fun ho_term_for_type_arg format type_enc T =
  if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)

(* This shouldn't clash with anything else. *)
val mangled_type_sep = "\000"

fun generic_mangled_type_name f (ATerm (name, [])) = f name
  | generic_mangled_type_name f (ATerm (name, tys)) =
    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
    ^ ")"
  | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"

fun mangled_type format type_enc =
  generic_mangled_type_name fst o ho_term_from_typ format type_enc

fun make_simple_type s =
  if s = tptp_bool_type orelse s = tptp_fun_type orelse
     s = tptp_individual_type then
    s
  else
    simple_type_prefix ^ ascii_of s

fun ho_type_from_ho_term type_enc pred_sym ary =
  let
    fun to_mangled_atype ty =
      AType ((make_simple_type (generic_mangled_type_name fst ty),
              generic_mangled_type_name snd ty), [])
    fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
      | to_poly_atype _ = raise Fail "unexpected type abstraction"
    val to_atype =
      if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
      else to_mangled_atype
    fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
    fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
      | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
      | to_fo _ _ = raise Fail "unexpected type abstraction"
    fun to_ho (ty as ATerm ((s, _), tys)) =
        if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
      | to_ho _ = raise Fail "unexpected type abstraction"
  in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end

fun ho_type_from_typ format type_enc pred_sym ary =
  ho_type_from_ho_term type_enc pred_sym ary
  o ho_term_from_typ format type_enc

fun mangled_const_name format type_enc T_args (s, s') =
  let
    val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
    fun type_suffix f g =
      fold_rev (curry (op ^) o g o prefix mangled_type_sep
                o generic_mangled_type_name f) ty_args ""
  in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end

val parse_mangled_ident =
  Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode

fun parse_mangled_type x =
  (parse_mangled_ident
   -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
                    [] >> ATerm) x
and parse_mangled_types x =
  (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x

fun unmangled_type s =
  s |> suffix ")" |> raw_explode
    |> Scan.finite Symbol.stopper
           (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
                                                quote s)) parse_mangled_type))
    |> fst

val unmangled_const_name = space_explode mangled_type_sep #> hd
fun unmangled_const s =
  let val ss = space_explode mangled_type_sep s in
    (hd ss, map unmangled_type (tl ss))
  end

fun introduce_proxies_in_iterm type_enc =
  let
    fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
      | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
                       _ =
        (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
           limitation. This works in conjuction with special code in
           "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
           possible. *)
        IAbs ((`I "P", p_T),
              IApp (IConst (`I ho_quant, T, []),
                    IAbs ((`I "X", x_T),
                          IApp (IConst (`I "P", p_T, []),
                                IConst (`I "X", x_T, [])))))
      | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
    fun intro top_level args (IApp (tm1, tm2)) =
        IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
      | intro top_level args (IConst (name as (s, _), T, T_args)) =
        (case proxify_const s of
           SOME proxy_base =>
           if top_level orelse is_type_enc_higher_order type_enc then
             case (top_level, s) of
               (_, "c_False") => IConst (`I tptp_false, T, [])
             | (_, "c_True") => IConst (`I tptp_true, T, [])
             | (false, "c_Not") => IConst (`I tptp_not, T, [])
             | (false, "c_conj") => IConst (`I tptp_and, T, [])
             | (false, "c_disj") => IConst (`I tptp_or, T, [])
             | (false, "c_implies") => IConst (`I tptp_implies, T, [])
             | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
             | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
             | (false, s) =>
               if is_tptp_equal s andalso length args = 2 then
                 IConst (`I tptp_equal, T, [])
               else
                 (* Use a proxy even for partially applied THF0 equality,
                    because the LEO-II and Satallax parsers complain about not
                    being able to infer the type of "=". *)
                 IConst (proxy_base |>> prefix const_prefix, T, T_args)
             | _ => IConst (name, T, [])
           else
             IConst (proxy_base |>> prefix const_prefix, T, T_args)
          | NONE => if s = tptp_choice then
                      tweak_ho_quant tptp_choice T args
                    else
                      IConst (name, T, T_args))
      | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
      | intro _ _ tm = tm
  in intro true [] end

fun mangle_type_args_in_iterm format type_enc =
  if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
    let
      fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
        | mangle (tm as IConst (_, _, [])) = tm
        | mangle (tm as IConst (name as (s, _), T, T_args)) =
          (case strip_prefix_and_unascii const_prefix s of
             NONE => tm
           | SOME s'' =>
             case type_arg_policy type_enc (invert_const s'') of
               Mangled_Type_Args =>
               IConst (mangled_const_name format type_enc T_args name, T, [])
             | _ => tm)
        | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
        | mangle tm = tm
    in mangle end
  else
    I

fun chop_fun 0 T = ([], T)
  | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
    chop_fun (n - 1) ran_T |>> cons dom_T
  | chop_fun _ T = ([], T)

fun filter_const_type_args _ _ _ [] = []
  | filter_const_type_args thy s ary T_args =
    let
      val U = robust_const_type thy s
      val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
      val U_args = (s, U) |> robust_const_typargs thy
    in
      U_args ~~ T_args
      |> map (fn (U, T) =>
                 if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
    end
    handle TYPE _ => T_args

fun filter_type_args_in_iterm thy type_enc =
  let
    fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
      | filt _ (tm as IConst (_, _, [])) = tm
      | filt ary (IConst (name as (s, _), T, T_args)) =
        (case strip_prefix_and_unascii const_prefix s of
           NONE =>
           (name,
            if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
              []
            else
              T_args)
         | SOME s'' =>
           let
             val s'' = invert_const s''
             fun filter_T_args false = T_args
               | filter_T_args true = filter_const_type_args thy s'' ary T_args
           in
             case type_arg_policy type_enc s'' of
               Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
             | No_Type_Args => (name, [])
             | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
           end)
        |> (fn (name, T_args) => IConst (name, T, T_args))
      | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
      | filt _ tm = tm
  in filt 0 end

fun iformula_from_prop ctxt format type_enc eq_as_iff =
  let
    val thy = Proof_Context.theory_of ctxt
    fun do_term bs t atomic_types =
      iterm_from_term thy format bs (Envir.eta_contract t)
      |>> (introduce_proxies_in_iterm type_enc
           #> mangle_type_args_in_iterm format type_enc
           #> AAtom)
      ||> union (op =) atomic_types
    fun do_quant bs q pos s T t' =
      let
        val s = singleton (Name.variant_list (map fst bs)) s
        val universal = Option.map (q = AExists ? not) pos
        val name =
          s |> `(case universal of
                   SOME true => make_all_bound_var
                 | SOME false => make_exist_bound_var
                 | NONE => make_bound_var)
      in
        do_formula ((s, (name, T)) :: bs) pos t'
        #>> mk_aquant q [(name, SOME T)]
      end
    and do_conn bs c pos1 t1 pos2 t2 =
      do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
    and do_formula bs pos t =
      case t of
        @{const Trueprop} $ t1 => do_formula bs pos t1
      | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
      | Const (@{const_name All}, _) $ Abs (s, T, t') =>
        do_quant bs AForall pos s T t'
      | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
        do_quant bs AExists pos s T t'
      | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
      | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
      | @{const HOL.implies} $ t1 $ t2 =>
        do_conn bs AImplies (Option.map not pos) t1 pos t2
      | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
        if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
      | _ => do_term bs t
  in do_formula [] end

fun presimplify_term _ [] t = t
  | presimplify_term ctxt presimp_consts t =
    t |> exists_Const (member (op =) presimp_consts o fst) t
         ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
            #> Meson.presimplify ctxt
            #> prop_of)

fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
fun conceal_bounds Ts t =
  subst_bounds (map (Free o apfst concealed_bound_name)
                    (0 upto length Ts - 1 ~~ Ts), t)
fun reveal_bounds Ts =
  subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
                    (0 upto length Ts - 1 ~~ Ts))

fun is_fun_equality (@{const_name HOL.eq},
                     Type (_, [Type (@{type_name fun}, _), _])) = true
  | is_fun_equality _ = false

fun extensionalize_term ctxt t =
  if exists_Const is_fun_equality t then
    let val thy = Proof_Context.theory_of ctxt in
      t |> cterm_of thy |> Meson.extensionalize_conv ctxt
        |> prop_of |> Logic.dest_equals |> snd
    end
  else
    t

fun simple_translate_lambdas do_lambdas ctxt t =
  let val thy = Proof_Context.theory_of ctxt in
    if Meson.is_fol_term thy t then
      t
    else
      let
        fun aux Ts t =
          case t of
            @{const Not} $ t1 => @{const Not} $ aux Ts t1
          | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
            t0 $ Abs (s, T, aux (T :: Ts) t')
          | (t0 as Const (@{const_name All}, _)) $ t1 =>
            aux Ts (t0 $ eta_expand Ts t1 1)
          | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
            t0 $ Abs (s, T, aux (T :: Ts) t')
          | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
            aux Ts (t0 $ eta_expand Ts t1 1)
          | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
          | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
          | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
          | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
              $ t1 $ t2 =>
            t0 $ aux Ts t1 $ aux Ts t2
          | _ =>
            if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
            else t |> Envir.eta_contract |> do_lambdas ctxt Ts
        val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
      in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
  end

fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
    do_cheaply_conceal_lambdas Ts t1
    $ do_cheaply_conceal_lambdas Ts t2
  | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
    Free (polymorphic_free_prefix ^ serial_string (),
          T --> fastype_of1 (T :: Ts, t))
  | do_cheaply_conceal_lambdas _ t = t

fun do_introduce_combinators ctxt Ts t =
  let val thy = Proof_Context.theory_of ctxt in
    t |> conceal_bounds Ts
      |> cterm_of thy
      |> Meson_Clausify.introduce_combinators_in_cterm
      |> prop_of |> Logic.dest_equals |> snd
      |> reveal_bounds Ts
  end
  (* A type variable of sort "{}" will make abstraction fail. *)
  handle THM _ => t |> do_cheaply_conceal_lambdas Ts
val introduce_combinators = simple_translate_lambdas do_introduce_combinators

fun preprocess_abstractions_in_terms trans_lambdas facts =
  let
    val (facts, lambda_ts) =
      facts |> map (snd o snd) |> trans_lambdas
            |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
    val lambda_facts =
      map2 (fn t => fn j =>
               ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
           lambda_ts (1 upto length lambda_ts)
  in (facts, lambda_facts) end

(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
fun freeze_term t =
  let
    fun aux (t $ u) = aux t $ aux u
      | aux (Abs (s, T, t)) = Abs (s, T, aux t)
      | aux (Var ((s, i), T)) =
        Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
      | aux t = t
  in t |> exists_subterm is_Var t ? aux end

fun presimp_prop ctxt presimp_consts t =
  let
    val thy = Proof_Context.theory_of ctxt
    val t = t |> Envir.beta_eta_contract
              |> transform_elim_prop
              |> Object_Logic.atomize_term thy
    val need_trueprop = (fastype_of t = @{typ bool})
  in
    t |> need_trueprop ? HOLogic.mk_Trueprop