src/HOL/Tools/ATP/atp_translate.ML
author blanchet
Thu Aug 25 23:38:09 2011 +0200 (2011-08-25)
changeset 44501 5bde887b4785
parent 44500 dbd98b549597
child 44502 c537d5e5a365
permissions -rw-r--r--
make polymorphic encodings more complete
     1 (*  Title:      HOL/Tools/ATP/atp_translate.ML
     2     Author:     Fabian Immler, TU Muenchen
     3     Author:     Makarius
     4     Author:     Jasmin Blanchette, TU Muenchen
     5 
     6 Translation of HOL to FOL for Metis and Sledgehammer.
     7 *)
     8 
     9 signature ATP_TRANSLATE =
    10 sig
    11   type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
    12   type connective = ATP_Problem.connective
    13   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    14   type format = ATP_Problem.format
    15   type formula_kind = ATP_Problem.formula_kind
    16   type 'a problem = 'a ATP_Problem.problem
    17 
    18   datatype locality =
    19     General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
    20     Chained
    21 
    22   datatype order = First_Order | Higher_Order
    23   datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    24   datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    25   datatype type_level =
    26     All_Types |
    27     Noninf_Nonmono_Types of soundness |
    28     Fin_Nonmono_Types |
    29     Const_Arg_Types |
    30     No_Types
    31   datatype type_uniformity = Uniform | Nonuniform
    32 
    33   datatype type_enc =
    34     Simple_Types of order * type_level |
    35     Guards of polymorphism * type_level * type_uniformity |
    36     Tags of polymorphism * type_level * type_uniformity
    37 
    38   val type_tag_idempotence : bool Config.T
    39   val type_tag_arguments : bool Config.T
    40   val no_lambdasN : string
    41   val concealedN : string
    42   val liftingN : string
    43   val combinatorsN : string
    44   val hybridN : string
    45   val lambdasN : string
    46   val smartN : string
    47   val schematic_var_prefix : string
    48   val fixed_var_prefix : string
    49   val tvar_prefix : string
    50   val tfree_prefix : string
    51   val const_prefix : string
    52   val type_const_prefix : string
    53   val class_prefix : string
    54   val polymorphic_free_prefix : string
    55   val skolem_const_prefix : string
    56   val old_skolem_const_prefix : string
    57   val new_skolem_const_prefix : string
    58   val type_decl_prefix : string
    59   val sym_decl_prefix : string
    60   val guards_sym_formula_prefix : string
    61   val tags_sym_formula_prefix : string
    62   val fact_prefix : string
    63   val conjecture_prefix : string
    64   val helper_prefix : string
    65   val class_rel_clause_prefix : string
    66   val arity_clause_prefix : string
    67   val tfree_clause_prefix : string
    68   val typed_helper_suffix : string
    69   val untyped_helper_suffix : string
    70   val type_tag_idempotence_helper_name : string
    71   val predicator_name : string
    72   val app_op_name : string
    73   val type_guard_name : string
    74   val type_tag_name : string
    75   val simple_type_prefix : string
    76   val prefixed_predicator_name : string
    77   val prefixed_app_op_name : string
    78   val prefixed_type_tag_name : string
    79   val ascii_of : string -> string
    80   val unascii_of : string -> string
    81   val strip_prefix_and_unascii : string -> string -> string option
    82   val proxy_table : (string * (string * (thm * (string * string)))) list
    83   val proxify_const : string -> (string * string) option
    84   val invert_const : string -> string
    85   val unproxify_const : string -> string
    86   val new_skolem_var_name_from_const : string -> string
    87   val atp_irrelevant_consts : string list
    88   val atp_schematic_consts_of : term -> typ list Symtab.table
    89   val type_enc_from_string : soundness -> string -> type_enc
    90   val is_type_enc_higher_order : type_enc -> bool
    91   val polymorphism_of_type_enc : type_enc -> polymorphism
    92   val level_of_type_enc : type_enc -> type_level
    93   val is_type_enc_quasi_sound : type_enc -> bool
    94   val is_type_enc_fairly_sound : type_enc -> bool
    95   val adjust_type_enc : format -> type_enc -> type_enc
    96   val mk_aconns :
    97     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
    98   val unmangled_const : string -> string * (string, 'b) ho_term list
    99   val unmangled_const_name : string -> string
   100   val helper_table : ((string * bool) * thm list) list
   101   val factsN : string
   102   val prepare_atp_problem :
   103     Proof.context -> format -> formula_kind -> formula_kind -> type_enc
   104     -> bool -> string -> bool -> bool -> term list -> term
   105     -> ((string * locality) * term) list
   106     -> string problem * string Symtab.table * int * int
   107        * (string * locality) list vector * int list * int Symtab.table
   108   val atp_problem_weights : string problem -> (string * real) list
   109 end;
   110 
   111 structure ATP_Translate : ATP_TRANSLATE =
   112 struct
   113 
   114 open ATP_Util
   115 open ATP_Problem
   116 
   117 type name = string * string
   118 
   119 val type_tag_idempotence =
   120   Attrib.setup_config_bool @{binding atp_type_tag_idempotence} (K true)
   121 val type_tag_arguments =
   122   Attrib.setup_config_bool @{binding atp_type_tag_arguments} (K true)
   123 
   124 val no_lambdasN = "no_lambdas"
   125 val concealedN = "concealed"
   126 val liftingN = "lifting"
   127 val combinatorsN = "combinators"
   128 val hybridN = "hybrid"
   129 val lambdasN = "lambdas"
   130 val smartN = "smart"
   131 
   132 val generate_info = false (* experimental *)
   133 
   134 fun isabelle_info s =
   135   if generate_info then SOME (ATerm ("[]", [ATerm ("isabelle_" ^ s, [])]))
   136   else NONE
   137 
   138 val introN = "intro"
   139 val elimN = "elim"
   140 val simpN = "simp"
   141 
   142 val bound_var_prefix = "B_"
   143 val all_bound_var_prefix = "BA_"
   144 val exist_bound_var_prefix = "BE_"
   145 val schematic_var_prefix = "V_"
   146 val fixed_var_prefix = "v_"
   147 val tvar_prefix = "T_"
   148 val tfree_prefix = "t_"
   149 val const_prefix = "c_"
   150 val type_const_prefix = "tc_"
   151 val simple_type_prefix = "s_"
   152 val class_prefix = "cl_"
   153 
   154 val polymorphic_free_prefix = "poly_free"
   155 
   156 val skolem_const_prefix = "ATP" ^ Long_Name.separator ^ "Sko"
   157 val old_skolem_const_prefix = skolem_const_prefix ^ "o"
   158 val new_skolem_const_prefix = skolem_const_prefix ^ "n"
   159 
   160 val type_decl_prefix = "ty_"
   161 val sym_decl_prefix = "sy_"
   162 val guards_sym_formula_prefix = "gsy_"
   163 val tags_sym_formula_prefix = "tsy_"
   164 val fact_prefix = "fact_"
   165 val conjecture_prefix = "conj_"
   166 val helper_prefix = "help_"
   167 val class_rel_clause_prefix = "clar_"
   168 val arity_clause_prefix = "arity_"
   169 val tfree_clause_prefix = "tfree_"
   170 
   171 val lambda_fact_prefix = "ATP.lambda_"
   172 val typed_helper_suffix = "_T"
   173 val untyped_helper_suffix = "_U"
   174 val type_tag_idempotence_helper_name = helper_prefix ^ "ti_idem"
   175 
   176 val predicator_name = "pp"
   177 val app_op_name = "aa"
   178 val type_guard_name = "gg"
   179 val type_tag_name = "tt"
   180 
   181 val prefixed_predicator_name = const_prefix ^ predicator_name
   182 val prefixed_app_op_name = const_prefix ^ app_op_name
   183 val prefixed_type_tag_name = const_prefix ^ type_tag_name
   184 
   185 (* Freshness almost guaranteed! *)
   186 val atp_weak_prefix = "ATP:"
   187 
   188 (*Escaping of special characters.
   189   Alphanumeric characters are left unchanged.
   190   The character _ goes to __
   191   Characters in the range ASCII space to / go to _A to _P, respectively.
   192   Other characters go to _nnn where nnn is the decimal ASCII code.*)
   193 val upper_a_minus_space = Char.ord #"A" - Char.ord #" "
   194 
   195 fun stringN_of_int 0 _ = ""
   196   | stringN_of_int k n =
   197     stringN_of_int (k - 1) (n div 10) ^ string_of_int (n mod 10)
   198 
   199 fun ascii_of_char c =
   200   if Char.isAlphaNum c then
   201     String.str c
   202   else if c = #"_" then
   203     "__"
   204   else if #" " <= c andalso c <= #"/" then
   205     "_" ^ String.str (Char.chr (Char.ord c + upper_a_minus_space))
   206   else
   207     (* fixed width, in case more digits follow *)
   208     "_" ^ stringN_of_int 3 (Char.ord c)
   209 
   210 val ascii_of = String.translate ascii_of_char
   211 
   212 (** Remove ASCII armoring from names in proof files **)
   213 
   214 (* We don't raise error exceptions because this code can run inside a worker
   215    thread. Also, the errors are impossible. *)
   216 val unascii_of =
   217   let
   218     fun un rcs [] = String.implode(rev rcs)
   219       | un rcs [#"_"] = un (#"_" :: rcs) [] (* ERROR *)
   220         (* Three types of _ escapes: __, _A to _P, _nnn *)
   221       | un rcs (#"_" :: #"_" :: cs) = un (#"_" :: rcs) cs
   222       | un rcs (#"_" :: c :: cs) =
   223         if #"A" <= c andalso c<= #"P" then
   224           (* translation of #" " to #"/" *)
   225           un (Char.chr (Char.ord c - upper_a_minus_space) :: rcs) cs
   226         else
   227           let val digits = List.take (c :: cs, 3) handle General.Subscript => [] in
   228             case Int.fromString (String.implode digits) of
   229               SOME n => un (Char.chr n :: rcs) (List.drop (cs, 2))
   230             | NONE => un (c :: #"_" :: rcs) cs (* ERROR *)
   231           end
   232       | un rcs (c :: cs) = un (c :: rcs) cs
   233   in un [] o String.explode end
   234 
   235 (* If string s has the prefix s1, return the result of deleting it,
   236    un-ASCII'd. *)
   237 fun strip_prefix_and_unascii s1 s =
   238   if String.isPrefix s1 s then
   239     SOME (unascii_of (String.extract (s, size s1, NONE)))
   240   else
   241     NONE
   242 
   243 val proxy_table =
   244   [("c_False", (@{const_name False}, (@{thm fFalse_def},
   245        ("fFalse", @{const_name ATP.fFalse})))),
   246    ("c_True", (@{const_name True}, (@{thm fTrue_def},
   247        ("fTrue", @{const_name ATP.fTrue})))),
   248    ("c_Not", (@{const_name Not}, (@{thm fNot_def},
   249        ("fNot", @{const_name ATP.fNot})))),
   250    ("c_conj", (@{const_name conj}, (@{thm fconj_def},
   251        ("fconj", @{const_name ATP.fconj})))),
   252    ("c_disj", (@{const_name disj}, (@{thm fdisj_def},
   253        ("fdisj", @{const_name ATP.fdisj})))),
   254    ("c_implies", (@{const_name implies}, (@{thm fimplies_def},
   255        ("fimplies", @{const_name ATP.fimplies})))),
   256    ("equal", (@{const_name HOL.eq}, (@{thm fequal_def},
   257        ("fequal", @{const_name ATP.fequal})))),
   258    ("c_All", (@{const_name All}, (@{thm fAll_def},
   259        ("fAll", @{const_name ATP.fAll})))),
   260    ("c_Ex", (@{const_name Ex}, (@{thm fEx_def},
   261        ("fEx", @{const_name ATP.fEx}))))]
   262 
   263 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
   264 
   265 (* Readable names for the more common symbolic functions. Do not mess with the
   266    table unless you know what you are doing. *)
   267 val const_trans_table =
   268   [(@{type_name Product_Type.prod}, "prod"),
   269    (@{type_name Sum_Type.sum}, "sum"),
   270    (@{const_name False}, "False"),
   271    (@{const_name True}, "True"),
   272    (@{const_name Not}, "Not"),
   273    (@{const_name conj}, "conj"),
   274    (@{const_name disj}, "disj"),
   275    (@{const_name implies}, "implies"),
   276    (@{const_name HOL.eq}, "equal"),
   277    (@{const_name All}, "All"),
   278    (@{const_name Ex}, "Ex"),
   279    (@{const_name If}, "If"),
   280    (@{const_name Set.member}, "member"),
   281    (@{const_name Meson.COMBI}, "COMBI"),
   282    (@{const_name Meson.COMBK}, "COMBK"),
   283    (@{const_name Meson.COMBB}, "COMBB"),
   284    (@{const_name Meson.COMBC}, "COMBC"),
   285    (@{const_name Meson.COMBS}, "COMBS")]
   286   |> Symtab.make
   287   |> fold (Symtab.update o swap o snd o snd o snd) proxy_table
   288 
   289 (* Invert the table of translations between Isabelle and ATPs. *)
   290 val const_trans_table_inv =
   291   const_trans_table |> Symtab.dest |> map swap |> Symtab.make
   292 val const_trans_table_unprox =
   293   Symtab.empty
   294   |> fold (fn (_, (isa, (_, (_, atp)))) => Symtab.update (atp, isa)) proxy_table
   295 
   296 val invert_const = perhaps (Symtab.lookup const_trans_table_inv)
   297 val unproxify_const = perhaps (Symtab.lookup const_trans_table_unprox)
   298 
   299 fun lookup_const c =
   300   case Symtab.lookup const_trans_table c of
   301     SOME c' => c'
   302   | NONE => ascii_of c
   303 
   304 fun ascii_of_indexname (v, 0) = ascii_of v
   305   | ascii_of_indexname (v, i) = ascii_of v ^ "_" ^ string_of_int i
   306 
   307 fun make_bound_var x = bound_var_prefix ^ ascii_of x
   308 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
   309 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
   310 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
   311 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
   312 
   313 fun make_schematic_type_var (x, i) =
   314       tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
   315 fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
   316 
   317 (* "HOL.eq" is mapped to the ATP's equality. *)
   318 fun make_fixed_const _ @{const_name HOL.eq} = tptp_old_equal
   319   | make_fixed_const (SOME (THF With_Choice)) "Hilbert_Choice.Eps"(*FIXME*) =
   320       tptp_choice
   321   | make_fixed_const _ c = const_prefix ^ lookup_const c
   322 
   323 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
   324 
   325 fun make_type_class clas = class_prefix ^ ascii_of clas
   326 
   327 fun new_skolem_var_name_from_const s =
   328   let val ss = s |> space_explode Long_Name.separator in
   329     nth ss (length ss - 2)
   330   end
   331 
   332 (* These are either simplified away by "Meson.presimplify" (most of the time) or
   333    handled specially via "fFalse", "fTrue", ..., "fequal". *)
   334 val atp_irrelevant_consts =
   335   [@{const_name False}, @{const_name True}, @{const_name Not},
   336    @{const_name conj}, @{const_name disj}, @{const_name implies},
   337    @{const_name HOL.eq}, @{const_name If}, @{const_name Let}]
   338 
   339 val atp_monomorph_bad_consts =
   340   atp_irrelevant_consts @
   341   (* These are ignored anyway by the relevance filter (unless they appear in
   342      higher-order places) but not by the monomorphizer. *)
   343   [@{const_name all}, @{const_name "==>"}, @{const_name "=="},
   344    @{const_name Trueprop}, @{const_name All}, @{const_name Ex},
   345    @{const_name Ex1}, @{const_name Ball}, @{const_name Bex}]
   346 
   347 fun add_schematic_const (x as (_, T)) =
   348   Monomorph.typ_has_tvars T ? Symtab.insert_list (op =) x
   349 val add_schematic_consts_of =
   350   Term.fold_aterms (fn Const (x as (s, _)) =>
   351                        not (member (op =) atp_monomorph_bad_consts s)
   352                        ? add_schematic_const x
   353                       | _ => I)
   354 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
   355 
   356 (** Definitions and functions for FOL clauses and formulas for TPTP **)
   357 
   358 (* The first component is the type class; the second is a "TVar" or "TFree". *)
   359 datatype type_literal =
   360   TyLitVar of name * name |
   361   TyLitFree of name * name
   362 
   363 
   364 (** Isabelle arities **)
   365 
   366 datatype arity_literal =
   367   TConsLit of name * name * name list |
   368   TVarLit of name * name
   369 
   370 fun gen_TVars 0 = []
   371   | gen_TVars n = ("T_" ^ string_of_int n) :: gen_TVars (n-1)
   372 
   373 val type_class = the_single @{sort type}
   374 
   375 fun add_packed_sort tvar =
   376   fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar))
   377 
   378 type arity_clause =
   379   {name : string,
   380    prem_lits : arity_literal list,
   381    concl_lits : arity_literal}
   382 
   383 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
   384 fun make_axiom_arity_clause (tcons, name, (cls, args)) =
   385   let
   386     val tvars = gen_TVars (length args)
   387     val tvars_srts = ListPair.zip (tvars, args)
   388   in
   389     {name = name,
   390      prem_lits = [] |> fold (uncurry add_packed_sort) tvars_srts |> map TVarLit,
   391      concl_lits = TConsLit (`make_type_class cls,
   392                             `make_fixed_type_const tcons,
   393                             tvars ~~ tvars)}
   394   end
   395 
   396 fun arity_clause _ _ (_, []) = []
   397   | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
   398     arity_clause seen n (tcons, ars)
   399   | arity_clause seen n (tcons, (ar as (class, _)) :: ars) =
   400     if member (op =) seen class then
   401       (* multiple arities for the same (tycon, class) pair *)
   402       make_axiom_arity_clause (tcons,
   403           lookup_const tcons ^ "___" ^ ascii_of class ^ "_" ^ string_of_int n,
   404           ar) ::
   405       arity_clause seen (n + 1) (tcons, ars)
   406     else
   407       make_axiom_arity_clause (tcons, lookup_const tcons ^ "___" ^
   408                                ascii_of class, ar) ::
   409       arity_clause (class :: seen) n (tcons, ars)
   410 
   411 fun multi_arity_clause [] = []
   412   | multi_arity_clause ((tcons, ars) :: tc_arlists) =
   413       arity_clause [] 1 (tcons, ars) @ multi_arity_clause tc_arlists
   414 
   415 (* Generate all pairs (tycon, class, sorts) such that tycon belongs to class in
   416    theory thy provided its arguments have the corresponding sorts. *)
   417 fun type_class_pairs thy tycons classes =
   418   let
   419     val alg = Sign.classes_of thy
   420     fun domain_sorts tycon = Sorts.mg_domain alg tycon o single
   421     fun add_class tycon class =
   422       cons (class, domain_sorts tycon class)
   423       handle Sorts.CLASS_ERROR _ => I
   424     fun try_classes tycon = (tycon, fold (add_class tycon) classes [])
   425   in map try_classes tycons end
   426 
   427 (*Proving one (tycon, class) membership may require proving others, so iterate.*)
   428 fun iter_type_class_pairs _ _ [] = ([], [])
   429   | iter_type_class_pairs thy tycons classes =
   430       let
   431         fun maybe_insert_class s =
   432           (s <> type_class andalso not (member (op =) classes s))
   433           ? insert (op =) s
   434         val cpairs = type_class_pairs thy tycons classes
   435         val newclasses =
   436           [] |> fold (fold (fold (fold maybe_insert_class) o snd) o snd) cpairs
   437         val (classes', cpairs') = iter_type_class_pairs thy tycons newclasses
   438       in (classes' @ classes, union (op =) cpairs' cpairs) end
   439 
   440 fun make_arity_clauses thy tycons =
   441   iter_type_class_pairs thy tycons ##> multi_arity_clause
   442 
   443 
   444 (** Isabelle class relations **)
   445 
   446 type class_rel_clause =
   447   {name : string,
   448    subclass : name,
   449    superclass : name}
   450 
   451 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
   452    in theory "thy". *)
   453 fun class_pairs _ [] _ = []
   454   | class_pairs thy subs supers =
   455       let
   456         val class_less = Sorts.class_less (Sign.classes_of thy)
   457         fun add_super sub super = class_less (sub, super) ? cons (sub, super)
   458         fun add_supers sub = fold (add_super sub) supers
   459       in fold add_supers subs [] end
   460 
   461 fun make_class_rel_clause (sub, super) =
   462   {name = sub ^ "_" ^ super, subclass = `make_type_class sub,
   463    superclass = `make_type_class super}
   464 
   465 fun make_class_rel_clauses thy subs supers =
   466   map make_class_rel_clause (class_pairs thy subs supers)
   467 
   468 (* intermediate terms *)
   469 datatype iterm =
   470   IConst of name * typ * typ list |
   471   IVar of name * typ |
   472   IApp of iterm * iterm |
   473   IAbs of (name * typ) * iterm
   474 
   475 fun ityp_of (IConst (_, T, _)) = T
   476   | ityp_of (IVar (_, T)) = T
   477   | ityp_of (IApp (t1, _)) = snd (dest_funT (ityp_of t1))
   478   | ityp_of (IAbs ((_, T), tm)) = T --> ityp_of tm
   479 
   480 (*gets the head of a combinator application, along with the list of arguments*)
   481 fun strip_iterm_comb u =
   482   let
   483     fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
   484       | stripc x = x
   485   in stripc (u, []) end
   486 
   487 fun atyps_of T = fold_atyps (insert (op =)) T []
   488 
   489 fun new_skolem_const_name s num_T_args =
   490   [new_skolem_const_prefix, s, string_of_int num_T_args]
   491   |> space_implode Long_Name.separator
   492 
   493 (* Converts an Isabelle/HOL term (with combinators) into an intermediate term.
   494    Also accumulates sort infomation. *)
   495 fun iterm_from_term thy format bs (P $ Q) =
   496     let
   497       val (P', P_atomics_Ts) = iterm_from_term thy format bs P
   498       val (Q', Q_atomics_Ts) = iterm_from_term thy format bs Q
   499     in (IApp (P', Q'), union (op =) P_atomics_Ts Q_atomics_Ts) end
   500   | iterm_from_term thy format _ (Const (c, T)) =
   501     (IConst (`(make_fixed_const (SOME format)) c, T,
   502              if String.isPrefix old_skolem_const_prefix c then
   503                [] |> Term.add_tvarsT T |> map TVar
   504              else
   505                (c, T) |> Sign.const_typargs thy),
   506      atyps_of T)
   507   | iterm_from_term _ _ _ (Free (s, T)) =
   508     (IConst (`make_fixed_var s, T,
   509              if String.isPrefix polymorphic_free_prefix s then [T] else []),
   510      atyps_of T)
   511   | iterm_from_term _ format _ (Var (v as (s, _), T)) =
   512     (if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
   513        let
   514          val Ts = T |> strip_type |> swap |> op ::
   515          val s' = new_skolem_const_name s (length Ts)
   516        in IConst (`(make_fixed_const (SOME format)) s', T, Ts) end
   517      else
   518        IVar ((make_schematic_var v, s), T), atyps_of T)
   519   | iterm_from_term _ _ bs (Bound j) =
   520     nth bs j |> (fn (_, (name, T)) => (IConst (name, T, []), atyps_of T))
   521   | iterm_from_term thy format bs (Abs (s, T, t)) =
   522     let
   523       fun vary s = s |> AList.defined (op =) bs s ? vary o Symbol.bump_string
   524       val s = vary s
   525       val name = `make_bound_var s
   526       val (tm, atomic_Ts) = iterm_from_term thy format ((s, (name, T)) :: bs) t
   527     in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end
   528 
   529 datatype locality =
   530   General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum |
   531   Chained
   532 
   533 datatype order = First_Order | Higher_Order
   534 datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
   535 datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
   536 datatype type_level =
   537   All_Types |
   538   Noninf_Nonmono_Types of soundness |
   539   Fin_Nonmono_Types |
   540   Const_Arg_Types |
   541   No_Types
   542 datatype type_uniformity = Uniform | Nonuniform
   543 
   544 datatype type_enc =
   545   Simple_Types of order * type_level |
   546   Guards of polymorphism * type_level * type_uniformity |
   547   Tags of polymorphism * type_level * type_uniformity
   548 
   549 fun try_unsuffixes ss s =
   550   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   551 
   552 fun type_enc_from_string soundness s =
   553   (case try (unprefix "poly_") s of
   554      SOME s => (SOME Polymorphic, s)
   555    | NONE =>
   556      case try (unprefix "raw_mono_") s of
   557        SOME s => (SOME Raw_Monomorphic, s)
   558      | NONE =>
   559        case try (unprefix "mono_") s of
   560          SOME s => (SOME Mangled_Monomorphic, s)
   561        | NONE => (NONE, s))
   562   ||> (fn s =>
   563           (* "_query" and "_bang" are for the ASCII-challenged Metis and
   564              Mirabelle. *)
   565           case try_unsuffixes ["?", "_query"] s of
   566             SOME s => (Noninf_Nonmono_Types soundness, s)
   567           | NONE =>
   568             case try_unsuffixes ["!", "_bang"] s of
   569               SOME s => (Fin_Nonmono_Types, s)
   570             | NONE => (All_Types, s))
   571   ||> apsnd (fn s =>
   572                 case try (unsuffix "_uniform") s of
   573                   SOME s => (Uniform, s)
   574                 | NONE => (Nonuniform, s))
   575   |> (fn (poly, (level, (uniformity, core))) =>
   576          case (core, (poly, level, uniformity)) of
   577            ("simple", (NONE, _, Nonuniform)) =>
   578            Simple_Types (First_Order, level)
   579          | ("simple_higher", (NONE, _, Nonuniform)) =>
   580            (case level of
   581               Noninf_Nonmono_Types _ => raise Same.SAME
   582             | _ => Simple_Types (Higher_Order, level))
   583          | ("guards", (SOME poly, _, _)) => Guards (poly, level, uniformity)
   584          | ("tags", (SOME Polymorphic, _, _)) =>
   585            Tags (Polymorphic, level, uniformity)
   586          | ("tags", (SOME poly, _, _)) => Tags (poly, level, uniformity)
   587          | ("args", (SOME poly, All_Types (* naja *), Nonuniform)) =>
   588            Guards (poly, Const_Arg_Types, Nonuniform)
   589          | ("erased", (NONE, All_Types (* naja *), Nonuniform)) =>
   590            Guards (Polymorphic, No_Types, Nonuniform)
   591          | _ => raise Same.SAME)
   592   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
   593 
   594 fun is_type_enc_higher_order (Simple_Types (Higher_Order, _)) = true
   595   | is_type_enc_higher_order _ = false
   596 
   597 fun polymorphism_of_type_enc (Simple_Types _) = Mangled_Monomorphic
   598   | polymorphism_of_type_enc (Guards (poly, _, _)) = poly
   599   | polymorphism_of_type_enc (Tags (poly, _, _)) = poly
   600 
   601 fun level_of_type_enc (Simple_Types (_, level)) = level
   602   | level_of_type_enc (Guards (_, level, _)) = level
   603   | level_of_type_enc (Tags (_, level, _)) = level
   604 
   605 fun uniformity_of_type_enc (Simple_Types _) = Uniform
   606   | uniformity_of_type_enc (Guards (_, _, uniformity)) = uniformity
   607   | uniformity_of_type_enc (Tags (_, _, uniformity)) = uniformity
   608 
   609 fun is_type_level_quasi_sound All_Types = true
   610   | is_type_level_quasi_sound (Noninf_Nonmono_Types _) = true
   611   | is_type_level_quasi_sound _ = false
   612 val is_type_enc_quasi_sound =
   613   is_type_level_quasi_sound o level_of_type_enc
   614 
   615 fun is_type_level_fairly_sound level =
   616   is_type_level_quasi_sound level orelse level = Fin_Nonmono_Types
   617 val is_type_enc_fairly_sound = is_type_level_fairly_sound o level_of_type_enc
   618 
   619 fun is_type_level_monotonicity_based (Noninf_Nonmono_Types _) = true
   620   | is_type_level_monotonicity_based Fin_Nonmono_Types = true
   621   | is_type_level_monotonicity_based _ = false
   622 
   623 fun adjust_type_enc (THF _) type_enc = type_enc
   624   | adjust_type_enc (TFF _) (Simple_Types (_, level)) =
   625     Simple_Types (First_Order, level)
   626   | adjust_type_enc format (Simple_Types (_, level)) =
   627     adjust_type_enc format (Guards (Mangled_Monomorphic, level, Uniform))
   628   | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
   629     (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
   630   | adjust_type_enc _ type_enc = type_enc
   631 
   632 fun lift_lambdas ctxt type_enc =
   633   map (close_form o Envir.eta_contract) #> rpair ctxt
   634   #-> Lambda_Lifting.lift_lambdas
   635           (if polymorphism_of_type_enc type_enc = Polymorphic then
   636              SOME polymorphic_free_prefix
   637            else
   638              NONE)
   639           Lambda_Lifting.is_quantifier
   640   #> fst
   641 
   642 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
   643     intentionalize_def t
   644   | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
   645     let
   646       fun lam T t = Abs (Name.uu, T, t)
   647       val (head, args) = strip_comb t ||> rev
   648       val head_T = fastype_of head
   649       val n = length args
   650       val arg_Ts = head_T |> binder_types |> take n |> rev
   651       val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
   652     in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
   653   | intentionalize_def t = t
   654 
   655 type translated_formula =
   656   {name : string,
   657    locality : locality,
   658    kind : formula_kind,
   659    iformula : (name, typ, iterm) formula,
   660    atomic_types : typ list}
   661 
   662 fun update_iformula f ({name, locality, kind, iformula, atomic_types}
   663                        : translated_formula) =
   664   {name = name, locality = locality, kind = kind, iformula = f iformula,
   665    atomic_types = atomic_types} : translated_formula
   666 
   667 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
   668 
   669 fun insert_type ctxt get_T x xs =
   670   let val T = get_T x in
   671     if exists (type_instance ctxt T o get_T) xs then xs
   672     else x :: filter_out (type_generalization ctxt T o get_T) xs
   673   end
   674 
   675 (* The Booleans indicate whether all type arguments should be kept. *)
   676 datatype type_arg_policy =
   677   Explicit_Type_Args of bool |
   678   Mangled_Type_Args of bool |
   679   No_Type_Args
   680 
   681 fun should_drop_arg_type_args (Simple_Types _) =
   682     false (* since TFF doesn't support overloading *)
   683   | should_drop_arg_type_args type_enc =
   684     level_of_type_enc type_enc = All_Types andalso
   685     uniformity_of_type_enc type_enc = Uniform
   686 
   687 fun type_arg_policy type_enc s =
   688   if s = type_tag_name then
   689     (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
   690        Mangled_Type_Args
   691      else
   692        Explicit_Type_Args) false
   693   else case type_enc of
   694     Tags (_, All_Types, Uniform) => No_Type_Args
   695   | _ =>
   696     let val level = level_of_type_enc type_enc in
   697       if level = No_Types orelse s = @{const_name HOL.eq} orelse
   698          (s = app_op_name andalso level = Const_Arg_Types) then
   699         No_Type_Args
   700       else
   701         should_drop_arg_type_args type_enc
   702         |> (if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
   703               Mangled_Type_Args
   704             else
   705               Explicit_Type_Args)
   706     end
   707 
   708 (* Make literals for sorted type variables. *)
   709 fun generic_add_sorts_on_type (_, []) = I
   710   | generic_add_sorts_on_type ((x, i), s :: ss) =
   711     generic_add_sorts_on_type ((x, i), ss)
   712     #> (if s = the_single @{sort HOL.type} then
   713           I
   714         else if i = ~1 then
   715           insert (op =) (TyLitFree (`make_type_class s, `make_fixed_type_var x))
   716         else
   717           insert (op =) (TyLitVar (`make_type_class s,
   718                                    (make_schematic_type_var (x, i), x))))
   719 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   720   | add_sorts_on_tfree _ = I
   721 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   722   | add_sorts_on_tvar _ = I
   723 
   724 fun type_literals_for_types type_enc add_sorts_on_typ Ts =
   725   [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
   726 
   727 fun mk_aconns c phis =
   728   let val (phis', phi') = split_last phis in
   729     fold_rev (mk_aconn c) phis' phi'
   730   end
   731 fun mk_ahorn [] phi = phi
   732   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   733 fun mk_aquant _ [] phi = phi
   734   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   735     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   736   | mk_aquant q xs phi = AQuant (q, xs, phi)
   737 
   738 fun close_universally atom_vars phi =
   739   let
   740     fun formula_vars bounds (AQuant (_, xs, phi)) =
   741         formula_vars (map fst xs @ bounds) phi
   742       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   743       | formula_vars bounds (AAtom tm) =
   744         union (op =) (atom_vars tm []
   745                       |> filter_out (member (op =) bounds o fst))
   746   in mk_aquant AForall (formula_vars [] phi []) phi end
   747 
   748 fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
   749   | iterm_vars (IConst _) = I
   750   | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
   751   | iterm_vars (IAbs (_, tm)) = iterm_vars tm
   752 fun close_iformula_universally phi = close_universally iterm_vars phi
   753 
   754 fun term_vars bounds (ATerm (name as (s, _), tms)) =
   755     (is_tptp_variable s andalso not (member (op =) bounds name))
   756     ? insert (op =) (name, NONE) #> fold (term_vars bounds) tms
   757   | term_vars bounds (AAbs ((name, _), tm)) = term_vars (name :: bounds) tm
   758 fun close_formula_universally phi = close_universally (term_vars []) phi
   759 
   760 val homo_infinite_type_name = @{type_name ind} (* any infinite type *)
   761 val homo_infinite_type = Type (homo_infinite_type_name, [])
   762 
   763 fun ho_term_from_typ format type_enc =
   764   let
   765     fun term (Type (s, Ts)) =
   766       ATerm (case (is_type_enc_higher_order type_enc, s) of
   767                (true, @{type_name bool}) => `I tptp_bool_type
   768              | (true, @{type_name fun}) => `I tptp_fun_type
   769              | _ => if s = homo_infinite_type_name andalso
   770                        is_format_typed format then
   771                       `I tptp_individual_type
   772                     else
   773                       `make_fixed_type_const s,
   774              map term Ts)
   775     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
   776     | term (TVar ((x as (s, _)), _)) =
   777       ATerm ((make_schematic_type_var x, s), [])
   778   in term end
   779 
   780 fun ho_term_for_type_arg format type_enc T =
   781   if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
   782 
   783 (* This shouldn't clash with anything else. *)
   784 val mangled_type_sep = "\000"
   785 
   786 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   787   | generic_mangled_type_name f (ATerm (name, tys)) =
   788     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
   789     ^ ")"
   790   | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
   791 
   792 fun mangled_type format type_enc =
   793   generic_mangled_type_name fst o ho_term_from_typ format type_enc
   794 
   795 val bool_atype = AType (`I tptp_bool_type)
   796 
   797 fun make_simple_type s =
   798   if s = tptp_bool_type orelse s = tptp_fun_type orelse
   799      s = tptp_individual_type then
   800     s
   801   else
   802     simple_type_prefix ^ ascii_of s
   803 
   804 fun ho_type_from_ho_term type_enc pred_sym ary =
   805   let
   806     fun to_atype ty =
   807       AType ((make_simple_type (generic_mangled_type_name fst ty),
   808               generic_mangled_type_name snd ty))
   809     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
   810     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
   811       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
   812       | to_fo _ _ = raise Fail "unexpected type abstraction"
   813     fun to_ho (ty as ATerm ((s, _), tys)) =
   814         if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
   815       | to_ho _ = raise Fail "unexpected type abstraction"
   816   in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
   817 
   818 fun ho_type_from_typ format type_enc pred_sym ary =
   819   ho_type_from_ho_term type_enc pred_sym ary
   820   o ho_term_from_typ format type_enc
   821 
   822 fun mangled_const_name format type_enc T_args (s, s') =
   823   let
   824     val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
   825     fun type_suffix f g =
   826       fold_rev (curry (op ^) o g o prefix mangled_type_sep
   827                 o generic_mangled_type_name f) ty_args ""
   828   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
   829 
   830 val parse_mangled_ident =
   831   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   832 
   833 fun parse_mangled_type x =
   834   (parse_mangled_ident
   835    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
   836                     [] >> ATerm) x
   837 and parse_mangled_types x =
   838   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   839 
   840 fun unmangled_type s =
   841   s |> suffix ")" |> raw_explode
   842     |> Scan.finite Symbol.stopper
   843            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   844                                                 quote s)) parse_mangled_type))
   845     |> fst
   846 
   847 val unmangled_const_name = space_explode mangled_type_sep #> hd
   848 fun unmangled_const s =
   849   let val ss = space_explode mangled_type_sep s in
   850     (hd ss, map unmangled_type (tl ss))
   851   end
   852 
   853 fun introduce_proxies type_enc =
   854   let
   855     fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
   856       | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
   857                        _ =
   858         (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
   859            limitation. This works in conjuction with special code in
   860            "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
   861            possible. *)
   862         IAbs ((`I "P", p_T),
   863               IApp (IConst (`I ho_quant, T, []),
   864                     IAbs ((`I "X", x_T),
   865                           IApp (IConst (`I "P", p_T, []),
   866                                 IConst (`I "X", x_T, [])))))
   867       | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
   868     fun intro top_level args (IApp (tm1, tm2)) =
   869         IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
   870       | intro top_level args (IConst (name as (s, _), T, T_args)) =
   871         (case proxify_const s of
   872            SOME proxy_base =>
   873            if top_level orelse is_type_enc_higher_order type_enc then
   874              case (top_level, s) of
   875                (_, "c_False") => IConst (`I tptp_false, T, [])
   876              | (_, "c_True") => IConst (`I tptp_true, T, [])
   877              | (false, "c_Not") => IConst (`I tptp_not, T, [])
   878              | (false, "c_conj") => IConst (`I tptp_and, T, [])
   879              | (false, "c_disj") => IConst (`I tptp_or, T, [])
   880              | (false, "c_implies") => IConst (`I tptp_implies, T, [])
   881              | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
   882              | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
   883              | (false, s) =>
   884                if is_tptp_equal s andalso length args = 2 then
   885                  IConst (`I tptp_equal, T, [])
   886                else
   887                  (* Use a proxy even for partially applied THF equality, because
   888                     the LEO-II and Satallax parsers complain about not being
   889                     able to infer the type of "=". *)
   890                  IConst (proxy_base |>> prefix const_prefix, T, T_args)
   891              | _ => IConst (name, T, [])
   892            else
   893              IConst (proxy_base |>> prefix const_prefix, T, T_args)
   894           | NONE => if s = tptp_choice then
   895                       (*this could be made neater by adding c_Eps as a proxy,
   896                         but we'd need to be able to "see" Hilbert_Choice.Eps
   897                         at this level in order to define fEps*)
   898                       tweak_ho_quant tptp_choice T args
   899                     else IConst (name, T, T_args))
   900       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
   901       | intro _ _ tm = tm
   902   in intro true [] end
   903 
   904 fun iformula_from_prop thy format type_enc eq_as_iff =
   905   let
   906     fun do_term bs t atomic_types =
   907       iterm_from_term thy format bs (Envir.eta_contract t)
   908       |>> (introduce_proxies type_enc #> AAtom)
   909       ||> union (op =) atomic_types
   910     fun do_quant bs q pos s T t' =
   911       let
   912         val s = singleton (Name.variant_list (map fst bs)) s
   913         val universal = Option.map (q = AExists ? not) pos
   914         val name =
   915           s |> `(case universal of
   916                    SOME true => make_all_bound_var
   917                  | SOME false => make_exist_bound_var
   918                  | NONE => make_bound_var)
   919       in
   920         do_formula ((s, (name, T)) :: bs) pos t'
   921         #>> mk_aquant q [(name, SOME T)]
   922       end
   923     and do_conn bs c pos1 t1 pos2 t2 =
   924       do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
   925     and do_formula bs pos t =
   926       case t of
   927         @{const Trueprop} $ t1 => do_formula bs pos t1
   928       | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
   929       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
   930         do_quant bs AForall pos s T t'
   931       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
   932         do_quant bs AExists pos s T t'
   933       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
   934       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
   935       | @{const HOL.implies} $ t1 $ t2 =>
   936         do_conn bs AImplies (Option.map not pos) t1 pos t2
   937       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
   938         if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
   939       | _ => do_term bs t
   940   in do_formula [] end
   941 
   942 fun presimplify_term _ [] t = t
   943   | presimplify_term ctxt presimp_consts t =
   944     t |> exists_Const (member (op =) presimp_consts o fst) t
   945          ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
   946             #> Meson.presimplify ctxt
   947             #> prop_of)
   948 
   949 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
   950 fun conceal_bounds Ts t =
   951   subst_bounds (map (Free o apfst concealed_bound_name)
   952                     (0 upto length Ts - 1 ~~ Ts), t)
   953 fun reveal_bounds Ts =
   954   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
   955                     (0 upto length Ts - 1 ~~ Ts))
   956 
   957 fun is_fun_equality (@{const_name HOL.eq},
   958                      Type (_, [Type (@{type_name fun}, _), _])) = true
   959   | is_fun_equality _ = false
   960 
   961 fun extensionalize_term ctxt t =
   962   if exists_Const is_fun_equality t then
   963     let val thy = Proof_Context.theory_of ctxt in
   964       t |> cterm_of thy |> Meson.extensionalize_conv ctxt
   965         |> prop_of |> Logic.dest_equals |> snd
   966     end
   967   else
   968     t
   969 
   970 fun simple_translate_lambdas do_lambdas ctxt t =
   971   let val thy = Proof_Context.theory_of ctxt in
   972     if Meson.is_fol_term thy t then
   973       t
   974     else
   975       let
   976         fun aux Ts t =
   977           case t of
   978             @{const Not} $ t1 => @{const Not} $ aux Ts t1
   979           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
   980             t0 $ Abs (s, T, aux (T :: Ts) t')
   981           | (t0 as Const (@{const_name All}, _)) $ t1 =>
   982             aux Ts (t0 $ eta_expand Ts t1 1)
   983           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
   984             t0 $ Abs (s, T, aux (T :: Ts) t')
   985           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
   986             aux Ts (t0 $ eta_expand Ts t1 1)
   987           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   988           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   989           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
   990           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
   991               $ t1 $ t2 =>
   992             t0 $ aux Ts t1 $ aux Ts t2
   993           | _ =>
   994             if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
   995             else t |> Envir.eta_contract |> do_lambdas ctxt Ts
   996         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
   997       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
   998   end
   999 
  1000 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
  1001     do_cheaply_conceal_lambdas Ts t1
  1002     $ do_cheaply_conceal_lambdas Ts t2
  1003   | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
  1004     Free (polymorphic_free_prefix ^ serial_string (),
  1005           T --> fastype_of1 (T :: Ts, t))
  1006   | do_cheaply_conceal_lambdas _ t = t
  1007 
  1008 fun do_introduce_combinators ctxt Ts t =
  1009   let val thy = Proof_Context.theory_of ctxt in
  1010     t |> conceal_bounds Ts
  1011       |> cterm_of thy
  1012       |> Meson_Clausify.introduce_combinators_in_cterm
  1013       |> prop_of |> Logic.dest_equals |> snd
  1014       |> reveal_bounds Ts
  1015   end
  1016   (* A type variable of sort "{}" will make abstraction fail. *)
  1017   handle THM _ => t |> do_cheaply_conceal_lambdas Ts
  1018 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
  1019 
  1020 fun preprocess_abstractions_in_terms trans_lambdas facts =
  1021   let
  1022     val (facts, lambda_ts) =
  1023       facts |> map (snd o snd) |> trans_lambdas
  1024             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
  1025     val lambda_facts =
  1026       map2 (fn t => fn j =>
  1027                ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
  1028            lambda_ts (1 upto length lambda_ts)
  1029   in (facts, lambda_facts) end
  1030 
  1031 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
  1032    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
  1033 fun freeze_term t =
  1034   let
  1035     fun aux (t $ u) = aux t $ aux u
  1036       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
  1037       | aux (Var ((s, i), T)) =
  1038         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
  1039       | aux t = t
  1040   in t |> exists_subterm is_Var t ? aux end
  1041 
  1042 fun presimp_prop ctxt presimp_consts t =
  1043   let
  1044     val thy = Proof_Context.theory_of ctxt
  1045     val t = t |> Envir.beta_eta_contract
  1046               |> transform_elim_prop
  1047               |> Object_Logic.atomize_term thy
  1048     val need_trueprop = (fastype_of t = @{typ bool})
  1049   in
  1050     t |> need_trueprop ? HOLogic.mk_Trueprop
  1051       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
  1052       |> extensionalize_term ctxt
  1053       |> presimplify_term ctxt presimp_consts
  1054       |> perhaps (try (HOLogic.dest_Trueprop))
  1055   end
  1056 
  1057 (* making fact and conjecture formulas *)
  1058 fun make_formula thy format type_enc eq_as_iff name loc kind t =
  1059   let
  1060     val (iformula, atomic_types) =
  1061       iformula_from_prop thy format type_enc eq_as_iff (SOME (kind <> Conjecture)) t []
  1062   in
  1063     {name = name, locality = loc, kind = kind, iformula = iformula,
  1064      atomic_types = atomic_types}
  1065   end
  1066 
  1067 fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
  1068   let val thy = Proof_Context.theory_of ctxt in
  1069     case t |> make_formula thy format type_enc (eq_as_iff andalso format <> CNF)
  1070                            name loc Axiom of
  1071       formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
  1072       if s = tptp_true then NONE else SOME formula
  1073     | formula => SOME formula
  1074   end
  1075 
  1076 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
  1077   | s_not_trueprop t = s_not t
  1078 
  1079 fun make_conjecture thy format type_enc =
  1080   map (fn ((name, loc), (kind, t)) =>
  1081           t |> kind = Conjecture ? s_not_trueprop
  1082             |> make_formula thy format type_enc (format <> CNF) name loc kind)
  1083 
  1084 (** Finite and infinite type inference **)
  1085 
  1086 type monotonicity_info =
  1087   {maybe_finite_Ts : typ list,
  1088    surely_finite_Ts : typ list,
  1089    maybe_infinite_Ts : typ list,
  1090    surely_infinite_Ts : typ list,
  1091    maybe_nonmono_Ts : typ list}
  1092 
  1093 (* These types witness that the type classes they belong to allow infinite
  1094    models and hence that any types with these type classes is monotonic. *)
  1095 val known_infinite_types =
  1096   [@{typ nat}, Type ("Int.int", []), @{typ "nat => bool"}]
  1097 
  1098 fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
  1099   soundness <> Sound andalso
  1100   is_type_surely_infinite ctxt (soundness <> Unsound) cached_Ts T
  1101 
  1102 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
  1103    dangerous because their "exhaust" properties can easily lead to unsound ATP
  1104    proofs. On the other hand, all HOL infinite types can be given the same
  1105    models in first-order logic (via Löwenheim-Skolem). *)
  1106 
  1107 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
  1108   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
  1109                              maybe_nonmono_Ts, ...}
  1110                        (Noninf_Nonmono_Types soundness) T =
  1111     exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  1112     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
  1113          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
  1114           is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
  1115   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
  1116                              maybe_nonmono_Ts, ...}
  1117                        Fin_Nonmono_Types T =
  1118     exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  1119     (exists (type_generalization ctxt T) surely_finite_Ts orelse
  1120      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
  1121       is_type_surely_finite ctxt T))
  1122   | should_encode_type _ _ _ _ = false
  1123 
  1124 fun should_guard_type ctxt mono (Guards (_, level, uniformity)) should_guard_var
  1125                       T =
  1126     (uniformity = Uniform orelse should_guard_var ()) andalso
  1127     should_encode_type ctxt mono level T
  1128   | should_guard_type _ _ _ _ _ = false
  1129 
  1130 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
  1131     String.isPrefix bound_var_prefix s orelse
  1132     String.isPrefix all_bound_var_prefix s
  1133   | is_maybe_universal_var (IVar _) = true
  1134   | is_maybe_universal_var _ = false
  1135 
  1136 datatype tag_site =
  1137   Top_Level of bool option |
  1138   Eq_Arg of bool option |
  1139   Elsewhere
  1140 
  1141 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
  1142   | should_tag_with_type ctxt mono (Tags (_, level, uniformity)) site u T =
  1143     (case uniformity of
  1144        Uniform => should_encode_type ctxt mono level T
  1145      | Nonuniform =>
  1146        case (site, is_maybe_universal_var u) of
  1147          (Eq_Arg _, true) => should_encode_type ctxt mono level T
  1148        | _ => false)
  1149   | should_tag_with_type _ _ _ _ _ _ = false
  1150 
  1151 fun homogenized_type ctxt mono level =
  1152   let
  1153     val should_encode = should_encode_type ctxt mono level
  1154     fun homo 0 T = if should_encode T then T else homo_infinite_type
  1155       | homo ary (Type (@{type_name fun}, [T1, T2])) =
  1156         homo 0 T1 --> homo (ary - 1) T2
  1157       | homo _ _ = raise Fail "expected function type"
  1158   in homo end
  1159 
  1160 (** predicators and application operators **)
  1161 
  1162 type sym_info =
  1163   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
  1164 
  1165 fun add_iterm_syms_to_table ctxt explicit_apply =
  1166   let
  1167     fun consider_var_arity const_T var_T max_ary =
  1168       let
  1169         fun iter ary T =
  1170           if ary = max_ary orelse type_instance ctxt var_T T orelse
  1171              type_instance ctxt T var_T then
  1172             ary
  1173           else
  1174             iter (ary + 1) (range_type T)
  1175       in iter 0 const_T end
  1176     fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1177       if explicit_apply = NONE andalso
  1178          (can dest_funT T orelse T = @{typ bool}) then
  1179         let
  1180           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
  1181           fun repair_min_arity {pred_sym, min_ary, max_ary, types} =
  1182             {pred_sym = pred_sym andalso not bool_vars',
  1183              min_ary = fold (fn T' => consider_var_arity T' T) types min_ary,
  1184              max_ary = max_ary, types = types}
  1185           val fun_var_Ts' =
  1186             fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
  1187         in
  1188           if bool_vars' = bool_vars andalso
  1189              pointer_eq (fun_var_Ts', fun_var_Ts) then
  1190             accum
  1191           else
  1192             ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_arity) sym_tab)
  1193         end
  1194       else
  1195         accum
  1196     fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1197       let val (head, args) = strip_iterm_comb tm in
  1198         (case head of
  1199            IConst ((s, _), T, _) =>
  1200            if String.isPrefix bound_var_prefix s orelse
  1201               String.isPrefix all_bound_var_prefix s then
  1202              add_universal_var T accum
  1203            else if String.isPrefix exist_bound_var_prefix s then
  1204              accum
  1205            else
  1206              let val ary = length args in
  1207                ((bool_vars, fun_var_Ts),
  1208                 case Symtab.lookup sym_tab s of
  1209                   SOME {pred_sym, min_ary, max_ary, types} =>
  1210                   let
  1211                     val pred_sym =
  1212                       pred_sym andalso top_level andalso not bool_vars
  1213                     val types' = types |> insert_type ctxt I T
  1214                     val min_ary =
  1215                       if is_some explicit_apply orelse
  1216                          pointer_eq (types', types) then
  1217                         min_ary
  1218                       else
  1219                         fold (consider_var_arity T) fun_var_Ts min_ary
  1220                   in
  1221                     Symtab.update (s, {pred_sym = pred_sym,
  1222                                        min_ary = Int.min (ary, min_ary),
  1223                                        max_ary = Int.max (ary, max_ary),
  1224                                        types = types'})
  1225                                   sym_tab
  1226                   end
  1227                 | NONE =>
  1228                   let
  1229                     val pred_sym = top_level andalso not bool_vars
  1230                     val min_ary =
  1231                       case explicit_apply of
  1232                         SOME true => 0
  1233                       | SOME false => ary
  1234                       | NONE => fold (consider_var_arity T) fun_var_Ts ary
  1235                   in
  1236                     Symtab.update_new (s, {pred_sym = pred_sym,
  1237                                            min_ary = min_ary, max_ary = ary,
  1238                                            types = [T]})
  1239                                       sym_tab
  1240                   end)
  1241              end
  1242          | IVar (_, T) => add_universal_var T accum
  1243          | IAbs ((_, T), tm) => accum |> add_universal_var T |> add false tm
  1244          | _ => accum)
  1245         |> fold (add false) args
  1246       end
  1247   in add true end
  1248 fun add_fact_syms_to_table ctxt explicit_apply =
  1249   K (add_iterm_syms_to_table ctxt explicit_apply)
  1250   |> formula_fold NONE |> fact_lift
  1251 
  1252 val tvar_a = TVar (("'a", 0), HOLogic.typeS)
  1253 
  1254 val default_sym_tab_entries : (string * sym_info) list =
  1255   (prefixed_predicator_name,
  1256    {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
  1257   (make_fixed_const NONE @{const_name undefined},
  1258    {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
  1259   ([tptp_false, tptp_true]
  1260    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
  1261   ([tptp_equal, tptp_old_equal]
  1262    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
  1263 
  1264 fun sym_table_for_facts ctxt explicit_apply facts =
  1265   ((false, []), Symtab.empty)
  1266   |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
  1267   |> fold Symtab.update default_sym_tab_entries
  1268 
  1269 fun min_arity_of sym_tab s =
  1270   case Symtab.lookup sym_tab s of
  1271     SOME ({min_ary, ...} : sym_info) => min_ary
  1272   | NONE =>
  1273     case strip_prefix_and_unascii const_prefix s of
  1274       SOME s =>
  1275       let val s = s |> unmangled_const_name |> invert_const in
  1276         if s = predicator_name then 1
  1277         else if s = app_op_name then 2
  1278         else if s = type_guard_name then 1
  1279         else 0
  1280       end
  1281     | NONE => 0
  1282 
  1283 (* True if the constant ever appears outside of the top-level position in
  1284    literals, or if it appears with different arities (e.g., because of different
  1285    type instantiations). If false, the constant always receives all of its
  1286    arguments and is used as a predicate. *)
  1287 fun is_pred_sym sym_tab s =
  1288   case Symtab.lookup sym_tab s of
  1289     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
  1290     pred_sym andalso min_ary = max_ary
  1291   | NONE => false
  1292 
  1293 val predicator_combconst =
  1294   IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
  1295 fun predicator tm = IApp (predicator_combconst, tm)
  1296 
  1297 fun introduce_predicators_in_iterm sym_tab tm =
  1298   case strip_iterm_comb tm of
  1299     (IConst ((s, _), _, _), _) =>
  1300     if is_pred_sym sym_tab s then tm else predicator tm
  1301   | _ => predicator tm
  1302 
  1303 fun list_app head args = fold (curry (IApp o swap)) args head
  1304 
  1305 val app_op = `(make_fixed_const NONE) app_op_name
  1306 
  1307 fun explicit_app arg head =
  1308   let
  1309     val head_T = ityp_of head
  1310     val (arg_T, res_T) = dest_funT head_T
  1311     val explicit_app = IConst (app_op, head_T --> head_T, [arg_T, res_T])
  1312   in list_app explicit_app [head, arg] end
  1313 fun list_explicit_app head args = fold explicit_app args head
  1314 
  1315 fun introduce_explicit_apps_in_iterm sym_tab =
  1316   let
  1317     fun aux tm =
  1318       case strip_iterm_comb tm of
  1319         (head as IConst ((s, _), _, _), args) =>
  1320         args |> map aux
  1321              |> chop (min_arity_of sym_tab s)
  1322              |>> list_app head
  1323              |-> list_explicit_app
  1324       | (head, args) => list_explicit_app head (map aux args)
  1325   in aux end
  1326 
  1327 fun chop_fun 0 T = ([], T)
  1328   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
  1329     chop_fun (n - 1) ran_T |>> cons dom_T
  1330   | chop_fun _ _ = raise Fail "unexpected non-function"
  1331 
  1332 fun filter_type_args _ _ _ [] = []
  1333   | filter_type_args thy s arity T_args =
  1334     let
  1335       (* will throw "TYPE" for pseudo-constants *)
  1336       val U = if s = app_op_name then
  1337                 @{typ "('a => 'b) => 'a => 'b"} |> Logic.varifyT_global
  1338               else
  1339                 s |> Sign.the_const_type thy
  1340     in
  1341       case Term.add_tvarsT (U |> chop_fun arity |> snd) [] of
  1342         [] => []
  1343       | res_U_vars =>
  1344         let val U_args = (s, U) |> Sign.const_typargs thy in
  1345           U_args ~~ T_args
  1346           |> map (fn (U, T) =>
  1347                      if member (op =) res_U_vars (dest_TVar U) then T
  1348                      else dummyT)
  1349         end
  1350     end
  1351     handle TYPE _ => T_args
  1352 
  1353 fun enforce_type_arg_policy_in_iterm ctxt format type_enc =
  1354   let
  1355     val thy = Proof_Context.theory_of ctxt
  1356     fun aux arity (IApp (tm1, tm2)) = IApp (aux (arity + 1) tm1, aux 0 tm2)
  1357       | aux arity (IConst (name as (s, _), T, T_args)) =
  1358         (case strip_prefix_and_unascii const_prefix s of
  1359            NONE =>
  1360            (name, if level_of_type_enc type_enc = No_Types orelse s = tptp_choice
  1361                   then [] else T_args)
  1362          | SOME s'' =>
  1363            let
  1364              val s'' = invert_const s''
  1365              fun filtered_T_args false = T_args
  1366                | filtered_T_args true = filter_type_args thy s'' arity T_args
  1367            in
  1368              case type_arg_policy type_enc s'' of
  1369                Explicit_Type_Args drop_args =>
  1370                (name, filtered_T_args drop_args)
  1371              | Mangled_Type_Args drop_args =>
  1372                (mangled_const_name format type_enc (filtered_T_args drop_args)
  1373                                    name, [])
  1374              | No_Type_Args => (name, [])
  1375            end)
  1376         |> (fn (name, T_args) => IConst (name, T, T_args))
  1377       | aux _ (IAbs (bound, tm)) = IAbs (bound, aux 0 tm)
  1378       | aux _ tm = tm
  1379   in aux 0 end
  1380 
  1381 fun repair_iterm ctxt format type_enc sym_tab =
  1382   not (is_type_enc_higher_order type_enc)
  1383   ? (introduce_explicit_apps_in_iterm sym_tab
  1384      #> introduce_predicators_in_iterm sym_tab)
  1385   #> enforce_type_arg_policy_in_iterm ctxt format type_enc
  1386 fun repair_fact ctxt format type_enc sym_tab =
  1387   update_iformula (formula_map (repair_iterm ctxt format type_enc sym_tab))
  1388 
  1389 (** Helper facts **)
  1390 
  1391 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
  1392 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
  1393 
  1394 (* The Boolean indicates that a fairly sound type encoding is needed. *)
  1395 val helper_table =
  1396   [(("COMBI", false), @{thms Meson.COMBI_def}),
  1397    (("COMBK", false), @{thms Meson.COMBK_def}),
  1398    (("COMBB", false), @{thms Meson.COMBB_def}),
  1399    (("COMBC", false), @{thms Meson.COMBC_def}),
  1400    (("COMBS", false), @{thms Meson.COMBS_def}),
  1401    ((predicator_name, false), [not_ffalse, ftrue]),
  1402    (("fFalse", false), [not_ffalse]),
  1403    (("fFalse", true), @{thms True_or_False}),
  1404    (("fTrue", false), [ftrue]),
  1405    (("fTrue", true), @{thms True_or_False}),
  1406    (("fNot", false),
  1407     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1408            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1409    (("fconj", false),
  1410     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
  1411         by (unfold fconj_def) fast+}),
  1412    (("fdisj", false),
  1413     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
  1414         by (unfold fdisj_def) fast+}),
  1415    (("fimplies", false),
  1416     @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
  1417         by (unfold fimplies_def) fast+}),
  1418    (("fequal", true),
  1419     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
  1420        However, this is done so for backward compatibility: Including the
  1421        equality helpers by default in Metis breaks a few existing proofs. *)
  1422     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1423            fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1424    (* Partial characterization of "fAll" and "fEx". A complete characterization
  1425       would require the axiom of choice for replay with Metis. *)
  1426    (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
  1427    (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
  1428    (("If", true), @{thms if_True if_False True_or_False})]
  1429   |> map (apsnd (map zero_var_indexes))
  1430 
  1431 fun fo_literal_from_type_literal (TyLitVar (class, name)) =
  1432     (true, ATerm (class, [ATerm (name, [])]))
  1433   | fo_literal_from_type_literal (TyLitFree (class, name)) =
  1434     (true, ATerm (class, [ATerm (name, [])]))
  1435 
  1436 fun formula_from_fo_literal (pos, t) = AAtom t |> not pos ? mk_anot
  1437 
  1438 fun bound_tvars type_enc Ts =
  1439   mk_ahorn (map (formula_from_fo_literal o fo_literal_from_type_literal)
  1440                 (type_literals_for_types type_enc add_sorts_on_tvar Ts))
  1441 
  1442 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
  1443   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
  1444    else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
  1445   |> bound_tvars type_enc atomic_Ts
  1446   |> close_formula_universally
  1447 
  1448 val type_tag = `(make_fixed_const NONE) type_tag_name
  1449 
  1450 fun type_tag_idempotence_fact type_enc =
  1451   let
  1452     fun var s = ATerm (`I s, [])
  1453     fun tag tm = ATerm (type_tag, [var "A", tm])
  1454     val tagged_var = tag (var "X")
  1455   in
  1456     Formula (type_tag_idempotence_helper_name, Axiom,
  1457              eq_formula type_enc [] false (tag tagged_var) tagged_var,
  1458              isabelle_info simpN, NONE)
  1459   end
  1460 
  1461 fun should_specialize_helper type_enc t =
  1462   polymorphism_of_type_enc type_enc <> Polymorphic andalso
  1463   level_of_type_enc type_enc <> No_Types andalso
  1464   not (null (Term.hidden_polymorphism t))
  1465 
  1466 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
  1467   case strip_prefix_and_unascii const_prefix s of
  1468     SOME mangled_s =>
  1469     let
  1470       val thy = Proof_Context.theory_of ctxt
  1471       val unmangled_s = mangled_s |> unmangled_const_name
  1472       fun dub needs_fairly_sound j k =
  1473         (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
  1474          (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
  1475          (if needs_fairly_sound then typed_helper_suffix
  1476           else untyped_helper_suffix),
  1477          Helper)
  1478       fun dub_and_inst needs_fairly_sound (th, j) =
  1479         let val t = prop_of th in
  1480           if should_specialize_helper type_enc t then
  1481             map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
  1482                 types
  1483           else
  1484             [t]
  1485         end
  1486         |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
  1487       val make_facts = map_filter (make_fact ctxt format type_enc false)
  1488       val fairly_sound = is_type_enc_fairly_sound type_enc
  1489     in
  1490       helper_table
  1491       |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
  1492                   if helper_s <> unmangled_s orelse
  1493                      (needs_fairly_sound andalso not fairly_sound) then
  1494                     []
  1495                   else
  1496                     ths ~~ (1 upto length ths)
  1497                     |> maps (dub_and_inst needs_fairly_sound)
  1498                     |> make_facts)
  1499     end
  1500   | NONE => []
  1501 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
  1502   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
  1503                   []
  1504 
  1505 (***************************************************************)
  1506 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
  1507 (***************************************************************)
  1508 
  1509 fun set_insert (x, s) = Symtab.update (x, ()) s
  1510 
  1511 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  1512 
  1513 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1514 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1515 
  1516 fun classes_of_terms get_Ts =
  1517   map (map snd o get_Ts)
  1518   #> List.foldl add_classes Symtab.empty
  1519   #> delete_type #> Symtab.keys
  1520 
  1521 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
  1522 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
  1523 
  1524 fun fold_type_constrs f (Type (s, Ts)) x =
  1525     fold (fold_type_constrs f) Ts (f (s, x))
  1526   | fold_type_constrs _ _ x = x
  1527 
  1528 (* Type constructors used to instantiate overloaded constants are the only ones
  1529    needed. *)
  1530 fun add_type_constrs_in_term thy =
  1531   let
  1532     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
  1533       | add (t $ u) = add t #> add u
  1534       | add (Const (x as (s, _))) =
  1535         if String.isPrefix skolem_const_prefix s then I
  1536         else x |> Sign.const_typargs thy |> fold (fold_type_constrs set_insert)
  1537       | add (Free (s, T)) =
  1538         if String.isPrefix polymorphic_free_prefix s then
  1539           T |> fold_type_constrs set_insert
  1540         else
  1541           I
  1542       | add (Abs (_, _, u)) = add u
  1543       | add _ = I
  1544   in add end
  1545 
  1546 fun type_constrs_of_terms thy ts =
  1547   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
  1548 
  1549 fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
  1550                        hyp_ts concl_t facts =
  1551   let
  1552     val thy = Proof_Context.theory_of ctxt
  1553     val presimp_consts = Meson.presimplified_consts ctxt
  1554     val fact_ts = facts |> map snd
  1555     (* Remove existing facts from the conjecture, as this can dramatically
  1556        boost an ATP's performance (for some reason). *)
  1557     val hyp_ts =
  1558       hyp_ts
  1559       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
  1560     val facts = facts |> map (apsnd (pair Axiom))
  1561     val conjs =
  1562       map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
  1563       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
  1564     val ((conjs, facts), lambdas) =
  1565       if preproc then
  1566         conjs @ facts
  1567         |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
  1568         |> preprocess_abstractions_in_terms trans_lambdas
  1569         |>> chop (length conjs)
  1570         |>> apfst (map (apsnd (apsnd freeze_term)))
  1571       else
  1572         ((conjs, facts), [])
  1573     val conjs = conjs |> make_conjecture thy format type_enc
  1574     val (fact_names, facts) =
  1575       facts
  1576       |> map_filter (fn (name, (_, t)) =>
  1577                         make_fact ctxt format type_enc true (name, t)
  1578                         |> Option.map (pair name))
  1579       |> ListPair.unzip
  1580     val lambdas =
  1581       lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
  1582     val all_ts = concl_t :: hyp_ts @ fact_ts
  1583     val subs = tfree_classes_of_terms all_ts
  1584     val supers = tvar_classes_of_terms all_ts
  1585     val tycons = type_constrs_of_terms thy all_ts
  1586     val (supers, arity_clauses) =
  1587       if level_of_type_enc type_enc = No_Types then ([], [])
  1588       else make_arity_clauses thy tycons supers
  1589     val class_rel_clauses = make_class_rel_clauses thy subs supers
  1590   in
  1591     (fact_names |> map single,
  1592      (conjs, facts @ lambdas, class_rel_clauses, arity_clauses))
  1593   end
  1594 
  1595 val type_guard = `(make_fixed_const NONE) type_guard_name
  1596 
  1597 fun type_guard_iterm ctxt format type_enc T tm =
  1598   IApp (IConst (type_guard, T --> @{typ bool}, [T])
  1599         |> enforce_type_arg_policy_in_iterm ctxt format type_enc, tm)
  1600 
  1601 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
  1602   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
  1603     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
  1604   | is_var_positively_naked_in_term _ _ _ _ = true
  1605 
  1606 fun should_guard_var_in_formula pos phi (SOME true) name =
  1607     formula_fold pos (is_var_positively_naked_in_term name) phi false
  1608   | should_guard_var_in_formula _ _ _ _ = true
  1609 
  1610 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
  1611   | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =
  1612     should_encode_type ctxt mono level T
  1613   | should_generate_tag_bound_decl _ _ _ _ _ = false
  1614 
  1615 fun mk_aterm format type_enc name T_args args =
  1616   ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
  1617 
  1618 fun tag_with_type ctxt format mono type_enc pos T tm =
  1619   IConst (type_tag, T --> T, [T])
  1620   |> enforce_type_arg_policy_in_iterm ctxt format type_enc
  1621   |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
  1622   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
  1623        | _ => raise Fail "unexpected lambda-abstraction")
  1624 and ho_term_from_iterm ctxt format mono type_enc =
  1625   let
  1626     fun aux site u =
  1627       let
  1628         val (head, args) = strip_iterm_comb u
  1629         val pos =
  1630           case site of
  1631             Top_Level pos => pos
  1632           | Eq_Arg pos => pos
  1633           | Elsewhere => NONE
  1634         val t =
  1635           case head of
  1636             IConst (name as (s, _), _, T_args) =>
  1637             let
  1638               val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
  1639             in
  1640               mk_aterm format type_enc name T_args (map (aux arg_site) args)
  1641             end
  1642           | IVar (name, _) =>
  1643             mk_aterm format type_enc name [] (map (aux Elsewhere) args)
  1644           | IAbs ((name, T), tm) =>
  1645             AAbs ((name, ho_type_from_typ format type_enc true 0 T),
  1646                   aux Elsewhere tm)
  1647           | IApp _ => raise Fail "impossible \"IApp\""
  1648         val T = ityp_of u
  1649       in
  1650         t |> (if should_tag_with_type ctxt mono type_enc site u T then
  1651                 tag_with_type ctxt format mono type_enc pos T
  1652               else
  1653                 I)
  1654       end
  1655   in aux end
  1656 and formula_from_iformula ctxt format mono type_enc should_guard_var =
  1657   let
  1658     val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
  1659     val do_bound_type =
  1660       case type_enc of
  1661         Simple_Types (_, level) =>
  1662         homogenized_type ctxt mono level 0
  1663         #> ho_type_from_typ format type_enc false 0 #> SOME
  1664       | _ => K NONE
  1665     fun do_out_of_bound_type pos phi universal (name, T) =
  1666       if should_guard_type ctxt mono type_enc
  1667              (fn () => should_guard_var pos phi universal name) T then
  1668         IVar (name, T)
  1669         |> type_guard_iterm ctxt format type_enc T
  1670         |> do_term pos |> AAtom |> SOME
  1671       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
  1672         let
  1673           val var = ATerm (name, [])
  1674           val tagged_var =
  1675             ATerm (type_tag, [ho_term_from_typ format type_enc T, var])
  1676         in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
  1677       else
  1678         NONE
  1679     fun do_formula pos (AQuant (q, xs, phi)) =
  1680         let
  1681           val phi = phi |> do_formula pos
  1682           val universal = Option.map (q = AExists ? not) pos
  1683         in
  1684           AQuant (q, xs |> map (apsnd (fn NONE => NONE
  1685                                         | SOME T => do_bound_type T)),
  1686                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
  1687                       (map_filter
  1688                            (fn (_, NONE) => NONE
  1689                              | (s, SOME T) =>
  1690                                do_out_of_bound_type pos phi universal (s, T))
  1691                            xs)
  1692                       phi)
  1693         end
  1694       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
  1695       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
  1696   in do_formula end
  1697 
  1698 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
  1699    of monomorphization). The TPTP explicitly forbids name clashes, and some of
  1700    the remote provers might care. *)
  1701 fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
  1702                           (j, {name, locality, kind, iformula, atomic_types}) =
  1703   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
  1704    iformula
  1705    |> close_iformula_universally
  1706    |> formula_from_iformula ctxt format mono type_enc
  1707                             should_guard_var_in_formula
  1708                             (if pos then SOME true else NONE)
  1709    |> bound_tvars type_enc atomic_types
  1710    |> close_formula_universally,
  1711    NONE,
  1712    case locality of
  1713      Intro => isabelle_info introN
  1714    | Elim => isabelle_info elimN
  1715    | Simp => isabelle_info simpN
  1716    | _ => NONE)
  1717   |> Formula
  1718 
  1719 fun formula_line_for_class_rel_clause ({name, subclass, superclass, ...}
  1720                                        : class_rel_clause) =
  1721   let val ty_arg = ATerm (`I "T", []) in
  1722     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
  1723              AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
  1724                                AAtom (ATerm (superclass, [ty_arg]))])
  1725              |> close_formula_universally, isabelle_info introN, NONE)
  1726   end
  1727 
  1728 fun fo_literal_from_arity_literal (TConsLit (c, t, args)) =
  1729     (true, ATerm (c, [ATerm (t, map (fn arg => ATerm (arg, [])) args)]))
  1730   | fo_literal_from_arity_literal (TVarLit (c, sort)) =
  1731     (false, ATerm (c, [ATerm (sort, [])]))
  1732 
  1733 fun formula_line_for_arity_clause ({name, prem_lits, concl_lits, ...}
  1734                                    : arity_clause) =
  1735   Formula (arity_clause_prefix ^ name, Axiom,
  1736            mk_ahorn (map (formula_from_fo_literal o apfst not
  1737                           o fo_literal_from_arity_literal) prem_lits)
  1738                     (formula_from_fo_literal
  1739                          (fo_literal_from_arity_literal concl_lits))
  1740            |> close_formula_universally, isabelle_info introN, NONE)
  1741 
  1742 fun formula_line_for_conjecture ctxt format mono type_enc
  1743         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
  1744   Formula (conjecture_prefix ^ name, kind,
  1745            formula_from_iformula ctxt format mono type_enc
  1746                should_guard_var_in_formula (SOME false)
  1747                (close_iformula_universally iformula)
  1748            |> bound_tvars type_enc atomic_types
  1749            |> close_formula_universally, NONE, NONE)
  1750 
  1751 fun free_type_literals type_enc ({atomic_types, ...} : translated_formula) =
  1752   atomic_types |> type_literals_for_types type_enc add_sorts_on_tfree
  1753                |> map fo_literal_from_type_literal
  1754 
  1755 fun formula_line_for_free_type j lit =
  1756   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis,
  1757            formula_from_fo_literal lit, NONE, NONE)
  1758 fun formula_lines_for_free_types type_enc facts =
  1759   let
  1760     val litss = map (free_type_literals type_enc) facts
  1761     val lits = fold (union (op =)) litss []
  1762   in map2 formula_line_for_free_type (0 upto length lits - 1) lits end
  1763 
  1764 (** Symbol declarations **)
  1765 
  1766 fun should_declare_sym type_enc pred_sym s =
  1767   (case type_enc of
  1768      Guards _ => not pred_sym
  1769    | _ => true) andalso
  1770   is_tptp_user_symbol s
  1771 
  1772 fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
  1773                              (conjs, facts) =
  1774   let
  1775     fun add_iterm_syms in_conj tm =
  1776       let val (head, args) = strip_iterm_comb tm in
  1777         (case head of
  1778            IConst ((s, s'), T, T_args) =>
  1779            let val pred_sym = is_pred_sym repaired_sym_tab s in
  1780              if should_declare_sym type_enc pred_sym s then
  1781                Symtab.map_default (s, [])
  1782                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
  1783                                          in_conj))
  1784              else
  1785                I
  1786            end
  1787          | IAbs (_, tm) => add_iterm_syms in_conj tm
  1788          | _ => I)
  1789         #> fold (add_iterm_syms in_conj) args
  1790       end
  1791     fun add_fact_syms in_conj =
  1792       K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
  1793     fun add_formula_var_types (AQuant (_, xs, phi)) =
  1794         fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
  1795         #> add_formula_var_types phi
  1796       | add_formula_var_types (AConn (_, phis)) =
  1797         fold add_formula_var_types phis
  1798       | add_formula_var_types _ = I
  1799     fun var_types () =
  1800       if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
  1801       else fold (fact_lift add_formula_var_types) (conjs @ facts) []
  1802     fun add_undefined_const T =
  1803       let
  1804         val (s, s') =
  1805           `(make_fixed_const (SOME format)) @{const_name undefined}
  1806           |> (case type_arg_policy type_enc @{const_name undefined} of
  1807                 Mangled_Type_Args _ => mangled_const_name format type_enc [T]
  1808               | _ => I)
  1809       in
  1810         Symtab.map_default (s, [])
  1811                            (insert_type ctxt #3 (s', [T], T, false, 0, false))
  1812       end
  1813   in
  1814     Symtab.empty
  1815     |> is_type_enc_fairly_sound type_enc
  1816        ? (fold (add_fact_syms true) conjs
  1817           #> fold (add_fact_syms false) facts
  1818           #> (case type_enc of
  1819                 Simple_Types _ => I
  1820               | _ => fold add_undefined_const (var_types ())))
  1821   end
  1822 
  1823 (* We add "bool" in case the helper "True_or_False" is included later. *)
  1824 val default_mono =
  1825   {maybe_finite_Ts = [@{typ bool}],
  1826    surely_finite_Ts = [@{typ bool}],
  1827    maybe_infinite_Ts = known_infinite_types,
  1828    surely_infinite_Ts = known_infinite_types,
  1829    maybe_nonmono_Ts = [@{typ bool}]}
  1830 
  1831 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  1832    out with monotonicity" paper presented at CADE 2011. *)
  1833 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
  1834   | add_iterm_mononotonicity_info ctxt level _
  1835         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
  1836         (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
  1837                   surely_infinite_Ts, maybe_nonmono_Ts}) =
  1838     if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
  1839       case level of
  1840         Noninf_Nonmono_Types soundness =>
  1841         if exists (type_instance ctxt T) surely_infinite_Ts orelse
  1842            member (type_aconv ctxt) maybe_finite_Ts T then
  1843           mono
  1844         else if is_type_kind_of_surely_infinite ctxt soundness
  1845                                                 surely_infinite_Ts T then
  1846           {maybe_finite_Ts = maybe_finite_Ts,
  1847            surely_finite_Ts = surely_finite_Ts,
  1848            maybe_infinite_Ts = maybe_infinite_Ts,
  1849            surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
  1850            maybe_nonmono_Ts = maybe_nonmono_Ts}
  1851         else
  1852           {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
  1853            surely_finite_Ts = surely_finite_Ts,
  1854            maybe_infinite_Ts = maybe_infinite_Ts,
  1855            surely_infinite_Ts = surely_infinite_Ts,
  1856            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
  1857       | Fin_Nonmono_Types =>
  1858         if exists (type_instance ctxt T) surely_finite_Ts orelse
  1859            member (type_aconv ctxt) maybe_infinite_Ts T then
  1860           mono
  1861         else if is_type_surely_finite ctxt T then
  1862           {maybe_finite_Ts = maybe_finite_Ts,
  1863            surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
  1864            maybe_infinite_Ts = maybe_infinite_Ts,
  1865            surely_infinite_Ts = surely_infinite_Ts,
  1866            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
  1867         else
  1868           {maybe_finite_Ts = maybe_finite_Ts,
  1869            surely_finite_Ts = surely_finite_Ts,
  1870            maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
  1871            surely_infinite_Ts = surely_infinite_Ts,
  1872            maybe_nonmono_Ts = maybe_nonmono_Ts}
  1873       | _ => mono
  1874     else
  1875       mono
  1876   | add_iterm_mononotonicity_info _ _ _ _ mono = mono
  1877 fun add_fact_mononotonicity_info ctxt level
  1878         ({kind, iformula, ...} : translated_formula) =
  1879   formula_fold (SOME (kind <> Conjecture))
  1880                (add_iterm_mononotonicity_info ctxt level) iformula
  1881 fun mononotonicity_info_for_facts ctxt type_enc facts =
  1882   let val level = level_of_type_enc type_enc in
  1883     default_mono
  1884     |> is_type_level_monotonicity_based level
  1885        ? fold (add_fact_mononotonicity_info ctxt level) facts
  1886   end
  1887 
  1888 fun add_iformula_monotonic_types ctxt mono type_enc =
  1889   let
  1890     val level = level_of_type_enc type_enc
  1891     val should_encode = should_encode_type ctxt mono level
  1892     fun add_type T = should_encode T ? insert_type ctxt I T
  1893     fun add_term (tm as IApp (tm1, tm2)) =
  1894         add_type (ityp_of tm) #> add_term tm1 #> add_term tm2
  1895       | add_term tm = add_type (ityp_of tm)
  1896   in formula_fold NONE (K add_term) end
  1897 fun add_fact_monotonic_types ctxt mono type_enc =
  1898   add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
  1899 fun monotonic_types_for_facts ctxt mono type_enc facts =
  1900   [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
  1901          is_type_level_monotonicity_based (level_of_type_enc type_enc))
  1902         ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
  1903 
  1904 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
  1905   Formula (guards_sym_formula_prefix ^
  1906            ascii_of (mangled_type format type_enc T),
  1907            Axiom,
  1908            IConst (`make_bound_var "X", T, [])
  1909            |> type_guard_iterm ctxt format type_enc T
  1910            |> AAtom
  1911            |> formula_from_iformula ctxt format mono type_enc
  1912                                     (K (K (K (K true)))) (SOME true)
  1913            |> bound_tvars type_enc (atyps_of T)
  1914            |> close_formula_universally,
  1915            isabelle_info introN, NONE)
  1916 
  1917 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
  1918   let val x_var = ATerm (`make_bound_var "X", []) in
  1919     Formula (tags_sym_formula_prefix ^
  1920              ascii_of (mangled_type format type_enc T),
  1921              Axiom,
  1922              eq_formula type_enc (atyps_of T) false
  1923                         (tag_with_type ctxt format mono type_enc NONE T x_var)
  1924                         x_var,
  1925              isabelle_info simpN, NONE)
  1926   end
  1927 
  1928 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
  1929   case type_enc of
  1930     Simple_Types _ => []
  1931   | Guards _ =>
  1932     map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
  1933   | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
  1934 
  1935 fun decl_line_for_sym ctxt format mono type_enc s
  1936                       (s', T_args, T, pred_sym, ary, _) =
  1937   let
  1938     val (T_arg_Ts, level) =
  1939       case type_enc of
  1940         Simple_Types (_, level) => ([], level)
  1941       | _ => (replicate (length T_args) homo_infinite_type, No_Types)
  1942   in
  1943     Decl (sym_decl_prefix ^ s, (s, s'),
  1944           (T_arg_Ts ---> (T |> homogenized_type ctxt mono level ary))
  1945           |> ho_type_from_typ format type_enc pred_sym (length T_arg_Ts + ary))
  1946   end
  1947 
  1948 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
  1949                                      j (s', T_args, T, _, ary, in_conj) =
  1950   let
  1951     val (kind, maybe_negate) =
  1952       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  1953       else (Axiom, I)
  1954     val (arg_Ts, res_T) = chop_fun ary T
  1955     val num_args = length arg_Ts
  1956     val bound_names =
  1957       1 upto num_args |> map (`I o make_bound_var o string_of_int)
  1958     val bounds =
  1959       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
  1960     val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
  1961     fun should_keep_arg_type T =
  1962       sym_needs_arg_types andalso
  1963       should_guard_type ctxt mono type_enc (K true) T
  1964     val bound_Ts =
  1965       arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
  1966   in
  1967     Formula (guards_sym_formula_prefix ^ s ^
  1968              (if n > 1 then "_" ^ string_of_int j else ""), kind,
  1969              IConst ((s, s'), T, T_args)
  1970              |> fold (curry (IApp o swap)) bounds
  1971              |> type_guard_iterm ctxt format type_enc res_T
  1972              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  1973              |> formula_from_iformula ctxt format mono type_enc
  1974                                       (K (K (K (K true)))) (SOME true)
  1975              |> n > 1 ? bound_tvars type_enc (atyps_of T)
  1976              |> close_formula_universally
  1977              |> maybe_negate,
  1978              isabelle_info introN, NONE)
  1979   end
  1980 
  1981 fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
  1982         type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  1983   let
  1984     val ident_base =
  1985       tags_sym_formula_prefix ^ s ^
  1986       (if n > 1 then "_" ^ string_of_int j else "")
  1987     val (kind, maybe_negate) =
  1988       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  1989       else (Axiom, I)
  1990     val (arg_Ts, res_T) = chop_fun ary T
  1991     val bound_names =
  1992       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
  1993     val bounds = bound_names |> map (fn name => ATerm (name, []))
  1994     val cst = mk_aterm format type_enc (s, s') T_args
  1995     val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
  1996     val should_encode =
  1997       should_encode_type ctxt mono (level_of_type_enc type_enc)
  1998     val tag_with = tag_with_type ctxt format mono type_enc NONE
  1999     val add_formula_for_res =
  2000       if should_encode res_T then
  2001         cons (Formula (ident_base ^ "_res", kind,
  2002                        eq (tag_with res_T (cst bounds)) (cst bounds),
  2003                        isabelle_info simpN, NONE))
  2004       else
  2005         I
  2006     fun add_formula_for_arg k =
  2007       let val arg_T = nth arg_Ts k in
  2008         if should_encode arg_T then
  2009           case chop k bounds of
  2010             (bounds1, bound :: bounds2) =>
  2011             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
  2012                            eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
  2013                               (cst bounds),
  2014                            isabelle_info simpN, NONE))
  2015           | _ => raise Fail "expected nonempty tail"
  2016         else
  2017           I
  2018       end
  2019   in
  2020     [] |> not pred_sym ? add_formula_for_res
  2021        |> Config.get ctxt type_tag_arguments
  2022           ? fold add_formula_for_arg (ary - 1 downto 0)
  2023   end
  2024 
  2025 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
  2026 
  2027 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
  2028                                 (s, decls) =
  2029   case type_enc of
  2030     Simple_Types _ =>
  2031     decls |> map (decl_line_for_sym ctxt format mono type_enc s)
  2032   | Guards (_, level, _) =>
  2033     let
  2034       val decls =
  2035         case decls of
  2036           decl :: (decls' as _ :: _) =>
  2037           let val T = result_type_of_decl decl in
  2038             if forall (type_generalization ctxt T o result_type_of_decl)
  2039                       decls' then
  2040               [decl]
  2041             else
  2042               decls
  2043           end
  2044         | _ => decls
  2045       val n = length decls
  2046       val decls =
  2047         decls |> filter (should_encode_type ctxt mono level
  2048                          o result_type_of_decl)
  2049     in
  2050       (0 upto length decls - 1, decls)
  2051       |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
  2052                                                  type_enc n s)
  2053     end
  2054   | Tags (_, _, uniformity) =>
  2055     (case uniformity of
  2056        Uniform => []
  2057      | Nonuniform =>
  2058        let val n = length decls in
  2059          (0 upto n - 1 ~~ decls)
  2060          |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
  2061                       conj_sym_kind mono type_enc n s)
  2062        end)
  2063 
  2064 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
  2065                                      mono_Ts sym_decl_tab =
  2066   let
  2067     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
  2068     val mono_lines =
  2069       problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
  2070     val decl_lines =
  2071       fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
  2072                                                      mono type_enc)
  2073                syms []
  2074   in mono_lines @ decl_lines end
  2075 
  2076 fun needs_type_tag_idempotence ctxt (Tags (poly, level, uniformity)) =
  2077     Config.get ctxt type_tag_idempotence andalso
  2078     poly <> Mangled_Monomorphic andalso
  2079     ((level = All_Types andalso uniformity = Nonuniform) orelse
  2080      is_type_level_monotonicity_based level)
  2081   | needs_type_tag_idempotence _ _ = false
  2082 
  2083 fun offset_of_heading_in_problem _ [] j = j
  2084   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
  2085     if heading = needle then j
  2086     else offset_of_heading_in_problem needle problem (j + length lines)
  2087 
  2088 val implicit_declsN = "Should-be-implicit typings"
  2089 val explicit_declsN = "Explicit typings"
  2090 val factsN = "Relevant facts"
  2091 val class_relsN = "Class relationships"
  2092 val aritiesN = "Arities"
  2093 val helpersN = "Helper facts"
  2094 val conjsN = "Conjectures"
  2095 val free_typesN = "Type variables"
  2096 
  2097 val explicit_apply = NONE (* for experiments *)
  2098 
  2099 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
  2100         lambda_trans readable_names preproc hyp_ts concl_t facts =
  2101   let
  2102     val type_enc = type_enc |> adjust_type_enc format
  2103     val lambda_trans =
  2104       if lambda_trans = smartN then
  2105         if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
  2106       else if lambda_trans = lambdasN andalso
  2107               not (is_type_enc_higher_order type_enc) then
  2108         error ("Lambda translation method incompatible with first-order \
  2109                \encoding.")
  2110       else
  2111         lambda_trans
  2112     val trans_lambdas =
  2113       if lambda_trans = no_lambdasN then
  2114         rpair []
  2115       else if lambda_trans = concealedN then
  2116         lift_lambdas ctxt type_enc ##> K []
  2117       else if lambda_trans = liftingN then
  2118         lift_lambdas ctxt type_enc
  2119       else if lambda_trans = combinatorsN then
  2120         map (introduce_combinators ctxt) #> rpair []
  2121       else if lambda_trans = hybridN then
  2122         lift_lambdas ctxt type_enc
  2123         ##> maps (fn t => [t, introduce_combinators ctxt
  2124                                   (intentionalize_def t)])
  2125       else if lambda_trans = lambdasN then
  2126         map (Envir.eta_contract) #> rpair []
  2127       else
  2128         error ("Unknown lambda translation method: " ^
  2129                quote lambda_trans ^ ".")
  2130     val (fact_names, (conjs, facts, class_rel_clauses, arity_clauses)) =
  2131       translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
  2132                          hyp_ts concl_t facts
  2133     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
  2134     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
  2135     val repair = repair_fact ctxt format type_enc sym_tab
  2136     val (conjs, facts) = (conjs, facts) |> pairself (map repair)
  2137     val repaired_sym_tab =
  2138       conjs @ facts |> sym_table_for_facts ctxt (SOME false)
  2139     val helpers =
  2140       repaired_sym_tab |> helper_facts_for_sym_table ctxt format type_enc
  2141                        |> map repair
  2142     val mono_Ts =
  2143       helpers @ conjs @ facts
  2144       |> monotonic_types_for_facts ctxt mono type_enc
  2145     val sym_decl_lines =
  2146       (conjs, helpers @ facts)
  2147       |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
  2148       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
  2149                                                type_enc mono_Ts
  2150     val helper_lines =
  2151       0 upto length helpers - 1 ~~ helpers
  2152       |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
  2153                                     type_enc)
  2154       |> (if needs_type_tag_idempotence ctxt type_enc then
  2155             cons (type_tag_idempotence_fact type_enc)
  2156           else
  2157             I)
  2158     (* Reordering these might confuse the proof reconstruction code or the SPASS
  2159        FLOTTER hack. *)
  2160     val problem =
  2161       [(explicit_declsN, sym_decl_lines),
  2162        (factsN,
  2163         map (formula_line_for_fact ctxt format fact_prefix ascii_of
  2164                                    (not exporter) (not exporter) mono
  2165                                    type_enc)
  2166             (0 upto length facts - 1 ~~ facts)),
  2167        (class_relsN, map formula_line_for_class_rel_clause class_rel_clauses),
  2168        (aritiesN, map formula_line_for_arity_clause arity_clauses),
  2169        (helpersN, helper_lines),
  2170        (conjsN,
  2171         map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
  2172        (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
  2173     val problem =
  2174       problem
  2175       |> (case format of
  2176             CNF => ensure_cnf_problem
  2177           | CNF_UEQ => filter_cnf_ueq_problem
  2178           | _ => I)
  2179       |> (if is_format_typed format then
  2180             declare_undeclared_syms_in_atp_problem type_decl_prefix
  2181                                                    implicit_declsN
  2182           else
  2183             I)
  2184     val (problem, pool) = problem |> nice_atp_problem readable_names
  2185     val helpers_offset = offset_of_heading_in_problem helpersN problem 0
  2186     val typed_helpers =
  2187       map_filter (fn (j, {name, ...}) =>
  2188                      if String.isSuffix typed_helper_suffix name then SOME j
  2189                      else NONE)
  2190                  ((helpers_offset + 1 upto helpers_offset + length helpers)
  2191                   ~~ helpers)
  2192     fun add_sym_arity (s, {min_ary, ...} : sym_info) =
  2193       if min_ary > 0 then
  2194         case strip_prefix_and_unascii const_prefix s of
  2195           SOME s => Symtab.insert (op =) (s, min_ary)
  2196         | NONE => I
  2197       else
  2198         I
  2199   in
  2200     (problem,
  2201      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  2202      offset_of_heading_in_problem conjsN problem 0,
  2203      offset_of_heading_in_problem factsN problem 0,
  2204      fact_names |> Vector.fromList,
  2205      typed_helpers,
  2206      Symtab.empty |> Symtab.fold add_sym_arity sym_tab)
  2207   end
  2208 
  2209 (* FUDGE *)
  2210 val conj_weight = 0.0
  2211 val hyp_weight = 0.1
  2212 val fact_min_weight = 0.2
  2213 val fact_max_weight = 1.0
  2214 val type_info_default_weight = 0.8
  2215 
  2216 fun add_term_weights weight (ATerm (s, tms)) =
  2217     is_tptp_user_symbol s ? Symtab.default (s, weight)
  2218     #> fold (add_term_weights weight) tms
  2219   | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
  2220 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
  2221     formula_fold NONE (K (add_term_weights weight)) phi
  2222   | add_problem_line_weights _ _ = I
  2223 
  2224 fun add_conjectures_weights [] = I
  2225   | add_conjectures_weights conjs =
  2226     let val (hyps, conj) = split_last conjs in
  2227       add_problem_line_weights conj_weight conj
  2228       #> fold (add_problem_line_weights hyp_weight) hyps
  2229     end
  2230 
  2231 fun add_facts_weights facts =
  2232   let
  2233     val num_facts = length facts
  2234     fun weight_of j =
  2235       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  2236                         / Real.fromInt num_facts
  2237   in
  2238     map weight_of (0 upto num_facts - 1) ~~ facts
  2239     |> fold (uncurry add_problem_line_weights)
  2240   end
  2241 
  2242 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  2243 fun atp_problem_weights problem =
  2244   let val get = these o AList.lookup (op =) problem in
  2245     Symtab.empty
  2246     |> add_conjectures_weights (get free_typesN @ get conjsN)
  2247     |> add_facts_weights (get factsN)
  2248     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
  2249             [explicit_declsN, class_relsN, aritiesN]
  2250     |> Symtab.dest
  2251     |> sort (prod_ord Real.compare string_ord o pairself swap)
  2252   end
  2253 
  2254 end;