src/HOL/Tools/ATP/atp_problem_generate.ML

 Translation of HOL to FOL for Metis and Sledgehammer.
 *)
 
 signature ATP_PROBLEM_GENERATE =
 sig
-  type ('a, 'b) ho_term = ('a, 'b) ATP_Problem.ho_term
-  type connective = ATP_Problem.connective
-  type ('a, 'b, 'c, 'd) formula = ('a, 'b, 'c, 'd) ATP_Problem.formula
+  type ('a, 'b) atp_term = ('a, 'b) ATP_Problem.atp_term
+  type atp_connective = ATP_Problem.atp_connective
+  type ('a, 'b, 'c, 'd) atp_formula = ('a, 'b, 'c, 'd) ATP_Problem.atp_formula
   type atp_format = ATP_Problem.atp_format
-  type formula_role = ATP_Problem.formula_role
-  type 'a problem = 'a ATP_Problem.problem
+  type atp_formula_role = ATP_Problem.atp_formula_role
+  type 'a atp_problem = 'a ATP_Problem.atp_problem
 
   datatype mode = Metis | Sledgehammer | Sledgehammer_Completish | Exporter
 
   datatype scope = Global | Local | Assum | Chained
   datatype status =

   val is_type_enc_sound : type_enc -> bool
   val type_enc_of_string : strictness -> string -> type_enc
   val adjust_type_enc : atp_format -> type_enc -> type_enc
   val is_lambda_free : term -> bool
   val mk_aconns :
-    connective -> ('a, 'b, 'c, 'd) formula list -> ('a, 'b, 'c, 'd) formula
-  val unmangled_const : string -> string * (string, 'b) ho_term list
+    atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
+    -> ('a, 'b, 'c, 'd) atp_formula
+  val unmangled_const : string -> string * (string, 'b) atp_term list
   val unmangled_const_name : string -> string list
   val helper_table : ((string * bool) * (status * thm) list) list
   val trans_lams_of_string :
     Proof.context -> type_enc -> string -> term list -> term list * term list
   val string_of_status : status -> string
   val factsN : string
   val prepare_atp_problem :
-    Proof.context -> atp_format -> formula_role -> type_enc -> mode -> string
-    -> bool -> bool -> bool -> term list -> term
+    Proof.context -> atp_format -> atp_formula_role -> type_enc -> mode
+    -> string -> bool -> bool -> bool -> term list -> term
     -> ((string * stature) * term) list
-    -> string problem * string Symtab.table * (string * stature) list vector
+    -> string atp_problem * string Symtab.table * (string * stature) list vector
        * (string * term) list * int Symtab.table
-  val atp_problem_selection_weights : string problem -> (string * real) list
-  val atp_problem_term_order_info : string problem -> (string * int) list
+  val atp_problem_selection_weights : string atp_problem -> (string * real) list
+  val atp_problem_term_order_info : string atp_problem -> (string * int) list
 end;
 
 structure ATP_Problem_Generate : ATP_PROBLEM_GENERATE =
 struct
 

   | intentionalize_def t = t
 
 type ifact =
   {name : string,
    stature : stature,
-   role : formula_role,
-   iformula : (string * string, typ, iterm, string * string) formula,
+   role : atp_formula_role,
+   iformula : (string * string, typ, iterm, string * string) atp_formula,
    atomic_types : typ list}
 
 fun update_iformula f ({name, stature, role, iformula, atomic_types} : ifact) =
   {name = name, stature = stature, role = role, iformula = f iformula,
    atomic_types = atomic_types} : ifact

              map term Ts)
     | term (TFree (s, _)) = AType (`make_tfree s, [])
     | term (TVar z) = AType (tvar_name z, [])
   in term end
 
-fun ho_term_of_ho_type (AType (name, tys)) =
-    ATerm ((name, []), map ho_term_of_ho_type tys)
-  | ho_term_of_ho_type _ = raise Fail "unexpected type"
+fun atp_term_of_ho_type (AType (name, tys)) =
+    ATerm ((name, []), map atp_term_of_ho_type tys)
+  | atp_term_of_ho_type _ = raise Fail "unexpected type"
 
 fun ho_type_of_type_arg type_enc T =
   if T = dummyT then NONE else SOME (raw_ho_type_of_typ type_enc T)
 
 (* This shouldn't clash with anything else. *)

 
 fun process_type_args type_enc T_args =
   if is_type_enc_native type_enc then
     (map (native_ho_type_of_typ type_enc false 0) T_args, [])
   else
-    ([], map_filter (Option.map ho_term_of_ho_type
+    ([], map_filter (Option.map atp_term_of_ho_type
                      o ho_type_of_type_arg type_enc) T_args)
 
 fun class_atom type_enc (cl, T) =
   let
     val cl = `make_class cl

   | _ => K NONE
 
 fun tag_with_type ctxt mono type_enc pos T tm =
   IConst (type_tag, T --> T, [T])
   |> mangle_type_args_in_iterm type_enc
-  |> ho_term_of_iterm ctxt mono type_enc pos
+  |> atp_term_of_iterm ctxt mono type_enc pos
   |> (fn ATerm ((s, tys), tms) => ATerm ((s, tys), tms @ [tm])
        | _ => raise Fail "unexpected lambda-abstraction")
-and ho_term_of_iterm ctxt mono type_enc pos =
+and atp_term_of_iterm ctxt mono type_enc pos =
   let
     fun term site u =
       let
         val (head, args) = strip_iterm_comb u
         val pos =

   in term (Top_Level pos) end
 and formula_of_iformula ctxt mono type_enc should_guard_var =
   let
     val thy = Proof_Context.theory_of ctxt
     val level = level_of_type_enc type_enc
-    val do_term = ho_term_of_iterm ctxt mono type_enc
+    val do_term = atp_term_of_iterm ctxt mono type_enc
     fun do_out_of_bound_type pos phi universal (name, T) =
       if should_guard_type ctxt mono type_enc
              (fn () => should_guard_var thy level pos phi universal name) T then
         IVar (name, T)
         |> type_guard_iterm type_enc T

         val (base_name as (base_s, _), T_args) =
           mangle_type_args_in_const type_enc base_name T_args
         val base_ary = min_ary_of sym_tab0 base_s
         fun do_const name = IConst (name, T, T_args)
         val filter_ty_args = filter_type_args_in_iterm thy ctrss type_enc
-        val ho_term_of = ho_term_of_iterm ctxt mono type_enc (SOME true)
+        val atp_term_of = atp_term_of_iterm ctxt mono type_enc (SOME true)
         val name1 as (s1, _) =
           base_name |> ary - 1 > base_ary ? aliased_uncurried (ary - 1)
         val name2 as (s2, _) = base_name |> aliased_uncurried ary
         val (arg_Ts, _) = chop_fun ary T
         val bound_names =

           |> filter_ty_args
         val do_bound_type = do_bound_type ctxt mono type_enc
         val eq =
           eq_formula type_enc (atomic_types_of T)
                      (map (apsnd do_bound_type) bounds) false
-                     (ho_term_of tm1) (ho_term_of tm2)
+                     (atp_term_of tm1) (atp_term_of tm2)
       in
         ([tm1, tm2],
          [Formula ((uncurried_alias_eq_prefix ^ s2, ""), role,
                    eq |> maybe_negate, NONE,
                    isabelle_info non_rec_defN helper_rank)])