# HG changeset patch
# User desharna
# Date 1638197117 -3600
# Node ID b4beb55c574eac369ed3079677fdf98197dd22ca
# Parent  e83224066f1944c57b9b4c62efc885675414d784
proper handling of Hilbert choice in TFX logics

diff -r e83224066f19 -r b4beb55c574e src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Sun Nov 28 21:16:35 2021 +0100
+++ b/src/HOL/ATP.thy	Mon Nov 29 15:45:17 2021 +0100
@@ -133,10 +133,17 @@
 "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
+lemma fChoice_iff_Ex: "P (fChoice P) \<longleftrightarrow> HOL.Ex P"
+  unfolding fChoice_def
   by (fact some_eq_ex)
 
+text \<open>
+We use the @{const HOL.Ex} constant on the right-hand side of @{thm [source] fChoice_iff_Ex} because
+we want to use the TPTP-native version if fChoice is introduced in a logic that supports FOOL.
+In logics that don't support it, it gets replaced by fEx during processing.
+Notice that we cannot use @{term "\<exists>x. P x"}, as existentials are not skolimized by the metis proof
+method but @{term "Ex P"} is eta-expanded if FOOL is supported.\<close>
+
 subsection \<open>Basic connection between ATPs and HOL\<close>
 
 ML_file \<open>Tools/lambda_lifting.ML\<close>
diff -r e83224066f19 -r b4beb55c574e src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sun Nov 28 21:16:35 2021 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Nov 29 15:45:17 2021 +0100
@@ -1320,6 +1320,7 @@
                   | "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)
+                  | "c_Choice" => proxy_const ()
                   | s =>
                     if is_tptp_equal s then
                       handle_fool 2 (IConst (`I tptp_equal, T, []))
@@ -1861,9 +1862,25 @@
       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)})]),
-   (("fChoice", false), [(General, @{thm fChoice_iff_fEx})])]
+   (("fChoice", true), [(General, @{thm fChoice_iff_Ex})])]
   |> map (apsnd (map (apsnd zero_var_indexes)))
 
+val () =
+  let
+    fun is_skolemizable \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> = true
+      | is_skolemizable _ = false
+
+    fun check_no_skolemizable_thm thm =
+      if Term.exists_subterm is_skolemizable (Thm.full_prop_of thm) then
+        error "Theorems of the helper table cannot contain skolemizable terms because they don't \
+        \get skolimized in metis."
+      else
+        ()
+  in
+    helper_table true
+    |> List.app (fn (_, thms) => List.app (check_no_skolemizable_thm o snd) thms)
+  end
+
 fun completish_helper_table with_combs =
   helper_table with_combs @
   [((predicator_name, true),