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