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