# HG changeset patch
# User desharna
# Date 1637490076 -3600
# Node ID f9908452b2824d1a80ef39cc9a4ed99c09dfb357
# Parent  b605ebd87a4748d15899c68da9ea975873ca9fd8
proper proxy for Hilbert choice in TPTP output

diff -r b605ebd87a47 -r f9908452b282 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Fri Nov 19 11:04:53 2021 +0100
+++ b/src/HOL/ATP.thy	Sun Nov 21 11:21:16 2021 +0100
@@ -7,7 +7,7 @@
 section \<open>Automatic Theorem Provers (ATPs)\<close>
 
 theory ATP
-  imports Meson
+  imports Meson Hilbert_Choice
 begin
 
 subsection \<open>ATP problems and proofs\<close>
@@ -50,6 +50,9 @@
 definition fequal :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where
 "fequal x y \<longleftrightarrow> (x = y)"
 
+definition fChoice :: "('a \<Rightarrow> bool) \<Rightarrow> 'a" where
+  "fChoice \<equiv> Hilbert_Choice.Eps"
+
 lemma fTrue_ne_fFalse: "fFalse \<noteq> fTrue"
 unfolding fFalse_def fTrue_def by simp
 
@@ -130,6 +133,9 @@
 "fequal x y = fFalse \<or> fequal (f x) (f y) = fTrue"
 unfolding fFalse_def fTrue_def fequal_def by auto
 
+lemma fChoice_iff_fEx: "P (fChoice P) \<longleftrightarrow> fEx P"
+  unfolding fChoice_def fEx_def
+  by (fact some_eq_ex)
 
 subsection \<open>Basic connection between ATPs and HOL\<close>
 
diff -r b605ebd87a47 -r f9908452b282 src/HOL/Tools/ATP/atp_problem.ML
--- a/src/HOL/Tools/ATP/atp_problem.ML	Fri Nov 19 11:04:53 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML	Sun Nov 21 11:21:16 2021 +0100
@@ -393,6 +393,10 @@
 
 fun is_format_higher_order (THF _) = true
   | is_format_higher_order _ = false
+
+fun is_format_higher_order_with_choice (THF (_, _, THF_With_Choice)) = true
+  | is_format_higher_order_with_choice _ = false
+
 fun is_format_typed (TFF _) = true
   | is_format_typed (THF _) = true
   | is_format_typed (DFG _) = true
@@ -519,7 +523,7 @@
             if ts = [] orelse is_format_higher_order format then
               app0 (s ^ "(" ^ declaration ^ ", " ^ definition ^ ", " ^ usage ^ ")") [] ts
             else
-              error (tptp_let ^ " is special syntax and more than three arguments is only \
+              error (tptp_let ^ " is special syntax and more than two arguments is only \
                 \supported in higher order")
           end
         | _ => error (tptp_let ^ " is special syntax and must have at least two arguments"))
@@ -529,19 +533,21 @@
           if ts = [] orelse is_format_higher_order format then
             app0 (s ^ "(" ^ of_term t1 ^ ", " ^ of_term t2 ^ ", " ^ of_term t3 ^ ")") [] ts
           else
