# 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: "\x\S. \y. Q x y ==> \f. \x\S. Q x (f x)" by (fast elim: someI) +lemma choice_iff: "(\x. \y. Q x y) \ (\f. \x. Q x (f x))" +by (fast elim: someI) + +lemma choice_iff': "(\x. P x \ (\y. Q x y)) \ (\f. \x. P x \ Q x (f x))" +by (fast elim: someI) + +lemma bchoice_iff: "(\x\S. \y. Q x y) \ (\f. \x\S. Q x (f x))" +by (fast elim: someI) + +lemma bchoice_iff': "(\x\S. P x \ (\y. Q x y)) \ (\f. \x\S. P x \ 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: "(\x. \y. P x y) \ (\f. \x. P x (f x))" by metis - subsection {* Interlude: Some properties of real sets *} lemma seq_mono_lemma: assumes "\(n::nat) \ m. (d n :: real) < e n" and "\n \ m. e n <= e m" @@ -1377,8 +1375,6 @@ finally show ?thesis . qed -lemma choice_iff': "(\xy. P x y) \ (\f. \xix. P i x) \ (\x::'a. \i ?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: "(\a\A. \b. P a b) \ (\f. \a\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: "(\x\A. \y. P x y) \ (\f. \x\A. P x (f x))" - by metis - lemma absolutely_integrable_on_indicator[simp]: fixes A :: "'a::ordered_euclidean_space set" shows "((indicator A :: _ \ real) absolutely_integrable_on X) \