author wenzelm Mon, 20 Sep 2021 13:52:09 +0200 changeset 74325 8d0c2d74ad63 parent 74324 308e74afab83 child 74326 b8a191ce08aa
tuned proofs --- eliminated 'guess';
 src/HOL/Filter.thy file | annotate | diff | comparison | revisions src/HOL/Library/Countable_Set.thy file | annotate | diff | comparison | revisions src/HOL/Library/Extended_Nonnegative_Real.thy file | annotate | diff | comparison | revisions src/HOL/Library/Extended_Real.thy file | annotate | diff | comparison | revisions
```--- 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)"
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```