-            error (tptp_ite ^" is special syntax and more than three arguments is only supported \
+            error (tptp_ite ^ " is special syntax and more than three arguments is only supported \
               \in higher order")
-        | _ => error "$ite is special syntax and must have at least three arguments")
+        | _ => error (tptp_ite ^ " is special syntax and must have at least three arguments"))
       else if s = tptp_choice then
         (case ts of
-          [AAbs (((s', ty), tm), args)] =>
+          (AAbs (((s', ty), tm), args) :: ts) =>
           (* 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 ())
+          if ts = [] orelse is_format_higher_order_with_choice format then
+            let val declaration = s' ^ " : " ^ of_type ty in
+              app0 ("(" ^ tptp_choice ^ "[" ^ declaration ^ "]: " ^ of_term tm ^ ")") [] (args @ ts)
+            end
+          else
+            error (tptp_choice ^ " is only supported in higher order")
+        | _ => error (tptp_choice ^ " must be followed by a lambda abstraction"))
       else
         (case (Symtab.lookup tptp_builtins s, ts) of
           (SOME {arity = 1, is_predicate = true}, [t]) =>
diff -r b605ebd87a47 -r f9908452b282 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Fri Nov 19 11:04:53 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Nov 21 11:21:16 2021 +0100
@@ -171,6 +171,8 @@
 fun is_type_enc_higher_order (Native (Higher_Order _, _, _, _)) = true
   | is_type_enc_higher_order _ = false
 
+fun has_type_enc_choice (Native (Higher_Order THF_With_Choice, _, _, _)) = true
+  | has_type_enc_choice _ = false
 fun has_type_enc_ite (Native (_, With_FOOL {with_ite, ...}, _, _)) = with_ite
   | has_type_enc_ite _ = false
 fun has_type_enc_let (Native (_, With_FOOL {with_let, ...}, _, _)) = with_let
@@ -331,7 +333,8 @@
    ("c_implies", (\<^const_name>\<open>implies\<close>, (@{thm fimplies_def}, ("fimplies", \<^const_name>\<open>fimplies\<close>)))),
    ("equal", (\<^const_name>\<open>HOL.eq\<close>, (@{thm fequal_def}, ("fequal", \<^const_name>\<open>fequal\<close>)))),
    ("c_All", (\<^const_name>\<open>All\<close>, (@{thm fAll_def}, ("fAll", \<^const_name>\<open>fAll\<close>)))),
-   ("c_Ex", (\<^const_name>\<open>Ex\<close>, (@{thm fEx_def}, ("fEx", \<^const_name>\<open>fEx\<close>))))]
+   ("c_Ex", (\<^const_name>\<open>Ex\<close>, (@{thm fEx_def}, ("fEx", \<^const_name>\<open>fEx\<close>)))),
+   ("c_Choice", (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, (@{thm fChoice_def}, ("fChoice", \<^const_name>\<open>fChoice\<close>))))]
 
 val proxify_const = AList.lookup (op =) proxy_table #> Option.map (snd o snd)
 
@@ -350,6 +353,7 @@
    (\<^const_name>\<open>If\<close>, "If"),
    (\<^const_name>\<open>Set.member\<close>, "member"),
    (\<^const_name>\<open>HOL.Let\<close>, "Let"),
+   (\<^const_name>\<open>Hilbert_Choice.Eps\<close>, "Choice"),
    (\<^const_name>\<open>Meson.COMBI\<close>, combinator_prefix ^ "I"),
    (\<^const_name>\<open>Meson.COMBK\<close>, combinator_prefix ^ "K"),
    (\<^const_name>\<open>Meson.COMBB\<close>, combinator_prefix ^ "B"),
@@ -387,15 +391,8 @@
 fun tvar_name ((x as (s, _)), _) = (make_tvar x, s)
 
 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
-local
-  val choice_const = (fst o dest_Const o HOLogic.choice_const) dummyT
-  fun default c = const_prefix ^ lookup_const c
-in
-  fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
-    | make_fixed_const (SOME (Native (Higher_Order THF_With_Choice, _, _, _))) c =
-      if c = choice_const then tptp_choice else default c
-    | make_fixed_const _ c = default c
-end
+fun make_fixed_const _ \<^const_name>\<open>HOL.eq\<close> = tptp_old_equal
+  | make_fixed_const _ c = const_prefix ^ lookup_const c
 
 fun make_fixed_type_const c = type_const_prefix ^ lookup_const c
 
@@ -1221,6 +1218,7 @@
     val is_fool = is_type_enc_fool type_enc
     val has_ite = has_type_enc_ite type_enc
     val has_let = has_type_enc_let type_enc
+    val has_choice = has_type_enc_choice type_enc
     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
@@ -1264,7 +1262,7 @@
               else
                 tm2'
             | IConst ((s, _), _, _) =>
-              if s = tptp_ho_forall orelse s = tptp_ho_exists then
+              if s = tptp_ho_forall orelse s = tptp_ho_exists orelse s = tptp_choice then
                 eta_expand_quantifier_body tm2'
               else
                 tm2'
@@ -1285,6 +1283,7 @@
                 fun plain_const () = IConst (name, T, [])
                 fun proxy_const () = IConst (proxy_base |>> prefix const_prefix, T, T_args)
                 fun handle_fool card x = if card = argc then x else proxy_const ()
+                fun handle_min_card card x = if argc < card then proxy_const () else x
               in
                 if top_level then
                   (case s of
@@ -1301,6 +1300,11 @@
                   | "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
+                  | "c_Choice" =>
+                    if has_choice then
+                      handle_min_card 1 (IConst (`I tptp_choice, T, []))
+                    else
+                      proxy_const ()
                   | s =>
                     if is_tptp_equal s then
                       tweak_ho_equal T argc
@@ -1856,7 +1860,8 @@
    (* Partial characterization of "fAll" and "fEx". A complete characterization
       would require the axiom of choice for replay with Metis. *)
    (("fAll", false), [(General, @{lemma "\<not> fAll P \<or> P x" by (auto simp: fAll_def)})]),
-   (("fEx", false), [(General, @{lemma "\<not> P x \<or> fEx P" by (auto simp: fEx_def)})])]
+   (("fEx", false), [(General, @{lemma "\<not> P x \<or> fEx P" by (auto simp: fEx_def)})]),
+   (("fChoice", false), [(General, @{thm fChoice_iff_fEx})])]
   |> map (apsnd (map (apsnd zero_var_indexes)))
 
 fun completish_helper_table with_combs =