--- a/src/HOL/Filter.thy Mon Sep 20 13:51:32 2021 +0200
+++ b/src/HOL/Filter.thy Mon Sep 20 13:52:09 2021 +0200
@@ -438,26 +438,27 @@
proof -
let ?F = "\<lambda>P. \<exists>X\<subseteq>B. finite X \<and> eventually P (Inf X)"
- { fix P have "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P"
- proof (rule eventually_Abs_filter is_filter.intro)+
- show "?F (\<lambda>x. True)"
- by (rule exI[of _ "{}"]) (simp add: le_fun_def)
- next
- fix P Q
- assume "?F P" then guess X ..
- moreover
- assume "?F Q" then guess Y ..
- ultimately show "?F (\<lambda>x. P x \<and> Q x)"
- by (intro exI[of _ "X \<union> Y"])
- (auto simp: Inf_union_distrib eventually_inf)
- next
- fix P Q
- assume "?F P" then guess X ..
- moreover assume "\<forall>x. P x \<longrightarrow> Q x"
- ultimately show "?F Q"
- by (intro exI[of _ X]) (auto elim: eventually_mono)
- qed }
- note eventually_F = this
+ have eventually_F: "eventually P (Abs_filter ?F) \<longleftrightarrow> ?F P" for P
+ proof (rule eventually_Abs_filter is_filter.intro)+
+ show "?F (\<lambda>x. True)"
+ by (rule exI[of _ "{}"]) (simp add: le_fun_def)
+ next
+ fix P Q
+ assume "?F P" "?F Q"
+ then obtain X Y where
+ "X \<subseteq> B" "finite X" "eventually P (\<Sqinter> X)"
+ "Y \<subseteq> B" "finite Y" "eventually Q (\<Sqinter> Y)" by blast
+ then show "?F (\<lambda>x. P x \<and> Q x)"
+ by (intro exI[of _ "X \<union> Y"]) (auto simp: Inf_union_distrib eventually_inf)
+ next
+ fix P Q
+ assume "?F P"
+ then obtain X where "X \<subseteq> B" "finite X" "eventually P (\<Sqinter> X)"
+ by blast
+ moreover assume "\<forall>x. P x \<longrightarrow> Q x"
+ ultimately show "?F Q"
+ by (intro exI[of _ X]) (auto elim: eventually_mono)
+ qed
have "Inf B = Abs_filter ?F"
proof (intro antisym Inf_greatest)
@@ -598,11 +599,12 @@
show ?case by (auto intro!: exI[of _ "\<lambda>_. True"])
next
case (2 P Q)
- from 2(1) guess P' by (elim exE conjE) note P' = this
- from 2(2) guess Q' by (elim exE conjE) note Q' = this
+ then obtain P' Q' where P'Q':
+ "eventually P' F" "\<forall>x. P' (f x) \<longrightarrow> P x"
+ "eventually Q' F" "\<forall>x. Q' (f x) \<longrightarrow> Q x"
+ by (elim exE conjE)
show ?case
- by (rule exI[of _ "\<lambda>x. P' x \<and> Q' x"])
- (insert P' Q', auto intro!: eventually_conj)
+ by (rule exI[of _ "\<lambda>x. P' x \<and> Q' x"]) (use P'Q' in \<open>auto intro!: eventually_conj\<close>)
next
case (3 P Q)
thus ?case by blast
--- a/src/HOL/Library/Countable_Set.thy Mon Sep 20 13:51:32 2021 +0200
+++ b/src/HOL/Library/Countable_Set.thy Mon Sep 20 13:52:09 2021 +0200
@@ -377,7 +377,8 @@
lemma infinite_countable_subset':
assumes X: "infinite X" shows "\<exists>C\<subseteq>X. countable C \<and> infinite C"
proof -
- from infinite_countable_subset[OF X] guess f ..
+ obtain f :: "nat \<Rightarrow> 'a" where "inj f" "range f \<subseteq> X"
+ using infinite_countable_subset [OF X] by blast
then show ?thesis
by (intro exI[of _ "range f"]) (auto simp: range_inj_infinite)
qed
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Sep 20 13:51:32 2021 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Mon Sep 20 13:52:09 2021 +0200
@@ -1150,7 +1150,8 @@
assume "infinite X" "X \<noteq> {}"
have "\<exists>y\<in>X. r < ennreal_of_enat y" if r: "r < top" for r
proof -
- from ennreal_Ex_less_of_nat[OF r] guess n .. note n = this
+ obtain n where n: "r < of_nat n"
+ using ennreal_Ex_less_of_nat[OF r] ..
have "\<not> (X \<subseteq> enat ` {.. n})"
using \<open>infinite X\<close> by (auto dest: finite_subset)
then obtain x where x: "x \<in> X" "x \<notin> enat ` {..n}"
@@ -1198,9 +1199,11 @@
using zero_neq_one by (intro exI)
show "\<And>x y::ennreal. x < y \<Longrightarrow> \<exists>z>x. z < y"
proof transfer
- fix x y :: ereal assume "0 \<le> x" and *: "x < y"
- moreover from dense[OF *] guess z ..
- ultimately show "\<exists>z\<in>Collect ((\<le>) 0). x < z \<and> z < y"
+ fix x y :: ereal
+ assume *: "0 \<le> x"
+ assume "x < y"
+ from dense[OF this] obtain z where "x < z \<and> z < y" ..
+ with * show "\<exists>z\<in>Collect ((\<le>) 0). x < z \<and> z < y"
by (intro bexI[of _ z]) auto
qed
qed (rule open_ennreal_def)
@@ -1693,8 +1696,9 @@
show "x \<le> (SUP i\<in>A. f i)"
proof (rule ennreal_le_epsilon)
fix e :: real assume "0 < e"
- from approx[OF this] guess i ..
- then have "x \<le> f i + e"
+ from approx[OF this] obtain i where "i \<in> A" and *: "x \<le> f i + ennreal e"
+ by blast
+ from * have "x \<le> f i + e"
by simp
also have "\<dots> \<le> (SUP i\<in>A. f i) + e"
by (intro add_mono \<open>i \<in> A\<close> SUP_upper order_refl)
@@ -1711,7 +1715,8 @@
show "(INF i\<in>A. f i) \<le> x"
proof (rule ennreal_le_epsilon)
fix e :: real assume "0 < e"
- from approx[OF this] guess i .. note i = this
+ from approx[OF this] obtain i where "i\<in>A" "f i \<le> x + ennreal e"
+ by blast
then have "(INF i\<in>A. f i) \<le> f i"
by (intro INF_lower)
also have "\<dots> \<le> x + e"
--- a/src/HOL/Library/Extended_Real.thy Mon Sep 20 13:51:32 2021 +0200
+++ b/src/HOL/Library/Extended_Real.thy Mon Sep 20 13:52:09 2021 +0200
@@ -2445,7 +2445,7 @@
then obtain l where "incseq l" and l: "l i < Sup A" and l_Sup: "l \<longlonglongrightarrow> Sup A" for i :: nat
by (auto dest: countable_approach)
- have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))"
+ have "\<exists>f. \<forall>n. (f n \<in> A \<and> l n \<le> f n) \<and> (f n \<le> f (Suc n))" (is "\<exists>f. ?P f")
proof (rule dependent_nat_choice)
show "\<exists>x. x \<in> A \<and> l 0 \<le> x"
using l[of 0] by (auto simp: less_Sup_iff)
@@ -2456,7 +2456,7 @@
ultimately show "\<exists>y. (y \<in> A \<and> l (Suc n) \<le> y) \<and> x \<le> y"
by (auto intro!: exI[of _ "max x y"] split: split_max)
qed
- then guess f .. note f = this
+ then obtain f where f: "?P f" ..
then have "range f \<subseteq> A" "incseq f"
by (auto simp: incseq_Suc_iff)
moreover
@@ -3632,17 +3632,17 @@
have "N \<subseteq> A \<Longrightarrow> (SUP i\<in>I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i\<in>I. f n i)" for N
proof (induction N rule: infinite_finite_induct)
case (insert n N)
- moreover have "(SUP i\<in>I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i\<in>I. f n i) + (SUP i\<in>I. \<Sum>l\<in>N. f l i)"
+ have "(SUP i\<in>I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i\<in>I. f n i) + (SUP i\<in>I. \<Sum>l\<in>N. f l i)"
proof (rule SUP_ereal_add_directed)
fix i assume "i \<in> I" then show "0 \<le> f n i" "0 \<le> (\<Sum>l\<in>N. f l i)"
using insert by (auto intro!: sum_nonneg nonneg)
next
fix i j assume "i \<in> I" "j \<in> I"
- from directed[OF \<open>insert n N \<subseteq> A\<close> this] guess k ..
- then show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)"
- by (intro bexI[of _ k]) (auto intro!: add_mono sum_mono)
+ from directed[OF insert(4) this]
+ show "\<exists>k\<in>I. f n i + (\<Sum>l\<in>N. f l j) \<le> f n k + (\<Sum>l\<in>N. f l k)"
+ by (auto intro!: add_mono sum_mono)
qed
- ultimately show ?case
+ with insert show ?case
by simp
qed (simp_all add: SUP_constant \<open>I \<noteq> {}\<close>)
from this[of A] show ?thesis by simp