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