src/HOL/Hilbert_Choice.thy

 done
 
 text\<open>Easier to apply than @{text someI} because the conclusion has only one
 occurrence of @{term P}.\<close>
 lemma someI2: "[| P a;  !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-by (blast intro: someI)
+  by (blast intro: someI)
 
 text\<open>Easier to apply than @{text someI2} if the witness comes from an
 existential formula\<close>
+
 lemma someI2_ex: "[| \<exists>a. P a; !!x. P x ==> Q x |] ==> Q (SOME x. P x)"
-by (blast intro: someI2)
+  by (blast intro: someI2)
+
+lemma someI2_bex: "[| \<exists>a\<in>A. P a; !!x. x \<in> A \<and> P x ==> Q x |] ==> Q (SOME x. x \<in> A \<and> P x)"
+  by (blast intro: someI2)
 
 lemma some_equality [intro]:
      "[| P a;  !!x. P x ==> x=a |] ==> (SOME x. P x) = a"
 by (blast intro: someI2)
 

 
 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)
 
 lemma dependent_nat_choice:
-  assumes  1: "\<exists>x. P 0 x" and 
+  assumes  1: "\<exists>x. P 0 x" and
            2: "\<And>x n. P n x \<Longrightarrow> \<exists>y. P (Suc n) y \<and> Q n x y"
   shows "\<exists>f. \<forall>n. P n (f n) \<and> Q n (f n) (f (Suc n))"
 proof (intro exI allI conjI)
   fix n def f \<equiv> "rec_nat (SOME x. P 0 x) (\<lambda>n x. SOME y. P (Suc n) y \<and> Q n x y)"
   have "P 0 (f 0)" "\<And>n. P n (f n) \<Longrightarrow> P (Suc n) (f (Suc n)) \<and> Q n (f n) (f (Suc n))"

 apply auto
 apply (force simp add: bij_is_inj)
 apply (blast intro: bij_is_surj [THEN surj_f_inv_f, symmetric])
 done
 
-lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A" 
+lemma bij_vimage_eq_inv_image: "bij f ==> f -` A = inv f ` A"
 apply (auto simp add: bij_is_surj [THEN surj_f_inv_f])
 apply (blast intro: bij_is_inj [THEN inv_into_f_f, symmetric])
 done
 
 lemma finite_fun_UNIVD1:

   { fix n have "Sseq n \<subseteq> S" "\<not> finite (Sseq n)" by (induct n) (auto simp add: Sseq_def inf) }
   moreover then have *: "\<And>n. pick n \<in> Sseq n"
     unfolding pick_def by (subst (asm) finite.simps) (auto simp add: ex_in_conv intro: someI_ex)
   ultimately have "range pick \<subseteq> S" by auto
   moreover
-  { fix n m                 
+  { fix n m
     have "pick n \<notin> Sseq (n + Suc m)" by (induct m) (auto simp add: Sseq_def pick_def)
     with * have "pick n \<noteq> pick (n + Suc m)" by auto
   }
   then have "inj pick" by (intro linorder_injI) (auto simp add: less_iff_Suc_add)
   ultimately show ?thesis by blast