src/HOL/Tools/ATP/atp_translate.ML
author blanchet
Wed Sep 07 13:50:17 2011 +0200 (2011-09-07)
changeset 44783 3634c6dba23f
parent 44782 ba4c0205267f
child 44785 f4975fa4a2f8
permissions -rw-r--r--
tuning
     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 heaviness = Heavy | Ann_Light | Arg_Light
    24   datatype type_level =
    25     All_Types |
    26     Noninf_Nonmono_Types of soundness * heaviness |
    27     Fin_Nonmono_Types of heaviness |
    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 heaviness = Heavy | Ann_Light | Arg_Light
   534 datatype type_level =
   535   All_Types |
   536   Noninf_Nonmono_Types of soundness * heaviness |
   537   Fin_Nonmono_Types of heaviness |
   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 heaviness_of_level (Noninf_Nonmono_Types (_, heaviness)) = heaviness
   558   | heaviness_of_level (Fin_Nonmono_Types heaviness) = heaviness
   559   | heaviness_of_level _ = Heavy
   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 fun try_unsuffixes ss s =
   575   fold (fn s' => fn NONE => try (unsuffix s') s | some => some) ss NONE
   576 
   577 val queries = ["?", "_query"]
   578 val bangs = ["!", "_bang"]
   579 
   580 fun type_enc_from_string soundness s =
   581   (case try (unprefix "poly_") s of
   582      SOME s => (SOME Polymorphic, s)
   583    | NONE =>
   584      case try (unprefix "raw_mono_") s of
   585        SOME s => (SOME Raw_Monomorphic, s)
   586      | NONE =>
   587        case try (unprefix "mono_") s of
   588          SOME s => (SOME Mangled_Monomorphic, s)
   589        | NONE => (NONE, s))
   590   ||> (fn s =>
   591           (* "_query" and "_bang" are for the ASCII-challenged Metis and
   592              Mirabelle. *)
   593           case try_unsuffixes queries s of
   594             SOME s =>
   595             (case try_unsuffixes queries s of
   596                SOME s => (Noninf_Nonmono_Types (soundness, Ann_Light), s)
   597              | NONE => (Noninf_Nonmono_Types (soundness, Heavy), s))
   598           | NONE =>
   599             case try_unsuffixes bangs s of
   600               SOME s =>
   601               (case try_unsuffixes bangs s of
   602                  SOME s => (Fin_Nonmono_Types Ann_Light, s)
   603                | NONE => (Fin_Nonmono_Types Heavy, s))
   604             | NONE => (All_Types, s))
   605   |> (fn (poly, (level, core)) =>
   606          case (core, (poly, level)) of
   607            ("simple", (SOME poly, _)) =>
   608            (case (poly, level) of
   609               (Polymorphic, All_Types) =>
   610               Simple_Types (First_Order, Polymorphic, All_Types)
   611             | (Mangled_Monomorphic, _) =>
   612               if heaviness_of_level level = Heavy then
   613                 Simple_Types (First_Order, Mangled_Monomorphic, level)
   614               else
   615                 raise Same.SAME
   616             | _ => raise Same.SAME)
   617          | ("simple_higher", (SOME poly, _)) =>
   618            (case (poly, level) of
   619               (Polymorphic, All_Types) =>
   620               Simple_Types (Higher_Order, Polymorphic, All_Types)
   621             | (_, Noninf_Nonmono_Types _) => raise Same.SAME
   622             | (Mangled_Monomorphic, _) =>
   623               if heaviness_of_level level = Heavy then
   624                 Simple_Types (Higher_Order, Mangled_Monomorphic, level)
   625               else
   626                 raise Same.SAME
   627             | _ => raise Same.SAME)
   628          | ("guards", (SOME poly, _)) => Guards (poly, level)
   629          | ("tags", (SOME Polymorphic, _)) => Tags (Polymorphic, level)
   630          | ("tags", (SOME poly, _)) => Tags (poly, level)
   631          | ("args", (SOME poly, All_Types (* naja *))) =>
   632            Guards (poly, Const_Arg_Types)
   633          | ("erased", (NONE, All_Types (* naja *))) =>
   634            Guards (Polymorphic, No_Types)
   635          | _ => raise Same.SAME)
   636   handle Same.SAME => error ("Unknown type system: " ^ quote s ^ ".")
   637 
   638 fun adjust_type_enc (THF (TPTP_Monomorphic, _, _))
   639                     (Simple_Types (order, _, level)) =
   640     Simple_Types (order, Mangled_Monomorphic, level)
   641   | adjust_type_enc (THF _) type_enc = type_enc
   642   | adjust_type_enc (TFF (TPTP_Monomorphic, _)) (Simple_Types (_, _, level)) =
   643     Simple_Types (First_Order, Mangled_Monomorphic, level)
   644   | adjust_type_enc (TFF _) (Simple_Types (_, poly, level)) =
   645     Simple_Types (First_Order, poly, level)
   646   | adjust_type_enc format (Simple_Types (_, poly, level)) =
   647     adjust_type_enc format (Guards (poly, level))
   648   | adjust_type_enc CNF_UEQ (type_enc as Guards stuff) =
   649     (if is_type_enc_fairly_sound type_enc then Tags else Guards) stuff
   650   | adjust_type_enc _ type_enc = type_enc
   651 
   652 fun lift_lambdas ctxt type_enc =
   653   map (close_form o Envir.eta_contract) #> rpair ctxt
   654   #-> Lambda_Lifting.lift_lambdas
   655           (if polymorphism_of_type_enc type_enc = Polymorphic then
   656              SOME polymorphic_free_prefix
   657            else
   658              NONE)
   659           Lambda_Lifting.is_quantifier
   660   #> fst
   661 
   662 fun intentionalize_def (Const (@{const_name All}, _) $ Abs (_, _, t)) =
   663     intentionalize_def t
   664   | intentionalize_def (Const (@{const_name HOL.eq}, _) $ t $ u) =
   665     let
   666       fun lam T t = Abs (Name.uu, T, t)
   667       val (head, args) = strip_comb t ||> rev
   668       val head_T = fastype_of head
   669       val n = length args
   670       val arg_Ts = head_T |> binder_types |> take n |> rev
   671       val u = u |> subst_atomic (args ~~ map Bound (0 upto n - 1))
   672     in HOLogic.eq_const head_T $ head $ fold lam arg_Ts u end
   673   | intentionalize_def t = t
   674 
   675 type translated_formula =
   676   {name : string,
   677    locality : locality,
   678    kind : formula_kind,
   679    iformula : (name, typ, iterm) formula,
   680    atomic_types : typ list}
   681 
   682 fun update_iformula f ({name, locality, kind, iformula, atomic_types}
   683                        : translated_formula) =
   684   {name = name, locality = locality, kind = kind, iformula = f iformula,
   685    atomic_types = atomic_types} : translated_formula
   686 
   687 fun fact_lift f ({iformula, ...} : translated_formula) = f iformula
   688 
   689 fun insert_type ctxt get_T x xs =
   690   let val T = get_T x in
   691     if exists (type_instance ctxt T o get_T) xs then xs
   692     else x :: filter_out (type_generalization ctxt T o get_T) xs
   693   end
   694 
   695 (* The Booleans indicate whether all type arguments should be kept. *)
   696 datatype type_arg_policy =
   697   Explicit_Type_Args of bool |
   698   Mangled_Type_Args |
   699   No_Type_Args
   700 
   701 fun should_drop_arg_type_args (Simple_Types _) = false
   702   | should_drop_arg_type_args type_enc =
   703     level_of_type_enc type_enc = All_Types
   704 
   705 fun type_arg_policy type_enc s =
   706   let val mangled = (polymorphism_of_type_enc type_enc = Mangled_Monomorphic) in
   707     if s = type_tag_name then
   708       if mangled then Mangled_Type_Args else Explicit_Type_Args false
   709     else case type_enc of
   710       Tags (_, All_Types) => No_Type_Args
   711     | _ =>
   712       let val level = level_of_type_enc type_enc in
   713         if level = No_Types orelse s = @{const_name HOL.eq} orelse
   714            (s = app_op_name andalso level = Const_Arg_Types) then
   715           No_Type_Args
   716         else if mangled then
   717           Mangled_Type_Args
   718         else
   719           Explicit_Type_Args (should_drop_arg_type_args type_enc)
   720       end
   721   end
   722 
   723 (* Make atoms for sorted type variables. *)
   724 fun generic_add_sorts_on_type (_, []) = I
   725   | generic_add_sorts_on_type ((x, i), s :: ss) =
   726     generic_add_sorts_on_type ((x, i), ss)
   727     #> (if s = the_single @{sort HOL.type} then
   728           I
   729         else if i = ~1 then
   730           insert (op =) (`make_type_class s, `make_fixed_type_var x)
   731         else
   732           insert (op =) (`make_type_class s,
   733                          (make_schematic_type_var (x, i), x)))
   734 fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
   735   | add_sorts_on_tfree _ = I
   736 fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
   737   | add_sorts_on_tvar _ = I
   738 
   739 val tvar_a_str = "'a"
   740 val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
   741 val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
   742 val itself_name = `make_fixed_type_const @{type_name itself}
   743 val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
   744 val tvar_a_atype = AType (tvar_a_name, [])
   745 val a_itself_atype = AType (itself_name, [tvar_a_atype])
   746 
   747 fun type_class_formula type_enc class arg =
   748   AAtom (ATerm (class, arg ::
   749       (case type_enc of
   750          Simple_Types (First_Order, Polymorphic, _) =>
   751          if avoid_first_order_dummy_type_vars then [ATerm (TYPE_name, [arg])]
   752          else []
   753        | _ => [])))
   754 fun formulas_for_types type_enc add_sorts_on_typ Ts =
   755   [] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
   756      |> map (fn (class, name) =>
   757                 type_class_formula type_enc class (ATerm (name, [])))
   758 
   759 fun mk_aconns c phis =
   760   let val (phis', phi') = split_last phis in
   761     fold_rev (mk_aconn c) phis' phi'
   762   end
   763 fun mk_ahorn [] phi = phi
   764   | mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
   765 fun mk_aquant _ [] phi = phi
   766   | mk_aquant q xs (phi as AQuant (q', xs', phi')) =
   767     if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
   768   | mk_aquant q xs phi = AQuant (q, xs, phi)
   769 
   770 fun close_universally atom_vars phi =
   771   let
   772     fun formula_vars bounds (AQuant (_, xs, phi)) =
   773         formula_vars (map fst xs @ bounds) phi
   774       | formula_vars bounds (AConn (_, phis)) = fold (formula_vars bounds) phis
   775       | formula_vars bounds (AAtom tm) =
   776         union (op =) (atom_vars tm []
   777                       |> filter_out (member (op =) bounds o fst))
   778   in mk_aquant AForall (formula_vars [] phi []) phi end
   779 
   780 fun iterm_vars (IApp (tm1, tm2)) = fold iterm_vars [tm1, tm2]
   781   | iterm_vars (IConst _) = I
   782   | iterm_vars (IVar (name, T)) = insert (op =) (name, SOME T)
   783   | iterm_vars (IAbs (_, tm)) = iterm_vars tm
   784 fun close_iformula_universally phi = close_universally iterm_vars phi
   785 
   786 fun term_vars type_enc =
   787   let
   788     fun vars bounds (ATerm (name as (s, _), tms)) =
   789         (if is_tptp_variable s andalso not (member (op =) bounds name) then
   790            (case type_enc of
   791               Simple_Types (_, Polymorphic, _) =>
   792               if String.isPrefix tvar_prefix s then SOME atype_of_types
   793               else NONE
   794             | _ => NONE)
   795            |> pair name |> insert (op =)
   796          else
   797            I)
   798         #> fold (vars bounds) tms
   799       | vars bounds (AAbs ((name, _), tm)) = vars (name :: bounds) tm
   800   in vars end
   801 fun close_formula_universally type_enc =
   802   close_universally (term_vars type_enc [])
   803 
   804 val fused_infinite_type_name = @{type_name ind} (* any infinite type *)
   805 val fused_infinite_type = Type (fused_infinite_type_name, [])
   806 
   807 fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
   808 
   809 fun ho_term_from_typ format type_enc =
   810   let
   811     fun term (Type (s, Ts)) =
   812       ATerm (case (is_type_enc_higher_order type_enc, s) of
   813                (true, @{type_name bool}) => `I tptp_bool_type
   814              | (true, @{type_name fun}) => `I tptp_fun_type
   815              | _ => if s = fused_infinite_type_name andalso
   816                        is_format_typed format then
   817                       `I tptp_individual_type
   818                     else
   819                       `make_fixed_type_const s,
   820              map term Ts)
   821     | term (TFree (s, _)) = ATerm (`make_fixed_type_var s, [])
   822     | term (TVar (x, _)) = ATerm (tvar_name x, [])
   823   in term end
   824 
   825 fun ho_term_for_type_arg format type_enc T =
   826   if T = dummyT then NONE else SOME (ho_term_from_typ format type_enc T)
   827 
   828 (* This shouldn't clash with anything else. *)
   829 val mangled_type_sep = "\000"
   830 
   831 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   832   | generic_mangled_type_name f (ATerm (name, tys)) =
   833     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
   834     ^ ")"
   835   | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
   836 
   837 fun mangled_type format type_enc =
   838   generic_mangled_type_name fst o ho_term_from_typ format type_enc
   839 
   840 fun make_simple_type s =
   841   if s = tptp_bool_type orelse s = tptp_fun_type orelse
   842      s = tptp_individual_type then
   843     s
   844   else
   845     simple_type_prefix ^ ascii_of s
   846 
   847 fun ho_type_from_ho_term type_enc pred_sym ary =
   848   let
   849     fun to_mangled_atype ty =
   850       AType ((make_simple_type (generic_mangled_type_name fst ty),
   851               generic_mangled_type_name snd ty), [])
   852     fun to_poly_atype (ATerm (name, tys)) = AType (name, map to_poly_atype tys)
   853       | to_poly_atype _ = raise Fail "unexpected type abstraction"
   854     val to_atype =
   855       if polymorphism_of_type_enc type_enc = Polymorphic then to_poly_atype
   856       else to_mangled_atype
   857     fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
   858     fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
   859       | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
   860       | to_fo _ _ = raise Fail "unexpected type abstraction"
   861     fun to_ho (ty as ATerm ((s, _), tys)) =
   862         if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
   863       | to_ho _ = raise Fail "unexpected type abstraction"
   864   in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
   865 
   866 fun ho_type_from_typ format type_enc pred_sym ary =
   867   ho_type_from_ho_term type_enc pred_sym ary
   868   o ho_term_from_typ format type_enc
   869 
   870 fun mangled_const_name format type_enc T_args (s, s') =
   871   let
   872     val ty_args = T_args |> map_filter (ho_term_for_type_arg format type_enc)
   873     fun type_suffix f g =
   874       fold_rev (curry (op ^) o g o prefix mangled_type_sep
   875                 o generic_mangled_type_name f) ty_args ""
   876   in (s ^ type_suffix fst ascii_of, s' ^ type_suffix snd I) end
   877 
   878 val parse_mangled_ident =
   879   Scan.many1 (not o member (op =) ["(", ")", ","]) >> implode
   880 
   881 fun parse_mangled_type x =
   882   (parse_mangled_ident
   883    -- Scan.optional ($$ "(" |-- Scan.optional parse_mangled_types [] --| $$ ")")
   884                     [] >> ATerm) x
   885 and parse_mangled_types x =
   886   (parse_mangled_type ::: Scan.repeat ($$ "," |-- parse_mangled_type)) x
   887 
   888 fun unmangled_type s =
   889   s |> suffix ")" |> raw_explode
   890     |> Scan.finite Symbol.stopper
   891            (Scan.error (!! (fn _ => raise Fail ("unrecognized mangled type " ^
   892                                                 quote s)) parse_mangled_type))
   893     |> fst
   894 
   895 val unmangled_const_name = space_explode mangled_type_sep #> hd
   896 fun unmangled_const s =
   897   let val ss = space_explode mangled_type_sep s in
   898     (hd ss, map unmangled_type (tl ss))
   899   end
   900 
   901 fun introduce_proxies_in_iterm type_enc =
   902   let
   903     fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
   904       | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _]))
   905                        _ =
   906         (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
   907            limitation. This works in conjuction with special code in
   908            "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
   909            possible. *)
   910         IAbs ((`I "P", p_T),
   911               IApp (IConst (`I ho_quant, T, []),
   912                     IAbs ((`I "X", x_T),
   913                           IApp (IConst (`I "P", p_T, []),
   914                                 IConst (`I "X", x_T, [])))))
   915       | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
   916     fun intro top_level args (IApp (tm1, tm2)) =
   917         IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
   918       | intro top_level args (IConst (name as (s, _), T, T_args)) =
   919         (case proxify_const s of
   920            SOME proxy_base =>
   921            if top_level orelse is_type_enc_higher_order type_enc then
   922              case (top_level, s) of
   923                (_, "c_False") => IConst (`I tptp_false, T, [])
   924              | (_, "c_True") => IConst (`I tptp_true, T, [])
   925              | (false, "c_Not") => IConst (`I tptp_not, T, [])
   926              | (false, "c_conj") => IConst (`I tptp_and, T, [])
   927              | (false, "c_disj") => IConst (`I tptp_or, T, [])
   928              | (false, "c_implies") => IConst (`I tptp_implies, T, [])
   929              | (false, "c_All") => tweak_ho_quant tptp_ho_forall T args
   930              | (false, "c_Ex") => tweak_ho_quant tptp_ho_exists T args
   931              | (false, s) =>
   932                if is_tptp_equal s andalso length args = 2 then
   933                  IConst (`I tptp_equal, T, [])
   934                else
   935                  (* Use a proxy even for partially applied THF0 equality,
   936                     because the LEO-II and Satallax parsers complain about not
   937                     being able to infer the type of "=". *)
   938                  IConst (proxy_base |>> prefix const_prefix, T, T_args)
   939              | _ => IConst (name, T, [])
   940            else
   941              IConst (proxy_base |>> prefix const_prefix, T, T_args)
   942           | NONE => if s = tptp_choice then
   943                       tweak_ho_quant tptp_choice T args
   944                     else
   945                       IConst (name, T, T_args))
   946       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
   947       | intro _ _ tm = tm
   948   in intro true [] end
   949 
   950 fun mangle_type_args_in_iterm format type_enc =
   951   if polymorphism_of_type_enc type_enc = Mangled_Monomorphic then
   952     let
   953       fun mangle (IApp (tm1, tm2)) = IApp (mangle tm1, mangle tm2)
   954         | mangle (tm as IConst (_, _, [])) = tm
   955         | mangle (tm as IConst (name as (s, _), T, T_args)) =
   956           (case strip_prefix_and_unascii const_prefix s of
   957              NONE => tm
   958            | SOME s'' =>
   959              case type_arg_policy type_enc (invert_const s'') of
   960                Mangled_Type_Args =>
   961                IConst (mangled_const_name format type_enc T_args name, T, [])
   962              | _ => tm)
   963         | mangle (IAbs (bound, tm)) = IAbs (bound, mangle tm)
   964         | mangle tm = tm
   965     in mangle end
   966   else
   967     I
   968 
   969 fun chop_fun 0 T = ([], T)
   970   | chop_fun n (Type (@{type_name fun}, [dom_T, ran_T])) =
   971     chop_fun (n - 1) ran_T |>> cons dom_T
   972   | chop_fun _ T = ([], T)
   973 
   974 fun filter_const_type_args _ _ _ [] = []
   975   | filter_const_type_args thy s ary T_args =
   976     let
   977       val U = robust_const_type thy s
   978       val arg_U_vars = fold Term.add_tvarsT (U |> chop_fun ary |> fst) []
   979       val U_args = (s, U) |> robust_const_typargs thy
   980     in
   981       U_args ~~ T_args
   982       |> map (fn (U, T) =>
   983                  if member (op =) arg_U_vars (dest_TVar U) then dummyT else T)
   984     end
   985     handle TYPE _ => T_args
   986 
   987 fun filter_type_args_in_iterm thy type_enc =
   988   let
   989     fun filt ary (IApp (tm1, tm2)) = IApp (filt (ary + 1) tm1, filt 0 tm2)
   990       | filt _ (tm as IConst (_, _, [])) = tm
   991       | filt ary (IConst (name as (s, _), T, T_args)) =
   992         (case strip_prefix_and_unascii const_prefix s of
   993            NONE =>
   994            (name,
   995             if level_of_type_enc type_enc = No_Types orelse s = tptp_choice then
   996               []
   997             else
   998               T_args)
   999          | SOME s'' =>
  1000            let
  1001              val s'' = invert_const s''
  1002              fun filter_T_args false = T_args
  1003                | filter_T_args true = filter_const_type_args thy s'' ary T_args
  1004            in
  1005              case type_arg_policy type_enc s'' of
  1006                Explicit_Type_Args drop_args => (name, filter_T_args drop_args)
  1007              | No_Type_Args => (name, [])
  1008              | Mangled_Type_Args => raise Fail "unexpected (un)mangled symbol"
  1009            end)
  1010         |> (fn (name, T_args) => IConst (name, T, T_args))
  1011       | filt _ (IAbs (bound, tm)) = IAbs (bound, filt 0 tm)
  1012       | filt _ tm = tm
  1013   in filt 0 end
  1014 
  1015 fun iformula_from_prop ctxt format type_enc eq_as_iff =
  1016   let
  1017     val thy = Proof_Context.theory_of ctxt
  1018     fun do_term bs t atomic_types =
  1019       iterm_from_term thy format bs (Envir.eta_contract t)
  1020       |>> (introduce_proxies_in_iterm type_enc
  1021            #> mangle_type_args_in_iterm format type_enc
  1022            #> AAtom)
  1023       ||> union (op =) atomic_types
  1024     fun do_quant bs q pos s T t' =
  1025       let
  1026         val s = singleton (Name.variant_list (map fst bs)) s
  1027         val universal = Option.map (q = AExists ? not) pos
  1028         val name =
  1029           s |> `(case universal of
  1030                    SOME true => make_all_bound_var
  1031                  | SOME false => make_exist_bound_var
  1032                  | NONE => make_bound_var)
  1033       in
  1034         do_formula ((s, (name, T)) :: bs) pos t'
  1035         #>> mk_aquant q [(name, SOME T)]
  1036       end
  1037     and do_conn bs c pos1 t1 pos2 t2 =
  1038       do_formula bs pos1 t1 ##>> do_formula bs pos2 t2 #>> uncurry (mk_aconn c)
  1039     and do_formula bs pos t =
  1040       case t of
  1041         @{const Trueprop} $ t1 => do_formula bs pos t1
  1042       | @{const Not} $ t1 => do_formula bs (Option.map not pos) t1 #>> mk_anot
  1043       | Const (@{const_name All}, _) $ Abs (s, T, t') =>
  1044         do_quant bs AForall pos s T t'
  1045       | Const (@{const_name Ex}, _) $ Abs (s, T, t') =>
  1046         do_quant bs AExists pos s T t'
  1047       | @{const HOL.conj} $ t1 $ t2 => do_conn bs AAnd pos t1 pos t2
  1048       | @{const HOL.disj} $ t1 $ t2 => do_conn bs AOr pos t1 pos t2
  1049       | @{const HOL.implies} $ t1 $ t2 =>
  1050         do_conn bs AImplies (Option.map not pos) t1 pos t2
  1051       | Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])) $ t1 $ t2 =>
  1052         if eq_as_iff then do_conn bs AIff NONE t1 NONE t2 else do_term bs t
  1053       | _ => do_term bs t
  1054   in do_formula [] end
  1055 
  1056 fun presimplify_term _ [] t = t
  1057   | presimplify_term ctxt presimp_consts t =
  1058     t |> exists_Const (member (op =) presimp_consts o fst) t
  1059          ? (Skip_Proof.make_thm (Proof_Context.theory_of ctxt)
  1060             #> Meson.presimplify ctxt
  1061             #> prop_of)
  1062 
  1063 fun concealed_bound_name j = atp_weak_prefix ^ string_of_int j
  1064 fun conceal_bounds Ts t =
  1065   subst_bounds (map (Free o apfst concealed_bound_name)
  1066                     (0 upto length Ts - 1 ~~ Ts), t)
  1067 fun reveal_bounds Ts =
  1068   subst_atomic (map (fn (j, T) => (Free (concealed_bound_name j, T), Bound j))
  1069                     (0 upto length Ts - 1 ~~ Ts))
  1070 
  1071 fun is_fun_equality (@{const_name HOL.eq},
  1072                      Type (_, [Type (@{type_name fun}, _), _])) = true
  1073   | is_fun_equality _ = false
  1074 
  1075 fun extensionalize_term ctxt t =
  1076   if exists_Const is_fun_equality t then
  1077     let val thy = Proof_Context.theory_of ctxt in
  1078       t |> cterm_of thy |> Meson.extensionalize_conv ctxt
  1079         |> prop_of |> Logic.dest_equals |> snd
  1080     end
  1081   else
  1082     t
  1083 
  1084 fun simple_translate_lambdas do_lambdas ctxt t =
  1085   let val thy = Proof_Context.theory_of ctxt in
  1086     if Meson.is_fol_term thy t then
  1087       t
  1088     else
  1089       let
  1090         fun aux Ts t =
  1091           case t of
  1092             @{const Not} $ t1 => @{const Not} $ aux Ts t1
  1093           | (t0 as Const (@{const_name All}, _)) $ Abs (s, T, t') =>
  1094             t0 $ Abs (s, T, aux (T :: Ts) t')
  1095           | (t0 as Const (@{const_name All}, _)) $ t1 =>
  1096             aux Ts (t0 $ eta_expand Ts t1 1)
  1097           | (t0 as Const (@{const_name Ex}, _)) $ Abs (s, T, t') =>
  1098             t0 $ Abs (s, T, aux (T :: Ts) t')
  1099           | (t0 as Const (@{const_name Ex}, _)) $ t1 =>
  1100             aux Ts (t0 $ eta_expand Ts t1 1)
  1101           | (t0 as @{const HOL.conj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  1102           | (t0 as @{const HOL.disj}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  1103           | (t0 as @{const HOL.implies}) $ t1 $ t2 => t0 $ aux Ts t1 $ aux Ts t2
  1104           | (t0 as Const (@{const_name HOL.eq}, Type (_, [@{typ bool}, _])))
  1105               $ t1 $ t2 =>
  1106             t0 $ aux Ts t1 $ aux Ts t2
  1107           | _ =>
  1108             if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
  1109             else t |> Envir.eta_contract |> do_lambdas ctxt Ts
  1110         val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single
  1111       in t |> aux [] |> singleton (Variable.export_terms ctxt' ctxt) end
  1112   end
  1113 
  1114 fun do_cheaply_conceal_lambdas Ts (t1 $ t2) =
  1115     do_cheaply_conceal_lambdas Ts t1
  1116     $ do_cheaply_conceal_lambdas Ts t2
  1117   | do_cheaply_conceal_lambdas Ts (Abs (_, T, t)) =
  1118     Free (polymorphic_free_prefix ^ serial_string (),
  1119           T --> fastype_of1 (T :: Ts, t))
  1120   | do_cheaply_conceal_lambdas _ t = t
  1121 
  1122 fun do_introduce_combinators ctxt Ts t =
  1123   let val thy = Proof_Context.theory_of ctxt in
  1124     t |> conceal_bounds Ts
  1125       |> cterm_of thy
  1126       |> Meson_Clausify.introduce_combinators_in_cterm
  1127       |> prop_of |> Logic.dest_equals |> snd
  1128       |> reveal_bounds Ts
  1129   end
  1130   (* A type variable of sort "{}" will make abstraction fail. *)
  1131   handle THM _ => t |> do_cheaply_conceal_lambdas Ts
  1132 val introduce_combinators = simple_translate_lambdas do_introduce_combinators
  1133 
  1134 fun preprocess_abstractions_in_terms trans_lambdas facts =
  1135   let
  1136     val (facts, lambda_ts) =
  1137       facts |> map (snd o snd) |> trans_lambdas
  1138             |>> map2 (fn (name, (kind, _)) => fn t => (name, (kind, t))) facts
  1139     val lambda_facts =
  1140       map2 (fn t => fn j =>
  1141                ((lambda_fact_prefix ^ Int.toString j, Helper), (Axiom, t)))
  1142            lambda_ts (1 upto length lambda_ts)
  1143   in (facts, lambda_facts) end
  1144 
  1145 (* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
  1146    same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
  1147 fun freeze_term t =
  1148   let
  1149     fun aux (t $ u) = aux t $ aux u
  1150       | aux (Abs (s, T, t)) = Abs (s, T, aux t)
  1151       | aux (Var ((s, i), T)) =
  1152         Free (atp_weak_prefix ^ s ^ "_" ^ string_of_int i, T)
  1153       | aux t = t
  1154   in t |> exists_subterm is_Var t ? aux end
  1155 
  1156 fun presimp_prop ctxt presimp_consts t =
  1157   let
  1158     val thy = Proof_Context.theory_of ctxt
  1159     val t = t |> Envir.beta_eta_contract
  1160               |> transform_elim_prop
  1161               |> Object_Logic.atomize_term thy
  1162     val need_trueprop = (fastype_of t = @{typ bool})
  1163   in
  1164     t |> need_trueprop ? HOLogic.mk_Trueprop
  1165       |> Raw_Simplifier.rewrite_term thy (Meson.unfold_set_const_simps ctxt) []
  1166       |> extensionalize_term ctxt
  1167       |> presimplify_term ctxt presimp_consts
  1168       |> perhaps (try (HOLogic.dest_Trueprop))
  1169   end
  1170 
  1171 (* making fact and conjecture formulas *)
  1172 fun make_formula ctxt format type_enc eq_as_iff name loc kind t =
  1173   let
  1174     val (iformula, atomic_types) =
  1175       iformula_from_prop ctxt format type_enc eq_as_iff
  1176                          (SOME (kind <> Conjecture)) t []
  1177   in
  1178     {name = name, locality = loc, kind = kind, iformula = iformula,
  1179      atomic_types = atomic_types}
  1180   end
  1181 
  1182 fun make_fact ctxt format type_enc eq_as_iff ((name, loc), t) =
  1183   case t |> make_formula ctxt format type_enc (eq_as_iff andalso format <> CNF)
  1184                          name loc Axiom of
  1185     formula as {iformula = AAtom (IConst ((s, _), _, _)), ...} =>
  1186     if s = tptp_true then NONE else SOME formula
  1187   | formula => SOME formula
  1188 
  1189 fun s_not_trueprop (@{const Trueprop} $ t) = @{const Trueprop} $ s_not t
  1190   | s_not_trueprop t = s_not t
  1191 
  1192 fun make_conjecture ctxt format type_enc =
  1193   map (fn ((name, loc), (kind, t)) =>
  1194           t |> kind = Conjecture ? s_not_trueprop
  1195             |> make_formula ctxt format type_enc (format <> CNF) name loc kind)
  1196 
  1197 (** Finite and infinite type inference **)
  1198 
  1199 type monotonicity_info =
  1200   {maybe_finite_Ts : typ list,
  1201    surely_finite_Ts : typ list,
  1202    maybe_infinite_Ts : typ list,
  1203    surely_infinite_Ts : typ list,
  1204    maybe_nonmono_Ts : typ list}
  1205 
  1206 (* These types witness that the type classes they belong to allow infinite
  1207    models and hence that any types with these type classes is monotonic. *)
  1208 val known_infinite_types =
  1209   [@{typ nat}, HOLogic.intT, HOLogic.realT, @{typ "nat => bool"}]
  1210 
  1211 fun is_type_kind_of_surely_infinite ctxt soundness cached_Ts T =
  1212   soundness <> Sound andalso is_type_surely_infinite ctxt true cached_Ts T
  1213 
  1214 (* Finite types such as "unit", "bool", "bool * bool", and "bool => bool" are
  1215    dangerous because their "exhaust" properties can easily lead to unsound ATP
  1216    proofs. On the other hand, all HOL infinite types can be given the same
  1217    models in first-order logic (via Löwenheim-Skolem). *)
  1218 
  1219 fun should_encode_type _ (_ : monotonicity_info) All_Types _ = true
  1220   | should_encode_type ctxt {maybe_finite_Ts, surely_infinite_Ts,
  1221                              maybe_nonmono_Ts, ...}
  1222                        (Noninf_Nonmono_Types (soundness, _)) T =
  1223     exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  1224     not (exists (type_instance ctxt T) surely_infinite_Ts orelse
  1225          (not (member (type_aconv ctxt) maybe_finite_Ts T) andalso
  1226           is_type_kind_of_surely_infinite ctxt soundness surely_infinite_Ts T))
  1227   | should_encode_type ctxt {surely_finite_Ts, maybe_infinite_Ts,
  1228                              maybe_nonmono_Ts, ...}
  1229                        (Fin_Nonmono_Types _) T =
  1230     exists (type_intersect ctxt T) maybe_nonmono_Ts andalso
  1231     (exists (type_generalization ctxt T) surely_finite_Ts orelse
  1232      (not (member (type_aconv ctxt) maybe_infinite_Ts T) andalso
  1233       is_type_surely_finite ctxt T))
  1234   | should_encode_type _ _ _ _ = false
  1235 
  1236 fun should_guard_type ctxt mono (Guards (_, level)) should_guard_var T =
  1237     (heaviness_of_level level = Heavy orelse should_guard_var ()) andalso
  1238     should_encode_type ctxt mono level T
  1239   | should_guard_type _ _ _ _ _ = false
  1240 
  1241 fun is_maybe_universal_var (IConst ((s, _), _, _)) =
  1242     String.isPrefix bound_var_prefix s orelse
  1243     String.isPrefix all_bound_var_prefix s
  1244   | is_maybe_universal_var (IVar _) = true
  1245   | is_maybe_universal_var _ = false
  1246 
  1247 datatype tag_site =
  1248   Top_Level of bool option |
  1249   Eq_Arg of bool option |
  1250   Elsewhere
  1251 
  1252 fun should_tag_with_type _ _ _ (Top_Level _) _ _ = false
  1253   | should_tag_with_type ctxt mono (Tags (_, level)) site u T =
  1254     (if heaviness_of_level level = Heavy then
  1255        should_encode_type ctxt mono level T
  1256      else case (site, is_maybe_universal_var u) of
  1257        (Eq_Arg _, true) => should_encode_type ctxt mono level T
  1258      | _ => false)
  1259   | should_tag_with_type _ _ _ _ _ _ = false
  1260 
  1261 fun fused_type ctxt mono level =
  1262   let
  1263     val should_encode = should_encode_type ctxt mono level
  1264     fun fuse 0 T = if should_encode T then T else fused_infinite_type
  1265       | fuse ary (Type (@{type_name fun}, [T1, T2])) =
  1266         fuse 0 T1 --> fuse (ary - 1) T2
  1267       | fuse _ _ = raise Fail "expected function type"
  1268   in fuse end
  1269 
  1270 (** predicators and application operators **)
  1271 
  1272 type sym_info =
  1273   {pred_sym : bool, min_ary : int, max_ary : int, types : typ list}
  1274 
  1275 fun add_iterm_syms_to_table ctxt explicit_apply =
  1276   let
  1277     fun consider_var_ary const_T var_T max_ary =
  1278       let
  1279         fun iter ary T =
  1280           if ary = max_ary orelse type_instance ctxt var_T T orelse
  1281              type_instance ctxt T var_T then
  1282             ary
  1283           else
  1284             iter (ary + 1) (range_type T)
  1285       in iter 0 const_T end
  1286     fun add_universal_var T (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1287       if explicit_apply = NONE andalso
  1288          (can dest_funT T orelse T = @{typ bool}) then
  1289         let
  1290           val bool_vars' = bool_vars orelse body_type T = @{typ bool}
  1291           fun repair_min_ary {pred_sym, min_ary, max_ary, types} =
  1292             {pred_sym = pred_sym andalso not bool_vars',
  1293              min_ary = fold (fn T' => consider_var_ary T' T) types min_ary,
  1294              max_ary = max_ary, types = types}
  1295           val fun_var_Ts' =
  1296             fun_var_Ts |> can dest_funT T ? insert_type ctxt I T
  1297         in
  1298           if bool_vars' = bool_vars andalso
  1299              pointer_eq (fun_var_Ts', fun_var_Ts) then
  1300             accum
  1301           else
  1302             ((bool_vars', fun_var_Ts'), Symtab.map (K repair_min_ary) sym_tab)
  1303         end
  1304       else
  1305         accum
  1306     fun add top_level tm (accum as ((bool_vars, fun_var_Ts), sym_tab)) =
  1307       let val (head, args) = strip_iterm_comb tm in
  1308         (case head of
  1309            IConst ((s, _), T, _) =>
  1310            if String.isPrefix bound_var_prefix s orelse
  1311               String.isPrefix all_bound_var_prefix s then
  1312              add_universal_var T accum
  1313            else if String.isPrefix exist_bound_var_prefix s then
  1314              accum
  1315            else
  1316              let val ary = length args in
  1317                ((bool_vars, fun_var_Ts),
  1318                 case Symtab.lookup sym_tab s of
  1319                   SOME {pred_sym, min_ary, max_ary, types} =>
  1320                   let
  1321                     val pred_sym =
  1322                       pred_sym andalso top_level andalso not bool_vars
  1323                     val types' = types |> insert_type ctxt I T
  1324                     val min_ary =
  1325                       if is_some explicit_apply orelse
  1326                          pointer_eq (types', types) then
  1327                         min_ary
  1328                       else
  1329                         fold (consider_var_ary T) fun_var_Ts min_ary
  1330                   in
  1331                     Symtab.update (s, {pred_sym = pred_sym,
  1332                                        min_ary = Int.min (ary, min_ary),
  1333                                        max_ary = Int.max (ary, max_ary),
  1334                                        types = types'})
  1335                                   sym_tab
  1336                   end
  1337                 | NONE =>
  1338                   let
  1339                     val pred_sym = top_level andalso not bool_vars
  1340                     val min_ary =
  1341                       case explicit_apply of
  1342                         SOME true => 0
  1343                       | SOME false => ary
  1344                       | NONE => fold (consider_var_ary T) fun_var_Ts ary
  1345                   in
  1346                     Symtab.update_new (s, {pred_sym = pred_sym,
  1347                                            min_ary = min_ary, max_ary = ary,
  1348                                            types = [T]})
  1349                                       sym_tab
  1350                   end)
  1351              end
  1352          | IVar (_, T) => add_universal_var T accum
  1353          | IAbs ((_, T), tm) => accum |> add_universal_var T |> add false tm
  1354          | _ => accum)
  1355         |> fold (add false) args
  1356       end
  1357   in add true end
  1358 fun add_fact_syms_to_table ctxt explicit_apply =
  1359   K (add_iterm_syms_to_table ctxt explicit_apply)
  1360   |> formula_fold NONE |> fact_lift
  1361 
  1362 val default_sym_tab_entries : (string * sym_info) list =
  1363   (prefixed_predicator_name,
  1364    {pred_sym = true, min_ary = 1, max_ary = 1, types = []})
  1365        (* FIXME: needed? *) ::
  1366   (make_fixed_const NONE @{const_name undefined},
  1367    {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
  1368   ([tptp_false, tptp_true]
  1369    |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
  1370   ([tptp_equal, tptp_old_equal]
  1371    |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = []}))
  1372 
  1373 fun sym_table_for_facts ctxt explicit_apply facts =
  1374   ((false, []), Symtab.empty)
  1375   |> fold (add_fact_syms_to_table ctxt explicit_apply) facts |> snd
  1376   |> fold Symtab.update default_sym_tab_entries
  1377 
  1378 fun min_ary_of sym_tab s =
  1379   case Symtab.lookup sym_tab s of
  1380     SOME ({min_ary, ...} : sym_info) => min_ary
  1381   | NONE =>
  1382     case strip_prefix_and_unascii const_prefix s of
  1383       SOME s =>
  1384       let val s = s |> unmangled_const_name |> invert_const in
  1385         if s = predicator_name then 1
  1386         else if s = app_op_name then 2
  1387         else if s = type_guard_name then 1
  1388         else 0
  1389       end
  1390     | NONE => 0
  1391 
  1392 (* True if the constant ever appears outside of the top-level position in
  1393    literals, or if it appears with different arities (e.g., because of different
  1394    type instantiations). If false, the constant always receives all of its
  1395    arguments and is used as a predicate. *)
  1396 fun is_pred_sym sym_tab s =
  1397   case Symtab.lookup sym_tab s of
  1398     SOME ({pred_sym, min_ary, max_ary, ...} : sym_info) =>
  1399     pred_sym andalso min_ary = max_ary
  1400   | NONE => false
  1401 
  1402 val app_op = `(make_fixed_const NONE) app_op_name
  1403 val predicator_combconst =
  1404   IConst (`(make_fixed_const NONE) predicator_name, @{typ "bool => bool"}, [])
  1405 
  1406 fun list_app head args = fold (curry (IApp o swap)) args head
  1407 fun predicator tm = IApp (predicator_combconst, tm)
  1408 
  1409 fun firstorderize_fact thy format type_enc sym_tab =
  1410   let
  1411     fun do_app arg head =
  1412       let
  1413         val head_T = ityp_of head
  1414         val (arg_T, res_T) = dest_funT head_T
  1415         val app =
  1416           IConst (app_op, head_T --> head_T, [arg_T, res_T])
  1417           |> mangle_type_args_in_iterm format type_enc
  1418       in list_app app [head, arg] end
  1419     fun list_app_ops head args = fold do_app args head
  1420     fun introduce_app_ops tm =
  1421       case strip_iterm_comb tm of
  1422         (head as IConst ((s, _), _, _), args) =>
  1423         args |> map introduce_app_ops
  1424              |> chop (min_ary_of sym_tab s)
  1425              |>> list_app head
  1426              |-> list_app_ops
  1427       | (head, args) => list_app_ops head (map introduce_app_ops args)
  1428     fun introduce_predicators tm =
  1429       case strip_iterm_comb tm of
  1430         (IConst ((s, _), _, _), _) =>
  1431         if is_pred_sym sym_tab s then tm else predicator tm
  1432       | _ => predicator tm
  1433     val do_iterm =
  1434       not (is_type_enc_higher_order type_enc)
  1435       ? (introduce_app_ops #> introduce_predicators)
  1436       #> filter_type_args_in_iterm thy type_enc
  1437   in update_iformula (formula_map do_iterm) end
  1438 
  1439 (** Helper facts **)
  1440 
  1441 val not_ffalse = @{lemma "~ fFalse" by (unfold fFalse_def) fast}
  1442 val ftrue = @{lemma "fTrue" by (unfold fTrue_def) fast}
  1443 
  1444 (* The Boolean indicates that a fairly sound type encoding is needed. *)
  1445 val helper_table =
  1446   [(("COMBI", false), @{thms Meson.COMBI_def}),
  1447    (("COMBK", false), @{thms Meson.COMBK_def}),
  1448    (("COMBB", false), @{thms Meson.COMBB_def}),
  1449    (("COMBC", false), @{thms Meson.COMBC_def}),
  1450    (("COMBS", false), @{thms Meson.COMBS_def}),
  1451    ((predicator_name, false), [not_ffalse, ftrue]),
  1452    (("fFalse", false), [not_ffalse]),
  1453    (("fFalse", true), @{thms True_or_False}),
  1454    (("fTrue", false), [ftrue]),
  1455    (("fTrue", true), @{thms True_or_False}),
  1456    (("fNot", false),
  1457     @{thms fNot_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1458            fNot_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1459    (("fconj", false),
  1460     @{lemma "~ P | ~ Q | fconj P Q" "~ fconj P Q | P" "~ fconj P Q | Q"
  1461         by (unfold fconj_def) fast+}),
  1462    (("fdisj", false),
  1463     @{lemma "~ P | fdisj P Q" "~ Q | fdisj P Q" "~ fdisj P Q | P | Q"
  1464         by (unfold fdisj_def) fast+}),
  1465    (("fimplies", false),
  1466     @{lemma "P | fimplies P Q" "~ Q | fimplies P Q" "~ fimplies P Q | ~ P | Q"
  1467         by (unfold fimplies_def) fast+}),
  1468    (("fequal", true),
  1469     (* This is a lie: Higher-order equality doesn't need a sound type encoding.
  1470        However, this is done so for backward compatibility: Including the
  1471        equality helpers by default in Metis breaks a few existing proofs. *)
  1472     @{thms fequal_def [THEN Meson.iff_to_disjD, THEN conjunct1]
  1473            fequal_def [THEN Meson.iff_to_disjD, THEN conjunct2]}),
  1474    (* Partial characterization of "fAll" and "fEx". A complete characterization
  1475       would require the axiom of choice for replay with Metis. *)
  1476    (("fAll", false), [@{lemma "~ fAll P | P x" by (auto simp: fAll_def)}]),
  1477    (("fEx", false), [@{lemma "~ P x | fEx P" by (auto simp: fEx_def)}]),
  1478    (("If", true), @{thms if_True if_False True_or_False})]
  1479   |> map (apsnd (map zero_var_indexes))
  1480 
  1481 fun bound_tvars type_enc =
  1482   mk_ahorn o formulas_for_types type_enc add_sorts_on_tvar
  1483 
  1484 fun eq_formula type_enc atomic_Ts pred_sym tm1 tm2 =
  1485   (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
  1486    else AAtom (ATerm (`I tptp_equal, [tm1, tm2])))
  1487   |> bound_tvars type_enc atomic_Ts
  1488   |> close_formula_universally type_enc
  1489 
  1490 val type_tag = `(make_fixed_const NONE) type_tag_name
  1491 
  1492 fun type_tag_idempotence_fact type_enc =
  1493   let
  1494     fun var s = ATerm (`I s, [])
  1495     fun tag tm = ATerm (type_tag, [var "A", tm])
  1496     val tagged_var = tag (var "X")
  1497   in
  1498     Formula (type_tag_idempotence_helper_name, Axiom,
  1499              eq_formula type_enc [] false (tag tagged_var) tagged_var,
  1500              isabelle_info simpN, NONE)
  1501   end
  1502 
  1503 fun should_specialize_helper type_enc t =
  1504   polymorphism_of_type_enc type_enc <> Polymorphic andalso
  1505   level_of_type_enc type_enc <> No_Types andalso
  1506   not (null (Term.hidden_polymorphism t))
  1507 
  1508 fun helper_facts_for_sym ctxt format type_enc (s, {types, ...} : sym_info) =
  1509   case strip_prefix_and_unascii const_prefix s of
  1510     SOME mangled_s =>
  1511     let
  1512       val thy = Proof_Context.theory_of ctxt
  1513       val unmangled_s = mangled_s |> unmangled_const_name
  1514       fun dub needs_fairly_sound j k =
  1515         (unmangled_s ^ "_" ^ string_of_int j ^ "_" ^ string_of_int k ^
  1516          (if mangled_s = unmangled_s then "" else "_" ^ ascii_of mangled_s) ^
  1517          (if needs_fairly_sound then typed_helper_suffix
  1518           else untyped_helper_suffix),
  1519          Helper)
  1520       fun dub_and_inst needs_fairly_sound (th, j) =
  1521         let val t = prop_of th in
  1522           if should_specialize_helper type_enc t then
  1523             map (fn T => specialize_type thy (invert_const unmangled_s, T) t)
  1524                 types
  1525           else
  1526             [t]
  1527         end
  1528         |> map (fn (k, t) => (dub needs_fairly_sound j k, t)) o tag_list 1
  1529       val make_facts = map_filter (make_fact ctxt format type_enc false)
  1530       val fairly_sound = is_type_enc_fairly_sound type_enc
  1531     in
  1532       helper_table
  1533       |> maps (fn ((helper_s, needs_fairly_sound), ths) =>
  1534                   if helper_s <> unmangled_s orelse
  1535                      (needs_fairly_sound andalso not fairly_sound) then
  1536                     []
  1537                   else
  1538                     ths ~~ (1 upto length ths)
  1539                     |> maps (dub_and_inst needs_fairly_sound)
  1540                     |> make_facts)
  1541     end
  1542   | NONE => []
  1543 fun helper_facts_for_sym_table ctxt format type_enc sym_tab =
  1544   Symtab.fold_rev (append o helper_facts_for_sym ctxt format type_enc) sym_tab
  1545                   []
  1546 
  1547 (***************************************************************)
  1548 (* Type Classes Present in the Axiom or Conjecture Clauses     *)
  1549 (***************************************************************)
  1550 
  1551 fun set_insert (x, s) = Symtab.update (x, ()) s
  1552 
  1553 fun add_classes (sorts, cset) = List.foldl set_insert cset (flat sorts)
  1554 
  1555 (* Remove this trivial type class (FIXME: similar code elsewhere) *)
  1556 fun delete_type cset = Symtab.delete_safe (the_single @{sort HOL.type}) cset
  1557 
  1558 fun classes_of_terms get_Ts =
  1559   map (map snd o get_Ts)
  1560   #> List.foldl add_classes Symtab.empty
  1561   #> delete_type #> Symtab.keys
  1562 
  1563 val tfree_classes_of_terms = classes_of_terms Misc_Legacy.term_tfrees
  1564 val tvar_classes_of_terms = classes_of_terms Misc_Legacy.term_tvars
  1565 
  1566 fun fold_type_constrs f (Type (s, Ts)) x =
  1567     fold (fold_type_constrs f) Ts (f (s, x))
  1568   | fold_type_constrs _ _ x = x
  1569 
  1570 (* Type constructors used to instantiate overloaded constants are the only ones
  1571    needed. *)
  1572 fun add_type_constrs_in_term thy =
  1573   let
  1574     fun add (Const (@{const_name Meson.skolem}, _) $ _) = I
  1575       | add (t $ u) = add t #> add u
  1576       | add (Const x) =
  1577         x |> robust_const_typargs thy |> fold (fold_type_constrs set_insert)
  1578       | add (Free (s, T)) =
  1579         if String.isPrefix polymorphic_free_prefix s then
  1580           T |> fold_type_constrs set_insert
  1581         else
  1582           I
  1583       | add (Abs (_, _, u)) = add u
  1584       | add _ = I
  1585   in add end
  1586 
  1587 fun type_constrs_of_terms thy ts =
  1588   Symtab.keys (fold (add_type_constrs_in_term thy) ts Symtab.empty)
  1589 
  1590 fun translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
  1591                        hyp_ts concl_t facts =
  1592   let
  1593     val thy = Proof_Context.theory_of ctxt
  1594     val presimp_consts = Meson.presimplified_consts ctxt
  1595     val fact_ts = facts |> map snd
  1596     (* Remove existing facts from the conjecture, as this can dramatically
  1597        boost an ATP's performance (for some reason). *)
  1598     val hyp_ts =
  1599       hyp_ts
  1600       |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
  1601     val facts = facts |> map (apsnd (pair Axiom))
  1602     val conjs =
  1603       map (pair prem_kind) hyp_ts @ [(Conjecture, s_not_trueprop concl_t)]
  1604       |> map2 (pair o rpair Local o string_of_int) (0 upto length hyp_ts)
  1605     val ((conjs, facts), lambdas) =
  1606       if preproc then
  1607         conjs @ facts
  1608         |> map (apsnd (apsnd (presimp_prop ctxt presimp_consts)))
  1609         |> preprocess_abstractions_in_terms trans_lambdas
  1610         |>> chop (length conjs)
  1611         |>> apfst (map (apsnd (apsnd freeze_term)))
  1612       else
  1613         ((conjs, facts), [])
  1614     val conjs = conjs |> make_conjecture ctxt format type_enc
  1615     val (fact_names, facts) =
  1616       facts
  1617       |> map_filter (fn (name, (_, t)) =>
  1618                         make_fact ctxt format type_enc true (name, t)
  1619                         |> Option.map (pair name))
  1620       |> ListPair.unzip
  1621     val lambdas =
  1622       lambdas |> map_filter (make_fact ctxt format type_enc true o apsnd snd)
  1623     val all_ts = concl_t :: hyp_ts @ fact_ts
  1624     val subs = tfree_classes_of_terms all_ts
  1625     val supers = tvar_classes_of_terms all_ts
  1626     val tycons = type_constrs_of_terms thy all_ts
  1627     val (supers, arity_clauses) =
  1628       if level_of_type_enc type_enc = No_Types then ([], [])
  1629       else make_arity_clauses thy tycons supers
  1630     val class_rel_clauses = make_class_rel_clauses thy subs supers
  1631   in
  1632     (fact_names |> map single, union (op =) subs supers, conjs, facts @ lambdas,
  1633      class_rel_clauses, arity_clauses)
  1634   end
  1635 
  1636 val type_guard = `(make_fixed_const NONE) type_guard_name
  1637 
  1638 fun type_guard_iterm format type_enc T tm =
  1639   IApp (IConst (type_guard, T --> @{typ bool}, [T])
  1640         |> mangle_type_args_in_iterm format type_enc, tm)
  1641 
  1642 fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
  1643   | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
  1644     accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
  1645   | is_var_positively_naked_in_term _ _ _ _ = true
  1646 
  1647 fun should_guard_var_in_formula pos phi (SOME true) name =
  1648     formula_fold pos (is_var_positively_naked_in_term name) phi false
  1649   | should_guard_var_in_formula _ _ _ _ = true
  1650 
  1651 fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
  1652   | should_generate_tag_bound_decl ctxt mono (Tags (_, level)) _ T =
  1653     heaviness_of_level level <> Heavy andalso
  1654     should_encode_type ctxt mono level T
  1655   | should_generate_tag_bound_decl _ _ _ _ _ = false
  1656 
  1657 fun mk_aterm format type_enc name T_args args =
  1658   ATerm (name, map_filter (ho_term_for_type_arg format type_enc) T_args @ args)
  1659 
  1660 fun tag_with_type ctxt format mono type_enc pos T tm =
  1661   IConst (type_tag, T --> T, [T])
  1662   |> mangle_type_args_in_iterm format type_enc
  1663   |> ho_term_from_iterm ctxt format mono type_enc (Top_Level pos)
  1664   |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
  1665        | _ => raise Fail "unexpected lambda-abstraction")
  1666 and ho_term_from_iterm ctxt format mono type_enc =
  1667   let
  1668     fun aux site u =
  1669       let
  1670         val (head, args) = strip_iterm_comb u
  1671         val pos =
  1672           case site of
  1673             Top_Level pos => pos
  1674           | Eq_Arg pos => pos
  1675           | Elsewhere => NONE
  1676         val t =
  1677           case head of
  1678             IConst (name as (s, _), _, T_args) =>
  1679             let
  1680               val arg_site = if is_tptp_equal s then Eq_Arg pos else Elsewhere
  1681             in
  1682               mk_aterm format type_enc name T_args (map (aux arg_site) args)
  1683             end
  1684           | IVar (name, _) =>
  1685             mk_aterm format type_enc name [] (map (aux Elsewhere) args)
  1686           | IAbs ((name, T), tm) =>
  1687             AAbs ((name, ho_type_from_typ format type_enc true 0 T),
  1688                   aux Elsewhere tm)
  1689           | IApp _ => raise Fail "impossible \"IApp\""
  1690         val T = ityp_of u
  1691       in
  1692         t |> (if should_tag_with_type ctxt mono type_enc site u T then
  1693                 tag_with_type ctxt format mono type_enc pos T
  1694               else
  1695                 I)
  1696       end
  1697   in aux end
  1698 and formula_from_iformula ctxt format mono type_enc should_guard_var =
  1699   let
  1700     val do_term = ho_term_from_iterm ctxt format mono type_enc o Top_Level
  1701     val do_bound_type =
  1702       case type_enc of
  1703         Simple_Types (_, _, level) => fused_type ctxt mono level 0
  1704         #> ho_type_from_typ format type_enc false 0 #> SOME
  1705       | _ => K NONE
  1706     fun do_out_of_bound_type pos phi universal (name, T) =
  1707       if should_guard_type ctxt mono type_enc
  1708              (fn () => should_guard_var pos phi universal name) T then
  1709         IVar (name, T)
  1710         |> type_guard_iterm format type_enc T
  1711         |> do_term pos |> AAtom |> SOME
  1712       else if should_generate_tag_bound_decl ctxt mono type_enc universal T then
  1713         let
  1714           val var = ATerm (name, [])
  1715           val tagged_var = var |> tag_with_type ctxt format mono type_enc pos T
  1716         in SOME (AAtom (ATerm (`I tptp_equal, [tagged_var, var]))) end
  1717       else
  1718         NONE
  1719     fun do_formula pos (AQuant (q, xs, phi)) =
  1720         let
  1721           val phi = phi |> do_formula pos
  1722           val universal = Option.map (q = AExists ? not) pos
  1723         in
  1724           AQuant (q, xs |> map (apsnd (fn NONE => NONE
  1725                                         | SOME T => do_bound_type T)),
  1726                   (if q = AForall then mk_ahorn else fold_rev (mk_aconn AAnd))
  1727                       (map_filter
  1728                            (fn (_, NONE) => NONE
  1729                              | (s, SOME T) =>
  1730                                do_out_of_bound_type pos phi universal (s, T))
  1731                            xs)
  1732                       phi)
  1733         end
  1734       | do_formula pos (AConn conn) = aconn_map pos do_formula conn
  1735       | do_formula pos (AAtom tm) = AAtom (do_term pos tm)
  1736   in do_formula end
  1737 
  1738 (* Each fact is given a unique fact number to avoid name clashes (e.g., because
  1739    of monomorphization). The TPTP explicitly forbids name clashes, and some of
  1740    the remote provers might care. *)
  1741 fun formula_line_for_fact ctxt format prefix encode freshen pos mono type_enc
  1742                           (j, {name, locality, kind, iformula, atomic_types}) =
  1743   (prefix ^ (if freshen then string_of_int j ^ "_" else "") ^ encode name, kind,
  1744    iformula
  1745    |> close_iformula_universally
  1746    |> formula_from_iformula ctxt format mono type_enc
  1747                             should_guard_var_in_formula
  1748                             (if pos then SOME true else NONE)
  1749    |> bound_tvars type_enc atomic_types
  1750    |> close_formula_universally type_enc,
  1751    NONE,
  1752    case locality of
  1753      Intro => isabelle_info introN
  1754    | Elim => isabelle_info elimN
  1755    | Simp => isabelle_info simpN
  1756    | _ => NONE)
  1757   |> Formula
  1758 
  1759 fun formula_line_for_class_rel_clause type_enc
  1760         ({name, subclass, superclass, ...} : class_rel_clause) =
  1761   let val ty_arg = ATerm (tvar_a_name, []) in
  1762     Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
  1763              AConn (AImplies,
  1764                     [type_class_formula type_enc subclass ty_arg,
  1765                      type_class_formula type_enc superclass ty_arg])
  1766              |> close_formula_universally type_enc, isabelle_info introN, NONE)
  1767   end
  1768 
  1769 fun formula_from_arity_atom type_enc (class, t, args) =
  1770   ATerm (t, map (fn arg => ATerm (arg, [])) args)
  1771   |> type_class_formula type_enc class
  1772 
  1773 fun formula_line_for_arity_clause type_enc
  1774         ({name, prem_atoms, concl_atom, ...} : arity_clause) =
  1775   Formula (arity_clause_prefix ^ name, Axiom,
  1776            mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
  1777                     (formula_from_arity_atom type_enc concl_atom)
  1778            |> close_formula_universally type_enc, isabelle_info introN, NONE)
  1779 
  1780 fun formula_line_for_conjecture ctxt format mono type_enc
  1781         ({name, kind, iformula, atomic_types, ...} : translated_formula) =
  1782   Formula (conjecture_prefix ^ name, kind,
  1783            formula_from_iformula ctxt format mono type_enc
  1784                should_guard_var_in_formula (SOME false)
  1785                (close_iformula_universally iformula)
  1786            |> bound_tvars type_enc atomic_types
  1787            |> close_formula_universally type_enc, NONE, NONE)
  1788 
  1789 fun formula_line_for_free_type j phi =
  1790   Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, NONE)
  1791 fun formula_lines_for_free_types type_enc (facts : translated_formula list) =
  1792   let
  1793     val phis =
  1794       fold (union (op =)) (map #atomic_types facts) []
  1795       |> formulas_for_types type_enc add_sorts_on_tfree
  1796   in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
  1797 
  1798 (** Symbol declarations **)
  1799 
  1800 fun decl_line_for_class order s =
  1801   let val name as (s, _) = `make_type_class s in
  1802     Decl (sym_decl_prefix ^ s, name,
  1803           if order = First_Order andalso avoid_first_order_dummy_type_vars then
  1804             ATyAbs ([tvar_a_name], AFun (a_itself_atype, bool_atype))
  1805           else
  1806             AFun (atype_of_types, bool_atype))
  1807   end
  1808 
  1809 fun decl_lines_for_classes type_enc classes =
  1810   case type_enc of
  1811     Simple_Types (order, Polymorphic, _) =>
  1812     map (decl_line_for_class order) classes
  1813   | _ => []
  1814 
  1815 fun sym_decl_table_for_facts ctxt format type_enc sym_tab (conjs, facts) =
  1816   let
  1817     fun add_iterm_syms in_conj tm =
  1818       let val (head, args) = strip_iterm_comb tm in
  1819         (case head of
  1820            IConst ((s, s'), T, T_args) =>
  1821            let
  1822              val pred_sym = is_pred_sym sym_tab s
  1823              val decl_sym =
  1824                (case type_enc of
  1825                   Guards _ => not pred_sym
  1826                 | _ => true) andalso
  1827                is_tptp_user_symbol s
  1828            in
  1829              if decl_sym then
  1830                Symtab.map_default (s, [])
  1831                    (insert_type ctxt #3 (s', T_args, T, pred_sym, length args,
  1832                                          in_conj))
  1833              else
  1834                I
  1835            end
  1836          | IAbs (_, tm) => add_iterm_syms in_conj tm
  1837          | _ => I)
  1838         #> fold (add_iterm_syms in_conj) args
  1839       end
  1840     fun add_fact_syms in_conj =
  1841       K (add_iterm_syms in_conj) |> formula_fold NONE |> fact_lift
  1842     fun add_formula_var_types (AQuant (_, xs, phi)) =
  1843         fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
  1844         #> add_formula_var_types phi
  1845       | add_formula_var_types (AConn (_, phis)) =
  1846         fold add_formula_var_types phis
  1847       | add_formula_var_types _ = I
  1848     fun var_types () =
  1849       if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
  1850       else fold (fact_lift add_formula_var_types) (conjs @ facts) []
  1851     fun add_undefined_const T =
  1852       let
  1853         val (s, s') =
  1854           `(make_fixed_const NONE) @{const_name undefined}
  1855           |> (case type_arg_policy type_enc @{const_name undefined} of
  1856                 Mangled_Type_Args => mangled_const_name format type_enc [T]
  1857               | _ => I)
  1858       in
  1859         Symtab.map_default (s, [])
  1860                            (insert_type ctxt #3 (s', [T], T, false, 0, false))
  1861       end
  1862     fun add_TYPE_const () =
  1863       let val (s, s') = TYPE_name in
  1864         Symtab.map_default (s, [])
  1865             (insert_type ctxt #3
  1866                          (s', [tvar_a], @{typ "'a itself"}, false, 0, false))
  1867       end
  1868   in
  1869     Symtab.empty
  1870     |> is_type_enc_fairly_sound type_enc
  1871        ? (fold (add_fact_syms true) conjs
  1872           #> fold (add_fact_syms false) facts
  1873           #> (case type_enc of
  1874                 Simple_Types (_, poly, _) =>
  1875                 if poly = Polymorphic then add_TYPE_const () else I
  1876               | _ => fold add_undefined_const (var_types ())))
  1877   end
  1878 
  1879 (* We add "bool" in case the helper "True_or_False" is included later. *)
  1880 fun default_mono level =
  1881   {maybe_finite_Ts = [@{typ bool}],
  1882    surely_finite_Ts = [@{typ bool}],
  1883    maybe_infinite_Ts = known_infinite_types,
  1884    surely_infinite_Ts =
  1885      case level of
  1886        Noninf_Nonmono_Types (Sound, _) => []
  1887      | _ => known_infinite_types,
  1888    maybe_nonmono_Ts = [@{typ bool}]}
  1889 
  1890 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
  1891    out with monotonicity" paper presented at CADE 2011. *)
  1892 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono
  1893   | add_iterm_mononotonicity_info ctxt level _
  1894         (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2))
  1895         (mono as {maybe_finite_Ts, surely_finite_Ts, maybe_infinite_Ts,
  1896                   surely_infinite_Ts, maybe_nonmono_Ts}) =
  1897     if is_tptp_equal s andalso exists is_maybe_universal_var [tm1, tm2] then
  1898       case level of
  1899         Noninf_Nonmono_Types (soundness, _) =>
  1900         if exists (type_instance ctxt T) surely_infinite_Ts orelse
  1901            member (type_aconv ctxt) maybe_finite_Ts T then
  1902           mono
  1903         else if is_type_kind_of_surely_infinite ctxt soundness
  1904                                                 surely_infinite_Ts T then
  1905           {maybe_finite_Ts = maybe_finite_Ts,
  1906            surely_finite_Ts = surely_finite_Ts,
  1907            maybe_infinite_Ts = maybe_infinite_Ts,
  1908            surely_infinite_Ts = surely_infinite_Ts |> insert_type ctxt I T,
  1909            maybe_nonmono_Ts = maybe_nonmono_Ts}
  1910         else
  1911           {maybe_finite_Ts = maybe_finite_Ts |> insert (type_aconv ctxt) T,
  1912            surely_finite_Ts = surely_finite_Ts,
  1913            maybe_infinite_Ts = maybe_infinite_Ts,
  1914            surely_infinite_Ts = surely_infinite_Ts,
  1915            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
  1916       | Fin_Nonmono_Types _ =>
  1917         if exists (type_instance ctxt T) surely_finite_Ts orelse
  1918            member (type_aconv ctxt) maybe_infinite_Ts T then
  1919           mono
  1920         else if is_type_surely_finite ctxt T then
  1921           {maybe_finite_Ts = maybe_finite_Ts,
  1922            surely_finite_Ts = surely_finite_Ts |> insert_type ctxt I T,
  1923            maybe_infinite_Ts = maybe_infinite_Ts,
  1924            surely_infinite_Ts = surely_infinite_Ts,
  1925            maybe_nonmono_Ts = maybe_nonmono_Ts |> insert_type ctxt I T}
  1926         else
  1927           {maybe_finite_Ts = maybe_finite_Ts,
  1928            surely_finite_Ts = surely_finite_Ts,
  1929            maybe_infinite_Ts = maybe_infinite_Ts |> insert (type_aconv ctxt) T,
  1930            surely_infinite_Ts = surely_infinite_Ts,
  1931            maybe_nonmono_Ts = maybe_nonmono_Ts}
  1932       | _ => mono
  1933     else
  1934       mono
  1935   | add_iterm_mononotonicity_info _ _ _ _ mono = mono
  1936 fun add_fact_mononotonicity_info ctxt level
  1937         ({kind, iformula, ...} : translated_formula) =
  1938   formula_fold (SOME (kind <> Conjecture))
  1939                (add_iterm_mononotonicity_info ctxt level) iformula
  1940 fun mononotonicity_info_for_facts ctxt type_enc facts =
  1941   let val level = level_of_type_enc type_enc in
  1942     default_mono level
  1943     |> is_type_level_monotonicity_based level
  1944        ? fold (add_fact_mononotonicity_info ctxt level) facts
  1945   end
  1946 
  1947 fun add_iformula_monotonic_types ctxt mono type_enc =
  1948   let
  1949     val level = level_of_type_enc type_enc
  1950     val should_encode = should_encode_type ctxt mono level
  1951     fun add_type T = not (should_encode T) ? insert_type ctxt I T
  1952     fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2
  1953       | add_args _ = I
  1954     and add_term tm = add_type (ityp_of tm) #> add_args tm
  1955   in formula_fold NONE (K add_term) end
  1956 fun add_fact_monotonic_types ctxt mono type_enc =
  1957   add_iformula_monotonic_types ctxt mono type_enc |> fact_lift
  1958 fun monotonic_types_for_facts ctxt mono type_enc facts =
  1959   [] |> (polymorphism_of_type_enc type_enc = Polymorphic andalso
  1960          is_type_level_monotonicity_based (level_of_type_enc type_enc))
  1961         ? fold (add_fact_monotonic_types ctxt mono type_enc) facts
  1962 
  1963 fun formula_line_for_guards_mono_type ctxt format mono type_enc T =
  1964   Formula (guards_sym_formula_prefix ^
  1965            ascii_of (mangled_type format type_enc T),
  1966            Axiom,
  1967            IConst (`make_bound_var "X", T, [])
  1968            |> type_guard_iterm format type_enc T
  1969            |> AAtom
  1970            |> formula_from_iformula ctxt format mono type_enc
  1971                                     (K (K (K (K true)))) (SOME true)
  1972            |> bound_tvars type_enc (atyps_of T)
  1973            |> close_formula_universally type_enc,
  1974            isabelle_info introN, NONE)
  1975 
  1976 fun formula_line_for_tags_mono_type ctxt format mono type_enc T =
  1977   let val x_var = ATerm (`make_bound_var "X", []) in
  1978     Formula (tags_sym_formula_prefix ^
  1979              ascii_of (mangled_type format type_enc T),
  1980              Axiom,
  1981              eq_formula type_enc (atyps_of T) false
  1982                         (tag_with_type ctxt format mono type_enc NONE T x_var)
  1983                         x_var,
  1984              isabelle_info simpN, NONE)
  1985   end
  1986 
  1987 fun problem_lines_for_mono_types ctxt format mono type_enc Ts =
  1988   case type_enc of
  1989     Simple_Types _ => []
  1990   | Guards _ =>
  1991     map (formula_line_for_guards_mono_type ctxt format mono type_enc) Ts
  1992   | Tags _ => map (formula_line_for_tags_mono_type ctxt format mono type_enc) Ts
  1993 
  1994 fun decl_line_for_sym ctxt format mono type_enc s
  1995                       (s', T_args, T, pred_sym, ary, _) =
  1996   let
  1997     val thy = Proof_Context.theory_of ctxt
  1998     val (T, T_args) =
  1999       if null T_args then
  2000         (T, [])
  2001       else case strip_prefix_and_unascii const_prefix s of
  2002         SOME s' =>
  2003         let
  2004           val s' = s' |> invert_const
  2005           val T = s' |> robust_const_type thy
  2006         in (T, robust_const_typargs thy (s', T)) end
  2007       | NONE =>
  2008         case strip_prefix_and_unascii fixed_var_prefix s of
  2009           SOME s' =>
  2010           if String.isPrefix polymorphic_free_prefix s' then (tvar_a, [tvar_a])
  2011           else raise Fail "unexpected type arguments to free variable"
  2012         | NONE => raise Fail "unexpected type arguments"
  2013   in
  2014     Decl (sym_decl_prefix ^ s, (s, s'),
  2015           T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
  2016             |> ho_type_from_typ format type_enc pred_sym ary
  2017             |> not (null T_args)
  2018                ? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
  2019   end
  2020 
  2021 fun formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono type_enc n s
  2022                                      j (s', T_args, T, _, ary, in_conj) =
  2023   let
  2024     val (kind, maybe_negate) =
  2025       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  2026       else (Axiom, I)
  2027     val (arg_Ts, res_T) = chop_fun ary T
  2028     val num_args = length arg_Ts
  2029     val bound_names =
  2030       1 upto num_args |> map (`I o make_bound_var o string_of_int)
  2031     val bounds =
  2032       bound_names ~~ arg_Ts |> map (fn (name, T) => IConst (name, T, []))
  2033     val sym_needs_arg_types = exists (curry (op =) dummyT) T_args
  2034     fun should_keep_arg_type T =
  2035       sym_needs_arg_types andalso
  2036       should_guard_type ctxt mono type_enc (K true) T
  2037     val bound_Ts =
  2038       arg_Ts |> map (fn T => if should_keep_arg_type T then SOME T else NONE)
  2039   in
  2040     Formula (guards_sym_formula_prefix ^ s ^
  2041              (if n > 1 then "_" ^ string_of_int j else ""), kind,
  2042              IConst ((s, s'), T, T_args)
  2043              |> fold (curry (IApp o swap)) bounds
  2044              |> type_guard_iterm format type_enc res_T
  2045              |> AAtom |> mk_aquant AForall (bound_names ~~ bound_Ts)
  2046              |> formula_from_iformula ctxt format mono type_enc
  2047                                       (K (K (K (K true)))) (SOME true)
  2048              |> n > 1 ? bound_tvars type_enc (atyps_of T)
  2049              |> close_formula_universally type_enc
  2050              |> maybe_negate,
  2051              isabelle_info introN, NONE)
  2052   end
  2053 
  2054 fun formula_lines_for_nonuniform_tags_sym_decl ctxt format conj_sym_kind mono
  2055         type_enc n s (j, (s', T_args, T, pred_sym, ary, in_conj)) =
  2056   let
  2057     val ident_base =
  2058       tags_sym_formula_prefix ^ s ^
  2059       (if n > 1 then "_" ^ string_of_int j else "")
  2060     val (kind, maybe_negate) =
  2061       if in_conj then (conj_sym_kind, conj_sym_kind = Conjecture ? mk_anot)
  2062       else (Axiom, I)
  2063     val (arg_Ts, res_T) = chop_fun ary T
  2064     val bound_names =
  2065       1 upto length arg_Ts |> map (`I o make_bound_var o string_of_int)
  2066     val bounds = bound_names |> map (fn name => ATerm (name, []))
  2067     val cst = mk_aterm format type_enc (s, s') T_args
  2068     val eq = maybe_negate oo eq_formula type_enc (atyps_of T) pred_sym
  2069     val should_encode =
  2070       should_encode_type ctxt mono (level_of_type_enc type_enc)
  2071     val tag_with = tag_with_type ctxt format mono type_enc NONE
  2072     val add_formula_for_res =
  2073       if should_encode res_T then
  2074         cons (Formula (ident_base ^ "_res", kind,
  2075                        eq (tag_with res_T (cst bounds)) (cst bounds),
  2076                        isabelle_info simpN, NONE))
  2077       else
  2078         I
  2079     fun add_formula_for_arg k =
  2080       let val arg_T = nth arg_Ts k in
  2081         if should_encode arg_T then
  2082           case chop k bounds of
  2083             (bounds1, bound :: bounds2) =>
  2084             cons (Formula (ident_base ^ "_arg" ^ string_of_int (k + 1), kind,
  2085                            eq (cst (bounds1 @ tag_with arg_T bound :: bounds2))
  2086                               (cst bounds),
  2087                            isabelle_info simpN, NONE))
  2088           | _ => raise Fail "expected nonempty tail"
  2089         else
  2090           I
  2091       end
  2092   in
  2093     [] |> not pred_sym ? add_formula_for_res
  2094        |> Config.get ctxt type_tag_arguments
  2095           ? fold add_formula_for_arg (ary - 1 downto 0)
  2096   end
  2097 
  2098 fun result_type_of_decl (_, _, T, _, ary, _) = chop_fun ary T |> snd
  2099 
  2100 fun problem_lines_for_sym_decls ctxt format conj_sym_kind mono type_enc
  2101                                 (s, decls) =
  2102   case type_enc of
  2103     Simple_Types _ =>
  2104     decls |> map (decl_line_for_sym ctxt format mono type_enc s)
  2105   | Guards (_, level) =>
  2106     let
  2107       val decls =
  2108         case decls of
  2109           decl :: (decls' as _ :: _) =>
  2110           let val T = result_type_of_decl decl in
  2111             if forall (type_generalization ctxt T o result_type_of_decl)
  2112                       decls' then
  2113               [decl]
  2114             else
  2115               decls
  2116           end
  2117         | _ => decls
  2118       val n = length decls
  2119       val decls =
  2120         decls |> filter (should_encode_type ctxt mono level
  2121                          o result_type_of_decl)
  2122     in
  2123       (0 upto length decls - 1, decls)
  2124       |-> map2 (formula_line_for_guards_sym_decl ctxt format conj_sym_kind mono
  2125                                                  type_enc n s)
  2126     end
  2127   | Tags (_, level) =>
  2128     if heaviness_of_level level = Heavy then
  2129       []
  2130     else
  2131       let val n = length decls in
  2132         (0 upto n - 1 ~~ decls)
  2133         |> maps (formula_lines_for_nonuniform_tags_sym_decl ctxt format
  2134                      conj_sym_kind mono type_enc n s)
  2135       end
  2136 
  2137 fun problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono type_enc
  2138                                      mono_Ts sym_decl_tab =
  2139   let
  2140     val syms = sym_decl_tab |> Symtab.dest |> sort_wrt fst
  2141     val mono_lines =
  2142       problem_lines_for_mono_types ctxt format mono type_enc mono_Ts
  2143     val decl_lines =
  2144       fold_rev (append o problem_lines_for_sym_decls ctxt format conj_sym_kind
  2145                                                      mono type_enc)
  2146                syms []
  2147   in mono_lines @ decl_lines end
  2148 
  2149 fun needs_type_tag_idempotence ctxt (Tags (poly, level)) =
  2150     Config.get ctxt type_tag_idempotence andalso
  2151     is_type_level_monotonicity_based level andalso
  2152     poly <> Mangled_Monomorphic
  2153   | needs_type_tag_idempotence _ _ = false
  2154 
  2155 fun offset_of_heading_in_problem _ [] j = j
  2156   | offset_of_heading_in_problem needle ((heading, lines) :: problem) j =
  2157     if heading = needle then j
  2158     else offset_of_heading_in_problem needle problem (j + length lines)
  2159 
  2160 val implicit_declsN = "Should-be-implicit typings"
  2161 val explicit_declsN = "Explicit typings"
  2162 val factsN = "Relevant facts"
  2163 val class_relsN = "Class relationships"
  2164 val aritiesN = "Arities"
  2165 val helpersN = "Helper facts"
  2166 val conjsN = "Conjectures"
  2167 val free_typesN = "Type variables"
  2168 
  2169 val explicit_apply = NONE (* for experiments *)
  2170 
  2171 fun prepare_atp_problem ctxt format conj_sym_kind prem_kind type_enc exporter
  2172         lambda_trans readable_names preproc hyp_ts concl_t facts =
  2173   let
  2174     val thy = Proof_Context.theory_of ctxt
  2175     val type_enc = type_enc |> adjust_type_enc format
  2176     val lambda_trans =
  2177       if lambda_trans = smartN then
  2178         if is_type_enc_higher_order type_enc then lambdasN else combinatorsN
  2179       else if lambda_trans = lambdasN andalso
  2180               not (is_type_enc_higher_order type_enc) then
  2181         error ("Lambda translation method incompatible with first-order \
  2182                \encoding.")
  2183       else
  2184         lambda_trans
  2185     val trans_lambdas =
  2186       if lambda_trans = no_lambdasN then
  2187         rpair []
  2188       else if lambda_trans = concealedN then
  2189         lift_lambdas ctxt type_enc ##> K []
  2190       else if lambda_trans = liftingN then
  2191         lift_lambdas ctxt type_enc
  2192       else if lambda_trans = combinatorsN then
  2193         map (introduce_combinators ctxt) #> rpair []
  2194       else if lambda_trans = hybridN then
  2195         lift_lambdas ctxt type_enc
  2196         ##> maps (fn t => [t, introduce_combinators ctxt
  2197                                   (intentionalize_def t)])
  2198       else if lambda_trans = lambdasN then
  2199         map (Envir.eta_contract) #> rpair []
  2200       else
  2201         error ("Unknown lambda translation method: " ^
  2202                quote lambda_trans ^ ".")
  2203     val (fact_names, classes, conjs, facts, class_rel_clauses, arity_clauses) =
  2204       translate_formulas ctxt format prem_kind type_enc trans_lambdas preproc
  2205                          hyp_ts concl_t facts
  2206     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt explicit_apply
  2207     val mono = conjs @ facts |> mononotonicity_info_for_facts ctxt type_enc
  2208     val firstorderize = firstorderize_fact thy format type_enc sym_tab
  2209     val (conjs, facts) = (conjs, facts) |> pairself (map firstorderize)
  2210     val sym_tab = conjs @ facts |> sym_table_for_facts ctxt (SOME false)
  2211     val helpers =
  2212       sym_tab |> helper_facts_for_sym_table ctxt format type_enc
  2213               |> map firstorderize
  2214     val mono_Ts =
  2215       helpers @ conjs @ facts
  2216       |> monotonic_types_for_facts ctxt mono type_enc
  2217     val class_decl_lines = decl_lines_for_classes type_enc classes
  2218     val sym_decl_lines =
  2219       (conjs, helpers @ facts)
  2220       |> sym_decl_table_for_facts ctxt format type_enc sym_tab
  2221       |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind mono
  2222                                                type_enc mono_Ts
  2223     val helper_lines =
  2224       0 upto length helpers - 1 ~~ helpers
  2225       |> map (formula_line_for_fact ctxt format helper_prefix I false true mono
  2226                                     type_enc)
  2227       |> (if needs_type_tag_idempotence ctxt type_enc then
  2228             cons (type_tag_idempotence_fact type_enc)
  2229           else
  2230             I)
  2231     (* Reordering these might confuse the proof reconstruction code or the SPASS
  2232        FLOTTER hack. *)
  2233     val problem =
  2234       [(explicit_declsN, class_decl_lines @ sym_decl_lines),
  2235        (factsN,
  2236         map (formula_line_for_fact ctxt format fact_prefix ascii_of
  2237                                    (not exporter) (not exporter) mono type_enc)
  2238             (0 upto length facts - 1 ~~ facts)),
  2239        (class_relsN,
  2240         map (formula_line_for_class_rel_clause type_enc) class_rel_clauses),
  2241        (aritiesN, map (formula_line_for_arity_clause type_enc) arity_clauses),
  2242        (helpersN, helper_lines),
  2243        (conjsN,
  2244         map (formula_line_for_conjecture ctxt format mono type_enc) conjs),
  2245        (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs))]
  2246     val problem =
  2247       problem
  2248       |> (case format of
  2249             CNF => ensure_cnf_problem
  2250           | CNF_UEQ => filter_cnf_ueq_problem
  2251           | FOF => I
  2252           | TFF (_, TPTP_Implicit) => I
  2253           | THF (_, TPTP_Implicit, _) => I
  2254           | _ => declare_undeclared_syms_in_atp_problem type_decl_prefix
  2255                                                         implicit_declsN)
  2256     val (problem, pool) = problem |> nice_atp_problem readable_names
  2257     val helpers_offset = offset_of_heading_in_problem helpersN problem 0
  2258     val typed_helpers =
  2259       map_filter (fn (j, {name, ...}) =>
  2260                      if String.isSuffix typed_helper_suffix name then SOME j
  2261                      else NONE)
  2262                  ((helpers_offset + 1 upto helpers_offset + length helpers)
  2263                   ~~ helpers)
  2264     fun add_sym_ary (s, {min_ary, ...} : sym_info) =
  2265       min_ary > 0 ? Symtab.insert (op =) (s, min_ary)
  2266   in
  2267     (problem,
  2268      case pool of SOME the_pool => snd the_pool | NONE => Symtab.empty,
  2269      offset_of_heading_in_problem conjsN problem 0,
  2270      offset_of_heading_in_problem factsN problem 0,
  2271      fact_names |> Vector.fromList,
  2272      typed_helpers,
  2273      Symtab.empty |> Symtab.fold add_sym_ary sym_tab)
  2274   end
  2275 
  2276 (* FUDGE *)
  2277 val conj_weight = 0.0
  2278 val hyp_weight = 0.1
  2279 val fact_min_weight = 0.2
  2280 val fact_max_weight = 1.0
  2281 val type_info_default_weight = 0.8
  2282 
  2283 fun add_term_weights weight (ATerm (s, tms)) =
  2284     is_tptp_user_symbol s ? Symtab.default (s, weight)
  2285     #> fold (add_term_weights weight) tms
  2286   | add_term_weights weight (AAbs (_, tm)) = add_term_weights weight tm
  2287 fun add_problem_line_weights weight (Formula (_, _, phi, _, _)) =
  2288     formula_fold NONE (K (add_term_weights weight)) phi
  2289   | add_problem_line_weights _ _ = I
  2290 
  2291 fun add_conjectures_weights [] = I
  2292   | add_conjectures_weights conjs =
  2293     let val (hyps, conj) = split_last conjs in
  2294       add_problem_line_weights conj_weight conj
  2295       #> fold (add_problem_line_weights hyp_weight) hyps
  2296     end
  2297 
  2298 fun add_facts_weights facts =
  2299   let
  2300     val num_facts = length facts
  2301     fun weight_of j =
  2302       fact_min_weight + (fact_max_weight - fact_min_weight) * Real.fromInt j
  2303                         / Real.fromInt num_facts
  2304   in
  2305     map weight_of (0 upto num_facts - 1) ~~ facts
  2306     |> fold (uncurry add_problem_line_weights)
  2307   end
  2308 
  2309 (* Weights are from 0.0 (most important) to 1.0 (least important). *)
  2310 fun atp_problem_weights problem =
  2311   let val get = these o AList.lookup (op =) problem in
  2312     Symtab.empty
  2313     |> add_conjectures_weights (get free_typesN @ get conjsN)
  2314     |> add_facts_weights (get factsN)
  2315     |> fold (fold (add_problem_line_weights type_info_default_weight) o get)
  2316             [explicit_declsN, class_relsN, aritiesN]
  2317     |> Symtab.dest
  2318     |> sort (prod_ord Real.compare string_ord o pairself swap)
  2319   end
  2320 
  2321 end;