merged
authordesharna
Wed, 16 Dec 2020 09:59:15 +0100
changeset 73163 3c8d60f1dc53
parent 73152 fa364c21df15 (current diff)
parent 73162 d78bd4432f05 (diff)
child 73164 590608c05386
merged
--- a/src/HOL/ATP.thy	Wed Dec 16 00:08:31 2020 +0100
+++ b/src/HOL/ATP.thy	Wed Dec 16 09:59:15 2020 +0100
@@ -1,6 +1,7 @@
 (*  Title:      HOL/ATP.thy
     Author:     Fabian Immler, TU Muenchen
     Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Martin Desharnais, UniBw Muenchen
 *)
 
 section \<open>Automatic Theorem Provers (ATPs)\<close>
--- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Dec 16 00:08:31 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Dec 16 09:59:15 2020 +0100
@@ -33,7 +33,7 @@
 
   datatype fool = Without_FOOL | With_FOOL
   datatype polymorphism = Monomorphic | Polymorphic
-  datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+  datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
 
   datatype atp_format =
     CNF |
@@ -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
@@ -191,7 +193,7 @@
 
 datatype fool = Without_FOOL | With_FOOL
 datatype polymorphism = Monomorphic | Polymorphic
-datatype thf_flavor = THF_Lambda_Bool_Free | THF_Without_Choice | THF_With_Choice
+datatype thf_flavor = THF_Lambda_Free | THF_Without_Choice | THF_With_Choice
 
 datatype atp_format =
   CNF |
@@ -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,7 +461,8 @@
    else
      "")
 
