moved (b)choice_iff(') to Hilbert_Choice
authorhoelzl
Fri Nov 16 19:14:23 2012 +0100 (2012-11-16)
changeset 5010565d5b18e1626
parent 50104 de19856feb54
child 50106 e12e4ad93183
moved (b)choice_iff(') to Hilbert_Choice
src/HOL/Hilbert_Choice.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
src/HOL/Probability/Lebesgue_Measure.thy
     1.1 --- a/src/HOL/Hilbert_Choice.thy	Fri Nov 16 18:45:57 2012 +0100
     1.2 +++ b/src/HOL/Hilbert_Choice.thy	Fri Nov 16 19:14:23 2012 +0100
     1.3 @@ -86,6 +86,17 @@
     1.4  lemma bchoice: "\<forall>x\<in>S. \<exists>y. Q x y ==> \<exists>f. \<forall>x\<in>S. Q x (f x)"
     1.5  by (fast elim: someI)
     1.6  
     1.7 +lemma choice_iff: "(\<forall>x. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x. Q x (f x))"
     1.8 +by (fast elim: someI)
     1.9 +
    1.10 +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))"
    1.11 +by (fast elim: someI)
    1.12 +
    1.13 +lemma bchoice_iff: "(\<forall>x\<in>S. \<exists>y. Q x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>S. Q x (f x))"
    1.14 +by (fast elim: someI)
    1.15 +
    1.16 +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))"
    1.17 +by (fast elim: someI)
    1.18  
    1.19  subsection {*Function Inverse*}
    1.20  
     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 18:45:57 2012 +0100
     2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Nov 16 19:14:23 2012 +0100
     2.3 @@ -398,8 +398,6 @@
     2.4    then show "h = g" by (simp add: ext)
     2.5  qed
     2.6  
     2.7 -lemma choice_iff: "(\<forall>x. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x. P x (f x))" by metis
     2.8 -
     2.9  subsection {* Interlude: Some properties of real sets *}
    2.10  
    2.11  lemma seq_mono_lemma: assumes "\<forall>(n::nat) \<ge> m. (d n :: real) < e n" and "\<forall>n \<ge> m. e n <= e m"
    2.12 @@ -1377,8 +1375,6 @@
    2.13    finally show ?thesis .
    2.14  qed
    2.15  
    2.16 -lemma choice_iff': "(\<forall>x<d. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x<d. P x (f x))" by metis
    2.17 -
    2.18  lemma lambda_skolem': "(\<forall>i<DIM('a::euclidean_space). \<exists>x. P i x) \<longleftrightarrow>
    2.19     (\<exists>x::'a. \<forall>i<DIM('a). P i (x$$i))" (is "?lhs \<longleftrightarrow> ?rhs")
    2.20  proof -
     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 18:45:57 2012 +0100
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Nov 16 19:14:23 2012 +0100
     3.3 @@ -3097,9 +3097,6 @@
     3.4    assume ?rhs thus ?lhs by (rule bolzano_weierstrass_imp_compact)
     3.5  qed
     3.6  
     3.7 -lemma bchoice_iff: "(\<forall>a\<in>A. \<exists>b. P a b) \<longleftrightarrow> (\<exists>f. \<forall>a\<in>A. P a (f a))"
     3.8 -  by metis
     3.9 -
    3.10  lemma nat_approx_posE:
    3.11    fixes e::real
    3.12    assumes "0 < e"
     4.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 18:45:57 2012 +0100
     4.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Fri Nov 16 19:14:23 2012 +0100
     4.3 @@ -9,9 +9,6 @@
     4.4    imports Finite_Product_Measure
     4.5  begin
     4.6  
     4.7 -lemma bchoice_iff: "(\<forall>x\<in>A. \<exists>y. P x y) \<longleftrightarrow> (\<exists>f. \<forall>x\<in>A. P x (f x))"
     4.8 -  by metis
     4.9 -
    4.10  lemma absolutely_integrable_on_indicator[simp]:
    4.11    fixes A :: "'a::ordered_euclidean_space set"
    4.12    shows "((indicator A :: _ \<Rightarrow> real) absolutely_integrable_on X) \<longleftrightarrow>