src/HOL/Library/FuncSet.thy
 changeset 53381 355a4cac5440 parent 53015 a1119cf551e8 child 54417 dbb8ecfe1337
```     1.1 --- a/src/HOL/Library/FuncSet.thy	Tue Sep 03 19:58:00 2013 +0200
1.2 +++ b/src/HOL/Library/FuncSet.thy	Tue Sep 03 22:04:23 2013 +0200
1.3 @@ -375,7 +375,8 @@
1.4    proof (rule ccontr)
1.5      assume "\<not> ?thesis"
1.6      then have "\<forall>i. \<exists>y. (i \<in> I \<longrightarrow> y \<in> F i) \<and> (i \<notin> I \<longrightarrow> y = undefined)" by auto
1.7 -    from choice[OF this] guess f ..
1.8 +    from choice[OF this]
1.9 +    obtain f where " \<forall>x. (x \<in> I \<longrightarrow> f x \<in> F x) \<and> (x \<notin> I \<longrightarrow> f x = undefined)" ..
1.10      then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
1.11      with `Pi\<^sub>E I F = {}` show False by auto
1.12    qed
1.13 @@ -437,8 +438,10 @@
1.14    shows "F i \<subseteq> F' i"
1.15  proof
1.16    fix x assume "x \<in> F i"
1.17 -  with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))" by auto
1.18 -  from choice[OF this] guess f .. note f = this
1.19 +  with ne have "\<forall>j. \<exists>y. ((j \<in> I \<longrightarrow> y \<in> F j \<and> (i = j \<longrightarrow> x = y)) \<and> (j \<notin> I \<longrightarrow> y = undefined))"
1.20 +    by auto
1.21 +  from choice[OF this] obtain f
1.22 +    where f: " \<forall>j. (j \<in> I \<longrightarrow> f j \<in> F j \<and> (i = j \<longrightarrow> x = f j)) \<and> (j \<notin> I \<longrightarrow> f j = undefined)" ..
1.23    then have "f \<in> Pi\<^sub>E I F" by (auto simp: extensional_def PiE_def)
1.24    then have "f \<in> Pi\<^sub>E I F'" using assms by simp
1.25    then show "x \<in> F' i" using f `i \<in> I` by (auto simp: PiE_def)
```