# HG changeset patch
# User desharna
# Date 1606410396 -3600
# Node ID 224eacc4d57987f077705aa734a2075c58710d14
# Parent  6771d34129c99b8f0ff463aa08573f5eb20fcb04
proper handling of builtins in TFX

diff -r 6771d34129c9 -r 224eacc4d579 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Thu Nov 26 13:47:29 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Thu Nov 26 18:06:36 2020 +0100
@@ -97,6 +97,8 @@
   val tptp_true : string
   val tptp_lambda : string
   val tptp_empty_list : string
+  val tptp_unary_builtins : string list
+  val tptp_binary_builtins : string list
   val dfg_individual_type : string
   val isabelle_info_prefix : string
   val isabelle_info : bool -> string -> int -> (string, 'a) atp_term list
@@ -257,6 +259,10 @@
 val tptp_lambda = "^"
 val tptp_empty_list = "[]"
 
+val tptp_unary_builtins = [tptp_not]
+val tptp_binary_builtins =
+  [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
+
 val dfg_individual_type = "iii" (* cannot clash *)
 
 val isabelle_info_prefix = "isabelle_"
@@ -455,14 +461,8 @@
    else
      "")
 
-local
-  val unary_builtins = [tptp_not]
-  val binary_builtins =
-    [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff, tptp_not_iff, tptp_equal]
-  val builtins = unary_builtins @ binary_builtins
-in
-
-fun tptp_string_of_term _ (ATerm ((s, []), [])) = s |> member (op =) builtins s ? parens
+fun tptp_string_of_term _ (ATerm ((s, []), [])) =
+    s |> member (op =) (tptp_unary_builtins @ tptp_binary_builtins) s ? parens
   | tptp_string_of_term format (ATerm ((s, tys), ts)) =
     let
       val of_type = string_of_type format
@@ -496,10 +496,10 @@
                "]: " ^ of_term tm ^ ""
                |> parens) (map of_term args)
         | _ => app ())
-      else if member (op =) unary_builtins s then
+      else if member (op =) tptp_unary_builtins s then
         (* generate e.g. "~ t" instead of "~ @ t". *)
         (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens)
-      else if member (op =) binary_builtins s then
+      else if member (op =) tptp_binary_builtins s then
         (* generate e.g. "t1 & t2" instead of "& @ t1 @ t2". *)
         (case ts of
           [t1, t2] => (of_term t1 |> parens) ^ " " ^ s ^ " " ^ (of_term t2 |> parens) |> parens
@@ -541,8 +541,6 @@
     |> parens
   | tptp_string_of_formula format (AAtom tm) = tptp_string_of_term format tm
 
-end
-
 fun tptp_string_of_format CNF = tptp_cnf
   | tptp_string_of_format CNF_UEQ = tptp_cnf
   | tptp_string_of_format FOF = tptp_fof
diff -r 6771d34129c9 -r 224eacc4d579 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 26 13:47:29 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Thu Nov 26 18:06:36 2020 +0100
@@ -1423,20 +1423,20 @@
 
 (** predicators and application operators **)
 
-type sym_info =
-  {pred_sym : bool, min_ary : int, max_ary : int, types : typ list,
-   in_conj : bool}
+type sym_info = {pred_sym : bool, min_ary : int, max_ary : int, types : typ list, in_conj : bool}
 
 fun default_sym_tab_entries type_enc =
-  (make_fixed_const NONE \<^const_name>\<open>undefined\<close>,
-     {pred_sym = false, min_ary = 0, max_ary = 0, types = [], in_conj = false}) ::
-  ([tptp_false, tptp_true]
-   |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = [], in_conj = false})) @
-  ([tptp_equal, tptp_old_equal]
-   |> map (rpair {pred_sym = true, min_ary = 2, max_ary = 2, types = [], in_conj = false}))
-  |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
-    ? cons (prefixed_predicator_name,
-      {pred_sym = true, min_ary = 1, max_ary = 1, types = [], in_conj = false})
+  let
+    fun mk_sym_info pred n =
+      {pred_sym = pred, min_ary = n, max_ary = n, types = [], in_conj = false}
+  in
+    (make_fixed_const NONE \<^const_name>\<open>undefined\<close>, mk_sym_info false 0) ::
+    (map (rpair (mk_sym_info true 0)) [tptp_false, tptp_true]) @
+    (map (rpair (mk_sym_info true 1)) tptp_unary_builtins) @
+    (map (rpair (mk_sym_info true 2)) (tptp_old_equal :: tptp_binary_builtins))
+    |> not (is_type_enc_fool type_enc orelse is_type_enc_full_higher_order type_enc)
+      ? cons (prefixed_predicator_name, mk_sym_info true 1)
+  end
 
 datatype app_op_level =
   Min_App_Op |