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)