--- a/src/HOL/Hilbert_Choice.thy Fri Nov 16 18:45:57 2012 +0100
+++ b/src/HOL/Hilbert_Choice.thy Fri Nov 16 19:14:23 2012 +0100
@@ -86,6 +86,17 @@
lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
by (fast elim: someI)
+lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))"
+by (fast elim: someI)
+
+lemma choice_iff': "(\<forall>x. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x. P x \<longrightarrow> Q x (f x))"
+by (fast elim: someI)
+
+lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))"
+by (fast elim: someI)
+
+lemma bchoice_iff': "(\<forall>x\<in>S. P x \<longrightarrow> (\<exists>y. Q x y)) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. P x \<longrightarrow> Q x (f x))"
+by (fast elim: someI)
subsection {*Function Inverse*}
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 16 18:45:57 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Fri Nov 16 19:14:23 2012 +0100
@@ -398,8 +398,6 @@
then show "h = g" by (simp add: ext)
qed
-lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
-
subsection {* Interlude: Some properties of real sets *}
lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"
@@ -1377,8 +1375,6 @@
finally show ?thesis .
qed
-lemma choice_iff': "(\<forall>x<d. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x<d. P x (f x))" by metis
-
lemma lambda_skolem': "(\<forall>i<DIM('a::euclidean_space). \<exists>x. P i x) \<longleftrightarrow>
(\<exists>x::'a. \<forall>i<DIM('a). P i (x$$i))" (is "?lhs \<longleftrightarrow> ?rhs")
proof -
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 16 18:45:57 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Fri Nov 16 19:14:23 2012 +0100
@@ -3097,9 +3097,6 @@
assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
qed
-lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
- by metis
-
lemma nat_approx_posE:
fixes e::real
assumes "0 < e"
--- a/src/HOL/Probability/Lebesgue_Measure.thy Fri Nov 16 18:45:57 2012 +0100
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Fri Nov 16 19:14:23 2012 +0100
@@ -9,9 +9,6 @@
imports Finite_Product_Measure
begin
-lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
- by metis
-
lemma absolutely_integrable_on_indicator[simp]:
fixes A :: "'a::ordered_euclidean_space set"
shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>