Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ATP.thy
changeset 74899 b4beb55c574e
parent 74896 f9908452b282 
--- 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>
isabelle