-fun tptp_string_of_term _ (ATerm ((s, []), [])) = s
+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
@@ -473,8 +480,8 @@
       else if s = tptp_ho_forall orelse s = tptp_ho_exists then
         (case ts of
           [AAbs (((s', ty), tm), [])] =>
-          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever
-             possible, to work around LEO-II 1.2.8 parser limitation. *)
+          (* Use syntactic sugar "!" and "?" instead of "!!" and "??" whenever possible, to work
+             around LEO-II, Leo-III, and Satallax parser limitation. *)
           tptp_string_of_formula format
               (AQuant (if s = tptp_ho_forall then AForall else AExists,
                       [(s', SOME ty)], AAtom tm))
@@ -482,19 +489,18 @@
       else if s = tptp_choice then
         (case ts of
           [AAbs (((s', ty), tm), args)] =>
-          (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is
-             always applied to an abstraction. *)
+          (* There is code in "ATP_Problem_Generate" to ensure that "Eps" is always applied to an
+             abstraction. *)
           tptp_string_of_app format
               (tptp_choice ^ "[" ^ s' ^ " : " ^ of_type ty ^
                "]: " ^ of_term tm ^ ""
                |> parens) (map of_term args)
         | _ => app ())
-      else if s = tptp_not then
-        (* agsyHOL doesn't like negations applied like this: "~ @ t". *)
-        (case ts of [t] => s ^ " " ^ (of_term t |> parens) |> parens | _ => s)
-      else if member (op =) [tptp_and, tptp_or, tptp_implies, tptp_if, tptp_iff,
-                             tptp_not_iff, tptp_equal] s then
-        (* agsyHOL doesn't like connectives applied like this: "& @ t1 @ t2". *)
+      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 =) 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
         | _ => app ())
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Dec 16 00:08:31 2020 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Dec 16 09:59:15 2020 +0100
@@ -2,6 +2,7 @@
     Author:     Fabian Immler, TU Muenchen
     Author:     Makarius
     Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Martin Desharnais, UniBw Muenchen
 
 Translation of HOL to FOL for Metis and Sledgehammer.
 *)
@@ -99,7 +100,7 @@
   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 is_first_order_lambda_free : term -> bool
   val do_cheaply_conceal_lambdas : typ list -> term -> term
   val mk_aconns :
     atp_connective -> ('a, 'b, 'c, 'd) atp_formula list
@@ -162,7 +163,7 @@
 
 fun is_type_enc_native (Native _) = true
   | is_type_enc_native _ = false
-fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Bool_Free, _, _, _)) = false
+fun is_type_enc_full_higher_order (Native (Higher_Order THF_Lambda_Free, _, _, _)) = false
   | is_type_enc_full_higher_order (Native (Higher_Order _, _, _, _)) = true
   | is_type_enc_full_higher_order _ = false
 fun is_type_enc_fool (Native (_, With_FOOL, _, _)) = true
@@ -654,11 +655,11 @@
           | (_, Undercover_Types) => raise Same.SAME
           | (Mangled_Monomorphic, _) =>
             if is_type_level_uniform level then
-              Native (Higher_Order THF_With_Choice, Without_FOOL, Mangled_Monomorphic, level)
+              Native (Higher_Order THF_With_Choice, fool, Mangled_Monomorphic, level)
             else
               raise Same.SAME
            | (poly as Raw_Polymorphic _, All_Types) =>
-             Native (Higher_Order THF_With_Choice, Without_FOOL, poly, All_Types)
+             Native (Higher_Order THF_With_Choice, fool, poly, All_Types)
            | _ => raise Same.SAME))
       end
 
@@ -695,8 +696,8 @@
   end
   handle Same.SAME => error ("Unknown type encoding: " ^ quote s)
 
-fun min_hologic THF_Lambda_Bool_Free _ = THF_Lambda_Bool_Free
-  | min_hologic _ THF_Lambda_Bool_Free = THF_Lambda_Bool_Free
+fun min_hologic THF_Lambda_Free _ = THF_Lambda_Free
+  | min_hologic _ THF_Lambda_Free = THF_Lambda_Free
   | min_hologic THF_Without_Choice _ = THF_Without_Choice
   | min_hologic _ THF_Without_Choice = THF_Without_Choice
   | min_hologic _ _ = THF_With_Choice
@@ -728,42 +729,62 @@
     (if is_type_enc_sound type_enc then Tags else Guards) stuff
   | adjust_type_enc _ type_enc = type_enc
 
-fun is_lambda_free t =
+fun is_first_order_lambda_free t =
   (case t of
-    \<^const>\<open>Not\<close> $ t1 => is_lambda_free t1
-  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
-  | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_lambda_free t1
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_lambda_free t'
-  | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_lambda_free t1
-  | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
-  | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
-  | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 => is_lambda_free t1 andalso is_lambda_free t2
+    \<^const>\<open>Not\<close> $ t1 => is_first_order_lambda_free t1
+  | Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+  | Const (\<^const_name>\<open>All\<close>, _) $ t1 => is_first_order_lambda_free t1
+  | Const (\<^const_name>\<open>Ex\<close>, _) $ Abs (_, _, t') => is_first_order_lambda_free t'
+  | Const (\<^const_name>\<open>Ex\<close>, _) $ t1 => is_first_order_lambda_free t1
+  | \<^const>\<open>HOL.conj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^const>\<open>HOL.disj\<close> $ t1 $ t2 => is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
+  | \<^const>\<open>HOL.implies\<close> $ t1 $ t2 =>
+    is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
   | Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _])) $ t1 $ t2 =>
-    is_lambda_free t1 andalso is_lambda_free t2
+    is_first_order_lambda_free t1 andalso is_first_order_lambda_free t2
   | _ => not (exists_subterm (fn Abs _ => true | _ => false) t))
 
-fun simple_translate_lambdas do_lambdas ctxt t =
-  if is_lambda_free t then
+fun simple_translate_lambdas do_lambdas ctxt type_enc t =
+  if is_first_order_lambda_free t then
     t
   else
     let
-      fun trans Ts t =
+      fun trans_first_order Ts t =
         (case t of
-          \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans Ts t1
+          \<^const>\<open>Not\<close> $ t1 => \<^const>\<open>Not\<close> $ trans_first_order Ts t1
         | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
-          t0 $ Abs (s, T, trans (T :: Ts) t')
-        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
+          t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 =>
+          trans_first_order Ts (t0 $ eta_expand Ts t1 1)
         | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
-          t0 $ Abs (s, T, trans (T :: Ts) t')
-        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans Ts (t0 $ eta_expand Ts t1 1)
-        | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
-        | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
-        | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 => t0 $ trans Ts t1 $ trans Ts t2
+          t0 $ Abs (s, T, trans_first_order (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 =>
+          trans_first_order Ts (t0 $ eta_expand Ts t1 1)
+        | (t0 as \<^const>\<open>HOL.conj\<close>) $ t1 $ t2 =>
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+        | (t0 as \<^const>\<open>HOL.disj\<close>) $ t1 $ t2 =>
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
+        | (t0 as \<^const>\<open>HOL.implies\<close>) $ t1 $ t2 =>
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
         | (t0 as Const (\<^const_name>\<open>HOL.eq\<close>, Type (_, [\<^typ>\<open>bool\<close>, _]))) $ t1 $ t2 =>
-          t0 $ trans Ts t1 $ trans Ts t2
+          t0 $ trans_first_order Ts t1 $ trans_first_order Ts t2
         | _ =>
           if not (exists_subterm (fn Abs _ => true | _ => false) t) then t
           else t |> Envir.eta_contract |> do_lambdas ctxt Ts)
+
+      fun trans_fool Ts t =
+        (case t of
+          (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ Abs (s, T, t') =>
+          t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>All\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ Abs (s, T, t') =>
+          t0 $ Abs (s, T, trans_fool (T :: Ts) t')
+        | (t0 as Const (\<^const_name>\<open>Ex\<close>, _)) $ t1 => trans_fool Ts (t0 $ eta_expand Ts t1 1)
+        | t1 $ t2 => trans_fool Ts t1 $ trans_fool Ts t2
+        | Abs _ => t |> Envir.eta_contract |> do_lambdas ctxt Ts
+        | _ => t)
+
+      val trans = if is_type_enc_fool type_enc then trans_fool else trans_first_order
       val (t, ctxt') = yield_singleton (Variable.import_terms true) t ctxt
     in t |> trans [] |> singleton (Variable.export_terms ctxt' ctxt) end
 
@@ -809,18 +830,18 @@
           Lambda_Lifting.is_quantifier
   #> fst
 
-fun lift_lams_part_2 ctxt (facts, lifted) =
+fun lift_lams_part_2 ctxt type_enc (facts, lifted) =
   (facts, lifted)
   (* Lambda-lifting sometimes leaves some lambdas around; we need some way to
      get rid of them *)
-  |> apply2 (map (introduce_combinators ctxt))
+  |> apply2 (map (introduce_combinators ctxt type_enc))
   |> apply2 (map constify_lifted)
   (* Requires bound variables not to clash with any schematic variables (as
      should be the case right after lambda-lifting). *)
   |>> map (hol_open_form (unprefix hol_close_form_prefix))
   ||> map (hol_open_form I)
 
-fun lift_lams ctxt = lift_lams_part_2 ctxt oo lift_lams_part_1 ctxt
+fun lift_lams ctxt type_enc = lift_lams_part_2 ctxt type_enc o lift_lams_part_1 ctxt type_enc
 
 fun intentionalize_def (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) =
     intentionalize_def t
@@ -1103,67 +1124,121 @@
 
 val unmangled_invert_const = invert_const o hd o unmangled_const_name
 
+fun vars_of_iterm vars (IConst ((s, _), _, _)) = insert (op =) s vars
+  | vars_of_iterm vars (IVar ((s, _), _)) = insert (op =) s vars
+  | vars_of_iterm vars (IApp (tm1, tm2)) = union (op =) (vars_of_iterm vars tm1) (vars_of_iterm vars tm2)
+  | vars_of_iterm vars (IAbs (_, tm)) = vars_of_iterm vars tm
+
+fun generate_unique_name gen unique n =
+  let val x = gen n in
+    if unique x then x else generate_unique_name gen unique (n + 1)
+  end
+
+fun eta_expand_quantifier_body (tm as IAbs _) = tm
+  | eta_expand_quantifier_body tm =
+    let
+      (* We accumulate all variables because E 2.5 does not support variable shadowing. *)
+      val vars = vars_of_iterm [] tm
+      val x = generate_unique_name
+        (fn n => "X" ^ (if n = 0 then "" else string_of_int n))
+        (fn name => not (exists (equal name) vars)) 0
+      val T = domain_type (ityp_of tm)
+    in
+      IAbs ((`I x, T), IApp (tm, IConst (`I x, T, [])))
+    end
+
 fun introduce_proxies_in_iterm type_enc =
   let
-    fun tweak_ho_quant ho_quant T [IAbs _] = IConst (`I ho_quant, T, [])
-      | tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) _ =
-        (* Eta-expand "!!" and "??", to work around LEO-II 1.2.8 parser
-           limitation. This works in conjuction with special code in
-           "ATP_Problem" that uses the syntactic sugar "!" and "?" whenever
-           possible. *)
+    fun tweak_ho_quant ho_quant (T as Type (_, [p_T as Type (_, [x_T, _]), _])) [] =
+        (* Eta-expand "!!" and "??", to work around LEO-II, Leo-III, and Satallax parser
+           limitations. This works in conjunction with special code in "ATP_Problem" that uses the
+           syntactic sugar "!" and "?" whenever possible. *)
         IAbs ((`I "P", p_T),
               IApp (IConst (`I ho_quant, T, []),
                     IAbs ((`I "X", x_T),
                           IApp (IConst (`I "P", p_T, []),
                                 IConst (`I "X", x_T, [])))))
-      | tweak_ho_quant _ _ _ = raise Fail "unexpected type for quantifier"
+      | tweak_ho_quant ho_quant T _ = IConst (`I ho_quant, T, [])
+    fun tweak_ho_equal T argc =
+      if argc = 2 then
+        IConst (`I tptp_equal, T, [])
+      else
+        (* Eta-expand partially applied THF equality, because the LEO-II and Satallax parsers
+           complain about not being able to infer the type of "=". *)
+        let val i_T = domain_type T in
+          IAbs ((`I "Y", i_T),
+                IAbs ((`I "Z", i_T),
+                      IApp (IApp (IConst (`I tptp_equal, T, []),
+                                  IConst (`I "Y", i_T, [])),
+                            IConst (`I "Z", i_T, []))))
+        end
     fun intro top_level args (IApp (tm1, tm2)) =
-        IApp (intro top_level (tm2 :: args) tm1, intro false [] tm2)
+        let
+          val tm1' = intro top_level (tm2 :: args) tm1
+          val tm2' = intro false [] tm2
+          val tm2'' =
+            (case tm1' of
+              IConst ((s, _), _, _) =>
+              if s = tptp_ho_forall orelse s = tptp_ho_exists then
+                eta_expand_quantifier_body tm2'
+              else
+                tm2'
+            | _ => tm2')
+        in
+          IApp (tm1', tm2'')
+        end
       | intro top_level args (IConst (name as (s, _), T, T_args)) =
         (case proxify_const s of
           SOME proxy_base =>
           let
             val argc = length args
-            val plain_const = IConst (name, T, [])
+            fun plain_const () = IConst (name, T, [])
             fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
-            val is_fool = is_type_enc_fool type_enc
-            fun if_card_matches card x = if not is_fool orelse card = argc then x else plain_const
+            fun handle_fool card x = if card = argc then x else proxy_const ()
           in
-            if top_level orelse is_fool orelse is_type_enc_full_higher_order type_enc then
-              (case (top_level, s) of
-                (_, "c_False") => IConst (`I tptp_false, T, [])
-              | (_, "c_True") => IConst (`I tptp_true, T, [])
-              | (false, "c_Not") => if_card_matches 1 (IConst (`I tptp_not, T, []))
-              | (false, "c_conj") => if_card_matches 2 (IConst (`I tptp_and, T, []))
-              | (false, "c_disj") => if_card_matches 2 (IConst (`I tptp_or, T, []))
-              | (false, "c_implies") => if_card_matches 2 (IConst (`I tptp_implies, T, []))
-              | (false, "c_All") => if_card_matches 1 (tweak_ho_quant tptp_ho_forall T args)
-              | (false, "c_Ex") => if_card_matches 1 (tweak_ho_quant tptp_ho_exists T args)
-              | (false, s) =>
+            if top_level then
+              (case s of
+                "c_False" => IConst (`I tptp_false, T, [])
+              | "c_True" => IConst (`I tptp_true, T, [])
+              | _ => plain_const ())
+            else if is_type_enc_full_higher_order type_enc then
+              (case s of
+                "c_False" => IConst (`I tptp_false, T, [])
+              | "c_True" => IConst (`I tptp_true, T, [])
+              | "c_Not" => IConst (`I tptp_not, T, [])
+              | "c_conj" => IConst (`I tptp_and, T, [])
+              | "c_disj" => IConst (`I tptp_or, T, [])
+              | "c_implies" => IConst (`I tptp_implies, T, [])
+              | "c_All" => tweak_ho_quant tptp_ho_forall T args
+              | "c_Ex" => tweak_ho_quant tptp_ho_exists T args
+              | s =>
                 if is_tptp_equal s then
-                  if argc = 2 then
-                    IConst (`I tptp_equal, T, [])
-                  else if is_fool then
-                    proxy_const ()
-                  else
-                    (* Eta-expand partially applied THF equality, because the
-                       LEO-II and Satallax parsers complain about not being able to
-                       infer the type of "=". *)
-                    let val i_T = domain_type T in
-                      IAbs ((`I "Y", i_T),
-                            IAbs ((`I "Z", i_T),
-                                  IApp (IApp (IConst (`I tptp_equal, T, []),
-                                              IConst (`I "Y", i_T, [])),
-                                        IConst (`I "Z", i_T, []))))
-                    end
+                  tweak_ho_equal T argc
                 else
-                  plain_const
-              | _ => plain_const)
+                  plain_const ())
+            else if is_type_enc_fool type_enc then
+              (case s of
+                "c_False" => IConst (`I tptp_false, T, [])
+              | "c_True" => IConst (`I tptp_true, T, [])
+              | "c_Not" => handle_fool 1 (IConst (`I tptp_not, T, []))
+              | "c_conj" => handle_fool 2 (IConst (`I tptp_and, T, []))
+              | "c_disj" => handle_fool 2 (IConst (`I tptp_or, T, []))
+              | "c_implies" => handle_fool 2 (IConst (`I tptp_implies, T, []))
+              | "c_All" => handle_fool 1 (tweak_ho_quant tptp_ho_forall T args)
+              | "c_Ex" => handle_fool 1 (tweak_ho_quant tptp_ho_exists T args)
+              | s =>
+                if is_tptp_equal s then
+                  handle_fool 2 (IConst (`I tptp_equal, T, []))
+                else
+                  plain_const ())
             else
-              IConst (proxy_base |>> prefix const_prefix, T, T_args)
+              proxy_const ()
           end
-         | NONE => if s = tptp_choice then tweak_ho_quant tptp_choice T args
-                   else IConst (name, T, T_args))
+         | NONE =>
+           if s = tptp_choice then
+             tweak_ho_quant tptp_choice T args
+           else
+             IConst (name, T, T_args))
       | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm)
       | intro _ _ tm = tm
   in intro true [] end
@@ -1423,20 +1498,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 |
@@ -1833,17 +1908,17 @@
   else if lam_trans = liftingN orelse lam_trans = lam_liftingN then
     lift_lams ctxt type_enc
   else if lam_trans = combsN then
-    map (introduce_combinators ctxt) #> rpair []
+    map (introduce_combinators ctxt type_enc) #> rpair []
   else if lam_trans = combs_and_liftingN then
     lift_lams_part_1 ctxt type_enc
-    ##> maps (fn t => [t, introduce_combinators ctxt (intentionalize_def t)])
-    #> lift_lams_part_2 ctxt
+    ##> maps (fn t => [t, introduce_combinators ctxt type_enc (intentionalize_def t)])
+    #> lift_lams_part_2 ctxt type_enc
   else if lam_trans = combs_or_liftingN then
     lift_lams_part_1 ctxt type_enc
     ##> map (fn t => (case head_of (strip_qnt_body \<^const_name>\<open>All\<close> t) of
                        \<^term>\<open>(=) ::bool => bool => bool\<close> => t
-                     | _ => introduce_combinators ctxt (intentionalize_def t)))
-    #> lift_lams_part_2 ctxt
+                     | _ => introduce_combinators ctxt type_enc (intentionalize_def t)))
+    #> lift_lams_part_2 ctxt type_enc
   else if lam_trans = keep_lamsN then
     map (Envir.eta_contract) #> rpair []
   else
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Dec 16 00:08:31 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML	Wed Dec 16 09:59:15 2020 +0100
@@ -296,7 +296,7 @@
        val modern = string_ord (getenv "E_VERSION", "2.3") <> LESS
        val (format, enc) =
          if modern then
-           (THF (With_FOOL, Monomorphic, THF_Lambda_Bool_Free), "mono_native_higher")
+           (THF (With_FOOL, Monomorphic, THF_Lambda_Free), "mono_native_higher")
          else
            (TFF (Without_FOOL, Monomorphic), "mono_native")
      in