--- 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>
--- 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),