--- a/src/HOL/Analysis/Abstract_Topology_2.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Abstract_Topology_2.thy Fri Sep 24 22:44:13 2021 +0200
@@ -50,9 +50,8 @@
proof (cases "x \<in> A")
assume x: "x \<in> A"
hence "indicator A x \<in> ({0<..<2} :: real set)" by simp
- hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set))"
- using 1 open_greaterThanLessThan by blast
- then guess U .. note U = this
+ with 1 obtain U where U: "open U" "x \<in> U" "\<forall>y\<in>U. indicator A y \<in> ({0<..<2} :: real set)"
+ using open_greaterThanLessThan by metis
hence "\<forall>y\<in>U. indicator A y > (0::real)"
unfolding greaterThanLessThan_def by auto
hence "U \<subseteq> A" using indicator_eq_0_iff by force
@@ -61,9 +60,8 @@
next
assume x: "x \<notin> A"
hence "indicator A x \<in> ({-1<..<1} :: real set)" by simp
- hence "\<exists>U. open U \<and> x \<in> U \<and> (\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set))"
- using 1 open_greaterThanLessThan by blast
- then guess U .. note U = this
+ with 1 obtain U where U: "open U" "x \<in> U" "\<forall>y\<in>U. indicator A y \<in> ({-1<..<1} :: real set)"
+ using 1 open_greaterThanLessThan by metis
hence "\<forall>y\<in>U. indicator A y < (1::real)"
unfolding greaterThanLessThan_def by auto
hence "U \<subseteq> -A" by auto
--- a/src/HOL/Analysis/Binary_Product_Measure.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Fri Sep 24 22:44:13 2021 +0200
@@ -242,7 +242,11 @@
lemma (in sigma_finite_measure) measurable_emeasure_Pair:
assumes Q: "Q \<in> sets (N \<Otimes>\<^sub>M M)" shows "(\<lambda>x. emeasure M (Pair x -` Q)) \<in> borel_measurable N" (is "?s Q \<in> _")
proof -
- from sigma_finite_disjoint guess F . note F = this
+ obtain F :: "nat \<Rightarrow> 'a set" where F:
+ "range F \<subseteq> sets M"
+ "\<Union> (range F) = space M"
+ "\<And>i. emeasure M (F i) \<noteq> \<infinity>"
+ "disjoint_family F" by (blast intro: sigma_finite_disjoint)
then have F_sets: "\<And>i. F i \<in> sets M" by auto
let ?C = "\<lambda>x i. F i \<inter> Pair x -` Q"
{ fix i
@@ -361,8 +365,16 @@
shows "\<exists>F::nat \<Rightarrow> ('a \<times> 'b) set. range F \<subseteq> E \<and> incseq F \<and> (\<Union>i. F i) = space M1 \<times> space M2 \<and>
(\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>)"
proof -
- from M1.sigma_finite_incseq guess F1 . note F1 = this
- from M2.sigma_finite_incseq guess F2 . note F2 = this
+ obtain F1 where F1: "range F1 \<subseteq> sets M1"
+ "\<Union> (range F1) = space M1"
+ "\<And>i. emeasure M1 (F1 i) \<noteq> \<infinity>"
+ "incseq F1"
+ by (rule M1.sigma_finite_incseq) blast
+ obtain F2 where F2: "range F2 \<subseteq> sets M2"
+ "\<Union> (range F2) = space M2"
+ "\<And>i. emeasure M2 (F2 i) \<noteq> \<infinity>"
+ "incseq F2"
+ by (rule M2.sigma_finite_incseq) blast
from F1 F2 have space: "space M1 = (\<Union>i. F1 i)" "space M2 = (\<Union>i. F2 i)" by auto
let ?F = "\<lambda>i. F1 i \<times> F2 i"
show ?thesis
@@ -396,9 +408,11 @@
sublocale\<^marker>\<open>tag unimportant\<close> pair_sigma_finite \<subseteq> P?: sigma_finite_measure "M1 \<Otimes>\<^sub>M M2"
proof
- from M1.sigma_finite_countable guess F1 ..
- moreover from M2.sigma_finite_countable guess F2 ..
- ultimately show
+ obtain F1 :: "'a set set" and F2 :: "'b set set" where
+ "countable F1 \<and> F1 \<subseteq> sets M1 \<and> \<Union> F1 = space M1 \<and> (\<forall>a\<in>F1. emeasure M1 a \<noteq> \<infinity>)"
+ "countable F2 \<and> F2 \<subseteq> sets M2 \<and> \<Union> F2 = space M2 \<and> (\<forall>a\<in>F2. emeasure M2 a \<noteq> \<infinity>)"
+ using M1.sigma_finite_countable M2.sigma_finite_countable by auto
+ then show
"\<exists>A. countable A \<and> A \<subseteq> sets (M1 \<Otimes>\<^sub>M M2) \<and> \<Union>A = space (M1 \<Otimes>\<^sub>M M2) \<and> (\<forall>a\<in>A. emeasure (M1 \<Otimes>\<^sub>M M2) a \<noteq> \<infinity>)"
by (intro exI[of _ "(\<lambda>(a, b). a \<times> b) ` (F1 \<times> F2)"] conjI)
(auto simp: M2.emeasure_pair_measure_Times space_pair_measure set_eq_iff subset_eq ennreal_mult_eq_top_iff)
@@ -422,8 +436,10 @@
lemma (in pair_sigma_finite) distr_pair_swap:
"M1 \<Otimes>\<^sub>M M2 = distr (M2 \<Otimes>\<^sub>M M1) (M1 \<Otimes>\<^sub>M M2) (\<lambda>(x, y). (y, x))" (is "?P = ?D")
proof -
- from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
+ obtain F :: "nat \<Rightarrow> ('a \<times> 'b) set" where F: "range F \<subseteq> ?E"
+ "incseq F" "\<Union> (range F) = space M1 \<times> space M2" "\<forall>i. emeasure (M1 \<Otimes>\<^sub>M M2) (F i) \<noteq> \<infinity>"
+ using sigma_finite_up_in_pair_measure_generator by auto
show ?thesis
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
show "?E \<subseteq> Pow (space ?P)"
@@ -432,9 +448,8 @@
by (simp add: sets_pair_measure space_pair_measure)
then show "sets ?D = sigma_sets (space ?P) ?E"
by simp
- next
- show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
- using F by (auto simp: space_pair_measure)
+ from F show "range F \<subseteq> ?E" "(\<Union>i. F i) = space ?P" "\<And>i. emeasure ?P (F i) \<noteq> \<infinity>"
+ by (auto simp: space_pair_measure)
next
fix X assume "X \<in> ?E"
then obtain A B where X[simp]: "X = A \<times> B" and A: "A \<in> sets M1" and B: "B \<in> sets M2" by auto
@@ -899,7 +914,9 @@
shows "sigma_finite_measure M"
proof -
interpret sigma_finite_measure "distr M N f" by fact
- from sigma_finite_countable guess A .. note A = this
+ obtain A where A: "countable A" "A \<subseteq> sets (distr M N f)"
+ "\<Union> A = space (distr M N f)" "\<forall>a\<in>A. emeasure (distr M N f) a \<noteq> \<infinity>"
+ using sigma_finite_countable by auto
show ?thesis
proof
show "\<exists>A. countable A \<and> A \<subseteq> sets M \<and> \<Union>A = space M \<and> (\<forall>a\<in>A. emeasure M a \<noteq> \<infinity>)"
@@ -933,9 +950,12 @@
interpret M1: sigma_finite_measure M1 by fact
interpret M2: sigma_finite_measure M2 by fact
interpret pair_sigma_finite M1 M2 ..
- from sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('a \<times> 'b) set" .. note F = this
let ?E = "{a \<times> b |a b. a \<in> sets M1 \<and> b \<in> sets M2}"
let ?P = "M1 \<Otimes>\<^sub>M M2"
+ obtain F :: "nat \<Rightarrow> ('a \<times> 'b) set" where F:
+ "range F \<subseteq> ?E" "incseq F" "\<Union> (range F) = space M1 \<times> space M2" "\<forall>i. emeasure ?P (F i) \<noteq> \<infinity>"
+ using sigma_finite_up_in_pair_measure_generator
+ by blast
show ?thesis
proof (rule measure_eqI_generator_eq[OF Int_stable_pair_measure_generator[of M1 M2]])
show "?E \<subseteq> Pow (space ?P)"
--- a/src/HOL/Analysis/Bochner_Integration.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Bochner_Integration.thy Fri Sep 24 22:44:13 2021 +0200
@@ -2952,8 +2952,12 @@
assumes f[measurable]: "case_prod f \<in> borel_measurable (N \<Otimes>\<^sub>M M)"
shows "(\<lambda>x. \<integral>y. f x y \<partial>M) \<in> borel_measurable N"
proof -
- from borel_measurable_implies_sequence_metric[OF f, of 0] guess s ..
- then have s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
+ from borel_measurable_implies_sequence_metric[OF f, of 0]
+ obtain s where s: "\<And>i. simple_function (N \<Otimes>\<^sub>M M) (s i)"
+ and "\<forall>x\<in>space (N \<Otimes>\<^sub>M M). (\<lambda>i. s i x) \<longlonglongrightarrow> (case x of (x, y) \<Rightarrow> f x y)"
+ and "\<forall>i. \<forall>x\<in>space (N \<Otimes>\<^sub>M M). dist (s i x) 0 \<le> 2 * dist (case x of (x, xa) \<Rightarrow> f x xa) 0"
+ by auto
+ then have *:
"\<And>x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> (\<lambda>i. s i (x, y)) \<longlonglongrightarrow> f x y"
"\<And>i x y. x \<in> space N \<Longrightarrow> y \<in> space M \<Longrightarrow> norm (s i (x, y)) \<le> 2 * norm (f x y)"
by (auto simp: space_pair_measure)
@@ -2970,7 +2974,7 @@
{ fix i x assume "x \<in> space N"
then have "simple_bochner_integral M (\<lambda>y. s i (x, y)) =
(\<Sum>z\<in>s i ` (space N \<times> space M). measure M {y \<in> space M. s i (x, y) = z} *\<^sub>R z)"
- using s(1)[THEN simple_functionD(1)]
+ using s[THEN simple_functionD(1)]
unfolding simple_bochner_integral_def
by (intro sum.mono_neutral_cong_left)
(auto simp: eq_commute space_pair_measure image_iff cong: conj_cong) }
@@ -2991,9 +2995,9 @@
show "\<And>i. (\<lambda>y. s i (x, y)) \<in> borel_measurable M"
using x by simp
show "AE xa in M. (\<lambda>i. s i (x, xa)) \<longlonglongrightarrow> f x xa"
- using x s(2) by auto
+ using x * by auto
show "\<And>i. AE xa in M. norm (s i (x, xa)) \<le> 2 * norm (f x xa)"
- using x s(3) by auto
+ using x * by auto
qed fact
moreover
{ fix i
@@ -3006,7 +3010,7 @@
by (intro simple_function_borel_measurable)
(auto simp: space_pair_measure dest: finite_subset)
have "(\<integral>\<^sup>+ y. ennreal (norm (s i (x, y))) \<partial>M) \<le> (\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M)"
- using x s by (intro nn_integral_mono) auto
+ using x * by (intro nn_integral_mono) auto
also have "(\<integral>\<^sup>+ y. 2 * norm (f x y) \<partial>M) < \<infinity>"
using int_2f unfolding integrable_iff_bounded by simp
finally show "(\<integral>\<^sup>+ xa. ennreal (norm (s i (x, xa))) \<partial>M) < \<infinity>" .
--- a/src/HOL/Analysis/Borel_Space.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Borel_Space.thy Fri Sep 24 22:44:13 2021 +0200
@@ -101,11 +101,10 @@
thus ?thesis by auto
qed
qed
- hence "\<exists>g :: real \<Rightarrow> nat \<times> rat . \<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}.
+ then obtain g :: "real \<Rightarrow> nat \<times> rat" where "\<forall>a \<in> {a\<in>A. \<not> continuous (at a within A) f}.
(fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (\<forall>x \<in> A. x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
(fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (\<forall>x \<in> A. x > a \<longrightarrow> f x > of_rat (snd (g a))))"
- by (rule bchoice)
- then guess g ..
+ by (rule bchoice [THEN exE]) blast
hence g: "\<And>a x. a \<in> A \<Longrightarrow> \<not> continuous (at a within A) f \<Longrightarrow> x \<in> A \<Longrightarrow>
(fst (g a) = 0 \<and> of_rat (snd (g a)) < f a \<and> (x < a \<longrightarrow> f x < of_rat (snd (g a)))) |
(fst (g a) = 1 \<and> of_rat (snd (g a)) > f a \<and> (x > a \<longrightarrow> f x > of_rat (snd (g a))))"
@@ -579,7 +578,8 @@
"borel = sigma UNIV (range lessThan :: 'a::{linorder_topology, second_countable_topology} set set)"
unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
- from countable_dense_setE guess D :: "'a set" . note D = this
+ obtain D :: "'a set" where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
+ by (rule countable_dense_setE) blast
interpret L: sigma_algebra UNIV "sigma_sets UNIV (range lessThan)"
by (rule sigma_algebra_sigma_sets) simp
@@ -617,7 +617,8 @@
"borel = sigma UNIV (range greaterThan :: 'a::{linorder_topology, second_countable_topology} set set)"
unfolding second_countable_borel_measurable[OF open_generated_order]
proof (intro sigma_eqI sigma_sets_eqI)
- from countable_dense_setE guess D :: "'a set" . note D = this
+ obtain D :: "'a set" where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
+ by (rule countable_dense_setE) blast
interpret L: sigma_algebra UNIV "sigma_sets UNIV (range greaterThan)"
by (rule sigma_algebra_sigma_sets) simp
@@ -1027,7 +1028,8 @@
then have *: "{x::'a. x\<bullet>i \<le> a} = (\<Union>k::nat. {.. (\<Sum>n\<in>Basis. (if n = i then a else real k)*\<^sub>R n)})"
proof (safe, simp_all add: eucl_le[where 'a='a] split: if_split_asm)
fix x :: 'a
- from real_arch_simple[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"] guess k::nat ..
+ obtain k where "Max ((\<bullet>) x ` Basis) \<le> real k"
+ using real_arch_simple by blast
then have "\<And>i. i \<in> Basis \<Longrightarrow> x\<bullet>i \<le> real k"
by (subst (asm) Max_le_iff) auto
then show "\<exists>k::nat. \<forall>ia\<in>Basis. ia \<noteq> i \<longrightarrow> x \<bullet> ia \<le> real k"
@@ -1048,8 +1050,8 @@
(\<Union>k::nat. {x. (\<Sum>n\<in>Basis. (if n = i then a else -real k) *\<^sub>R n) <e x})" using i
proof (safe, simp_all add: eucl_less_def split: if_split_asm)
fix x :: 'a
- from reals_Archimedean2[of "Max ((\<lambda>i. -x\<bullet>i)`Basis)"]
- guess k::nat .. note k = this
+ obtain k where k: "Max ((\<bullet>) (- x) ` Basis) < real k"
+ using reals_Archimedean2 by blast
{ fix i :: 'a assume "i \<in> Basis"
then have "-x\<bullet>i < real k"
using k by (subst (asm) Max_less_iff) auto
@@ -1074,8 +1076,8 @@
also have *: "{x::'a. x\<bullet>i < a} = (\<Union>k::nat. {x. x <e (\<Sum>n\<in>Basis. (if n = i then a else real k) *\<^sub>R n)})" using \<open>i\<in> Basis\<close>
proof (safe, simp_all add: eucl_less_def split: if_split_asm)
fix x :: 'a
- from reals_Archimedean2[of "Max ((\<lambda>i. x\<bullet>i)`Basis)"]
- guess k::nat .. note k = this
+ obtain k where k: "Max ((\<bullet>) x ` Basis) < real k"
+ using reals_Archimedean2 by blast
{ fix i :: 'a assume "i \<in> Basis"
then have "x\<bullet>i < real k"
using k by (subst (asm) Max_less_iff) auto
@@ -1098,8 +1100,8 @@
have *: "{..a} = (\<Union>n::nat. {- real n *\<^sub>R One .. a})"
proof (safe, simp_all add: eucl_le[where 'a='a])
fix x :: 'a
- from real_arch_simple[of "Max ((\<lambda>i. - x\<bullet>i)`Basis)"]
- guess k::nat .. note k = this
+ obtain k where k: "Max ((\<bullet>) (- x) ` Basis) \<le> real k"
+ using real_arch_simple by blast
{ fix i :: 'a assume "i \<in> Basis"
with k have "- x\<bullet>i \<le> real k"
by (subst (asm) Max_le_iff) (auto simp: field_simps)
@@ -1808,9 +1810,7 @@
proof -
from assms is_real_interval have "\<exists>a b::real. S = {} \<or> S = UNIV \<or> S = {..<b} \<or> S = {..b} \<or>
S = {a<..} \<or> S = {a..} \<or> S = {a<..<b} \<or> S = {a<..b} \<or> S = {a..<b} \<or> S = {a..b}" by auto
- then guess a ..
- then guess b ..
- thus ?thesis
+ then show ?thesis
by auto
qed
--- a/src/HOL/Analysis/Caratheodory.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Caratheodory.thy Fri Sep 24 22:44:13 2021 +0200
@@ -564,8 +564,9 @@
let ?R = generated_ring
have "\<forall>a\<in>?R. \<exists>m. \<exists>C\<subseteq>M. a = \<Union>C \<and> finite C \<and> disjoint C \<and> m = (\<Sum>c\<in>C. \<mu> c)"
by (auto simp: generated_ring_def)
- from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this
-
+ from bchoice[OF this] obtain \<mu>'
+ where \<mu>'_spec: "\<forall>x\<in>generated_ring. \<exists>C\<subseteq>M. x = \<Union> C \<and> finite C \<and> disjoint C \<and> \<mu>' x = sum \<mu> C"
+ by blast
{ fix C assume C: "C \<subseteq> M" "finite C" "disjoint C"
fix D assume D: "D \<subseteq> M" "finite D" "disjoint D"
assume "\<Union>C = \<Union>D"
@@ -609,15 +610,19 @@
fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a"
by (simp add: disjoint_def)
next
- fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
+ fix a assume "a \<in> ?R"
+ then obtain Ca where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca" ..
with \<mu>'[of Ca] \<open>volume M \<mu>\<close>[THEN volume_positive]
show "0 \<le> \<mu>' a"
by (auto intro!: sum_nonneg)
next
show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto
next
- fix a assume "a \<in> ?R" then guess Ca .. note Ca = this
- fix b assume "b \<in> ?R" then guess Cb .. note Cb = this
+ fix a b assume "a \<in> ?R" "b \<in> ?R"
+ then obtain Ca Cb
+ where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+ and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+ by (meson generated_ringE)
assume "a \<inter> b = {}"
with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto
then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto
@@ -650,7 +655,7 @@
fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C"
have "\<exists>F'. bij_betw F' {..<card C} C"
by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto
- then guess F' .. note F' = this
+ then obtain F' where "bij_betw F' {..<card C} C" ..
then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}"
by (auto simp: bij_betw_def)
{ fix i j assume *: "i < card C" "j < card C" "i \<noteq> j"
@@ -698,10 +703,12 @@
have "countably_additive generated_ring \<mu>_r"
proof (rule countably_additiveI)
- fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
+ fix A' :: "nat \<Rightarrow> 'a set"
+ assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'"
and Un_A: "(\<Union>i. A' i) \<in> generated_ring"
- from generated_ringE[OF Un_A] guess C' . note C' = this
+ obtain C' where C': "finite C'" "disjoint C'" "C' \<subseteq> M" "\<Union> (range A') = \<Union> C'"
+ using generated_ringE[OF Un_A] by auto
{ fix c assume "c \<in> C'"
moreover define A where [abs_def]: "A i = A' i \<inter> c" for i
@@ -717,11 +724,11 @@
proof
fix i
from A have Ai: "A i \<in> generated_ring" by auto
- from generated_ringE[OF this] guess C . note C = this
-
+ from generated_ringE[OF this] obtain C
+ where C: "finite C" "disjoint C" "C \<subseteq> M" "A i = \<Union> C" by auto
have "\<exists>F'. bij_betw F' {..<card C} C"
by (rule finite_same_card_bij[OF _ \<open>finite C\<close>]) auto
- then guess F .. note F = this
+ then obtain F where F: "bij_betw F {..<card C} C" ..
define f where [abs_def]: "f i = (if i < card C then F i else {})" for i
then have f: "bij_betw f {..< card C} C"
by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto
@@ -750,7 +757,9 @@
ultimately show "?P i"
by blast
qed
- from choice[OF this] guess f .. note f = this
+ from choice[OF this] obtain f
+ where f: "\<forall>x. \<mu>_r (A x) = (\<Sum>j. \<mu>_r (f x j)) \<and> disjoint_family (f x) \<and> \<Union> (range (f x)) = A x \<and> (\<forall>j. f x j \<in> M)"
+ ..
then have UN_f_eq: "(\<Union>i. case_prod f (prod_decode i)) = (\<Union>i. A i)"
unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff)
@@ -808,8 +817,8 @@
finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)"
using C' by simp
qed
- from G.caratheodory'[OF \<open>positive generated_ring \<mu>_r\<close> \<open>countably_additive generated_ring \<mu>_r\<close>]
- guess \<mu>' ..
+ obtain \<mu>' where "(\<forall>s\<in>generated_ring. \<mu>' s = \<mu>_r s) \<and> measure_space \<Omega> (sigma_sets \<Omega> generated_ring) \<mu>'"
+ using G.caratheodory'[OF pos \<open>countably_additive generated_ring \<mu>_r\<close>] by auto
with V show ?thesis
unfolding sigma_sets_generated_ring_eq
by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic)
--- a/src/HOL/Analysis/Complete_Measure.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Complete_Measure.thy Fri Sep 24 22:44:13 2021 +0200
@@ -52,16 +52,18 @@
show "{} \<in> ?A" by auto
next
let ?C = "space M"
- fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' .
+ fix A assume "A \<in> ?A"
+ then obtain S N N'
+ where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
+ by (rule completionE)
then show "space M - A \<in> ?A"
by (intro completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"]) auto
next
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A"
then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'"
by (auto simp: image_subset_iff)
- from choice[OF this] guess S ..
- from choice[OF this] guess N ..
- from choice[OF this] guess N' ..
+ then obtain S N N' where "\<forall>x. A x = S x \<union> N x \<and> S x \<in> sets M \<and> N' x \<in> null_sets M \<and> N x \<subseteq> N' x"
+ by metis
then show "\<Union>(A ` UNIV) \<in> ?A"
using null_sets_UN[of N']
by (intro completionI[of _ "\<Union>(S ` UNIV)" "\<Union>(N ` UNIV)" "\<Union>(N' ` UNIV)"]) auto
@@ -104,7 +106,8 @@
show ?thesis
unfolding main_part_def null_part_def if_not_P[OF nA]
proof (rule someI2_ex)
- from assms[THEN sets_completionE] guess S N N' . note A = this
+ from assms obtain S N N' where A: "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
+ by (blast intro: sets_completionE)
let ?P = "(S, N - S)"
show "\<exists>p. split_completion M A p"
unfolding split_completion_def if_not_P[OF nA] using A
@@ -140,12 +143,11 @@
assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0"
proof -
have S: "S \<in> sets (completion M)" using assms by auto
- have "S - main_part M S \<in> sets M" using assms by auto
- moreover
+ have *: "S - main_part M S \<in> sets M" using assms by auto
from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
have "S - main_part M S = null_part M S" by auto
- ultimately show sets: "null_part M S \<in> sets M" by auto
- from null_part[OF S] guess N ..
+ with * show sets: "null_part M S \<in> sets M" by auto
+ from null_part[OF S] obtain N where "N \<in> null_sets M \<and> null_part M S \<subseteq> N" ..
with emeasure_eq_0[of N _ "null_part M S"] sets
show "emeasure M (null_part M S) = 0" by auto
qed
@@ -159,10 +161,10 @@
then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto
have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N"
using null_part[OF S] by auto
- from choice[OF this] guess N .. note N = this
+ then obtain N where N: "\<forall>x. N x \<in> null_sets M \<and> null_part M (S x) \<subseteq> N x" by metis
then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto
- have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto
- from null_part[OF this] guess N' .. note N' = this
+ from S have "(\<Union>i. S i) \<in> sets (completion M)" by auto
+ from null_part[OF this] obtain N' where N': "N' \<in> null_sets M \<and> null_part M (\<Union> (range S)) \<subseteq> N'" ..
let ?N = "(\<Union>i. N i) \<union> N'"
have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto
have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N"
@@ -288,21 +290,24 @@
assumes g: "g \<in> borel_measurable (completion M)"
shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
proof -
- from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
- from this(1)[THEN completion_ex_simple_function]
+ obtain f :: "nat \<Rightarrow> 'a \<Rightarrow> ennreal"
+ where *: "\<And>i. simple_function (completion M) (f i)"
+ and **: "\<And>x. (SUP i. f i x) = g x"
+ using g[THEN borel_measurable_implies_simple_function_sequence'] by metis
+ from *[THEN completion_ex_simple_function]
have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" ..
- from this[THEN choice] obtain f' where
- sf: "\<And>i. simple_function M (f' i)" and
- AE: "\<forall>i. AE x in M. f i x = f' i x" by auto
+ then obtain f'
+ where sf: "\<And>i. simple_function M (f' i)"
+ and AE: "\<forall>i. AE x in M. f i x = f' i x"
+ by metis
show ?thesis
proof (intro bexI)
from AE[unfolded AE_all_countable[symmetric]]
show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
proof (elim AE_mp, safe intro!: AE_I2)
fix x assume eq: "\<forall>i. f i x = f' i x"
- moreover have "g x = (SUP i. f i x)"
- unfolding f by (auto split: split_max)
- ultimately show "g x = ?f x" by auto
+ have "g x = (SUP i. f i x)" by (auto simp: ** split: split_max)
+ with eq show "g x = ?f x" by auto
qed
show "?f \<in> borel_measurable M"
using sf[THEN borel_measurable_simple_function] by auto
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Fri Sep 24 22:44:13 2021 +0200
@@ -269,11 +269,24 @@
qed
lemma Int_stable_prod_algebra: "Int_stable (prod_algebra I M)"
-proof (unfold Int_stable_def, safe)
+ unfolding Int_stable_def
+proof safe
fix A assume "A \<in> prod_algebra I M"
- from prod_algebraE[OF this] guess J E . note A = this
+ from prod_algebraE[OF this] obtain J E where A:
+ "A = prod_emb I M J (Pi\<^sub>E J E)"
+ "finite J"
+ "J \<noteq> {} \<or> I = {}"
+ "J \<subseteq> I"
+ "\<And>i. i \<in> J \<Longrightarrow> E i \<in> sets (M i)"
+ by auto
fix B assume "B \<in> prod_algebra I M"
- from prod_algebraE[OF this] guess K F . note B = this
+ from prod_algebraE[OF this] obtain K F where B:
+ "B = prod_emb I M K (Pi\<^sub>E K F)"
+ "finite K"
+ "K \<noteq> {} \<or> I = {}"
+ "K \<subseteq> I"
+ "\<And>i. i \<in> K \<Longrightarrow> F i \<in> sets (M i)"
+ by auto
have "A \<inter> B = prod_emb I M (J \<union> K) (\<Pi>\<^sub>E i\<in>J \<union> K. (if i \<in> J then E i else space (M i)) \<inter>
(if i \<in> K then F i else space (M i)))"
unfolding A B using A(2,3,4) A(5)[THEN sets.sets_into_space] B(2,3,4)
@@ -360,7 +373,13 @@
proof (rule sigma_sets_eqI)
interpret R: sigma_algebra ?\<Omega> "sigma_sets ?\<Omega> ?R" by (rule sigma_algebra_sigma_sets) auto
fix A assume "A \<in> prod_algebra I M"
- from prod_algebraE[OF this] guess J X . note X = this
+ from prod_algebraE[OF this] obtain J X where X:
+ "A = prod_emb I M J (Pi\<^sub>E J X)"
+ "finite J"
+ "J \<noteq> {} \<or> I = {}"
+ "J \<subseteq> I"
+ "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
+ by auto
show "A \<in> sigma_sets ?\<Omega> ?R"
proof cases
assume "I = {}"
@@ -525,7 +544,13 @@
using sets_PiM prod_algebra_sets_into_space space
proof (rule measurable_sigma_sets)
fix A assume "A \<in> prod_algebra I M"
- from prod_algebraE[OF this] guess J X .
+ from prod_algebraE[OF this] obtain J X where
+ "A = prod_emb I M J (Pi\<^sub>E J X)"
+ "finite J"
+ "J \<noteq> {} \<or> I = {}"
+ "J \<subseteq> I"
+ "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
+ by auto
with sets[of J X] show "f -` A \<inter> space N \<in> sets N" by auto
qed
@@ -537,7 +562,14 @@
using sets_PiM prod_algebra_sets_into_space space
proof (rule measurable_sigma_sets)
fix A assume "A \<in> prod_algebra I M"
- from prod_algebraE[OF this] guess J X . note X = this
+ from prod_algebraE[OF this] obtain J X
+ where X:
+ "A = prod_emb I M J (Pi\<^sub>E J X)"
+ "finite J"
+ "J \<noteq> {} \<or> I = {}"
+ "J \<subseteq> I"
+ "\<And>i. i \<in> J \<Longrightarrow> X i \<in> sets (M i)"
+ by auto
then have "f -` A \<inter> space N = {\<omega> \<in> space N. \<forall>i\<in>J. f \<omega> i \<in> X i}"
using space by (auto simp: prod_emb_def del: PiE_I)
also have "\<dots> \<in> sets N" using X(3,2,4,5) by (rule sets)
@@ -844,7 +876,9 @@
proof -
have "\<forall>i::'i. \<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> sets (M i) \<and> incseq F \<and> (\<Union>i. F i) = space (M i) \<and> (\<forall>k. emeasure (M i) (F k) \<noteq> \<infinity>)"
using M.sigma_finite_incseq by metis
- from choice[OF this] guess F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set" ..
+ then obtain F :: "'i \<Rightarrow> nat \<Rightarrow> 'a set"
+ where "\<forall>x. range (F x) \<subseteq> sets (M x) \<and> incseq (F x) \<and> \<Union> (range (F x)) = space (M x) \<and> (\<forall>k. emeasure (M x) (F x k) \<noteq> \<infinity>)"
+ by metis
then have F: "\<And>i. range (F i) \<subseteq> sets (M i)" "\<And>i. incseq (F i)" "\<And>i. (\<Union>j. F i j) = space (M i)" "\<And>i k. emeasure (M i) (F i k) \<noteq> \<infinity>"
by auto
let ?F = "\<lambda>k. \<Pi>\<^sub>E i\<in>I. F i k"
@@ -950,8 +984,11 @@
shows "P = PiM I M"
proof -
interpret finite_product_sigma_finite M I
- proof qed fact
- from sigma_finite_pairs guess C .. note C = this
+ by standard fact
+ from sigma_finite_pairs obtain C where C:
+ "\<forall>i\<in>I. range (C i) \<subseteq> sets (M i)" "\<forall>k. \<forall>i\<in>I. emeasure (M i) (C i k) \<noteq> \<infinity>"
+ "incseq (\<lambda>k. \<Pi>\<^sub>E i\<in>I. C i k)" "(\<Union>k. \<Pi>\<^sub>E i\<in>I. C i k) = space (Pi\<^sub>M I M)"
+ by auto
show ?thesis
proof (rule measure_eqI_PiM_finite[OF I refl P, symmetric])
show "(\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets (M i)) \<Longrightarrow> (Pi\<^sub>M I M) (Pi\<^sub>E I A) = P (Pi\<^sub>E I A)" for A
--- a/src/HOL/Analysis/Gamma_Function.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Gamma_Function.thy Fri Sep 24 22:44:13 2021 +0200
@@ -388,7 +388,9 @@
have "summable (\<lambda>k. inverse ((real_of_nat k)^2))"
by (rule inverse_power_summable) simp
- from summable_partial_sum_bound[OF this e'] guess M . note M = this
+ from summable_partial_sum_bound[OF this e']
+ obtain M where M: "\<And>m n. M \<le> m \<Longrightarrow> norm (\<Sum>k = m..n. inverse ((real k)\<^sup>2)) < e'"
+ by auto
define N where "N = max 2 (max (nat \<lceil>2 * (norm z + d)\<rceil>) M)"
{
@@ -910,7 +912,8 @@
assume n: "n = 0"
let ?f = "\<lambda>k z. inverse (of_nat (Suc k)) - inverse (z + of_nat k)"
let ?F = "\<lambda>z. \<Sum>k. ?f k z" and ?f' = "\<lambda>k z. inverse ((z + of_nat k)\<^sup>2)"
- from no_nonpos_Int_in_ball'[OF z] guess d . note d = this
+ from no_nonpos_Int_in_ball'[OF z] obtain d where d: "0 < d" "\<And>t. t \<in> ball z d \<Longrightarrow> t \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ by auto
from z have summable: "summable (\<lambda>k. inverse (of_nat (Suc k)) - inverse (z + of_nat k))"
by (intro summable_Digamma) force
from z have conv: "uniformly_convergent_on (ball z d) (\<lambda>k z. \<Sum>i<k. inverse ((z + of_nat i)\<^sup>2))"
@@ -931,7 +934,8 @@
next
assume n: "n \<noteq> 0"
from z have z': "z \<noteq> 0" by auto
- from no_nonpos_Int_in_ball'[OF z] guess d . note d = this
+ from no_nonpos_Int_in_ball'[OF z] obtain d where d: "0 < d" "\<And>t. t \<in> ball z d \<Longrightarrow> t \<notin> \<int>\<^sub>\<le>\<^sub>0"
+ by auto
define n' where "n' = Suc n"
from n have n': "n' \<ge> 2" by (simp add: n'_def)
have "((\<lambda>z. \<Sum>k. inverse ((z + of_nat k) ^ n')) has_field_derivative
@@ -1293,7 +1297,9 @@
case False
have "rGamma_series z \<longlonglongrightarrow> exp (- ln_Gamma z)"
proof (rule Lim_transform_eventually)
- from ln_Gamma_series_complex_converges'[OF False] guess d by (elim exE conjE)
+ from ln_Gamma_series_complex_converges'[OF False]
+ obtain d where "0 < d" "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n)"
+ by auto
from this(1) uniformly_convergent_imp_convergent[OF this(2), of z]
have "ln_Gamma_series z \<longlonglongrightarrow> lim (ln_Gamma_series z)" by (simp add: convergent_LIMSEQ_iff)
thus "(\<lambda>n. exp (-ln_Gamma_series z n)) \<longlonglongrightarrow> exp (- ln_Gamma z)"
@@ -1762,9 +1768,12 @@
proof -
have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
- then guess \<xi> by (elim exE conjE) note \<xi> = this
- note \<xi>(3)
- also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> > 0"
+ then obtain \<xi>
+ where \<xi>: "x < \<xi>" "\<xi> < y"
+ and Polygamma: "Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
+ by auto
+ note Polygamma
+ also from \<xi> assms have "(y - x) * Polygamma (Suc n) \<xi> > 0"
by (intro mult_pos_pos Polygamma_real_odd_pos) (auto elim!: nonpos_Ints_cases)
finally show ?thesis by simp
qed
@@ -1775,9 +1784,12 @@
proof -
have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
- then guess \<xi> by (elim exE conjE) note \<xi> = this
- note \<xi>(3)
- also from \<xi>(1,2) assms have "(y - x) * Polygamma (Suc n) \<xi> < 0"
+ then obtain \<xi>
+ where \<xi>: "x < \<xi>" "\<xi> < y"
+ and Polygamma: "Polygamma n y - Polygamma n x = (y - x) * Polygamma (Suc n) \<xi>"
+ by auto
+ note Polygamma
+ also from \<xi> assms have "(y - x) * Polygamma (Suc n) \<xi> < 0"
by (intro mult_pos_neg Polygamma_real_even_neg) simp_all
finally show ?thesis by simp
qed
@@ -1809,9 +1821,11 @@
proof -
have "\<exists>\<xi>. x < \<xi> \<and> \<xi> < y \<and> ln_Gamma y - ln_Gamma x = (y - x) * Digamma \<xi>"
using assms by (intro MVT2 derivative_intros impI allI) (auto elim!: nonpos_Ints_cases)
- then guess \<xi> by (elim exE conjE) note \<xi> = this
- note \<xi>(3)
- also from \<xi>(1,2) assms have "(y - x) * Digamma \<xi> > 0"
+ then obtain \<xi> where \<xi>: "x < \<xi>" "\<xi> < y"
+ and ln_Gamma: "ln_Gamma y - ln_Gamma x = (y - x) * Digamma \<xi>"
+ by auto
+ note ln_Gamma
+ also from \<xi> assms have "(y - x) * Digamma \<xi> > 0"
by (intro mult_pos_pos Digamma_real_ge_three_halves_pos) simp_all
finally show ?thesis by simp
qed
--- a/src/HOL/Analysis/Interval_Integral.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Sep 24 22:44:13 2021 +0200
@@ -72,7 +72,7 @@
ultimately show thesis
by (intro that[of "\<lambda>i. b' - d / Suc (Suc i)"])
(auto simp: real incseq_def intro!: divide_left_mono)
-qed (insert \<open>a < b\<close>, auto)
+qed (use \<open>a < b\<close> in auto)
lemma ereal_decseq_approx:
fixes a b :: ereal
@@ -81,7 +81,12 @@
"decseq X" "\<And>i. a < X i" "\<And>i. X i < b" "X \<longlonglongrightarrow> a"
proof -
have "-b < -a" using \<open>a < b\<close> by simp
- from ereal_incseq_approx[OF this] guess X .
+ from ereal_incseq_approx[OF this] obtain X where
+ "incseq X"
+ "\<And>i. - b < ereal (X i)"
+ "\<And>i. ereal (X i) < - a"
+ "(\<lambda>x. ereal (X x)) \<longlonglongrightarrow> - a"
+ by auto
then show thesis
apply (intro that[of "\<lambda>i. - X i"])
apply (auto simp: decseq_def incseq_def simp flip: uminus_ereal.simps)
@@ -98,8 +103,18 @@
"l \<longlonglongrightarrow> a" "u \<longlonglongrightarrow> b"
proof -
from dense[OF \<open>a < b\<close>] obtain c where "a < c" "c < b" by safe
- from ereal_incseq_approx[OF \<open>c < b\<close>] guess u . note u = this
- from ereal_decseq_approx[OF \<open>a < c\<close>] guess l . note l = this
+ from ereal_incseq_approx[OF \<open>c < b\<close>] obtain u where u:
+ "incseq u"
+ "\<And>i. c < ereal (u i)"
+ "\<And>i. ereal (u i) < b"
+ "(\<lambda>x. ereal (u x)) \<longlonglongrightarrow> b"
+ by auto
+ from ereal_decseq_approx[OF \<open>a < c\<close>] obtain l where l:
+ "decseq l"
+ "\<And>i. a < ereal (l i)"
+ "\<And>i. ereal (l i) < c"
+ "(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a"
+ by auto
{ fix i from less_trans[OF \<open>l i < c\<close> \<open>c < u i\<close>] have "l i < u i" by simp }
have "einterval a b = (\<Union>i. {l i .. u i})"
proof (auto simp: einterval_iff)
@@ -944,8 +959,15 @@
"set_integrable lborel (einterval A B) f"
"(LBINT x=A..B. f x) = (LBINT x=a..b. (f (g x) * g' x))"
proof -
- from einterval_Icc_approximation[OF \<open>a < b\<close>] guess u l . note approx [simp] = this
- note less_imp_le [simp]
+ from einterval_Icc_approximation[OF \<open>a < b\<close>] obtain u l where approx [simp]:
+ "einterval a b = (\<Union>i. {l i..u i})"
+ "incseq u"
+ "decseq l"
+ "\<And>i. l i < u i"
+ "\<And>i. a < ereal (l i)"
+ "\<And>i. ereal (u i) < b"
+ "(\<lambda>x. ereal (l x)) \<longlonglongrightarrow> a"
+ "(\<lambda>x. ereal (u x)) \<longlonglongrightarrow> b" by this auto
have aless[simp]: "\<And>x i. l i \<le> x \<Longrightarrow> a < ereal x"
by (rule order_less_le_trans, rule approx, force)
have lessb[simp]: "\<And>x i. x \<le> u i \<Longrightarrow> ereal x < b"
@@ -976,7 +998,7 @@
hence B3: "\<And>i. g (u i) \<le> B"
by (intro incseq_le, auto simp: incseq_def)
have "ereal (g (l 0)) \<le> ereal (g (u 0))"
- by auto
+ by (auto simp: less_imp_le)
then show "A \<le> B"
by (meson A3 B3 order.trans)
{ fix x :: real
@@ -1002,7 +1024,7 @@
have "(LBINT x=l i.. u i. g' x *\<^sub>R f (g x)) = (LBINT y=g (l i)..g (u i). f y)"
apply (rule interval_integral_substitution_finite [OF _ DERIV_subset [OF deriv_g]])
unfolding has_field_derivative_iff_has_vector_derivative[symmetric]
- apply (auto intro!: continuous_at_imp_continuous_on contf contg')
+ apply (auto simp: less_imp_le intro!: continuous_at_imp_continuous_on contf contg')
done
then show ?thesis
by (simp add: ac_simps)
@@ -1031,7 +1053,7 @@
hence "(\<lambda>i. (LBINT y=g (l i)..g (u i). f y)) \<longlonglongrightarrow> ?l"
by (simp add: eq1)
then show "(\<lambda>i. set_lebesgue_integral lborel {g (l i)<..<g (u i)} f) \<longlonglongrightarrow> ?l"
- unfolding interval_lebesgue_integral_def by auto
+ unfolding interval_lebesgue_integral_def by (auto simp: less_imp_le)
have "\<And>x i. g (l i) \<le> x \<Longrightarrow> x \<le> g (u i) \<Longrightarrow> 0 \<le> f x"
using aless f_nonneg img lessb by blast
then show "\<And>x i. x \<in> {g (l i)<..<g (u i)} \<Longrightarrow> 0 \<le> f x"
--- a/src/HOL/Analysis/Measure_Space.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Sep 24 22:44:13 2021 +0200
@@ -1142,7 +1142,9 @@
assumes AE: "AE x in M. P x" and sets: "{x\<in>space M. P x} \<in> sets M" (is "?P \<in> sets M")
shows "emeasure M {x\<in>space M. P x} = emeasure M (space M)"
proof -
- from AE_E[OF AE] guess N . note N = this
+ from AE_E[OF AE] obtain N
+ where N: "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
+ by auto
with sets have "emeasure M (space M) \<le> emeasure M (?P \<union> N)"
by (intro emeasure_mono) auto
also have "\<dots> \<le> emeasure M ?P + emeasure M N"
@@ -1513,10 +1515,13 @@
and AE: "AE x in distr M M' f. P x"
shows "AE x in M. P (f x)"
proof -
- from AE[THEN AE_E] guess N .
+ from AE[THEN AE_E] obtain N
+ where "{x \<in> space (distr M M' f). \<not> P x} \<subseteq> N"
+ "emeasure (distr M M' f) N = 0"
+ "N \<in> sets (distr M M' f)"
+ by auto
with f show ?thesis
- unfolding eventually_ae_filter
- by (intro bexI[of _ "f -` N \<inter> space M"])
+ by (simp add: eventually_ae_filter, intro bexI[of _ "f -` N \<inter> space M"])
(auto simp: emeasure_distr measurable_def)
qed
@@ -2352,9 +2357,9 @@
show "(\<lambda>i. ?M (F i)) \<longlonglongrightarrow> ?M (\<Union>i. F i)"
proof cases
assume "\<exists>i. \<forall>j\<ge>i. F i = F j"
- then guess i .. note i = this
- { fix j from i \<open>incseq F\<close> have "F j \<subseteq> F i"
- by (cases "i \<le> j") (auto simp: incseq_def) }
+ then obtain i where i: "\<forall>j\<ge>i. F i = F j" ..
+ with \<open>incseq F\<close> have "F j \<subseteq> F i" for j
+ by (cases "i \<le> j") (auto simp: incseq_def)
then have eq: "(\<Union>i. F i) = F i"
by auto
with i show ?thesis
@@ -2375,7 +2380,7 @@
fix n :: nat show "\<exists>k::nat\<in>UNIV. of_nat n \<le> ?M (F k)"
proof (induct n)
case (Suc n)
- then guess k .. note k = this
+ then obtain k where "of_nat n \<le> ?M (F k)" ..
moreover have "finite (F k) \<Longrightarrow> finite (F (f k)) \<Longrightarrow> card (F k) < card (F (f k))"
using \<open>F k \<subset> F (f k)\<close> by (simp add: psubset_card_mono)
moreover have "finite (F (f k)) \<Longrightarrow> finite (F k)"
@@ -2842,16 +2847,19 @@
show "finite_measure (restrict_space M A)" "finite_measure (restrict_space N A)"
by (auto simp: space_restrict_space emeasure_restrict_space less_top intro!: finite_measureI)
qed (simp add: sets_restrict_space)
- then guess Y ..
then show ?thesis
- apply (intro bexI[of _ Y] conjI ballI conjI)
- apply (simp_all add: sets_restrict_space emeasure_restrict_space)
- apply safe
- subgoal for X Z
- by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1)
- subgoal for X Z
- by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1 ac_simps)
- apply auto
+ apply -
+ apply (erule bexE)
+ subgoal for Y
+ apply (intro bexI[of _ Y] conjI ballI conjI)
+ apply (simp_all add: sets_restrict_space emeasure_restrict_space)
+ apply safe
+ subgoal for X Z
+ by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1)
+ subgoal for X Z
+ by (erule ballE[of _ _ X]) (auto simp add: Int_absorb1 ac_simps)
+ apply auto
+ done
done
qed
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Fri Sep 24 22:44:13 2021 +0200
@@ -862,7 +862,9 @@
unfolding nn_integral_def
proof (safe intro!: SUP_mono)
fix n assume n: "simple_function M n" "n \<le> u"
- from ae[THEN AE_E] guess N . note N = this
+ from ae[THEN AE_E] obtain N
+ where N: "{x \<in> space M. \<not> u x \<le> v x} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
+ by auto
then have ae_N: "AE x in M. x \<notin> N" by (auto intro: AE_not_in)
let ?n = "\<lambda>x. n x * indicator (space M - N) x"
have "AE x in M. n x \<le> ?n x" "simple_function M ?n"
@@ -1000,7 +1002,9 @@
proof -
from f have "AE x in M. \<forall>i. f i x \<le> f (Suc i) x"
by (simp add: AE_all_countable)
- from this[THEN AE_E] guess N . note N = this
+ from this[THEN AE_E] obtain N
+ where N: "{x \<in> space M. \<not> (\<forall>i. f i x \<le> f (Suc i) x)} \<subseteq> N" "emeasure M N = 0" "N \<in> sets M"
+ by auto
let ?f = "\<lambda>i x. if x \<in> space M - N then f i x else 0"
have f_eq: "AE x in M. \<forall>i. ?f i x = f i x" using N by (auto intro!: AE_I[of _ _ N])
then have "(\<integral>\<^sup>+ x. (SUP i. f i x) \<partial>M) = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>M)"
@@ -1045,14 +1049,24 @@
shows "(\<integral>\<^sup>+ x. a * f x + g x \<partial>M) = a * integral\<^sup>N M f + integral\<^sup>N M g"
(is "integral\<^sup>N M ?L = _")
proof -
- from borel_measurable_implies_simple_function_sequence'[OF f(1)] guess u .
+ obtain u
+ where "\<And>i. simple_function M (u i)" "incseq u" "\<And>i x. u i x < top" "\<And>x. (SUP i. u i x) = f x"
+ using borel_measurable_implies_simple_function_sequence' f(1)
+ by auto
note u = nn_integral_monotone_convergence_simple[OF this(2,1)] this
- from borel_measurable_implies_simple_function_sequence'[OF g(1)] guess v .
+
+ obtain v where
+ "\<And>i. simple_function M (v i)" "incseq v" "\<And>i x. v i x < top" "\<And>x. (SUP i. v i x) = g x"
+ using borel_measurable_implies_simple_function_sequence' g(1)
+ by auto
note v = nn_integral_monotone_convergence_simple[OF this(2,1)] this
+
let ?L' = "\<lambda>i x. a * u i x + v i x"
have "?L \<in> borel_measurable M" using assms by auto
- from borel_measurable_implies_simple_function_sequence'[OF this] guess l .
+ from borel_measurable_implies_simple_function_sequence'[OF this]
+ obtain l where "\<And>i. simple_function M (l i)" "incseq l" "\<And>i x. l i x < top" "\<And>x. (SUP i. l i x) = a * f x + g x"
+ by auto
note l = nn_integral_monotone_convergence_simple[OF this(2,1)] this
have inc: "incseq (\<lambda>i. a * integral\<^sup>S M (u i))" "incseq (\<lambda>i. integral\<^sup>S M (v i))"
--- a/src/HOL/Analysis/Radon_Nikodym.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Radon_Nikodym.thy Fri Sep 24 22:44:13 2021 +0200
@@ -261,7 +261,10 @@
from this[THEN bspec, OF sets.top] show "integral\<^sup>N M g \<le> N (space M)"
by (simp cong: nn_integral_cong)
qed
- from ennreal_SUP_countable_SUP [OF \<open>G \<noteq> {}\<close>, of "integral\<^sup>N M"] guess ys .. note ys = this
+ from ennreal_SUP_countable_SUP [OF \<open>G \<noteq> {}\<close>, of "integral\<^sup>N M"]
+ obtain ys :: "nat \<Rightarrow> ennreal"
+ where ys: "range ys \<subseteq> integral\<^sup>N M ` G \<and> Sup (integral\<^sup>N M ` G) = Sup (range ys)"
+ by auto
then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>N M g = ys n"
proof safe
fix n assume "range ys \<subseteq> integral\<^sup>N M ` G"
@@ -774,8 +777,11 @@
next
assume eq: "density M f = density M g"
interpret f: sigma_finite_measure "density M f" by fact
- from f.sigma_finite_incseq guess A . note cover = this
-
+ from f.sigma_finite_incseq obtain A where cover: "range A \<subseteq> sets (density M f)"
+ "\<Union> (range A) = space (density M f)"
+ "\<And>i. emeasure (density M f) (A i) \<noteq> \<infinity>"
+ "incseq A"
+ by auto
have "AE x in M. \<forall>i. x \<in> A i \<longrightarrow> f x = g x"
unfolding AE_all_countable
proof
@@ -821,7 +827,9 @@
using fin by (auto elim!: AE_Ball_mp simp: less_top ennreal_mult_less_top)
next
assume AE: "AE x in M. f x \<noteq> \<infinity>"
- from sigma_finite guess Q . note Q = this
+ from sigma_finite obtain Q :: "nat \<Rightarrow> 'a set"
+ where Q: "range Q \<subseteq> sets M" "\<Union> (range Q) = space M" "\<And>i. emeasure M (Q i) \<noteq> \<infinity>"
+ by auto
define A where "A i =
f -` (case i of 0 \<Rightarrow> {\<infinity>} | Suc n \<Rightarrow> {.. ennreal(of_nat (Suc n))}) \<inter> space M" for i
{ fix i j have "A i \<inter> Q j \<in> sets M"
@@ -977,7 +985,8 @@
let ?M' = "distr M M' T" and ?N' = "distr N M' T"
interpret M': sigma_finite_measure ?M'
proof
- from sigma_finite_countable guess F .. note F = this
+ from sigma_finite_countable obtain F
+ where F: "countable F \<and> F \<subseteq> sets M \<and> \<Union> F = space M \<and> (\<forall>a\<in>F. emeasure M a \<noteq> \<infinity>)" ..
show "\<exists>A. countable A \<and> A \<subseteq> sets (distr M M' T) \<and> \<Union>A = space (distr M M' T) \<and> (\<forall>a\<in>A. emeasure (distr M M' T) a \<noteq> \<infinity>)"
proof (intro exI conjI ballI)
show *: "(\<lambda>A. T' -` A \<inter> space ?M') ` F \<subseteq> sets ?M'"
@@ -992,7 +1001,7 @@
have Fi: "A \<in> sets M" using F \<open>A\<in>F\<close> by auto
ultimately show "emeasure ?M' X \<noteq> \<infinity>"
using F T T' \<open>A\<in>F\<close> by (simp add: emeasure_distr)
- qed (insert F, auto)
+ qed (use F in auto)
qed
have "(RN_deriv ?M' ?N') \<circ> T \<in> borel_measurable M"
using T ac by measurable
--- a/src/HOL/Analysis/Regularity.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Regularity.thy Fri Sep 24 22:44:13 2021 +0200
@@ -30,7 +30,9 @@
(\<And>e. e > 0 \<Longrightarrow> \<exists>B. A \<subseteq> B \<and> open B \<and> emeasure M B \<le> emeasure M A + ennreal e) \<Longrightarrow> ?outer A"
by (rule ennreal_approx_INF)
(force intro!: emeasure_mono simp: emeasure_eq_measure sb)+
- from countable_dense_setE guess X::"'a set" . note X = this
+ from countable_dense_setE obtain X :: "'a set"
+ where X: "countable X" "\<And>Y :: 'a set. open Y \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> \<exists>d\<in>X. d \<in> Y"
+ by auto
{
fix r::real assume "r > 0" hence "\<And>y. open (ball y r)" "\<And>y. ball y r \<noteq> {}" by auto
with X(2)[OF this]
@@ -114,7 +116,7 @@
proof safe
show "complete K" using \<open>closed K\<close> by (simp add: complete_eq_closed)
fix e'::real assume "0 < e'"
- from nat_approx_posE[OF this] guess n . note n = this
+ then obtain n where n: "1 / real (Suc n) < e'" by (rule nat_approx_posE)
let ?k = "from_nat_into X ` {0..k e (Suc n)}"
have "finite ?k" by simp
moreover have "K \<subseteq> (\<Union>x\<in>?k. ball x e')" unfolding K_def B_def using n by force
@@ -164,12 +166,11 @@
proof (auto simp del: of_nat_Suc, rule ccontr)
fix x
assume "infdist x A \<noteq> 0"
- hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
- from nat_approx_posE[OF this] guess n .
- moreover
+ then have pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
+ then obtain n where n: "1 / real (Suc n) < infdist x A" by (rule nat_approx_posE)
assume "\<forall>i. infdist x A < 1 / real (Suc i)"
- hence "infdist x A < 1 / real (Suc n)" by auto
- ultimately show False by simp
+ then have "infdist x A < 1 / real (Suc n)" by auto
+ with n show False by simp
qed
also have "M \<dots> = (INF n. emeasure M (?G (1 / real (Suc n))))"
proof (rule INF_emeasure_decseq[symmetric], safe)
--- a/src/HOL/Analysis/Set_Integral.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Set_Integral.thy Fri Sep 24 22:44:13 2021 +0200
@@ -415,7 +415,7 @@
show "(\<lambda>i. indicator (A i) x *\<^sub>R f x) \<longlonglongrightarrow> indicator (\<Union>i. A i) x *\<^sub>R f x"
proof cases
assume "\<exists>i. x \<in> A i"
- then guess i ..
+ then obtain i where "x \<in> A i" ..
then have *: "eventually (\<lambda>i. x \<in> A i) sequentially"
using \<open>x \<in> A i\<close> \<open>mono A\<close> by (auto simp: eventually_sequentially mono_def)
show ?thesis
--- a/src/HOL/Analysis/Sigma_Algebra.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Sigma_Algebra.thy Fri Sep 24 22:44:13 2021 +0200
@@ -669,7 +669,8 @@
case (Union a)
then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x"
by (auto simp: image_iff Bex_def)
- from choice[OF this] guess f ..
+ then obtain f where "\<forall>x. f x \<in> sigma_sets sp st \<and> a x = A \<inter> f x"
+ by metis
then show ?case
by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union
simp add: image_iff)
@@ -771,8 +772,9 @@
next
case (Union F)
then have "\<forall>i. \<exists>B. F i = X -` B \<inter> \<Omega> \<and> B \<in> sigma_sets \<Omega>' M'" by auto
- from choice[OF this] guess A .. note A = this
- with A show ?case
+ then obtain A where "\<forall>x. F x = X -` A x \<inter> \<Omega> \<and> A x \<in> sigma_sets \<Omega>' M'"
+ by metis
+ then show ?case
by (auto simp: vimage_UN[symmetric] intro: sigma_sets.Union)
qed
qed
@@ -843,13 +845,15 @@
and "a \<inter> b = {}"
shows "a \<union> b \<in> generated_ring"
proof -
- from a guess Ca .. note Ca = this
- from b guess Cb .. note Cb = this
+ from a b obtain Ca Cb
+ where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+ and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+ using generated_ringE by metis
show ?thesis
proof
- show "disjoint (Ca \<union> Cb)"
- using \<open>a \<inter> b = {}\<close> Ca Cb by (auto intro!: disjoint_union)
- qed (insert Ca Cb, auto)
+ from \<open>a \<inter> b = {}\<close> Ca Cb show "disjoint (Ca \<union> Cb)"
+ by (auto intro!: disjoint_union)
+ qed (use Ca Cb in auto)
qed
lemma (in semiring_of_sets) generated_ring_empty: "{} \<in> generated_ring"
@@ -867,8 +871,10 @@
assumes a: "a \<in> generated_ring" and b: "b \<in> generated_ring"
shows "a \<inter> b \<in> generated_ring"
proof -
- from a guess Ca .. note Ca = this
- from b guess Cb .. note Cb = this
+ from a b obtain Ca Cb
+ where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+ and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+ using generated_ringE by metis
define C where "C = (\<lambda>(a,b). a \<inter> b)` (Ca\<times>Cb)"
show ?thesis
proof
@@ -890,7 +896,7 @@
then show ?thesis by auto
qed
qed
- qed (insert Ca Cb, auto simp: C_def)
+ qed (use Ca Cb in \<open>auto simp: C_def\<close>)
qed
lemma (in semiring_of_sets) generated_ring_Inter:
@@ -909,9 +915,12 @@
using sets_into_space by (auto simp: generated_ring_def generated_ring_empty)
show "{} \<in> ?R" by (rule generated_ring_empty)
- { fix a assume a: "a \<in> ?R" then guess Ca .. note Ca = this
- fix b assume b: "b \<in> ?R" then guess Cb .. note Cb = this
-
+ {
+ fix a b assume "a \<in> ?R" "b \<in> ?R"
+ then obtain Ca Cb
+ where Ca: "finite Ca" "disjoint Ca" "Ca \<subseteq> M" "a = \<Union> Ca"
+ and Cb: "finite Cb" "disjoint Cb" "Cb \<subseteq> M" "b = \<Union> Cb"
+ using generated_ringE by metis
show "a - b \<in> ?R"
proof cases
assume "Cb = {}" with Cb \<open>a \<in> ?R\<close> show ?thesis
@@ -932,7 +941,8 @@
show "finite Ca" "finite Cb" "Cb \<noteq> {}" by fact+
qed
finally show "a - b \<in> ?R" .
- qed }
+ qed
+ }
note Diff = this
fix a b assume sets: "a \<in> ?R" "b \<in> ?R"
--- a/src/HOL/Analysis/Summation_Tests.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Analysis/Summation_Tests.thy Fri Sep 24 22:44:13 2021 +0200
@@ -115,7 +115,7 @@
define n where "n = nat \<lceil>log c K\<rceil>"
from unbounded have "\<exists>m>n. c < root m (norm (f m))" unfolding bdd_above_def
by (auto simp: not_le)
- then guess m by (elim exE conjE) note m = this
+ then obtain m where m: "n < m" "c < root m (norm (f m))" by auto
from c K have "K = c powr log c K" by (simp add: powr_def log_def)
also from c have "c powr log c K \<le> c powr real n" unfolding n_def
by (intro powr_mono, linarith, simp)
@@ -526,7 +526,7 @@
with assms show ?thesis by simp
next
assume "\<exists>l'. l = ereal l' \<and> l' > 0"
- then guess l' by (elim exE conjE) note l' = this
+ then obtain l' where l': "l = ereal l'" "0 < l'" by auto
hence "l \<noteq> \<infinity>" by auto
have "l * ereal (norm z) < l * conv_radius f"
by (intro ereal_mult_strict_left_mono) (simp_all add: l' assms)
--- a/src/HOL/Combinatorics/Multiset_Permutations.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Combinatorics/Multiset_Permutations.thy Fri Sep 24 22:44:13 2021 +0200
@@ -131,7 +131,7 @@
lemma permutations_of_multiset_not_empty [simp]: "permutations_of_multiset A \<noteq> {}"
proof -
- from ex_mset[of A] guess xs ..
+ from ex_mset[of A] obtain xs where "mset xs = A" ..
thus ?thesis by (auto simp: permutations_of_multiset_def)
qed
@@ -142,7 +142,8 @@
from ex_mset[of A] obtain ys where ys: "mset ys = A" ..
with A have "mset xs = mset (map f ys)"
by (simp add: permutations_of_multiset_def)
- from mset_eq_permutation[OF this] guess \<sigma> . note \<sigma> = this
+ then obtain \<sigma> where \<sigma>: "\<sigma> permutes {..<length (map f ys)}" "permute_list \<sigma> (map f ys) = xs"
+ by (rule mset_eq_permutation)
with ys have "xs = map f (permute_list \<sigma> ys)"
by (simp add: permute_list_map)
moreover from \<sigma> ys have "permute_list \<sigma> ys \<in> permutations_of_multiset A"
--- a/src/HOL/Complex_Analysis/Complex_Residues.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Complex_Analysis/Complex_Residues.thy Fri Sep 24 22:44:13 2021 +0200
@@ -363,9 +363,11 @@
assumes "f has_fps_expansion F"
shows "residue (\<lambda>z. f z / z ^ Suc n) 0 = fps_nth F n"
proof -
- from has_fps_expansion_imp_holomorphic[OF assms] guess s . note s = this
- have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
- using assms s unfolding has_fps_expansion_def
+ from has_fps_expansion_imp_holomorphic[OF assms] obtain s
+ where "open s" "0 \<in> s" "f holomorphic_on s" "\<And>z. z \<in> s \<Longrightarrow> f z = eval_fps F z"
+ by auto
+ with assms have "residue (\<lambda>z. f z / (z - 0) ^ Suc n) 0 = (deriv ^^ n) f 0 / fact n"
+ unfolding has_fps_expansion_def
by (intro residue_holomorphic_over_power[of s]) (auto simp: zero_ereal_def)
also from assms have "\<dots> = fps_nth F n"
by (subst fps_nth_fps_expansion) auto
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Fri Sep 24 22:44:13 2021 +0200
@@ -755,8 +755,7 @@
thus ?thesis by (intro exI[of _ "{#normalize a#}"]) auto
next
case True
- then guess b by (elim exE conjE) note b = this
-
+ then obtain b where b: "b dvd a" "\<not> is_unit b" "\<not> a dvd b" by auto
from b have "?fctrs b \<subseteq> ?fctrs a" by (auto intro: dvd_trans)
moreover from b have "normalize a \<notin> ?fctrs b" "normalize a \<in> ?fctrs a" by simp_all
hence "?fctrs b \<noteq> ?fctrs a" by blast
@@ -766,7 +765,8 @@
moreover from \<open>a \<noteq> 0\<close> b have "b \<noteq> 0" by auto
ultimately have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize b"
by (intro less) auto
- then guess A .. note A = this
+ then obtain A where A: "(\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (\<Prod>\<^sub># A) = normalize b"
+ by auto
define c where "c = a div b"
from b have c: "a = b * c" by (simp add: c_def)
@@ -785,7 +785,8 @@
by (rule psubset_card_mono)
with \<open>c \<noteq> 0\<close> have "\<exists>A. (\<forall>x. x \<in># A \<longrightarrow> prime_elem x) \<and> normalize (prod_mset A) = normalize c"
by (intro less) auto
- then guess B .. note B = this
+ then obtain B where B: "(\<forall>x. x \<in># B \<longrightarrow> prime_elem x) \<and> normalize (\<Prod>\<^sub># B) = normalize c"
+ by auto
show ?thesis
proof (rule exI[of _ "A + B"]; safe)
@@ -840,7 +841,15 @@
case False
hence "a \<noteq> 0" "b \<noteq> 0" by blast+
note nz = \<open>x \<noteq> 0\<close> this
- from nz[THEN prime_factorization_exists'] guess A B C . note ABC = this
+ from nz[THEN prime_factorization_exists'] obtain A B C
+ where ABC:
+ "\<And>z. z \<in># A \<Longrightarrow> prime z"
+ "normalize (\<Prod>\<^sub># A) = normalize x"
+ "\<And>z. z \<in># B \<Longrightarrow> prime z"
+ "normalize (\<Prod>\<^sub># B) = normalize a"
+ "\<And>z. z \<in># C \<Longrightarrow> prime z"
+ "normalize (\<Prod>\<^sub># C) = normalize b"
+ by this blast
have "irreducible (prod_mset A)"
by (subst irreducible_cong[OF ABC(2)]) fact
@@ -855,7 +864,7 @@
normalize (prod_mset A) dvd normalize (prod_mset C)" by simp
thus ?thesis unfolding ABC by simp
qed auto
-qed (insert assms, simp_all add: irreducible_def)
+qed (use assms in \<open>simp_all add: irreducible_def\<close>)
lemma finite_divisor_powers:
assumes "y \<noteq> 0" "\<not>is_unit x"
@@ -867,7 +876,14 @@
next
case False
note nz = this \<open>y \<noteq> 0\<close>
- from nz[THEN prime_factorization_exists'] guess A B . note AB = this
+ from nz[THEN prime_factorization_exists'] obtain A B
+ where AB:
+ "\<And>z. z \<in># A \<Longrightarrow> prime z"
+ "normalize (\<Prod>\<^sub># A) = normalize x"
+ "\<And>z. z \<in># B \<Longrightarrow> prime z"
+ "normalize (\<Prod>\<^sub># B) = normalize y"
+ by this blast
+
from AB assms have "A \<noteq> {#}" by (auto simp: normalize_1_iff)
from AB(2,4) prod_mset_primes_finite_divisor_powers [of A B, OF AB(1,3) this]
have "finite {n. prod_mset A ^ n dvd prod_mset B}" by simp
@@ -883,7 +899,8 @@
assumes "x \<noteq> 0"
shows "finite {p. prime p \<and> p dvd x}"
proof -
- from prime_factorization_exists'[OF assms] guess A . note A = this
+ from prime_factorization_exists'[OF assms] obtain A
+ where A: "\<And>z. z \<in># A \<Longrightarrow> prime z" "normalize (\<Prod>\<^sub># A) = normalize x" by this blast
have "{p. prime p \<and> p dvd x} \<subseteq> set_mset A"
proof safe
fix p assume p: "prime p" and dvd: "p dvd x"
@@ -925,12 +942,14 @@
assumes "a \<noteq> 0" "\<not>is_unit a"
shows "\<exists>b. b dvd a \<and> prime b"
proof -
- from prime_factorization_exists'[OF assms(1)] guess A . note A = this
- moreover from A and assms have "A \<noteq> {#}" by auto
+ from prime_factorization_exists'[OF assms(1)]
+ obtain A where A: "\<And>z. z \<in># A \<Longrightarrow> prime z" "normalize (\<Prod>\<^sub># A) = normalize a"
+ by this blast
+ with assms have "A \<noteq> {#}" by auto
then obtain x where "x \<in># A" by blast
with A(1) have *: "x dvd normalize (prod_mset A)" "prime x"
by (auto simp: dvd_prod_mset)
- hence "x dvd a" unfolding A by simp
+ hence "x dvd a" by (simp add: A(2))
with * show ?thesis by blast
qed
@@ -939,7 +958,9 @@
shows "P x"
proof (cases "x = 0")
case False
- from prime_factorization_exists'[OF this] guess A . note A = this
+ from prime_factorization_exists'[OF this]
+ obtain A where A: "\<And>z. z \<in># A \<Longrightarrow> prime z" "normalize (\<Prod>\<^sub># A) = normalize x"
+ by this blast
from A obtain u where u: "is_unit u" "x = u * prod_mset A"
by (elim associatedE2)
@@ -959,7 +980,7 @@
shows "is_unit a"
proof (rule ccontr)
assume "\<not>is_unit a"
- from prime_divisor_exists[OF assms(1) this] guess b by (elim exE conjE)
+ from prime_divisor_exists[OF assms(1) this] obtain b where "b dvd a" "prime b" by auto
with assms(2)[of b] show False by (simp add: prime_def)
qed
@@ -1138,7 +1159,8 @@
next
define n where "n = multiplicity p x"
from assms have "\<not>is_unit p" by simp
- from multiplicity_decompose'[OF False this] guess y . note y = this [folded n_def]
+ from multiplicity_decompose'[OF False this]
+ obtain y where y [folded n_def]: "x = p ^ multiplicity p x * y" "\<not> p dvd y" .
from y have "p ^ Suc n dvd q * x \<longleftrightarrow> p ^ n * p dvd p ^ n * (q * y)" by (simp add: mult_ac)
also from assms have "\<dots> \<longleftrightarrow> p dvd q * y" by simp
also have "\<dots> \<longleftrightarrow> p dvd q \<or> p dvd y" by (rule prime_elem_dvd_mult_iff) fact+
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Fri Sep 24 22:44:13 2021 +0200
@@ -4079,7 +4079,7 @@
from v have [simp]: "length v = Suc m" by (simp add: A_def natpermute_def)
from v have "\<exists>j. j \<le> m \<and> v ! j = k"
by (auto simp: set_conv_nth A_def natpermute_def less_Suc_eq_le)
- then guess j by (elim exE conjE) note j = this
+ then obtain j where j: "j \<le> m" "v ! j = k" by auto
from v have "k = sum_list v" by (simp add: A_def natpermute_def)
also have "\<dots> = (\<Sum>i=0..m. v ! i)"
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy Fri Sep 24 22:44:13 2021 +0200
@@ -64,8 +64,13 @@
obtains d where "fst x = fst (normalize_quot x) * d" "snd x = snd (normalize_quot x) * d"
"d dvd fst x" "d dvd snd x" "d \<noteq> 0"
proof -
- from normalize_quotE[OF assms, of "fst x"] guess d .
- from this show ?thesis unfolding prod.collapse by (intro that[of d])
+ from normalize_quotE[OF assms, of "fst x"] obtain d where
+ "fst x = fst (normalize_quot (fst x, snd x)) * d"
+ "snd x = snd (normalize_quot (fst x, snd x)) * d"
+ "d dvd fst x"
+ "d dvd snd x"
+ "d \<noteq> 0" .
+ then show ?thesis unfolding prod.collapse by (intro that[of d])
qed
lemma coprime_normalize_quot:
@@ -130,7 +135,13 @@
define x' where "x' = normalize_quot x"
obtain a b where [simp]: "x = (a, b)" by (cases x)
from rel have "b \<noteq> 0" by simp
- from normalize_quotE[OF this, of a] guess d .
+ from normalize_quotE[OF this, of a] obtain d
+ where
+ "a = fst (normalize_quot (a, b)) * d"
+ "b = snd (normalize_quot (a, b)) * d"
+ "d dvd a"
+ "d dvd b"
+ "d \<noteq> 0" .
hence "a = fst x' * d" "b = snd x' * d" "d \<noteq> 0" "snd x' \<noteq> 0" by (simp_all add: x'_def)
thus "fractrel (case x' of (a, b) \<Rightarrow> if b = 0 then (0, 1) else (a, b)) x"
by (auto simp add: case_prod_unfold)
@@ -173,8 +184,20 @@
snd x * snd y * (fst (normalize_quot x) * snd (normalize_quot y) +
snd (normalize_quot x) * fst (normalize_quot y))"
proof -
- from normalize_quotE'[OF assms(1)] guess d . note d = this
- from normalize_quotE'[OF assms(2)] guess e . note e = this
+ from normalize_quotE'[OF assms(1)] obtain d
+ where d:
+ "fst x = fst (normalize_quot x) * d"
+ "snd x = snd (normalize_quot x) * d"
+ "d dvd fst x"
+ "d dvd snd x"
+ "d \<noteq> 0" .
+ from normalize_quotE'[OF assms(2)] obtain e
+ where e:
+ "fst y = fst (normalize_quot y) * e"
+ "snd y = snd (normalize_quot y) * e"
+ "e dvd fst y"
+ "e dvd snd y"
+ "e \<noteq> 0" .
show ?thesis by (simp_all add: d e algebra_simps)
qed
@@ -218,9 +241,16 @@
from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
with assms have "normalize b = b" "normalize d = d"
by (auto intro: normalize_unit_factor_eqI)
- from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
+ from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] obtain k
+ where
+ "c = fst (normalize_quot (c, b)) * k"
+ "b = snd (normalize_quot (c, b)) * k"
+ "k dvd c" "k dvd b" "k \<noteq> 0" .
note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
- from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
+ from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] obtain l
+ where "a = fst (normalize_quot (a, d)) * l"
+ "d = snd (normalize_quot (a, d)) * l"
+ "l dvd a" "l dvd d" "l \<noteq> 0" .
note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
from k l show "a * c * (f * h) = b * d * (e * g)"
by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
@@ -241,8 +271,18 @@
(fst (normalize_quot x) * fst (normalize_quot y),
snd (normalize_quot x) * snd (normalize_quot y))"
proof -
- from normalize_quotE'[OF assms(1)] guess d . note d = this
- from normalize_quotE'[OF assms(2)] guess e . note e = this
+ from normalize_quotE'[OF assms(1)] obtain d where d:
+ "fst x = fst (normalize_quot x) * d"
+ "snd x = snd (normalize_quot x) * d"
+ "d dvd fst x"
+ "d dvd snd x"
+ "d \<noteq> 0" .
+ from normalize_quotE'[OF assms(2)] obtain e where e:
+ "fst y = fst (normalize_quot y) * e"
+ "snd y = snd (normalize_quot y) * e"
+ "e dvd fst y"
+ "e dvd snd y"
+ "e \<noteq> 0" .
show ?thesis by (simp_all add: d e algebra_simps normalize_quot_eq_iff)
qed
@@ -269,7 +309,11 @@
defines "a' \<equiv> fst (normalize_quot (a, b))" and "b' \<equiv> snd (normalize_quot (a, b))"
shows "normalize_quot (b, a) = (b' div unit_factor a', a' div unit_factor a')"
proof (rule normalize_quotI)
- from normalize_quotE[OF assms(2), of a] guess d . note d = this [folded assms(3,4)]
+ from normalize_quotE[OF assms(2), of a] obtain d where
+ "a = fst (normalize_quot (a, b)) * d"
+ "b = snd (normalize_quot (a, b)) * d"
+ "d dvd a" "d dvd b" "d \<noteq> 0" .
+ note d = this [folded assms(3,4)]
show "b * (a' div unit_factor a') = a * (b' div unit_factor a')"
using assms(1,2) d
by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
@@ -301,7 +345,10 @@
by simp_all
from \<open>is_unit v\<close> have "coprime v = top"
by (simp add: fun_eq_iff is_unit_left_imp_coprime)
- from normalize_quotE[OF False, of x] guess d .
+ from normalize_quotE[OF False, of x] obtain d where
+ "x = fst (normalize_quot (x, y)) * d"
+ "y = snd (normalize_quot (x, y)) * d"
+ "d dvd x" "d dvd y" "d \<noteq> 0" .
note d = this[folded assms(2,3)]
from assms have "coprime x' y'" "unit_factor y' = 1"
by (simp_all add: coprime_normalize_quot)
@@ -318,7 +365,12 @@
shows "normalize_quot (x, y div u) = (x' * u, y')"
proof (cases "y = 0")
case False
- from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
+ from normalize_quotE[OF this, of x]
+ obtain d where d:
+ "x = fst (normalize_quot (x, y)) * d"
+ "y = snd (normalize_quot (x, y)) * d"
+ "d dvd x" "d dvd y" "d \<noteq> 0" .
+ note d = this[folded assms(2,3)]
from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
with d \<open>is_unit u\<close> show ?thesis
by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
--- a/src/HOL/Computational_Algebra/Polynomial.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Fri Sep 24 22:44:13 2021 +0200
@@ -2661,11 +2661,14 @@
shows "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) x"
proof (cases a b rule: linorder_cases)
case less
- from poly_MVT[OF less, of p] guess x by (elim exE conjE)
+ from poly_MVT[OF less, of p] obtain x
+ where "a < x" "x < b" "poly p b - poly p a = (b - a) * poly (pderiv p) x"
+ by auto
then show ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
next
case greater
- from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
+ from poly_MVT[OF greater, of p] obtain x
+ where "b < x" "x < a" "poly p a - poly p b = (a - b) * poly (pderiv p) x" by auto
then show ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
qed (use assms in auto)
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy Fri Sep 24 22:44:13 2021 +0200
@@ -357,9 +357,15 @@
shows "p dvd q"
proof -
from assms(1) obtain r where r: "fract_poly q = fract_poly p * r" by (erule dvdE)
- from content_decompose_fract[of r] guess c r' . note r' = this
+ from content_decompose_fract[of r]
+ obtain c r' where r': "r = smult c (map_poly to_fract r')" "content r' = 1" .
from r r' have eq: "fract_poly q = smult c (fract_poly (p * r'))" by simp
- from fract_poly_smult_eqE[OF this] guess a b . note ab = this
+ from fract_poly_smult_eqE[OF this] obtain a b
+ where ab:
+ "c = to_fract b / to_fract a"
+ "smult a q = smult b (p * r')"
+ "coprime a b"
+ "normalize a = a" .
have "content (smult a q) = content (smult b (p * r'))" by (simp only: ab(2))
hence eq': "normalize b = a * content q" by (simp add: assms content_mult r' ab(4))
have "1 = gcd a (normalize b)" by (simp add: ab)
@@ -444,7 +450,7 @@
proof safe
assume p: "irreducible p"
- from content_decompose[of p] guess p' . note p' = this
+ from content_decompose[of p] obtain p' where p': "p = smult (content p) p'" "content p' = 1" .
hence "p = [:content p:] * p'" by simp
from p this have "[:content p:] dvd 1 \<or> p' dvd 1" by (rule irreducibleD)
moreover have "\<not>p' dvd 1"
@@ -470,12 +476,16 @@
qed
next
fix q r assume qr: "fract_poly p = q * r"
- from content_decompose_fract[of q] guess cg q' . note q = this
- from content_decompose_fract[of r] guess cr r' . note r = this
+ from content_decompose_fract[of q]
+ obtain cg q' where q: "q = smult cg (map_poly to_fract q')" "content q' = 1" .
+ from content_decompose_fract[of r]
+ obtain cr r' where r: "r = smult cr (map_poly to_fract r')" "content r' = 1" .
from qr q r p have nz: "cg \<noteq> 0" "cr \<noteq> 0" by auto
from qr have eq: "fract_poly p = smult (cr * cg) (fract_poly (q' * r'))"
by (simp add: q r)
- from fract_poly_smult_eqE[OF this] guess a b . note ab = this
+ from fract_poly_smult_eqE[OF this] obtain a b
+ where ab: "cr * cg = to_fract b / to_fract a"
+ "smult a p = smult b (q' * r')" "coprime a b" "normalize a = a" .
hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
then have "normalize b = gcd a b"
@@ -641,7 +651,12 @@
finally have eq: "fract_poly p = smult c' (fract_poly e)" .
also obtain b where b: "c' = to_fract b" "is_unit b"
proof -
- from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
+ from fract_poly_smult_eqE[OF eq]
+ obtain a b where ab:
+ "c' = to_fract b / to_fract a"
+ "smult a p = smult b e"
+ "coprime a b"
+ "normalize a = a" .
from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
with assms content_e have "a = normalize b" by (simp add: ab(4))
with ab have ab': "a = 1" "is_unit b"
@@ -673,7 +688,8 @@
define B where "B = image_mset (\<lambda>x. [:x:]) (prime_factorization (content p))"
have "\<exists>A. (\<forall>p. p \<in># A \<longrightarrow> prime_elem p) \<and> prod_mset A = normalize (primitive_part p)"
by (rule poly_prime_factorization_exists_content_1) (insert assms, simp_all)
- then guess A by (elim exE conjE) note A = this
+ then obtain A where A: "\<forall>p. p \<in># A \<longrightarrow> prime_elem p" "\<Prod>\<^sub># A = normalize (primitive_part p)"
+ by blast
have "normalize (prod_mset (A + B)) = normalize (prod_mset A * normalize (prod_mset B))"
by simp
also from assms have "normalize (prod_mset B) = normalize [:content p:]"
--- a/src/HOL/Number_Theory/Residue_Primitive_Roots.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Number_Theory/Residue_Primitive_Roots.thy Fri Sep 24 22:44:13 2021 +0200
@@ -755,7 +755,15 @@
from assms have "n \<noteq> 0" by auto
from False have "\<exists>p\<in>prime_factors n. p \<noteq> 2"
using assms Ex_other_prime_factor[of n 2] by auto
- from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this] guess p k n' . note p = this
+ from divide_out_primepow_ex[OF \<open>n \<noteq> 0\<close> this]
+ obtain p k n'
+ where p:
+ "p \<noteq> 2"
+ "prime p"
+ "p dvd n"
+ "\<not> p dvd n'"
+ "0 < k"
+ "n = p ^ k * n'" .
from p have coprime: "coprime (p ^ k) n'"
using p prime_imp_coprime by auto
have "odd p"
--- a/src/HOL/Probability/Discrete_Topology.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Discrete_Topology.thy Fri Sep 24 22:44:13 2021 +0200
@@ -32,10 +32,10 @@
instance discrete :: (type) complete_space
proof
- fix X::"nat\<Rightarrow>'a discrete" assume "Cauchy X"
- hence "\<exists>n. \<forall>m\<ge>n. X n = X m"
+ fix X::"nat\<Rightarrow>'a discrete"
+ assume "Cauchy X"
+ then obtain n where "\<forall>m\<ge>n. X n = X m"
by (force simp: dist_discrete_def Cauchy_def split: if_split_asm dest:spec[where x=1])
- then guess n ..
thus "convergent X"
by (intro convergentI[where L="X n"] tendstoI eventually_sequentiallyI[of n])
(simp add: dist_discrete_def)
--- a/src/HOL/Probability/Fin_Map.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Fin_Map.thy Fri Sep 24 22:44:13 2021 +0200
@@ -195,10 +195,20 @@
have "\<forall>i. \<exists>A. countable A \<and> (\<forall>a\<in>A. x i \<in> a) \<and> (\<forall>a\<in>A. open a) \<and>
(\<forall>S. open S \<and> x i \<in> S \<longrightarrow> (\<exists>a\<in>A. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A \<longrightarrow> b \<in> A \<longrightarrow> a \<inter> b \<in> A)" (is "\<forall>i. ?th i")
proof
- fix i from first_countable_basis_Int_stableE[of "x i"] guess A .
+ fix i from first_countable_basis_Int_stableE[of "x i"]
+ obtain A where
+ "countable A"
+ "\<And>C. C \<in> A \<Longrightarrow> (x)\<^sub>F i \<in> C"
+ "\<And>C. C \<in> A \<Longrightarrow> open C"
+ "\<And>S. open S \<Longrightarrow> (x)\<^sub>F i \<in> S \<Longrightarrow> \<exists>A\<in>A. A \<subseteq> S"
+ "\<And>C D. C \<in> A \<Longrightarrow> D \<in> A \<Longrightarrow> C \<inter> D \<in> A"
+ by auto
thus "?th i" by (intro exI[where x=A]) simp
qed
- then guess A unfolding choice_iff .. note A = this
+ then obtain A
+ where A: "\<forall>i. countable (A i) \<and> Ball (A i) ((\<in>) ((x)\<^sub>F i)) \<and> Ball (A i) open \<and>
+ (\<forall>S. open S \<and> (x)\<^sub>F i \<in> S \<longrightarrow> (\<exists>a\<in>A i. a \<subseteq> S)) \<and> (\<forall>a b. a \<in> A i \<longrightarrow> b \<in> A i \<longrightarrow> a \<inter> b \<in> A i)"
+ by (auto simp: choice_iff)
hence open_sub: "\<And>i S. i\<in>domain x \<Longrightarrow> open (S i) \<Longrightarrow> x i\<in>(S i) \<Longrightarrow> (\<exists>a\<in>A i. a\<subseteq>(S i))" by auto
have A_notempty: "\<And>i. i \<in> domain x \<Longrightarrow> A i \<noteq> {}" using open_sub[of _ "\<lambda>_. UNIV"] by auto
let ?A = "(\<lambda>f. Pi' (domain x) f) ` (Pi\<^sub>E (domain x) A)"
@@ -492,7 +502,8 @@
fix i assume "i \<in> d"
from p[OF \<open>i \<in> d\<close>, THEN metric_LIMSEQ_D, OF \<open>0 < e\<close>]
show "\<exists>no. \<forall>n\<ge>no. dist (p i n) (q i) < e" .
- qed then guess ni .. note ni = this
+ qed
+ then obtain ni where ni: "\<forall>i\<in>d. \<forall>n\<ge>ni i. dist (p i n) (q i) < e" ..
define N where "N = max Nd (Max (ni ` d))"
show "\<exists>N. \<forall>n\<ge>N. dist (P n) Q < e"
proof (safe intro!: exI[where x="N"])
@@ -586,10 +597,13 @@
proof (rule bchoice, safe)
fix i assume "i \<in> domain x"
hence "open (a i)" "x i \<in> a i" using a by auto
- from topological_basisE[OF basis_proj this] guess b' .
+ from topological_basisE[OF basis_proj this] obtain b'
+ where "b' \<in> basis_proj" "(x)\<^sub>F i \<in> b'" "b' \<subseteq> a i"
+ by blast
thus "\<exists>y. x i \<in> y \<and> y \<subseteq> a i \<and> y \<in> basis_proj" by auto
qed
- then guess B .. note B = this
+ then obtain B where B: "\<forall>i\<in>domain x. (x)\<^sub>F i \<in> B i \<and> B i \<subseteq> a i \<and> B i \<in> basis_proj"
+ by auto
define B' where "B' = Pi' (domain x) (\<lambda>i. (B i)::'b set)"
have "B' \<subseteq> Pi' (domain x) a" using B by (auto intro!: Pi'_mono simp: B'_def)
also note \<open>\<dots> \<subseteq> O'\<close>
@@ -1016,7 +1030,7 @@
shows "sets (PiF {I} M) = sigma_sets (space (PiF {I} M)) P"
proof
let ?P = "sigma (space (Pi\<^sub>F {I} M)) P"
- from \<open>finite I\<close>[THEN ex_bij_betw_finite_nat] guess T ..
+ from \<open>finite I\<close>[THEN ex_bij_betw_finite_nat] obtain T where "bij_betw T I {0..<card I}" ..
then have T: "\<And>i. i \<in> I \<Longrightarrow> T i < card I" "\<And>i. i\<in>I \<Longrightarrow> the_inv_into I T (T i) = i"
by (auto simp add: bij_betw_def set_eq_iff image_iff the_inv_into_f_f simp del: \<open>finite I\<close>)
have P_closed: "P \<subseteq> Pow (space (Pi\<^sub>F {I} M))"
@@ -1080,7 +1094,9 @@
shows "sets (PiF {I} (\<lambda>_. borel::'b::second_countable_topology measure)) =
sigma_sets (space (PiF {I} (\<lambda>_. borel))) {Pi' I F |F. (\<forall>i\<in>I. F i \<in> Collect open)}"
proof -
- from open_countable_basisE[OF open_UNIV] guess S::"'b set set" . note S = this
+ from open_countable_basisE[OF open_UNIV] obtain S::"'b set set"
+ where S: "S \<subseteq> (SOME B. countable B \<and> topological_basis B)" "UNIV = \<Union> S"
+ by auto
show ?thesis
proof (rule sigma_fprod_algebra_sigma_eq)
show "finite I" by simp
--- a/src/HOL/Probability/Independent_Family.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Independent_Family.thy Fri Sep 24 22:44:13 2021 +0200
@@ -423,7 +423,7 @@
have "sigma_sets (space M) (\<Union>i\<in>I j. E i) = sigma_sets (space M) (?E j)"
proof (rule sigma_sets_eqI)
fix A assume "A \<in> (\<Union>i\<in>I j. E i)"
- then guess i ..
+ then obtain i where "i \<in> I j" "A \<in> E i" ..
then show "A \<in> sigma_sets (space M) (?E j)"
by (auto intro!: sigma_sets.intros(2-) exI[of _ "{i}"] exI[of _ "\<lambda>i. A"])
next
@@ -446,13 +446,14 @@
and "\<forall>j\<in>K. A j \<in> ?E j"
then have "\<forall>j\<in>K. \<exists>E' L. A j = (\<Inter>l\<in>L. E' l) \<and> finite L \<and> L \<noteq> {} \<and> L \<subseteq> I j \<and> (\<forall>l\<in>L. E' l \<in> E l)"
by simp
- from bchoice[OF this] guess E' ..
+ from bchoice[OF this] obtain E'
+ where "\<forall>x\<in>K. \<exists>L. A x = \<Inter> (E' x ` L) \<and> finite L \<and> L \<noteq> {} \<and> L \<subseteq> I x \<and> (\<forall>l\<in>L. E' x l \<in> E l)"
+ ..
from bchoice[OF this] obtain L
where A: "\<And>j. j\<in>K \<Longrightarrow> A j = (\<Inter>l\<in>L j. E' j l)"
and L: "\<And>j. j\<in>K \<Longrightarrow> finite (L j)" "\<And>j. j\<in>K \<Longrightarrow> L j \<noteq> {}" "\<And>j. j\<in>K \<Longrightarrow> L j \<subseteq> I j"
and E': "\<And>j l. j\<in>K \<Longrightarrow> l \<in> L j \<Longrightarrow> E' j l \<in> E l"
by auto
-
{ fix k l j assume "k \<in> K" "j \<in> K" "l \<in> L j" "l \<in> L k"
have "k = j"
proof (rule ccontr)
@@ -747,8 +748,9 @@
then show "?A \<subseteq> Pow (space M)" by auto
show "Int_stable ?A"
proof (rule Int_stableI)
- fix a assume "a \<in> ?A" then guess n .. note a = this
- fix b assume "b \<in> ?A" then guess m .. note b = this
+ fix a b assume "a \<in> ?A" "b \<in> ?A" then obtain n m
+ where a: "n \<in> UNIV" "a \<in> sigma_sets (space M) (\<Union> (A ` {..n}))"
+ and b: "m \<in> UNIV" "b \<in> sigma_sets (space M) (\<Union> (A ` {..m}))" by auto
interpret Amn: sigma_algebra "space M" "sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
using A sets.sets_into_space[of _ M] by (intro sigma_algebra_sigma_sets) auto
have "sigma_sets (space M) (\<Union>i\<in>{..n}. A i) \<subseteq> sigma_sets (space M) (\<Union>i\<in>{..max m n}. A i)"
@@ -1083,8 +1085,14 @@
{ fix i show "emeasure ?D (\<Pi>\<^sub>E i\<in>I. space (M' i)) \<noteq> \<infinity>" by auto }
next
fix E assume E: "E \<in> prod_algebra I M'"
- from prod_algebraE[OF E] guess J Y . note J = this
-
+ from prod_algebraE[OF E] obtain J Y
+ where J:
+ "E = prod_emb I M' J (Pi\<^sub>E J Y)"
+ "finite J"
+ "J \<noteq> {} \<or> I = {}"
+ "J \<subseteq> I"
+ "\<And>i. i \<in> J \<Longrightarrow> Y i \<in> sets (M' i)"
+ by auto
from E have "E \<in> sets ?P" by (auto simp: sets_PiM)
then have "emeasure ?D E = emeasure M (?X -` E \<inter> space M)"
by (simp add: emeasure_distr X)
--- a/src/HOL/Probability/Information.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Information.thy Fri Sep 24 22:44:13 2021 +0200
@@ -273,7 +273,13 @@
proof -
interpret N: prob_space N by fact
have "finite_measure N" by unfold_locales
- from real_RN_deriv[OF this ac] guess D . note D = this
+ from real_RN_deriv[OF this ac] obtain D
+ where D:
+ "random_variable borel D"
+ "AE x in M. RN_deriv M N x = ennreal (D x)"
+ "AE x in N. 0 < D x"
+ "\<And>x. 0 \<le> D x"
+ by this auto
have "N = density M (RN_deriv M N)"
using ac by (rule density_RN_deriv[symmetric])
--- a/src/HOL/Probability/Levy.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Levy.thy Fri Sep 24 22:44:13 2021 +0200
@@ -422,7 +422,9 @@
by (subst (asm) dist_complex_def, drule spec, erule mp, auto)
hence "\<exists>N. \<forall>n \<ge> N. cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by (simp add: eventually_sequentially)
- then guess N ..
+ then obtain N
+ where "\<forall>n\<ge>N. cmod ((CLBINT t:{- d / 2..d / 2}. 1 - char (M n) t) -
+ (CLBINT t:{- d / 2..d / 2}. 1 - char M' t)) < d * \<epsilon> / 4" ..
hence N: "\<And>n. n \<ge> N \<Longrightarrow> cmod ((CLBINT t:{-d/2..d/2}. 1 - char (M n) t) -
(CLBINT t:{-d/2..d/2}. 1 - char M' t)) < d * \<epsilon> / 4" by auto
{ fix n
--- a/src/HOL/Probability/Probability_Measure.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Probability_Measure.thy Fri Sep 24 22:44:13 2021 +0200
@@ -220,7 +220,8 @@
using \<open>I \<noteq> {}\<close> by auto
next
fix k assume "k \<in> (\<lambda>x. q x + ?F x * (expectation X - x)) ` I"
- then guess x .. note x = this
+ then obtain x
+ where x: "k = q x + (INF t\<in>{x<..} \<inter> I. (q x - q t) / (x - t)) * (expectation X - x)" "x \<in> I" ..
have "q x + ?F x * (expectation X - x) = expectation (\<lambda>w. q x + ?F x * (X w - x))"
using prob_space by (simp add: X)
also have "\<dots> \<le> expectation (\<lambda>w. q (X w))"
@@ -320,7 +321,8 @@
assumes ae: "AE x in M. P x"
obtains S where "S \<subseteq> {x \<in> space M. P x}" "S \<in> events" "prob S = 1"
proof -
- from ae[THEN AE_E] guess N .
+ from ae[THEN AE_E] obtain N
+ where "{x \<in> space M. \<not> P x} \<subseteq> N" "emeasure M N = 0" "N \<in> events" by auto
then show thesis
by (intro that[of "space M - N"])
(auto simp: prob_compl prob_space emeasure_eq_measure measure_nonneg)
@@ -365,7 +367,12 @@
assumes ae: "AE x in M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))"
shows "(\<lambda>n. \<P>(x in M. P n x)) sums \<P>(x in M. Q x)"
proof -
- from ae[THEN AE_E_prob] guess S . note S = this
+ from ae[THEN AE_E_prob] obtain S
+ where S:
+ "S \<subseteq> {x \<in> space M. (\<forall>n. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. P n x))}"
+ "S \<in> events"
+ "prob S = 1"
+ by auto
then have disj: "disjoint_family (\<lambda>n. {x\<in>space M. P n x} \<inter> S)"
by (auto simp: disjoint_family_on_def)
from S have ae_S:
@@ -390,7 +397,12 @@
assumes ae: "AE x in M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n\<in>I. P n x))"
shows "\<P>(x in M. Q x) = (\<Sum>n\<in>I. \<P>(x in M. P n x))"
proof -
- from ae[THEN AE_E_prob] guess S . note S = this
+ from ae[THEN AE_E_prob] obtain S
+ where S:
+ "S \<subseteq> {x \<in> space M. (\<forall>n\<in>I. P n x \<longrightarrow> Q x) \<and> (Q x \<longrightarrow> (\<exists>!n. n \<in> I \<and> P n x))}"
+ "S \<in> events"
+ "prob S = 1"
+ by auto
then have disj: "disjoint_family_on (\<lambda>n. {x\<in>space M. P n x} \<inter> S) I"
by (auto simp: disjoint_family_on_def)
from S have ae_S:
@@ -692,7 +704,10 @@
interpret T: sigma_finite_measure T by fact
interpret ST: pair_sigma_finite S T ..
- from ST.sigma_finite_up_in_pair_measure_generator guess F :: "nat \<Rightarrow> ('b \<times> 'c) set" .. note F = this
+ from ST.sigma_finite_up_in_pair_measure_generator
+ obtain F :: "nat \<Rightarrow> ('b \<times> 'c) set"
+ where F: "range F \<subseteq> {A \<times> B |A B. A \<in> sets S \<and> B \<in> sets T} \<and> incseq F \<and>
+ \<Union> (range F) = space S \<times> space T \<and> (\<forall>i. emeasure (S \<Otimes>\<^sub>M T) (F i) \<noteq> \<infinity>)" ..
let ?E = "{a \<times> b |a b. a \<in> sets S \<and> b \<in> sets T}"
let ?P = "S \<Otimes>\<^sub>M T"
show "distr M ?P (\<lambda>x. (X x, Y x)) = density ?P f" (is "?L = ?R")
--- a/src/HOL/Probability/Projective_Limit.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Projective_Limit.thy Fri Sep 24 22:44:13 2021 +0200
@@ -49,7 +49,8 @@
proof atomize_elim
have "strict_mono ((+) m)" by (simp add: strict_mono_def)
have "\<forall>n. (f o (\<lambda>i. m + i)) n \<in> S" using assms by auto
- from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this] guess l r .
+ from seq_compactE[OF \<open>compact S\<close>[unfolded compact_eq_seq_compact_metric] this]
+ obtain l r where "l \<in> S" "strict_mono r" "(f \<circ> (+) m \<circ> r) \<longlonglongrightarrow> l" by blast
hence "l \<in> S" "strict_mono ((\<lambda>i. m + i) o r) \<and> (f \<circ> ((\<lambda>i. m + i) o r)) \<longlonglongrightarrow> l"
using strict_mono_o[OF \<open>strict_mono ((+) m)\<close> \<open>strict_mono r\<close>] by (auto simp: o_def)
thus "\<exists>l r. l \<in> S \<and> strict_mono r \<and> (f \<circ> r) \<longlonglongrightarrow> l" by blast
@@ -59,7 +60,8 @@
proof
fix n and s :: "nat \<Rightarrow> nat"
assume "strict_mono s"
- from proj_in_KE[of n] guess n0 . note n0 = this
+ from proj_in_KE[of n] obtain n0 where n0: "\<And>m. n0 \<le> m \<Longrightarrow> (f m)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
+ by blast
have "\<forall>i \<ge> n0. ((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0"
proof safe
fix i assume "n0 \<le> i"
@@ -68,7 +70,9 @@
with n0 show "((f \<circ> s) i)\<^sub>F n \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0 "
by auto
qed
- from compactE'[OF compact_projset this] guess ls rs .
+ then obtain ls rs
+ where "ls \<in> (\<lambda>k. (k)\<^sub>F n) ` K n0" "strict_mono rs" "((\<lambda>i. ((f \<circ> s) i)\<^sub>F n) \<circ> rs) \<longlonglongrightarrow> ls"
+ by (rule compactE'[OF compact_projset])
thus "\<exists>r'. strict_mono r' \<and> (\<exists>l. (\<lambda>i. ((f \<circ> (s \<circ> r')) i)\<^sub>F n) \<longlonglongrightarrow> l)" by (auto simp: o_def)
qed
--- a/src/HOL/Probability/Stopping_Time.thy Fri Sep 24 11:04:18 2021 +0000
+++ b/src/HOL/Probability/Stopping_Time.thy Fri Sep 24 22:44:13 2021 +0200
@@ -143,8 +143,9 @@
lemma stopping_time_less_const:
assumes T: "stopping_time F T" shows "Measurable.pred (F t) (\<lambda>\<omega>. T \<omega> < t)"
proof -
- guess D :: "'t set" by (rule countable_dense_setE)
- note D = this
+ obtain D :: "'t set"
+ where D: "countable D" "\<And>X. open X \<Longrightarrow> X \<noteq> {} \<Longrightarrow> \<exists>d\<in>D. d \<in> X"
+ using countable_dense_setE by auto
show ?thesis
proof cases
assume *: "\<forall>t'<t. \<exists>t''. t' < t'' \<and> t'' < t"