# HG changeset patch
# User wenzelm
# Date 1632138729 -7200
# Node ID 8d0c2d74ad63586edeea90317da85c6e188f81c5
# Parent  308e74afab83276f8ede46db31377318384e2e48
tuned proofs --- eliminated 'guess';

diff -r 308e74afab83 -r 8d0c2d74ad63 src/HOL/Filter.thy
--- 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
diff -r 308e74afab83 -r 8d0c2d74ad63 src/HOL/Library/Countable_Set.thy
--- 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
diff -r 308e74afab83 -r 8d0c2d74ad63 src/HOL/Library/Extended_Nonnegative_Real.thy
--- 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"
diff -r 308e74afab83 -r 8d0c2d74ad63 src/HOL/Library/Extended_Real.thy
--- 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