# HG changeset patch
# User hoelzl
# Date 1353089663 -3600
# Node ID 65d5b18e162654aba09f135c54daee1cd41b7d43
# Parent  de19856feb5468549d04ff5095134fe7fa8f5e81
moved (b)choice_iff(') to Hilbert_Choice

diff -r de19856feb54 -r 65d5b18e1626 src/HOL/Hilbert_Choice.thy
--- 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*}
 
diff -r de19856feb54 -r 65d5b18e1626 src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- 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 -
diff -r de19856feb54 -r 65d5b18e1626 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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"
diff -r de19856feb54 -r 65d5b18e1626 src/HOL/Probability/Lebesgue_Measure.thy
--- 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>