--- a/src/HOL/Analysis/Binary_Product_Measure.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Binary_Product_Measure.thy Thu Nov 08 09:11:52 2018 +0100
@@ -613,7 +613,7 @@
have [simp]: "snd \<in> X \<times> Y \<rightarrow> Y" "fst \<in> X \<times> Y \<rightarrow> X"
by auto
let ?XY = "{{fst -` a \<inter> X \<times> Y | a. a \<in> A}, {snd -` b \<inter> X \<times> Y | b. b \<in> B}}"
- have "sets ?P = sets (SUP xy:?XY. sigma (X \<times> Y) xy)"
+ have "sets ?P = sets (SUP xy\<in>?XY. sigma (X \<times> Y) xy)"
by (simp add: vimage_algebra_sigma sets_pair_eq_sets_fst_snd A B)
also have "\<dots> = sets (sigma (X \<times> Y) (\<Union>?XY))"
by (intro Sup_sigma arg_cong[where f=sets]) auto
@@ -713,7 +713,7 @@
also have "{sigma ?\<Omega> {fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, sigma ?\<Omega> {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}} =
sigma ?\<Omega> ` {{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}"
by auto
- also have "sets (SUP S:{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}. sigma ?\<Omega> S) =
+ also have "sets (SUP S\<in>{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}. sigma ?\<Omega> S) =
sets (sigma ?\<Omega> (\<Union>{{fst -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Ea}, {snd -` Aa \<inter> ?\<Omega> |Aa. Aa \<in> Eb}}))"
using Ea(1) Eb(1) by (intro sets_Sup_sigma) auto
also have "\<dots> \<subseteq> sets (sigma ?\<Omega> ?E)"
--- a/src/HOL/Analysis/Borel_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -811,14 +811,14 @@
fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
assumes [simp]: "countable I"
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
- shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+ shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> borel_measurable M"
by%unimportant (rule borel_measurableI_greater) (simp add: less_SUP_iff)
lemma%unimportant borel_measurable_INF[measurable (raw)]:
fixes F :: "_ \<Rightarrow> _ \<Rightarrow> _::{complete_linorder, linorder_topology, second_countable_topology}"
assumes [simp]: "countable I"
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
- shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+ shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
by (rule borel_measurableI_less) (simp add: INF_less_iff)
lemma%unimportant borel_measurable_cSUP[measurable (raw)]:
@@ -826,7 +826,7 @@
assumes [simp]: "countable I"
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
assumes bdd: "\<And>x. x \<in> space M \<Longrightarrow> bdd_above ((\<lambda>i. F i x) ` I)"
- shows "(\<lambda>x. SUP i:I. F i x) \<in> borel_measurable M"
+ shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> borel_measurable M"
proof cases
assume "I = {}" then show ?thesis
unfolding \<open>I = {}\<close> image_empty by simp
@@ -837,9 +837,9 @@
fix y
have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} \<in> sets M"
by measurable
- also have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} = {x \<in> space M. (SUP i:I. F i x) \<le> y}"
+ also have "{x \<in> space M. \<forall>i\<in>I. F i x \<le> y} = {x \<in> space M. (SUP i\<in>I. F i x) \<le> y}"
by (simp add: cSUP_le_iff \<open>I \<noteq> {}\<close> bdd cong: conj_cong)
- finally show "{x \<in> space M. (SUP i:I. F i x) \<le> y} \<in> sets M" .
+ finally show "{x \<in> space M. (SUP i\<in>I. F i x) \<le> y} \<in> sets M" .
qed
qed
@@ -848,7 +848,7 @@
assumes [simp]: "countable I"
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
assumes bdd: "\<And>x. x \<in> space M \<Longrightarrow> bdd_below ((\<lambda>i. F i x) ` I)"
- shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+ shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
proof%unimportant cases
assume "I = {}" then show ?thesis
unfolding \<open>I = {}\<close> image_empty by simp
@@ -859,9 +859,9 @@
fix y
have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} \<in> sets M"
by measurable
- also have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} = {x \<in> space M. y \<le> (INF i:I. F i x)}"
+ also have "{x \<in> space M. \<forall>i\<in>I. y \<le> F i x} = {x \<in> space M. y \<le> (INF i\<in>I. F i x)}"
by (simp add: le_cINF_iff \<open>I \<noteq> {}\<close> bdd cong: conj_cong)
- finally show "{x \<in> space M. y \<le> (INF i:I. F i x)} \<in> sets M" .
+ finally show "{x \<in> space M. y \<le> (INF i\<in>I. F i x)} \<in> sets M" .
qed
qed
@@ -1958,22 +1958,22 @@
fixes F :: "_ \<Rightarrow> _ \<Rightarrow> real"
assumes [simp]: "countable I"
assumes F[measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> borel_measurable M"
- shows "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable M"
+ shows "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable M"
proof%unimportant (rule measurable_piecewise_restrict)
let ?\<Omega> = "{x\<in>space M. bdd_below ((\<lambda>i. F i x)`I)}"
show "countable {?\<Omega>, - ?\<Omega>}" "space M \<subseteq> \<Union>{?\<Omega>, - ?\<Omega>}" "\<And>X. X \<in> {?\<Omega>, - ?\<Omega>} \<Longrightarrow> X \<inter> space M \<in> sets M"
by auto
- fix X assume "X \<in> {?\<Omega>, - ?\<Omega>}" then show "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable (restrict_space M X)"
+ fix X assume "X \<in> {?\<Omega>, - ?\<Omega>}" then show "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable (restrict_space M X)"
proof safe
- show "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable (restrict_space M ?\<Omega>)"
+ show "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable (restrict_space M ?\<Omega>)"
by (intro borel_measurable_cINF measurable_restrict_space1 F)
(auto simp: space_restrict_space)
- show "(\<lambda>x. INF i:I. F i x) \<in> borel_measurable (restrict_space M (-?\<Omega>))"
+ show "(\<lambda>x. INF i\<in>I. F i x) \<in> borel_measurable (restrict_space M (-?\<Omega>))"
proof (subst measurable_cong)
fix x assume "x \<in> space (restrict_space M (-?\<Omega>))"
then have "\<not> (\<forall>i\<in>I. - F i x \<le> y)" for y
by (auto simp: space_restrict_space bdd_above_def bdd_above_uminus[symmetric])
- then show "(INF i:I. F i x) = - (THE x. False)"
+ then show "(INF i\<in>I. F i x) = - (THE x. False)"
by (auto simp: space_restrict_space Inf_real_def Sup_real_def Least_def simp del: Set.ball_simps(10))
qed simp
qed
--- a/src/HOL/Analysis/Bounded_Continuous_Function.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Continuous_Function.thy Thu Nov 08 09:11:52 2018 +0100
@@ -45,7 +45,7 @@
is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
- where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ where "uniformity_bcontfun = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy Thu Nov 08 09:11:52 2018 +0100
@@ -150,7 +150,7 @@
where "dist_blinfun a b = norm (a - b)"
definition [code del]:
- "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ "(uniformity :: (('a \<Rightarrow>\<^sub>L 'b) \<times> ('a \<Rightarrow>\<^sub>L 'b)) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition open_blinfun :: "('a \<Rightarrow>\<^sub>L 'b) set \<Rightarrow> bool"
where [code del]: "open_blinfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
--- a/src/HOL/Analysis/Caratheodory.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Caratheodory.thy Thu Nov 08 09:11:52 2018 +0100
@@ -22,7 +22,7 @@
using assms by (simp add: fun_eq_iff)
have reindex: "\<And>B. (\<Sum>x\<in>B. f (prod_decode x)) = sum f (prod_decode ` B)"
by (simp add: sum.reindex[OF inj_prod_decode] comp_def)
- have "(SUP n. \<Sum>i<n. f (prod_decode i)) = (SUP p : UNIV \<times> UNIV. \<Sum>i<fst p. \<Sum>n<snd p. f (i, n))"
+ have "(SUP n. \<Sum>i<n. f (prod_decode i)) = (SUP p \<in> UNIV \<times> UNIV. \<Sum>i<fst p. \<Sum>n<snd p. f (i, n))"
proof (intro SUP_eq; clarsimp simp: sum.cartesian_product reindex)
fix n
let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))"
@@ -299,7 +299,7 @@
definition%important outer_measure :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ennreal) \<Rightarrow> 'a set \<Rightarrow> ennreal" where
"outer_measure M f X =
- (INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
+ (INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i)}. \<Sum>i. f (A i))"
lemma%unimportant (in ring_of_sets) outer_measure_agrees:
assumes posf: "positive M f" and ca: "countably_additive M f" and s: "s \<in> M"
@@ -321,7 +321,7 @@
next
have "(\<Sum>i. f (if i = 0 then s else {})) \<le> f s"
using positiveD1[OF posf] by (subst suminf_finite[of "{0}"]) auto
- with s show "(INF A:{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
+ with s show "(INF A\<in>{A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> UNION UNIV A}. \<Sum>i. f (A i)) \<le> f s"
by (intro INF_lower2[of "\<lambda>i. if i = 0 then s else {}"])
(auto simp: disjoint_family_on_def)
qed
--- a/src/HOL/Analysis/Complete_Measure.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy Thu Nov 08 09:11:52 2018 +0100
@@ -452,7 +452,7 @@
locale cld_measure = complete_measure M + locally_determined_measure M for M :: "'a measure"
definition outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
- where "outer_measure_of M A = (INF B : {B\<in>sets M. A \<subseteq> B}. emeasure M B)"
+ where "outer_measure_of M A = (INF B \<in> {B\<in>sets M. A \<subseteq> B}. emeasure M B)"
lemma outer_measure_of_eq[simp]: "A \<in> sets M \<Longrightarrow> outer_measure_of M A = emeasure M A"
by (auto simp: outer_measure_of_def intro!: INF_eqI emeasure_mono)
--- a/src/HOL/Analysis/Connected.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy Thu Nov 08 09:11:52 2018 +0100
@@ -1057,14 +1057,14 @@
proof
assume L: ?lhs
then have "is_interval S" "compact S" by auto
- define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x:S. x \<bullet> i) *\<^sub>R i"
- define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x:S. x \<bullet> i) *\<^sub>R i"
- have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
+ define a where "a \<equiv> \<Sum>i\<in>Basis. (INF x\<in>S. x \<bullet> i) *\<^sub>R i"
+ define b where "b \<equiv> \<Sum>i\<in>Basis. (SUP x\<in>S. x \<bullet> i) *\<^sub>R i"
+ have 1: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
by (simp add: cInf_lower bounded_inner_imp_bdd_below compact_imp_bounded L)
- have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+ have 2: "\<And>x i. \<lbrakk>x \<in> S; i \<in> Basis\<rbrakk> \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
by (simp add: cSup_upper bounded_inner_imp_bdd_above compact_imp_bounded L)
- have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x:S. x \<bullet> i) \<le> x \<bullet> i"
- and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x:S. x \<bullet> i)" for x
+ have 3: "x \<in> S" if inf: "\<And>i. i \<in> Basis \<Longrightarrow> (INF x\<in>S. x \<bullet> i) \<le> x \<bullet> i"
+ and sup: "\<And>i. i \<in> Basis \<Longrightarrow> x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)" for x
proof (rule mem_box_componentwiseI [OF \<open>is_interval S\<close>])
fix i::'a
assume i: "i \<in> Basis"
@@ -1074,14 +1074,14 @@
using continuous_attains_inf [OF \<open>compact S\<close> False cont] by blast
obtain b where "b \<in> S" and b: "\<And>y. y\<in>S \<Longrightarrow> y \<bullet> i \<le> b \<bullet> i"
using continuous_attains_sup [OF \<open>compact S\<close> False cont] by blast
- have "a \<bullet> i \<le> (INF x:S. x \<bullet> i)"
+ have "a \<bullet> i \<le> (INF x\<in>S. x \<bullet> i)"
by (simp add: False a cINF_greatest)
also have "\<dots> \<le> x \<bullet> i"
by (simp add: i inf)
finally have ai: "a \<bullet> i \<le> x \<bullet> i" .
- have "x \<bullet> i \<le> (SUP x:S. x \<bullet> i)"
+ have "x \<bullet> i \<le> (SUP x\<in>S. x \<bullet> i)"
by (simp add: i sup)
- also have "(SUP x:S. x \<bullet> i) \<le> b \<bullet> i"
+ also have "(SUP x\<in>S. x \<bullet> i) \<le> b \<bullet> i"
by (simp add: False b cSUP_least)
finally have bi: "x \<bullet> i \<le> b \<bullet> i" .
show "x \<bullet> i \<in> (\<lambda>x. x \<bullet> i) ` S"
@@ -1282,12 +1282,12 @@
subsection \<open>Infimum Distance\<close>
-definition%important "infdist x A = (if A = {} then 0 else INF a:A. dist x a)"
+definition%important "infdist x A = (if A = {} then 0 else INF a\<in>A. dist x a)"
lemma bdd_below_image_dist[intro, simp]: "bdd_below (dist x ` A)"
by (auto intro!: zero_le_dist)
-lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a:A. dist x a)"
+lemma infdist_notempty: "A \<noteq> {} \<Longrightarrow> infdist x A = (INF a\<in>A. dist x a)"
by (simp add: infdist_def)
lemma infdist_nonneg: "0 \<le> infdist x A"
@@ -2665,7 +2665,7 @@
subsection \<open>The diameter of a set\<close>
definition%important diameter :: "'a::metric_space set \<Rightarrow> real" where
- "diameter S = (if S = {} then 0 else SUP (x,y):S\<times>S. dist x y)"
+ "diameter S = (if S = {} then 0 else SUP (x,y)\<in>S\<times>S. dist x y)"
lemma diameter_empty [simp]: "diameter{} = 0"
by (auto simp: diameter_def)
@@ -2696,7 +2696,7 @@
by (simp add: dist_commute)
qed
moreover have "(x,y) \<in> s\<times>s" using s by auto
- ultimately have "dist x y \<le> (SUP (x,y):s\<times>s. dist x y)"
+ ultimately have "dist x y \<le> (SUP (x,y)\<in>s\<times>s. dist x y)"
by (rule cSUP_upper2) simp
with \<open>x \<in> s\<close> show ?thesis
by (auto simp: diameter_def)
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -5474,7 +5474,7 @@
apply (erule_tac x="x - y" in ballE)
apply (auto simp: inner_diff)
done
- define k where "k = (SUP x:T. a \<bullet> x)"
+ define k where "k = (SUP x\<in>T. a \<bullet> x)"
show ?thesis
apply (rule_tac x="-a" in exI)
apply (rule_tac x="-(k + b / 2)" in exI)
@@ -5580,7 +5580,7 @@
using \<open>T \<noteq> {}\<close> by (auto intro: bdd_aboveI2[OF *])
show ?thesis
using \<open>a\<noteq>0\<close>
- by (intro exI[of _ a] exI[of _ "SUP x:S. a \<bullet> x"])
+ by (intro exI[of _ a] exI[of _ "SUP x\<in>S. a \<bullet> x"])
(auto intro!: cSUP_upper bdd cSUP_least \<open>a \<noteq> 0\<close> \<open>S \<noteq> {}\<close> *)
qed
--- a/src/HOL/Analysis/Embed_Measure.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Embed_Measure.thy Thu Nov 08 09:11:52 2018 +0100
@@ -381,24 +381,24 @@
assumes nonempty: "Y \<noteq> {}"
and chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
and countable: "countable B"
- shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space B) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
+ shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space B) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space B))"
(is "?lhs = ?rhs")
proof -
let ?f = "(\<lambda>i x. f i (from_nat_into B x) * indicator (to_nat_on B ` B) x)"
- have "?lhs = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
+ have "?lhs = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B (to_nat_on B x))) \<partial>count_space B"
by(rule nn_integral_cong)(simp add: countable)
- also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
+ also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. f i (from_nat_into B x)) \<partial>count_space (to_nat_on B ` B)"
by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
- also have "\<dots> = \<integral>\<^sup>+ x. (SUP i:Y. ?f i x) \<partial>count_space UNIV"
+ also have "\<dots> = \<integral>\<^sup>+ x. (SUP i\<in>Y. ?f i x) \<partial>count_space UNIV"
by(simp add: nn_integral_count_space_indicator ennreal_indicator[symmetric] SUP_mult_right_ennreal nonempty)
- also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
+ also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. ?f i x \<partial>count_space UNIV)"
proof(rule nn_integral_monotone_convergence_SUP_nat)
show "Complete_Partial_Order.chain (\<le>) (?f ` Y)"
by(rule chain_imageI[OF chain, unfolded image_image])(auto intro!: le_funI split: split_indicator dest: le_funD)
qed fact
- also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
+ also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B x) \<partial>count_space (to_nat_on B ` B))"
by(simp add: nn_integral_count_space_indicator)
- also have "\<dots> = (SUP i:Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
+ also have "\<dots> = (SUP i\<in>Y. \<integral>\<^sup>+ x. f i (from_nat_into B (to_nat_on B x)) \<partial>count_space B)"
by(simp add: embed_measure_count_space'[symmetric] inj_on_to_nat_on countable nn_integral_embed_measure' measurable_embed_measure1)
also have "\<dots> = ?rhs"
by(intro arg_cong2[where f="SUPREMUM"] ext nn_integral_cong_AE)(simp_all add: AE_count_space countable)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Nov 08 09:11:52 2018 +0100
@@ -2150,7 +2150,7 @@
have D_2: "bdd_above (?f`?D)"
by (metis * mem_Collect_eq bdd_aboveI2)
note D = D_1 D_2
- let ?S = "SUP x:?D. ?f x"
+ let ?S = "SUP x\<in>?D. ?f x"
have *: "\<exists>\<gamma>. gauge \<gamma> \<and>
(\<forall>p. p tagged_division_of cbox a b \<and>
\<gamma> fine p \<longrightarrow>
@@ -2533,7 +2533,7 @@
have D_2: "bdd_above (?f`?D)"
by (intro bdd_aboveI2[where M=B] assms(2)[rule_format]) simp
note D = D_1 D_2
- let ?S = "SUP d:?D. ?f d"
+ let ?S = "SUP d\<in>?D. ?f d"
have "\<And>a b. f integrable_on cbox a b"
using assms(1) integrable_on_subcbox by blast
then have f_int: "\<And>a b. f absolutely_integrable_on cbox a b"
@@ -3807,7 +3807,7 @@
by (intro tendsto_lowerbound[OF lim])
(auto simp: eventually_at_top_linorder)
- have "(SUP i::nat. ?f i x) = ?fR x" for x
+ have "(SUP i. ?f i x) = ?fR x" for x
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
obtain n where "x - a < real n"
using reals_Archimedean2[of "x - a"] ..
@@ -3816,16 +3816,16 @@
then show "(\<lambda>n. ?f n x) \<longlonglongrightarrow> ?fR x"
by (rule Lim_eventually)
qed (auto simp: nonneg incseq_def le_fun_def split: split_indicator)
- then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i::nat. ?f i x) \<partial>lborel)"
+ then have "integral\<^sup>N lborel ?fR = (\<integral>\<^sup>+ x. (SUP i. ?f i x) \<partial>lborel)"
by simp
- also have "\<dots> = (SUP i::nat. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
+ also have "\<dots> = (SUP i. (\<integral>\<^sup>+ x. ?f i x \<partial>lborel))"
proof (rule nn_integral_monotone_convergence_SUP)
show "incseq ?f"
using nonneg by (auto simp: incseq_def le_fun_def split: split_indicator)
show "\<And>i. (?f i) \<in> borel_measurable lborel"
using f_borel by auto
qed
- also have "\<dots> = (SUP i::nat. ennreal (F (a + real i) - F a))"
+ also have "\<dots> = (SUP i. ennreal (F (a + real i) - F a))"
by (subst nn_integral_FTC_Icc[OF f_borel f nonneg]) auto
also have "\<dots> = T - F a"
proof (rule LIMSEQ_unique[OF LIMSEQ_SUP])
--- a/src/HOL/Analysis/Extended_Real_Limits.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy Thu Nov 08 09:11:52 2018 +0100
@@ -298,7 +298,7 @@
lemma%important Liminf_within:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
- shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
+ shows "Liminf (at x within S) f = (SUP e\<in>{0<..}. INF y\<in>(S \<inter> ball x e - {x}). f y)"
unfolding Liminf_def eventually_at
proof%unimportant (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
fix P d
@@ -318,7 +318,7 @@
lemma%important Limsup_within:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
- shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
+ shows "Limsup (at x within S) f = (INF e\<in>{0<..}. SUP y\<in>(S \<inter> ball x e - {x}). f y)"
unfolding Limsup_def eventually_at
proof%unimportant (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
fix P d
@@ -338,17 +338,17 @@
lemma Liminf_at:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
- shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
+ shows "Liminf (at x) f = (SUP e\<in>{0<..}. INF y\<in>(ball x e - {x}). f y)"
using Liminf_within[of x UNIV f] by simp
lemma Limsup_at:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
- shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
+ shows "Limsup (at x) f = (INF e\<in>{0<..}. SUP y\<in>(ball x e - {x}). f y)"
using Limsup_within[of x UNIV f] by simp
lemma min_Liminf_at:
fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_linorder"
- shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
+ shows "min (f x) (Liminf (at x) f) = (SUP e\<in>{0<..}. INF y\<in>ball x e. f y)"
unfolding inf_min[symmetric] Liminf_at
apply (subst inf_commute)
apply (subst SUP_inf)
@@ -1231,16 +1231,16 @@
lemma limsup_shift:
"limsup (\<lambda>n. u (n+1)) = limsup u"
proof -
- have "(SUP m:{n+1..}. u m) = (SUP m:{n..}. u (m + 1))" for n
+ have "(SUP m\<in>{n+1..}. u m) = (SUP m\<in>{n..}. u (m + 1))" for n
apply (rule SUP_eq) using Suc_le_D by auto
- then have a: "(INF n. SUP m:{n..}. u (m + 1)) = (INF n. (SUP m:{n+1..}. u m))" by auto
- have b: "(INF n. (SUP m:{n+1..}. u m)) = (INF n:{1..}. (SUP m:{n..}. u m))"
+ then have a: "(INF n. SUP m\<in>{n..}. u (m + 1)) = (INF n. (SUP m\<in>{n+1..}. u m))" by auto
+ have b: "(INF n. (SUP m\<in>{n+1..}. u m)) = (INF n\<in>{1..}. (SUP m\<in>{n..}. u m))"
apply (rule INF_eq) using Suc_le_D by auto
- have "(INF n:{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
+ have "(INF n\<in>{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \<Rightarrow> 'a"
apply (rule INF_eq) using \<open>decseq v\<close> decseq_Suc_iff by auto
- moreover have "decseq (\<lambda>n. (SUP m:{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
- ultimately have c: "(INF n:{1..}. (SUP m:{n..}. u m)) = (INF n. (SUP m:{n..}. u m))" by simp
- have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m:{n..}. u (m + 1))" using a b c by simp
+ moreover have "decseq (\<lambda>n. (SUP m\<in>{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
+ ultimately have c: "(INF n\<in>{1..}. (SUP m\<in>{n..}. u m)) = (INF n. (SUP m\<in>{n..}. u m))" by simp
+ have "(INF n. SUPREMUM {n..} u) = (INF n. SUP m\<in>{n..}. u (m + 1))" using a b c by simp
then show ?thesis by (auto cong: limsup_INF_SUP)
qed
@@ -1255,16 +1255,16 @@
lemma liminf_shift:
"liminf (\<lambda>n. u (n+1)) = liminf u"
proof -
- have "(INF m:{n+1..}. u m) = (INF m:{n..}. u (m + 1))" for n
+ have "(INF m\<in>{n+1..}. u m) = (INF m\<in>{n..}. u (m + 1))" for n
apply (rule INF_eq) using Suc_le_D by (auto)
- then have a: "(SUP n. INF m:{n..}. u (m + 1)) = (SUP n. (INF m:{n+1..}. u m))" by auto
- have b: "(SUP n. (INF m:{n+1..}. u m)) = (SUP n:{1..}. (INF m:{n..}. u m))"
+ then have a: "(SUP n. INF m\<in>{n..}. u (m + 1)) = (SUP n. (INF m\<in>{n+1..}. u m))" by auto
+ have b: "(SUP n. (INF m\<in>{n+1..}. u m)) = (SUP n\<in>{1..}. (INF m\<in>{n..}. u m))"
apply (rule SUP_eq) using Suc_le_D by (auto)
- have "(SUP n:{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
+ have "(SUP n\<in>{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \<Rightarrow> 'a"
apply (rule SUP_eq) using \<open>incseq v\<close> incseq_Suc_iff by auto
- moreover have "incseq (\<lambda>n. (INF m:{n..}. u m))" by (simp add: INF_superset_mono mono_def)
- ultimately have c: "(SUP n:{1..}. (INF m:{n..}. u m)) = (SUP n. (INF m:{n..}. u m))" by simp
- have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m:{n..}. u (m + 1))" using a b c by simp
+ moreover have "incseq (\<lambda>n. (INF m\<in>{n..}. u m))" by (simp add: INF_superset_mono mono_def)
+ ultimately have c: "(SUP n\<in>{1..}. (INF m\<in>{n..}. u m)) = (SUP n. (INF m\<in>{n..}. u m))" by simp
+ have "(SUP n. INFIMUM {n..} u) = (SUP n. INF m\<in>{n..}. u (m + 1))" using a b c by simp
then show ?thesis by (auto cong: liminf_SUP_INF)
qed
@@ -1281,7 +1281,7 @@
assumes "Limsup F u > c"
shows "\<exists>i. u i > c"
proof%unimportant -
- have "(INF P:{P. eventually P F}. SUP x:{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
+ have "(INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
qed
@@ -1297,7 +1297,7 @@
by (intro dependent_nat_choice) (auto simp: conj_commute)
then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<le> u (r n)"
by (auto simp: strict_mono_Suc_iff)
- define umax where "umax = (\<lambda>n. (SUP m:{n..}. u m))"
+ define umax where "umax = (\<lambda>n. (SUP m\<in>{n..}. u m))"
have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
then have "umax \<longlonglongrightarrow> limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
then have *: "(umax o r) \<longlonglongrightarrow> limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
@@ -1373,7 +1373,7 @@
then have "u i \<le> u (r(Suc n))" using r by simp
then have "u i \<le> (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
}
- then have "(SUP i:{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
+ then have "(SUP i\<in>{N<..}. u i) \<le> (SUP n. (u o r) n)" using SUP_least by blast
then have "limsup u \<le> (SUP n. (u o r) n)" unfolding Limsup_def
by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
@@ -1390,7 +1390,7 @@
by (intro dependent_nat_choice) (auto simp: conj_commute)
then obtain r :: "nat \<Rightarrow> nat" where "strict_mono r" and mono: "\<And>n m. r n \<le> m \<Longrightarrow> u m \<ge> u (r n)"
by (auto simp: strict_mono_Suc_iff)
- define umin where "umin = (\<lambda>n. (INF m:{n..}. u m))"
+ define umin where "umin = (\<lambda>n. (INF m\<in>{n..}. u m))"
have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
then have "umin \<longlonglongrightarrow> liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
then have *: "(umin o r) \<longlonglongrightarrow> liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \<open>strict_mono r\<close>)
@@ -1467,7 +1467,7 @@
then have "u i \<ge> u (r(Suc n))" using r by simp
then have "u i \<ge> (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
}
- then have "(INF i:{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
+ then have "(INF i\<in>{N<..}. u i) \<ge> (INF n. (u o r) n)" using INF_greatest by blast
then have "liminf u \<ge> (INF n. (u o r) n)" unfolding Liminf_def
by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
@@ -1757,7 +1757,7 @@
using * by (intro SUP_upper2[of x]) auto
moreover have "0 \<le> (SUPREMUM {x..} u)" for x
using * by (intro SUP_upper2[of x]) auto
- ultimately show "(SUP n. INF n:{n..}. max 0 (u n - v n))
+ ultimately show "(SUP n. INF n\<in>{n..}. max 0 (u n - v n))
\<le> max 0 ((INF x. max 0 (SUPREMUM {x..} u)) - (INF x. max 0 (SUPREMUM {x..} v)))"
by (auto simp: * ereal_diff_positive max.absorb2 liminf_SUP_INF[symmetric] limsup_INF_SUP[symmetric] ereal_liminf_limsup_minus)
qed
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Thu Nov 08 09:11:52 2018 +0100
@@ -459,7 +459,7 @@
definition%important [code del]:
"(uniformity :: (('a^'b::_) \<times> ('a^'b::_)) filter) =
- (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
instance%unimportant
by standard (rule uniformity_vec_def)
--- a/src/HOL/Analysis/Finite_Product_Measure.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Finite_Product_Measure.thy Thu Nov 08 09:11:52 2018 +0100
@@ -389,7 +389,7 @@
qed
lemma%unimportant sets_PiM_eq_proj:
- "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
+ "I \<noteq> {} \<Longrightarrow> sets (PiM I M) = sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. space (M i)) (\<lambda>x. x i) (M i))"
apply (simp add: sets_PiM_single)
apply (subst sets_Sup_eq[where X="\<Pi>\<^sub>E i\<in>I. space (M i)"])
apply auto []
@@ -422,9 +422,9 @@
let ?F = "\<lambda>i. {(\<lambda>x. x i) -` A \<inter> Pi\<^sub>E I \<Omega> |A. A \<in> E i}"
assume "I \<noteq> {}"
then have "sets (Pi\<^sub>M I (\<lambda>i. sigma (\<Omega> i) (E i))) =
- sets (SUP i:I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
+ sets (SUP i\<in>I. vimage_algebra (\<Pi>\<^sub>E i\<in>I. \<Omega> i) (\<lambda>x. x i) (sigma (\<Omega> i) (E i)))"
by (subst sets_PiM_eq_proj) (auto simp: space_measure_of_conv)
- also have "\<dots> = sets (SUP i:I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
+ also have "\<dots> = sets (SUP i\<in>I. sigma (Pi\<^sub>E I \<Omega>) (?F i))"
using E by (intro sets_SUP_cong arg_cong[where f=sets] vimage_algebra_sigma) auto
also have "\<dots> = sets (sigma (Pi\<^sub>E I \<Omega>) (\<Union>i\<in>I. ?F i))"
using \<open>I \<noteq> {}\<close> by (intro arg_cong[where f=sets] SUP_sigma_sigma) auto
--- a/src/HOL/Analysis/Function_Topology.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Function_Topology.thy Thu Nov 08 09:11:52 2018 +0100
@@ -1220,7 +1220,7 @@
"dist x y = (\<Sum>n. (1/2)^n * min (dist (x (from_nat n)) (y (from_nat n))) 1)"
definition%important uniformity_fun_def:
- "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e:{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
+ "(uniformity::(('a \<Rightarrow> 'b) \<times> ('a \<Rightarrow> 'b)) filter) = (INF e\<in>{0<..}. principal {(x, y). dist (x::('a\<Rightarrow>'b)) y < e})"
text \<open>Except for the first one, the auxiliary lemmas below are only useful when proving the
instance: once it is proved, they become trivial consequences of the general theory of metric
--- a/src/HOL/Analysis/Gamma_Function.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Gamma_Function.thy Thu Nov 08 09:11:52 2018 +0100
@@ -372,7 +372,7 @@
shows "uniformly_convergent_on (ball z d) (\<lambda>n z. ln_Gamma_series z n :: complex)"
proof (intro Cauchy_uniformly_convergent uniformly_Cauchy_onI')
fix e :: real assume e: "e > 0"
- define e'' where "e'' = (SUP t:ball z d. norm t + norm t^2)"
+ define e'' where "e'' = (SUP t\<in>ball z d. norm t + norm t^2)"
define e' where "e' = e / (2*e'')"
have "bounded ((\<lambda>t. norm t + norm t^2) ` cball z d)"
by (intro compact_imp_bounded compact_continuous_image) (auto intro!: continuous_intros)
@@ -2270,7 +2270,7 @@
qed
ultimately have compact: "compact B" by (subst compact_eq_bounded_closed) blast
- define M where "M = (SUP z:B. norm (h' z))"
+ define M where "M = (SUP z\<in>B. norm (h' z))"
have "compact (h' ` B)"
by (intro compact_continuous_image continuous_on_subset[OF h'_cont] compact) blast+
hence bdd: "bdd_above ((\<lambda>z. norm (h' z)) ` B)"
--- a/src/HOL/Analysis/Improper_Integral.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Improper_Integral.thy Thu Nov 08 09:11:52 2018 +0100
@@ -674,9 +674,9 @@
qed
qed
define \<gamma> where "\<gamma> \<equiv> \<lambda>x. \<gamma>0 x \<inter>
- ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m:Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
+ ball x ((\<epsilon>/8 / (norm(f x) + 1)) * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / content(cbox a b))"
have "gauge (\<lambda>x. ball x
- (\<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
+ (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b))))"
using \<open>0 < content (cbox a b)\<close> \<open>0 < \<epsilon>\<close> a_less_b
apply (auto simp: gauge_def divide_simps mult_less_0_iff zero_less_mult_iff add_nonneg_eq_0_iff finite_less_Inf_iff)
apply (meson add_nonneg_nonneg mult_nonneg_nonneg norm_ge_zero not_less zero_le_numeral)
@@ -693,7 +693,7 @@
have "finite S"
using S by blast
have "\<gamma>0 fine S" and fineS:
- "(\<lambda>x. ball x (\<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
+ "(\<lambda>x. ball x (\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / ((8 * norm (f x) + 8) * content (cbox a b)))) fine S"
using \<open>\<gamma> fine S\<close> by (auto simp: \<gamma>_def fine_Int)
then have "(\<Sum>(x,K) \<in> S. norm (content K *\<^sub>R h x - integral K h)) < \<epsilon>/2"
by (intro \<gamma>0 that fineS)
@@ -735,11 +735,11 @@
using that by auto
ultimately have "norm (h x) \<le> (\<epsilon> * (b \<bullet> i - a \<bullet> i)) / (4 * content (cbox a b) * ?\<Delta>)"
proof -
- have "dist x u < \<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
- "dist x v < \<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
+ have "dist x u < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
+ "dist x v < \<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
using fineS u_less_v uv xK
by (force simp: fine_def mem_box field_simps dest!: bspec)+
- moreover have "\<epsilon> * (INF m:Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
+ moreover have "\<epsilon> * (INF m\<in>Basis. b \<bullet> m - a \<bullet> m) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2
\<le> \<epsilon> * (b \<bullet> i - a \<bullet> i) / (4 * (norm (f x) + 1) * content (cbox a b)) / 2"
apply (intro mult_left_mono divide_right_mono)
using \<open>i \<in> Basis\<close> \<open>0 < \<epsilon>\<close> apply (auto simp: intro!: cInf_le_finite)
--- a/src/HOL/Analysis/Lebesgue_Measure.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy Thu Nov 08 09:11:52 2018 +0100
@@ -1189,7 +1189,7 @@
using emeasure_bounded_finite[of "?B n"] by (auto simp: emeasure_A)
interpret A: finite_measure ?A
by rule fact
- have "emeasure ?A B + ?e n > (INF U:{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
+ have "emeasure ?A B + ?e n > (INF U\<in>{U. B \<subseteq> U \<and> open U}. emeasure ?A U)"
using \<open>0<e\<close> by (auto simp: outer_regular[OF _ finite_A B, symmetric])
then obtain U where U: "B \<subseteq> U" "open U" and muU: "?\<mu> (?B n \<inter> B) + ?e n > ?\<mu> (?B n \<inter> U)"
unfolding INF_less_iff by (auto simp: emeasure_A)
--- a/src/HOL/Analysis/Measurable.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Measurable.thy Thu Nov 08 09:11:52 2018 +0100
@@ -392,32 +392,32 @@
fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
assumes [simp]: "countable I"
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
- shows "(\<lambda>x. SUP i:I. F i x) \<in> measurable M (count_space UNIV)"
+ shows "(\<lambda>x. SUP i\<in>I. F i x) \<in> measurable M (count_space UNIV)"
unfolding measurable_count_space_eq2_countable
proof (safe intro!: UNIV_I)
fix a
- have "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M =
+ have "(\<lambda>x. SUP i\<in>I. F i x) -` {a} \<inter> space M =
{x\<in>space M. (\<forall>i\<in>I. F i x \<le> a) \<and> (\<forall>b. (\<forall>i\<in>I. F i x \<le> b) \<longrightarrow> a \<le> b)}"
unfolding SUP_le_iff[symmetric] by auto
also have "\<dots> \<in> sets M"
by measurable
- finally show "(\<lambda>x. SUP i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+ finally show "(\<lambda>x. SUP i\<in>I. F i x) -` {a} \<inter> space M \<in> sets M" .
qed
lemma measurable_INF[measurable]:
fixes F :: "'i \<Rightarrow> 'a \<Rightarrow> 'b::{complete_lattice, countable}"
assumes [simp]: "countable I"
assumes [measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> measurable M (count_space UNIV)"
- shows "(\<lambda>x. INF i:I. F i x) \<in> measurable M (count_space UNIV)"
+ shows "(\<lambda>x. INF i\<in>I. F i x) \<in> measurable M (count_space UNIV)"
unfolding measurable_count_space_eq2_countable
proof (safe intro!: UNIV_I)
fix a
- have "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M =
+ have "(\<lambda>x. INF i\<in>I. F i x) -` {a} \<inter> space M =
{x\<in>space M. (\<forall>i\<in>I. a \<le> F i x) \<and> (\<forall>b. (\<forall>i\<in>I. b \<le> F i x) \<longrightarrow> b \<le> a)}"
unfolding le_INF_iff[symmetric] by auto
also have "\<dots> \<in> sets M"
by measurable
- finally show "(\<lambda>x. INF i:I. F i x) -` {a} \<inter> space M \<in> sets M" .
+ finally show "(\<lambda>x. INF i\<in>I. F i x) -` {a} \<inter> space M \<in> sets M" .
qed
lemma measurable_lfp_coinduct[consumes 1, case_names continuity step]:
--- a/src/HOL/Analysis/Measure_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -582,12 +582,12 @@
assumes I: "I \<noteq> {}" and F: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> i \<le> j \<Longrightarrow> F j \<subseteq> F i"
assumes F_sets[measurable]: "\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M"
and fin: "\<And>i. i \<in> I \<Longrightarrow> emeasure M (F i) \<noteq> \<infinity>"
- shows "emeasure M (\<Inter>i\<in>I. F i) = (INF i:I. emeasure M (F i))"
+ shows "emeasure M (\<Inter>i\<in>I. F i) = (INF i\<in>I. emeasure M (F i))"
proof cases
assume "finite I"
have "(\<Inter>i\<in>I. F i) = F (Max I)"
using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F) auto
- moreover have "(INF i:I. emeasure M (F i)) = emeasure M (F (Max I))"
+ moreover have "(INF i\<in>I. emeasure M (F i)) = emeasure M (F (Max I))"
using I \<open>finite I\<close> by (intro antisym INF_lower INF_greatest F emeasure_mono) auto
ultimately show ?thesis
by simp
@@ -611,7 +611,7 @@
show "decseq (\<lambda>i. F (L i))"
using L by (intro antimonoI F L_mono) auto
qed (insert L fin, auto)
- also have "\<dots> = (INF i:I. emeasure M (F i))"
+ also have "\<dots> = (INF i\<in>I. emeasure M (F i))"
proof (intro antisym INF_greatest)
show "i \<in> I \<Longrightarrow> (INF i. emeasure M (F (L i))) \<le> emeasure M (F i)" for i
by (intro INF_lower2[of i]) auto
@@ -990,7 +990,7 @@
subsection \<open>The almost everywhere filter (i.e.\ quantifier)\<close>
definition%important ae_filter :: "'a measure \<Rightarrow> 'a filter" where
- "ae_filter M = (INF N:null_sets M. principal (space M - N))"
+ "ae_filter M = (INF N\<in>null_sets M. principal (space M - N))"
abbreviation almost_everywhere :: "'a measure \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
"almost_everywhere M P \<equiv> eventually P (ae_filter M)"
@@ -2702,7 +2702,7 @@
by (intro bdd_aboveI[where M="measure M (space M)"])
(auto simp: d_def field_simps subset_eq intro!: add_increasing M.finite_measure_mono)
- define \<gamma> where "\<gamma> = (SUP X:sets M. d X)"
+ define \<gamma> where "\<gamma> = (SUP X\<in>sets M. d X)"
have le_\<gamma>[intro]: "X \<in> sets M \<Longrightarrow> d X \<le> \<gamma>" for X
by (auto simp: \<gamma>_def intro!: cSUP_upper)
@@ -2876,7 +2876,7 @@
definition%important sup_measure' :: "'a measure \<Rightarrow> 'a measure \<Rightarrow> 'a measure"
where
- "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+ "sup_measure' A B = measure_of (space A) (sets A) (\<lambda>X. SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
lemma assumes [simp]: "sets B = sets A"
shows space_sup_measure'[simp]: "space (sup_measure' A B) = space A"
@@ -2885,7 +2885,7 @@
lemma emeasure_sup_measure':
assumes sets_eq[simp]: "sets B = sets A" and [simp, intro]: "X \<in> sets A"
- shows "emeasure (sup_measure' A B) X = (SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+ shows "emeasure (sup_measure' A B) X = (SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
(is "_ = ?S X")
proof -
note sets_eq_imp_space_eq[OF sets_eq, simp]
@@ -2893,12 +2893,12 @@
using sup_measure'_def
proof (rule emeasure_measure_of)
let ?d = "\<lambda>X Y. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)"
- show "countably_additive (sets (sup_measure' A B)) (\<lambda>X. SUP Y : sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
+ show "countably_additive (sets (sup_measure' A B)) (\<lambda>X. SUP Y \<in> sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y))"
proof (rule countably_additiveI, goal_cases)
case (1 X)
then have [measurable]: "\<And>i. X i \<in> sets A" and "disjoint_family X"
by auto
- have "(\<Sum>i. ?S (X i)) = (SUP Y:sets A. \<Sum>i. ?d (X i) Y)"
+ have "(\<Sum>i. ?S (X i)) = (SUP Y\<in>sets A. \<Sum>i. ?d (X i) Y)"
proof (rule ennreal_suminf_SUP_eq_directed)
fix J :: "nat set" and a b assume "finite J" and [measurable]: "a \<in> sets A" "b \<in> sets A"
have "\<exists>c\<in>sets A. c \<subseteq> X i \<and> (\<forall>a\<in>sets A. ?d (X i) a \<le> ?d (X i) c)" for i
@@ -2988,7 +2988,7 @@
assumes B: "\<And>Y. Y \<subseteq> X \<Longrightarrow> Y \<in> sets A \<Longrightarrow> emeasure B Y \<le> emeasure C Y"
shows "emeasure (sup_measure' A B) X \<le> emeasure C X"
proof (subst emeasure_sup_measure')
- show "(SUP Y:sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)) \<le> emeasure C X"
+ show "(SUP Y\<in>sets A. emeasure A (X \<inter> Y) + emeasure B (X \<inter> - Y)) \<le> emeasure C X"
unfolding \<open>sets A = sets C\<close>
proof (intro SUP_least)
fix Y assume [measurable]: "Y \<in> sets C"
@@ -3137,10 +3137,10 @@
definition Sup_lexord :: "('a \<Rightarrow> 'b::complete_lattice) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> ('a set \<Rightarrow> 'a) \<Rightarrow> 'a set \<Rightarrow> 'a"
where
- "Sup_lexord k c s A = (let U = (SUP a:A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
+ "Sup_lexord k c s A = (let U = (SUP a\<in>A. k a) in if \<exists>a\<in>A. k a = U then c {a\<in>A. k a = U} else s A)"
lemma Sup_lexord:
- "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a:A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a:A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
+ "(\<And>a S. a \<in> A \<Longrightarrow> k a = (SUP a\<in>A. k a) \<Longrightarrow> S = {a'\<in>A. k a' = k a} \<Longrightarrow> P (c S)) \<Longrightarrow> ((\<And>a. a \<in> A \<Longrightarrow> k a \<noteq> (SUP a\<in>A. k a)) \<Longrightarrow> P (s A)) \<Longrightarrow>
P (Sup_lexord k c s A)"
by (auto simp: Sup_lexord_def Let_def)
@@ -3197,7 +3197,7 @@
definition%important Sup_measure' :: "'a measure set \<Rightarrow> 'a measure"
where
"Sup_measure' M = measure_of (\<Union>a\<in>M. space a) (\<Union>a\<in>M. sets a)
- (\<lambda>X. (SUP P:{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
+ (\<lambda>X. (SUP P\<in>{P. finite P \<and> P \<subseteq> M }. sup_measure.F id P X))"
lemma space_Sup_measure'2: "space (Sup_measure' M) = (\<Union>m\<in>M. space m)"
unfolding Sup_measure'_def by (intro space_measure_of[OF UN_space_closed])
@@ -3218,7 +3218,7 @@
lemma emeasure_Sup_measure':
assumes sets_eq[simp]: "\<And>m. m \<in> M \<Longrightarrow> sets m = sets A" and "X \<in> sets A" "M \<noteq> {}"
- shows "emeasure (Sup_measure' M) X = (SUP P:{P. finite P \<and> P \<subseteq> M}. sup_measure.F id P X)"
+ shows "emeasure (Sup_measure' M) X = (SUP P\<in>{P. finite P \<and> P \<subseteq> M}. sup_measure.F id P X)"
(is "_ = ?S X")
using Sup_measure'_def
proof (rule emeasure_measure_of)
@@ -3245,7 +3245,7 @@
with ij show "\<exists>k\<in>{P. finite P \<and> P \<subseteq> M}. \<forall>n\<in>N. ?\<mu> i (F n) \<le> ?\<mu> k (F n) \<and> ?\<mu> j (F n) \<le> ?\<mu> k (F n)"
by (safe intro!: bexI[of _ "i \<union> j"]) auto
next
- show "(SUP P : {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P : {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
+ show "(SUP P \<in> {P. finite P \<and> P \<subseteq> M}. \<Sum>n. ?\<mu> P (F n)) = (SUP P \<in> {P. finite P \<and> P \<subseteq> M}. ?\<mu> P (UNION UNIV F))"
proof (intro SUP_cong refl)
fix i assume i: "i \<in> {P. finite P \<and> P \<subseteq> M}"
show "(\<Sum>n. ?\<mu> i (F n)) = ?\<mu> i (UNION UNIV F)"
@@ -3337,7 +3337,7 @@
fix X assume "X \<in> sets x"
show "emeasure x X \<le> emeasure (Sup_measure' S') X"
proof (subst emeasure_Sup_measure'[OF _ \<open>X \<in> sets x\<close>])
- show "emeasure x X \<le> (SUP P : {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X)"
+ show "emeasure x X \<le> (SUP P \<in> {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X)"
using \<open>x\<in>S'\<close> by (intro SUP_upper2[where i="{x}"]) auto
qed (insert \<open>x\<in>S'\<close> S', auto)
qed
@@ -3401,7 +3401,7 @@
show "emeasure (Sup_measure' S') X \<le> emeasure x X"
unfolding ***
proof (subst emeasure_Sup_measure'[OF _ \<open>X \<in> sets (Sup_measure' S')\<close>])
- show "(SUP P : {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X) \<le> emeasure x X"
+ show "(SUP P \<in> {P. finite P \<and> P \<subseteq> S'}. emeasure (sup_measure.F id P) X) \<le> emeasure x X"
proof (safe intro!: SUP_least)
fix P assume P: "finite P" "P \<subseteq> S'"
show "emeasure (sup_measure.F id P) X \<le> emeasure x X"
@@ -3455,7 +3455,7 @@
lemma sets_SUP:
assumes "\<And>x. x \<in> I \<Longrightarrow> sets (M x) = sets N"
- shows "I \<noteq> {} \<Longrightarrow> sets (SUP i:I. M i) = sets N"
+ shows "I \<noteq> {} \<Longrightarrow> sets (SUP i\<in>I. M i) = sets N"
unfolding Sup_measure_def
using assms assms[THEN sets_eq_imp_space_eq]
sets_Sup_measure'[where A=N and M="M`I"]
@@ -3463,27 +3463,27 @@
lemma emeasure_SUP:
assumes sets: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N" "I \<noteq> {}"
- shows "emeasure (SUP i:I. M i) X = (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emeasure (SUP i:J. M i) X)"
+ shows "emeasure (SUP i\<in>I. M i) X = (SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. emeasure (SUP i\<in>J. M i) X)"
proof -
interpret sup_measure: comm_monoid_set sup "bot :: 'b measure"
by standard (auto intro!: antisym)
- have eq: "finite J \<Longrightarrow> sup_measure.F id J = (SUP i:J. i)" for J :: "'b measure set"
+ have eq: "finite J \<Longrightarrow> sup_measure.F id J = (SUP i\<in>J. i)" for J :: "'b measure set"
by (induction J rule: finite_induct) auto
- have 1: "J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (SUP x:J. M x) = sets N" for J
+ have 1: "J \<noteq> {} \<Longrightarrow> J \<subseteq> I \<Longrightarrow> sets (SUP x\<in>J. M x) = sets N" for J
by (intro sets_SUP sets) (auto )
from \<open>I \<noteq> {}\<close> obtain i where "i\<in>I" by auto
- have "Sup_measure' (M`I) X = (SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X)"
+ have "Sup_measure' (M`I) X = (SUP P\<in>{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X)"
using sets by (intro emeasure_Sup_measure') auto
- also have "Sup_measure' (M`I) = (SUP i:I. M i)"
+ also have "Sup_measure' (M`I) = (SUP i\<in>I. M i)"
unfolding Sup_measure_def using \<open>I \<noteq> {}\<close> sets sets(1)[THEN sets_eq_imp_space_eq]
by (intro Sup_lexord1[where P="\<lambda>x. _ = x"]) auto
- also have "(SUP P:{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X) =
- (SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. (SUP i:J. M i) X)"
+ also have "(SUP P\<in>{P. finite P \<and> P \<subseteq> M`I}. sup_measure.F id P X) =
+ (SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. (SUP i\<in>J. M i) X)"
proof (intro SUP_eq)
fix J assume "J \<in> {P. finite P \<and> P \<subseteq> M`I}"
then obtain J' where J': "J' \<subseteq> I" "finite J'" and J: "J = M`J'" and "finite J"
using finite_subset_image[of J M I] by auto
- show "\<exists>j\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. sup_measure.F id J X \<le> (SUP i:j. M i) X"
+ show "\<exists>j\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I}. sup_measure.F id J X \<le> (SUP i\<in>j. M i) X"
proof cases
assume "J' = {}" with \<open>i \<in> I\<close> show ?thesis
by (auto simp add: J)
@@ -3493,7 +3493,7 @@
qed
next
fix J assume J: "J \<in> {P. P \<noteq> {} \<and> finite P \<and> P \<subseteq> I}"
- show "\<exists>J'\<in>{J. finite J \<and> J \<subseteq> M`I}. (SUP i:J. M i) X \<le> sup_measure.F id J' X"
+ show "\<exists>J'\<in>{J. finite J \<and> J \<subseteq> M`I}. (SUP i\<in>J. M i) X \<le> sup_measure.F id J' X"
using J by (intro bexI[of _ "M`J"]) (auto simp add: eq simp del: id_apply)
qed
finally show ?thesis .
@@ -3502,14 +3502,14 @@
lemma emeasure_SUP_chain:
assumes sets: "\<And>i. i \<in> A \<Longrightarrow> sets (M i) = sets N" "X \<in> sets N"
assumes ch: "Complete_Partial_Order.chain (\<le>) (M ` A)" and "A \<noteq> {}"
- shows "emeasure (SUP i:A. M i) X = (SUP i:A. emeasure (M i) X)"
+ shows "emeasure (SUP i\<in>A. M i) X = (SUP i\<in>A. emeasure (M i) X)"
proof (subst emeasure_SUP[OF sets \<open>A \<noteq> {}\<close>])
- show "(SUP J:{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i:A. emeasure (M i) X)"
+ show "(SUP J\<in>{J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}. emeasure (SUPREMUM J M) X) = (SUP i\<in>A. emeasure (M i) X)"
proof (rule SUP_eq)
fix J assume "J \<in> {J. J \<noteq> {} \<and> finite J \<and> J \<subseteq> A}"
then have J: "Complete_Partial_Order.chain (\<le>) (M ` J)" "finite J" "J \<noteq> {}" and "J \<subseteq> A"
using ch[THEN chain_subset, of "M`J"] by auto
- with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j:J. M j) = M j"
+ with in_chain_finite[OF J(1)] obtain j where "j \<in> J" "(SUP j\<in>J. M j) = M j"
by auto
with \<open>J \<subseteq> A\<close> show "\<exists>j\<in>A. emeasure (SUPREMUM J M) X \<le> emeasure (M j) X"
by auto
@@ -3554,20 +3554,20 @@
lemma Sup_lexord_rel:
assumes "\<And>i. i \<in> I \<Longrightarrow> k (A i) = k (B i)"
- "R (c (A ` {a \<in> I. k (B a) = (SUP x:I. k (B x))})) (c (B ` {a \<in> I. k (B a) = (SUP x:I. k (B x))}))"
+ "R (c (A ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))})) (c (B ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))}))"
"R (s (A`I)) (s (B`I))"
shows "R (Sup_lexord k c s (A`I)) (Sup_lexord k c s (B`I))"
proof -
- have "A ` {a \<in> I. k (B a) = (SUP x:I. k (B x))} = {a \<in> A ` I. k a = (SUP x:I. k (B x))}"
+ have "A ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} = {a \<in> A ` I. k a = (SUP x\<in>I. k (B x))}"
using assms(1) by auto
- moreover have "B ` {a \<in> I. k (B a) = (SUP x:I. k (B x))} = {a \<in> B ` I. k a = (SUP x:I. k (B x))}"
+ moreover have "B ` {a \<in> I. k (B a) = (SUP x\<in>I. k (B x))} = {a \<in> B ` I. k a = (SUP x\<in>I. k (B x))}"
by auto
ultimately show ?thesis
using assms by (auto simp: Sup_lexord_def Let_def)
qed
lemma sets_SUP_cong:
- assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i:I. M i) = sets (SUP i:I. N i)"
+ assumes eq: "\<And>i. i \<in> I \<Longrightarrow> sets (M i) = sets (N i)" shows "sets (SUP i\<in>I. M i) = sets (SUP i\<in>I. N i)"
unfolding Sup_measure_def
using eq eq[THEN sets_eq_imp_space_eq]
apply (intro Sup_lexord_rel[where R="\<lambda>x y. sets x = sets y"])
@@ -3627,17 +3627,17 @@
lemma measurable_SUP2:
"I \<noteq> {} \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> f \<in> measurable N (M i)) \<Longrightarrow>
- (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i:I. M i)"
+ (\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> space (M i) = space (M j)) \<Longrightarrow> f \<in> measurable N (SUP i\<in>I. M i)"
by (auto intro!: measurable_Sup2)
lemma sets_Sup_sigma:
assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
- shows "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+ shows "sets (SUP m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
proof -
{ fix a m assume "a \<in> sigma_sets \<Omega> m" "m \<in> M"
then have "a \<in> sigma_sets \<Omega> (\<Union>M)"
by induction (auto intro: sigma_sets.intros(2-)) }
- then show "sets (SUP m:M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
+ then show "sets (SUP m\<in>M. sigma \<Omega> m) = sets (sigma \<Omega> (\<Union>M))"
apply (subst sets_Sup_eq[where X="\<Omega>"])
apply (auto simp add: M) []
apply auto []
@@ -3649,14 +3649,14 @@
lemma Sup_sigma:
assumes [simp]: "M \<noteq> {}" and M: "\<And>m. m \<in> M \<Longrightarrow> m \<subseteq> Pow \<Omega>"
- shows "(SUP m:M. sigma \<Omega> m) = (sigma \<Omega> (\<Union>M))"
+ shows "(SUP m\<in>M. sigma \<Omega> m) = (sigma \<Omega> (\<Union>M))"
proof (intro antisym SUP_least)
have *: "\<Union>M \<subseteq> Pow \<Omega>"
using M by auto
- show "sigma \<Omega> (\<Union>M) \<le> (SUP m:M. sigma \<Omega> m)"
+ show "sigma \<Omega> (\<Union>M) \<le> (SUP m\<in>M. sigma \<Omega> m)"
proof (intro less_eq_measure.intros(3))
- show "space (sigma \<Omega> (\<Union>M)) = space (SUP m:M. sigma \<Omega> m)"
- "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m:M. sigma \<Omega> m)"
+ show "space (sigma \<Omega> (\<Union>M)) = space (SUP m\<in>M. sigma \<Omega> m)"
+ "sets (sigma \<Omega> (\<Union>M)) = sets (SUP m\<in>M. sigma \<Omega> m)"
using sets_Sup_sigma[OF assms] sets_Sup_sigma[OF assms, THEN sets_eq_imp_space_eq]
by auto
qed (simp add: emeasure_sigma le_fun_def)
@@ -3665,12 +3665,12 @@
qed
lemma SUP_sigma_sigma:
- "M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m:M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
+ "M \<noteq> {} \<Longrightarrow> (\<And>m. m \<in> M \<Longrightarrow> f m \<subseteq> Pow \<Omega>) \<Longrightarrow> (SUP m\<in>M. sigma \<Omega> (f m)) = sigma \<Omega> (\<Union>m\<in>M. f m)"
using Sup_sigma[of "f`M" \<Omega>] by auto
lemma sets_vimage_Sup_eq:
assumes *: "M \<noteq> {}" "f \<in> X \<rightarrow> Y" "\<And>m. m \<in> M \<Longrightarrow> space m = Y"
- shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m : M. vimage_algebra X f m)"
+ shows "sets (vimage_algebra X f (Sup M)) = sets (SUP m \<in> M. vimage_algebra X f m)"
(is "?IS = ?SI")
proof
show "?IS \<subseteq> ?SI"
@@ -3767,12 +3767,12 @@
using x by (induct rule: sigma_sets.induct) (insert a, auto)
qed
-lemma in_sets_SUP: "i \<in> I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> space (M i) = Y) \<Longrightarrow> X \<in> sets (M i) \<Longrightarrow> X \<in> sets (SUP i:I. M i)"
+lemma in_sets_SUP: "i \<in> I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> space (M i) = Y) \<Longrightarrow> X \<in> sets (M i) \<Longrightarrow> X \<in> sets (SUP i\<in>I. M i)"
by (intro in_sets_Sup[where X=Y]) auto
lemma measurable_SUP1:
"i \<in> I \<Longrightarrow> f \<in> measurable (M i) N \<Longrightarrow> (\<And>m n. m \<in> I \<Longrightarrow> n \<in> I \<Longrightarrow> space (M m) = space (M n)) \<Longrightarrow>
- f \<in> measurable (SUP i:I. M i) N"
+ f \<in> measurable (SUP i\<in>I. M i) N"
by (auto intro: measurable_Sup1)
lemma sets_image_in_sets':
--- a/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy Thu Nov 08 09:11:52 2018 +0100
@@ -811,7 +811,7 @@
subsection \<open>Integral on nonnegative functions\<close>
definition nn_integral :: "'a measure \<Rightarrow> ('a \<Rightarrow> ennreal) \<Rightarrow> ennreal" ("integral\<^sup>N") where
- "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
+ "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f}. integral\<^sup>S M g)"
syntax
"_nn_integral" :: "pttrn \<Rightarrow> ennreal \<Rightarrow> 'a measure \<Rightarrow> ennreal" ("\<integral>\<^sup>+((2 _./ _)/ \<partial>_)" [60,61] 110)
@@ -820,7 +820,7 @@
"\<integral>\<^sup>+x. f \<partial>M" == "CONST nn_integral M (\<lambda>x. f)"
lemma nn_integral_def_finite:
- "integral\<^sup>N M f = (SUP g : {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)"
+ "integral\<^sup>N M f = (SUP g \<in> {g. simple_function M g \<and> g \<le> f \<and> (\<forall>x. g x < top)}. integral\<^sup>S M g)"
(is "_ = SUPREMUM ?A ?f")
unfolding nn_integral_def
proof (safe intro!: antisym SUP_least)
@@ -1342,7 +1342,7 @@
assumes u: "\<And>i. u i \<in> borel_measurable M"
shows "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) \<le> liminf (\<lambda>n. integral\<^sup>N M (u n))"
proof -
- have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
+ have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) = (SUP n. \<integral>\<^sup>+ x. (INF i\<in>{n..}. u i x) \<partial>M)"
unfolding liminf_SUP_INF using u
by (intro nn_integral_monotone_convergence_SUP_AE)
(auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
@@ -1361,7 +1361,7 @@
using bounds by (auto simp: AE_all_countable)
then have "(\<integral>\<^sup>+ x. (SUP n. u n x) \<partial>M) \<le> (\<integral>\<^sup>+ x. w x \<partial>M)"
by (auto intro!: nn_integral_mono_AE elim: eventually_mono intro: SUP_least)
- then have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (INF n. \<integral>\<^sup>+ x. (SUP i:{n..}. u i x) \<partial>M)"
+ then have "(\<integral>\<^sup>+ x. limsup (\<lambda>n. u n x) \<partial>M) = (INF n. \<integral>\<^sup>+ x. (SUP i\<in>{n..}. u i x) \<partial>M)"
unfolding limsup_INF_SUP using bnd w
by (intro nn_integral_monotone_convergence_INF_AE')
(auto intro!: AE_I2 intro: SUP_least SUP_subset_mono)
@@ -1875,24 +1875,24 @@
fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
assumes chain: "Complete_Partial_Order.chain (\<le>) (f ` Y)"
and nonempty: "Y \<noteq> {}"
- shows "(\<integral>\<^sup>+ x. (SUP i:Y. f i x) \<partial>count_space UNIV) = (SUP i:Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
+ shows "(\<integral>\<^sup>+ x. (SUP i\<in>Y. f i x) \<partial>count_space UNIV) = (SUP i\<in>Y. (\<integral>\<^sup>+ x. f i x \<partial>count_space UNIV))"
(is "?lhs = ?rhs" is "integral\<^sup>N ?M _ = _")
proof (rule order_class.order.antisym)
show "?rhs \<le> ?lhs"
by (auto intro!: SUP_least SUP_upper nn_integral_mono)
next
- have "\<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i:Y. f i x) = (SUP i. g i)" for x
+ have "\<exists>g. incseq g \<and> range g \<subseteq> (\<lambda>i. f i x) ` Y \<and> (SUP i\<in>Y. f i x) = (SUP i. g i)" for x
by (rule ennreal_Sup_countable_SUP) (simp add: nonempty)
then obtain g where incseq: "\<And>x. incseq (g x)"
and range: "\<And>x. range (g x) \<subseteq> (\<lambda>i. f i x) ` Y"
- and sup: "\<And>x. (SUP i:Y. f i x) = (SUP i. g x i)" by moura
+ and sup: "\<And>x. (SUP i\<in>Y. f i x) = (SUP i. g x i)" by moura
from incseq have incseq': "incseq (\<lambda>i x. g x i)"
by(blast intro: incseq_SucI le_funI dest: incseq_SucD)
have "?lhs = \<integral>\<^sup>+ x. (SUP i. g x i) \<partial>?M" by(simp add: sup)
also have "\<dots> = (SUP i. \<integral>\<^sup>+ x. g x i \<partial>?M)" using incseq'
by(rule nn_integral_monotone_convergence_SUP) simp
- also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+ also have "\<dots> \<le> (SUP i\<in>Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
proof(rule SUP_least)
fix n
have "\<And>x. \<exists>i. g x n = f i x \<and> i \<in> Y" using range by blast
@@ -1902,7 +1902,7 @@
by(rule nn_integral_count_space_nat)
also have "\<dots> = (SUP m. \<Sum>x<m. g x n)"
by(rule suminf_eq_SUP)
- also have "\<dots> \<le> (SUP i:Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
+ also have "\<dots> \<le> (SUP i\<in>Y. \<integral>\<^sup>+ x. f i x \<partial>?M)"
proof(rule SUP_mono)
fix m
show "\<exists>m'\<in>Y. (\<Sum>x<m. g x n) \<le> (\<integral>\<^sup>+ x. f m' x \<partial>?M)"
@@ -1916,7 +1916,7 @@
with chain have chain': "Complete_Partial_Order.chain (\<le>) (f ` ?Y)" by(rule chain_subset)
hence "Sup (f ` ?Y) \<in> f ` ?Y"
by(rule ccpo_class.in_chain_finite)(auto simp add: True lessThan_empty_iff)
- then obtain m' where "m' < m" and m': "(SUP i:?Y. f i) = f (I m')" by auto
+ then obtain m' where "m' < m" and m': "(SUP i\<in>?Y. f i) = f (I m')" by auto
have "I m' \<in> Y" using I by blast
have "(\<Sum>x<m. g x n) \<le> (\<Sum>x<m. f (I m') x)"
proof(rule sum_mono)
@@ -1924,7 +1924,7 @@
assume "x \<in> {..<m}"
hence "x < m" by simp
have "g x n = f (I x) x" by(simp add: I)
- also have "\<dots> \<le> (SUP i:?Y. f i) x" unfolding Sup_fun_def image_image
+ also have "\<dots> \<le> (SUP i\<in>?Y. f i) x" unfolding Sup_fun_def image_image
using \<open>x \<in> {..<m}\<close> by (rule Sup_upper [OF imageI])
also have "\<dots> = f (I m') x" unfolding m' by simp
finally show "g x n \<le> f (I m') x" .
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -11,8 +11,8 @@
assumes eucl_less_le_not_le: "x < y \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x"
assumes eucl_inf: "inf x y = (\<Sum>i\<in>Basis. inf (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
assumes eucl_sup: "sup x y = (\<Sum>i\<in>Basis. sup (x \<bullet> i) (y \<bullet> i) *\<^sub>R i)"
- assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x:X. x \<bullet> i) *\<^sub>R i)"
- assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x:X. x \<bullet> i) *\<^sub>R i)"
+ assumes eucl_Inf: "Inf X = (\<Sum>i\<in>Basis. (INF x\<in>X. x \<bullet> i) *\<^sub>R i)"
+ assumes eucl_Sup: "Sup X = (\<Sum>i\<in>Basis. (SUP x\<in>X. x \<bullet> i) *\<^sub>R i)"
assumes eucl_abs: "\<bar>x\<bar> = (\<Sum>i\<in>Basis. \<bar>x \<bullet> i\<bar> *\<^sub>R i)"
begin
@@ -49,8 +49,8 @@
by (simp_all add: eucl_inf eucl_sup inner_sum_left inner_Basis if_distrib comm_monoid_add_class.sum.delta
cong: if_cong)
-lemma%unimportant inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x:X. f x) \<bullet> i = (INF x:X. f x \<bullet> i)"
- and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x:X. f x) \<bullet> i = (SUP x:X. f x \<bullet> i)"
+lemma%unimportant inner_Basis_INF_left: "i \<in> Basis \<Longrightarrow> (INF x\<in>X. f x) \<bullet> i = (INF x\<in>X. f x \<bullet> i)"
+ and inner_Basis_SUP_left: "i \<in> Basis \<Longrightarrow> (SUP x\<in>X. f x) \<bullet> i = (SUP x\<in>X. f x \<bullet> i)"
using eucl_Sup [of "f ` X"] eucl_Inf [of "f ` X"] by (simp_all add: comp_def)
lemma%unimportant abs_inner: "i \<in> Basis \<Longrightarrow> \<bar>x\<bar> \<bullet> i = \<bar>x \<bullet> i\<bar>"
@@ -284,8 +284,8 @@
definition%important "inf x y = (\<chi> i. inf (x $ i) (y $ i))"
definition%important "sup x y = (\<chi> i. sup (x $ i) (y $ i))"
-definition%important "Inf X = (\<chi> i. (INF x:X. x $ i))"
-definition%important "Sup X = (\<chi> i. (SUP x:X. x $ i))"
+definition%important "Inf X = (\<chi> i. (INF x\<in>X. x $ i))"
+definition%important "Sup X = (\<chi> i. (SUP x\<in>X. x $ i))"
definition%important "\<bar>x\<bar> = (\<chi> i. \<bar>x $ i\<bar>)"
instance
--- a/src/HOL/Analysis/Polytope.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Polytope.thy Thu Nov 08 09:11:52 2018 +0100
@@ -2080,7 +2080,7 @@
case False
then obtain h' where h': "h' \<in> F - {h}" by auto
define inff where "inff =
- (INF j:F - {h}.
+ (INF j\<in>F - {h}.
if 0 < a j \<bullet> y - a j \<bullet> w
then (b j - a j \<bullet> w) / (a j \<bullet> y - a j \<bullet> w)
else 1)"
--- a/src/HOL/Analysis/Product_Vector.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy Thu Nov 08 09:11:52 2018 +0100
@@ -127,7 +127,7 @@
definition [code del]:
"(uniformity :: (('a \<times> 'b) \<times> ('a \<times> 'b)) filter) =
- (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
instance
by standard (rule uniformity_prod_def)
--- a/src/HOL/Analysis/Radon_Nikodym.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Radon_Nikodym.thy Thu Nov 08 09:11:52 2018 +0100
@@ -254,7 +254,7 @@
using f \<open>A \<in> sets M\<close> by (auto intro!: SUP_least simp: G_D)
qed }
note SUP_in_G = this
- let ?y = "SUP g : G. integral\<^sup>N M g"
+ let ?y = "SUP g \<in> G. integral\<^sup>N M g"
have y_le: "?y \<le> N (space M)" unfolding G_def
proof (safe intro!: SUP_least)
fix g assume "\<forall>A\<in>sets M. (\<integral>\<^sup>+x. g x * indicator A x \<partial>M) \<le> N A"
@@ -390,7 +390,7 @@
(\<forall>A\<in>sets M. A \<inter> (\<Union>i. B i) = {} \<longrightarrow> (emeasure M A = 0 \<and> N A = 0) \<or> (emeasure M A > 0 \<and> N A = \<infinity>))"
proof%unimportant -
let ?Q = "{Q\<in>sets M. N Q \<noteq> \<infinity>}"
- let ?a = "SUP Q:?Q. emeasure M Q"
+ let ?a = "SUP Q\<in>?Q. emeasure M Q"
have "{} \<in> ?Q" by auto
then have Q_not_empty: "?Q \<noteq> {}" by blast
have "?a \<le> emeasure M (space M)" using sets.sets_into_space
@@ -404,7 +404,7 @@
then have "\<forall>i. \<exists>Q'. Q'' i = emeasure M Q' \<and> Q' \<in> ?Q" by auto
from choice[OF this] obtain Q' where Q': "\<And>i. Q'' i = emeasure M (Q' i)" "\<And>i. Q' i \<in> ?Q"
by auto
- then have a_Lim: "?a = (SUP i::nat. emeasure M (Q' i))" using a by simp
+ then have a_Lim: "?a = (SUP i. emeasure M (Q' i))" using a by simp
let ?O = "\<lambda>n. \<Union>i\<le>n. Q' i"
have Union: "(SUP i. emeasure M (?O i)) = emeasure M (\<Union>i. ?O i)"
proof (rule SUP_emeasure_incseq[of ?O])
--- a/src/HOL/Analysis/Regularity.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Regularity.thy Thu Nov 08 09:11:52 2018 +0100
@@ -14,9 +14,9 @@
assumes "emeasure M (space M) \<noteq> \<infinity>"
assumes "B \<in> sets borel"
shows inner_regular: "emeasure M B =
- (SUP K : {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
+ (SUP K \<in> {K. K \<subseteq> B \<and> compact K}. emeasure M K)" (is "?inner B")
and outer_regular: "emeasure M B =
- (INF U : {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
+ (INF U \<in> {U. B \<subseteq> U \<and> open U}. emeasure M U)" (is "?outer B")
proof%unimportant -
have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel)
hence sU: "space M = UNIV" by simp
@@ -183,7 +183,7 @@
finally
have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" .
moreover
- have "\<dots> \<ge> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+ have "\<dots> \<ge> (INF U\<in>{U. A \<subseteq> U \<and> open U}. emeasure M U)"
proof (intro INF_mono)
fix m
have "?G (1 / real (Suc m)) \<in> {U. A \<subseteq> U \<and> open U}" using open_G by auto
@@ -193,7 +193,7 @@
by blast
qed
moreover
- have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
+ have "emeasure M A \<le> (INF U\<in>{U. A \<subseteq> U \<and> open U}. emeasure M U)"
by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
ultimately show ?thesis by simp
qed (auto intro!: INF_eqI)
@@ -217,38 +217,38 @@
from compl have [simp]: "B \<in> sets M" by (auto simp: sb borel_eq_closed)
case 2
have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
- also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)"
+ also have "\<dots> = (INF K\<in>{K. K \<subseteq> B \<and> compact K}. M (space M) - M K)"
by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner)
- also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
+ also have "\<dots> = (INF U\<in>{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
- also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
+ also have "\<dots> \<ge> (INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
by (rule INF_superset_mono) (auto simp add: compact_imp_closed)
- also have "(INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
- (INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
+ also have "(INF U\<in>{U. U \<subseteq> B \<and> closed U}. M (space M - U)) =
+ (INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U)"
unfolding INF_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
by (rule INF_cong) (auto simp add: sU Compl_eq_Diff_UNIV [symmetric, simp])
finally have
- "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
+ "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<le> emeasure M (space M - B)" .
moreover have
- "(INF U:{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
+ "(INF U\<in>{U. space M - B \<subseteq> U \<and> open U}. emeasure M U) \<ge> emeasure M (space M - B)"
by (auto simp: sb sU intro!: INF_greatest emeasure_mono)
ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb])
case 1
have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
- also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) - M U)"
+ also have "\<dots> = (SUP U\<in> {U. B \<subseteq> U \<and> open U}. M (space M) - M U)"
unfolding outer by (subst ennreal_INF_const_minus) auto
- also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
+ also have "\<dots> = (SUP U\<in>{U. B \<subseteq> U \<and> open U}. M (space M - U))"
by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
- also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
+ also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"
unfolding SUP_image [of _ "\<lambda>u. space M - u" _, symmetric, unfolded comp_def]
by (rule SUP_cong) (auto simp add: sU)
- also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+ also have "\<dots> = (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
proof (safe intro!: antisym SUP_least)
fix K assume "closed K" "K \<subseteq> space M - B"
from closed_in_D[OF \<open>closed K\<close>]
- have K_inner: "emeasure M K = (SUP K:{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
- show "emeasure M K \<le> (SUP K:{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
+ have K_inner: "emeasure M K = (SUP K\<in>{Ka. Ka \<subseteq> K \<and> compact Ka}. emeasure M K)" by simp
+ show "emeasure M K \<le> (SUP K\<in>{K. K \<subseteq> space M - B \<and> compact K}. emeasure M K)"
unfolding K_inner using \<open>K \<subseteq> space M - B\<close>
by (auto intro!: SUP_upper SUP_least)
qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed)
@@ -284,7 +284,7 @@
proof
fix i
from \<open>0 < e\<close> have "0 < e/(2*Suc n0)" by simp
- have "emeasure M (D i) = (SUP K:{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
+ have "emeasure M (D i) = (SUP K\<in>{K. K \<subseteq> (D i) \<and> compact K}. emeasure M K)"
using union by blast
from SUP_approx_ennreal[OF \<open>0 < e/(2*Suc n0)\<close> _ this]
show "\<exists>K. K \<subseteq> D i \<and> compact K \<and> emeasure M (D i) \<le> emeasure M K + e/(2*Suc n0)"
@@ -327,7 +327,7 @@
proof
fix i::nat
from \<open>0 < e\<close> have "0 < e/(2 powr Suc i)" by simp
- have "emeasure M (D i) = (INF U:{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
+ have "emeasure M (D i) = (INF U\<in>{U. (D i) \<subseteq> U \<and> open U}. emeasure M U)"
using union by blast
from INF_approx_ennreal[OF \<open>0 < e/(2 powr Suc i)\<close> this]
show "\<exists>U. D i \<subseteq> U \<and> open U \<and> e/(2 powr Suc i) > emeasure M U - emeasure M (D i)"
--- a/src/HOL/Analysis/Riemann_Mapping.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy Thu Nov 08 09:11:52 2018 +0100
@@ -168,7 +168,7 @@
by (simp add: deq norm_mult divide_simps o_def)
qed
qed
- define l where "l \<equiv> SUP h:F. norm (deriv h 0)"
+ define l where "l \<equiv> SUP h\<in>F. norm (deriv h 0)"
have eql: "norm (deriv f 0) = l" if le: "l \<le> norm (deriv f 0)" and "f \<in> F" for f
apply (rule order_antisym [OF _ le])
using \<open>f \<in> F\<close> bdd cSUP_upper by (fastforce simp: l_def)
--- a/src/HOL/Analysis/Tagged_Division.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Tagged_Division.thy Thu Nov 08 09:11:52 2018 +0100
@@ -133,10 +133,10 @@
subsection%important \<open>Bounds on intervals where they exist\<close>
definition%important interval_upperbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
- where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x:s. x\<bullet>i) *\<^sub>R i)"
+ where "interval_upperbound s = (\<Sum>i\<in>Basis. (SUP x\<in>s. x\<bullet>i) *\<^sub>R i)"
definition%important interval_lowerbound :: "('a::euclidean_space) set \<Rightarrow> 'a"
- where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x:s. x\<bullet>i) *\<^sub>R i)"
+ where "interval_lowerbound s = (\<Sum>i\<in>Basis. (INF x\<in>s. x\<bullet>i) *\<^sub>R i)"
lemma interval_upperbound[simp]:
"\<forall>i\<in>Basis. a\<bullet>i \<le> b\<bullet>i \<Longrightarrow>
@@ -169,10 +169,10 @@
shows "interval_upperbound (A \<times> B) = (interval_upperbound A, interval_upperbound B)"
proof%unimportant-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:A. x \<bullet> i) *\<^sub>R i)"
+ have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>A. x \<bullet> i) *\<^sub>R i)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (SUP x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x:B. x \<bullet> i) *\<^sub>R i)"
+ have "(\<Sum>i\<in>Basis. (SUP x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (SUP x\<in>B. x \<bullet> i) *\<^sub>R i)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
ultimately show ?thesis unfolding interval_upperbound_def
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
@@ -183,10 +183,10 @@
shows "interval_lowerbound (A \<times> B) = (interval_lowerbound A, interval_lowerbound B)"
proof%unimportant-
from assms have fst_image_times': "A = fst ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:A. x \<bullet> i) *\<^sub>R i)"
+ have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (i, 0)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>A. x \<bullet> i) *\<^sub>R i)"
by (subst (2) fst_image_times') (simp del: fst_image_times add: o_def inner_Pair_0)
moreover from assms have snd_image_times': "B = snd ` (A \<times> B)" by simp
- have "(\<Sum>i\<in>Basis. (INF x:A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x:B. x \<bullet> i) *\<^sub>R i)"
+ have "(\<Sum>i\<in>Basis. (INF x\<in>A \<times> B. x \<bullet> (0, i)) *\<^sub>R i) = (\<Sum>i\<in>Basis. (INF x\<in>B. x \<bullet> i) *\<^sub>R i)"
by (subst (2) snd_image_times') (simp del: snd_image_times add: o_def inner_Pair_0)
ultimately show ?thesis unfolding interval_lowerbound_def
by (subst sum_Basis_prod_eq) (auto simp add: sum_prod)
@@ -2576,7 +2576,7 @@
text \<open>Divisions over all gauges towards finer divisions.\<close>
definition%important division_filter :: "'a::euclidean_space set \<Rightarrow> ('a \<times> 'a set) set filter"
- where "division_filter s = (INF g:{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
+ where "division_filter s = (INF g\<in>{g. gauge g}. principal {p. p tagged_division_of s \<and> g fine p})"
lemma%important eventually_division_filter:
"(\<forall>\<^sub>F p in division_filter s. P p) \<longleftrightarrow>
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -4189,7 +4189,7 @@
next
fix A
assume A: "\<forall>a\<in>A. closed a" "\<forall>B\<subseteq>A. finite B \<longrightarrow> U \<inter> \<Inter>B \<noteq> {}" "U \<inter> \<Inter>A = {}"
- define F where "F = (INF a:insert U A. principal a)"
+ define F where "F = (INF a\<in>insert U A. principal a)"
have "F \<noteq> bot"
unfolding F_def
proof (rule INF_filter_not_bot)
@@ -4197,7 +4197,7 @@
assume X: "X \<subseteq> insert U A" "finite X"
with A(2)[THEN spec, of "X - {U}"] have "U \<inter> \<Inter>(X - {U}) \<noteq> {}"
by auto
- with X show "(INF a:X. principal a) \<noteq> bot"
+ with X show "(INF a\<in>X. principal a) \<noteq> bot"
by (auto simp: INF_principal_finite principal_eq_bot_iff)
qed
moreover
--- a/src/HOL/Analysis/Uniform_Limit.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy Thu Nov 08 09:11:52 2018 +0100
@@ -13,7 +13,7 @@
subsection \<open>Definition\<close>
definition%important uniformly_on :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b::metric_space) \<Rightarrow> ('a \<Rightarrow> 'b) filter"
- where "uniformly_on S l = (INF e:{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
+ where "uniformly_on S l = (INF e\<in>{0 <..}. principal {f. \<forall>x\<in>S. dist (f x) (l x) < e})"
abbreviation%important
"uniform_limit S f l \<equiv> filterlim f (uniformly_on S l)"
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy Thu Nov 08 09:11:52 2018 +0100
@@ -202,7 +202,7 @@
by (induct I rule: finite_induct; simp add: const mult)
definition%important normf :: "('a::t2_space \<Rightarrow> real) \<Rightarrow> real"
- where "normf f \<equiv> SUP x:S. \<bar>f x\<bar>"
+ where "normf f \<equiv> SUP x\<in>S. \<bar>f x\<bar>"
lemma%unimportant normf_upper: "\<lbrakk>continuous_on S f; x \<in> S\<rbrakk> \<Longrightarrow> \<bar>f x\<bar> \<le> normf f"
apply (simp add: normf_def)
--- a/src/HOL/Complete_Lattices.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Complete_Lattices.thy Thu Nov 08 09:11:52 2018 +0100
@@ -32,12 +32,6 @@
end
-syntax (input)
- "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
- "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
- "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10)
- "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
-
syntax
"_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
"_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _\<in>_./ _)" [0, 0, 10] 10)
@@ -50,6 +44,12 @@
"_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_./ _)" [0, 10] 10)
"_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
+syntax (input) \<comment> \<open>legacy input syntax\<close>
+ "_INF1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _./ _)" [0, 10] 10)
+ "_INF" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3INF _:_./ _)" [0, 0, 10] 10)
+ "_SUP1" :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _./ _)" [0, 10] 10)
+ "_SUP" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b" ("(3SUP _:_./ _)" [0, 0, 10] 10)
+
translations
"\<Sqinter>x y. f" \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. f"
"\<Sqinter>x. f" \<rightleftharpoons> "\<Sqinter>CONST range (\<lambda>x. f)"
@@ -236,7 +236,7 @@
lemma INF_mono: "(\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (\<Sqinter>n\<in>A. f n) \<le> (\<Sqinter>n\<in>B. g n)"
using Inf_mono [of "g ` B" "f ` A"] by auto
-lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:A. g x)"
+lemma INF_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>A. g x)"
by (rule INF_mono) auto
lemma Sup_mono:
@@ -252,7 +252,7 @@
lemma SUP_mono: "(\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (\<Squnion>n\<in>A. f n) \<le> (\<Squnion>n\<in>B. g n)"
using Sup_mono [of "f ` A" "g ` B"] by auto
-lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:A. g x)"
+lemma SUP_mono': "(\<And>x. f x \<le> g x) \<Longrightarrow> (\<Squnion>x\<in>A. f x) \<le> (\<Squnion>x\<in>A. g x)"
by (rule SUP_mono) auto
lemma INF_superset_mono: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (\<Sqinter>x\<in>A. f x) \<le> (\<Sqinter>x\<in>B. g x)"
--- a/src/HOL/Complex.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Complex.thy Thu Nov 08 09:11:52 2018 +0100
@@ -308,7 +308,7 @@
definition dist_complex_def: "dist x y = cmod (x - y)"
definition uniformity_complex_def [code del]:
- "(uniformity :: (complex \<times> complex) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ "(uniformity :: (complex \<times> complex) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition open_complex_def [code del]:
"open (U :: complex set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
--- a/src/HOL/Computational_Algebra/Formal_Power_Series.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Computational_Algebra/Formal_Power_Series.thy Thu Nov 08 09:11:52 2018 +0100
@@ -821,7 +821,7 @@
begin
definition uniformity_fps_def [code del]:
- "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ "(uniformity :: ('a fps \<times> 'a fps) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition open_fps_def' [code del]:
"open (U :: 'a fps set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
@@ -1470,40 +1470,40 @@
lemma fps_Gcd:
assumes "A - {0} \<noteq> {}"
- shows "Gcd A = fps_X ^ (INF f:A-{0}. subdegree f)"
+ shows "Gcd A = fps_X ^ (INF f\<in>A-{0}. subdegree f)"
proof (rule sym, rule GcdI)
fix f assume "f \<in> A"
- thus "fps_X ^ (INF f:A - {0}. subdegree f) dvd f"
+ thus "fps_X ^ (INF f\<in>A - {0}. subdegree f) dvd f"
by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cINF_lower)
next
fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> d dvd f"
from assms obtain f where "f \<in> A - {0}" by auto
with d[of f] have [simp]: "d \<noteq> 0" by auto
- from d assms have "subdegree d \<le> (INF f:A-{0}. subdegree f)"
+ from d assms have "subdegree d \<le> (INF f\<in>A-{0}. subdegree f)"
by (intro cINF_greatest) (auto simp: fps_dvd_iff[symmetric])
- with d assms show "d dvd fps_X ^ (INF f:A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
+ with d assms show "d dvd fps_X ^ (INF f\<in>A-{0}. subdegree f)" by (simp add: fps_dvd_iff)
qed simp_all
lemma fps_Gcd_altdef: "Gcd (A :: 'a :: field fps set) =
- (if A \<subseteq> {0} then 0 else fps_X ^ (INF f:A-{0}. subdegree f))"
+ (if A \<subseteq> {0} then 0 else fps_X ^ (INF f\<in>A-{0}. subdegree f))"
using fps_Gcd by auto
lemma fps_Lcm:
assumes "A \<noteq> {}" "0 \<notin> A" "bdd_above (subdegree`A)"
- shows "Lcm A = fps_X ^ (SUP f:A. subdegree f)"
+ shows "Lcm A = fps_X ^ (SUP f\<in>A. subdegree f)"
proof (rule sym, rule LcmI)
fix f assume "f \<in> A"
moreover from assms(3) have "bdd_above (subdegree ` A)" by auto
- ultimately show "f dvd fps_X ^ (SUP f:A. subdegree f)" using assms(2)
+ ultimately show "f dvd fps_X ^ (SUP f\<in>A. subdegree f)" using assms(2)
by (cases "f = 0") (auto simp: fps_dvd_iff intro!: cSUP_upper)
next
fix d assume d: "\<And>f. f \<in> A \<Longrightarrow> f dvd d"
from assms obtain f where f: "f \<in> A" "f \<noteq> 0" by auto
- show "fps_X ^ (SUP f:A. subdegree f) dvd d"
+ show "fps_X ^ (SUP f\<in>A. subdegree f) dvd d"
proof (cases "d = 0")
assume "d \<noteq> 0"
moreover from d have "\<And>f. f \<in> A \<Longrightarrow> f \<noteq> 0 \<Longrightarrow> f dvd d" by blast
- ultimately have "subdegree d \<ge> (SUP f:A. subdegree f)" using assms
+ ultimately have "subdegree d \<ge> (SUP f\<in>A. subdegree f)" using assms
by (intro cSUP_least) (auto simp: fps_dvd_iff)
with \<open>d \<noteq> 0\<close> show ?thesis by (simp add: fps_dvd_iff)
qed simp_all
@@ -1512,7 +1512,7 @@
lemma fps_Lcm_altdef:
"Lcm (A :: 'a :: field fps set) =
(if 0 \<in> A \<or> \<not>bdd_above (subdegree`A) then 0 else
- if A = {} then 1 else fps_X ^ (SUP f:A. subdegree f))"
+ if A = {} then 1 else fps_X ^ (SUP f\<in>A. subdegree f))"
proof (cases "bdd_above (subdegree`A)")
assume unbounded: "\<not>bdd_above (subdegree`A)"
have "Lcm A = 0"
--- a/src/HOL/Filter.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Filter.thy Thu Nov 08 09:11:52 2018 +0100
@@ -524,14 +524,14 @@
lemma eventually_INF_finite:
assumes "finite A"
- shows "eventually P (INF x:A. F x) \<longleftrightarrow>
+ shows "eventually P (\<Sqinter> x\<in>A. F x) \<longleftrightarrow>
(\<exists>Q. (\<forall>x\<in>A. eventually (Q x) (F x)) \<and> (\<forall>y. (\<forall>x\<in>A. Q x y) \<longrightarrow> P y))"
using assms
proof (induction arbitrary: P rule: finite_induct)
case (insert a A P)
from insert.hyps have [simp]: "x \<noteq> a" if "x \<in> A" for x
using that by auto
- have "eventually P (INF x:insert a A. F x) \<longleftrightarrow>
+ have "eventually P (\<Sqinter> x\<in>insert a A. F x) \<longleftrightarrow>
(\<exists>Q R S. eventually Q (F a) \<and> (( (\<forall>x\<in>A. eventually (S x) (F x)) \<and>
(\<forall>y. (\<forall>x\<in>A. S x y) \<longrightarrow> R y)) \<and> (\<forall>x. Q x \<and> R x \<longrightarrow> P x)))"
unfolding ex_simps by (simp add: eventually_inf insert.IH)
@@ -915,7 +915,7 @@
subsection \<open>Increasing finite subsets\<close>
definition finite_subsets_at_top where
- "finite_subsets_at_top A = (INF X:{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
+ "finite_subsets_at_top A = (\<Sqinter> X\<in>{X. finite X \<and> X \<subseteq> A}. principal {Y. finite Y \<and> X \<subseteq> Y \<and> Y \<subseteq> A})"
lemma eventually_finite_subsets_at_top:
"eventually P (finite_subsets_at_top A) \<longleftrightarrow>
@@ -1345,7 +1345,7 @@
"(\<And>m. m \<in> J \<Longrightarrow> \<exists>i\<in>I. filtermap f (F i) \<le> G m) \<Longrightarrow> LIM x (\<Sqinter>i\<in>I. F i). f x :> (\<Sqinter>j\<in>J. G j)"
unfolding filterlim_def by (rule order_trans[OF filtermap_INF INF_mono])
-lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (INF x:A. G x)"
+lemma filterlim_INF': "x \<in> A \<Longrightarrow> filterlim f F (G x) \<Longrightarrow> filterlim f F (\<Sqinter> x\<in>A. G x)"
unfolding filterlim_def by (rule order.trans[OF filtermap_mono[OF INF_lower]])
lemma filterlim_filtercomap_iff: "filterlim f (filtercomap g G) F \<longleftrightarrow> filterlim (g \<circ> f) G F"
@@ -1859,7 +1859,7 @@
if "(F, G) \<in> SS'" for P Q F G by simp_all
show "rel_filter A (Sup S) (Sup S')"
proof
- let ?Z = "SUP (F, G):SS'. Z F G"
+ let ?Z = "\<Squnion>(F, G)\<in>SS'. Z F G"
show *: "\<forall>\<^sub>F (x, y) in ?Z. A x y" using Z by(auto simp add: eventually_Sup)
show "map_filter_on {(x, y). A x y} fst ?Z = Sup S" "map_filter_on {(x, y). A x y} snd ?Z = Sup S'"
unfolding filter_eq_iff
--- a/src/HOL/IMP/Collecting.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/IMP/Collecting.thy Thu Nov 08 09:11:52 2018 +0100
@@ -94,7 +94,7 @@
dest: size_annos_same)
definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
-"Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
+"Inf_acom c M = annotate (\<lambda>p. INF C\<in>M. anno C p) c"
global_interpretation
Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
--- a/src/HOL/Library/Countable_Complete_Lattices.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Countable_Complete_Lattices.thy Thu Nov 08 09:11:52 2018 +0100
@@ -27,58 +27,58 @@
show "a \<le> top" by (auto intro: ccInf_greatest simp only: ccInf_empty [symmetric])
qed
-lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i :A. f i) \<le> f i"
+lemma ccINF_lower: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> (INF i \<in> A. f i) \<le> f i"
using ccInf_lower [of "f ` A"] by simp
-lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i :A. f i)"
+lemma ccINF_greatest: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> u \<le> f i) \<Longrightarrow> u \<le> (INF i \<in> A. f i)"
using ccInf_greatest [of "f ` A"] by auto
-lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i :A. f i)"
+lemma ccSUP_upper: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> (SUP i \<in> A. f i)"
using ccSup_upper [of "f ` A"] by simp
-lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i :A. f i) \<le> u"
+lemma ccSUP_least: "countable A \<Longrightarrow> (\<And>i. i \<in> A \<Longrightarrow> f i \<le> u) \<Longrightarrow> (SUP i \<in> A. f i) \<le> u"
using ccSup_least [of "f ` A"] by auto
lemma ccInf_lower2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> u \<le> v \<Longrightarrow> Inf A \<le> v"
using ccInf_lower [of A u] by auto
-lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i :A. f i) \<le> u"
+lemma ccINF_lower2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> f i \<le> u \<Longrightarrow> (INF i \<in> A. f i) \<le> u"
using ccINF_lower [of A i f] by auto
lemma ccSup_upper2: "countable A \<Longrightarrow> u \<in> A \<Longrightarrow> v \<le> u \<Longrightarrow> v \<le> Sup A"
using ccSup_upper [of A u] by auto
-lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i :A. f i)"
+lemma ccSUP_upper2: "countable A \<Longrightarrow> i \<in> A \<Longrightarrow> u \<le> f i \<Longrightarrow> u \<le> (SUP i \<in> A. f i)"
using ccSUP_upper [of A i f] by auto
lemma le_ccInf_iff: "countable A \<Longrightarrow> b \<le> Inf A \<longleftrightarrow> (\<forall>a\<in>A. b \<le> a)"
by (auto intro: ccInf_greatest dest: ccInf_lower)
-lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i :A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
+lemma le_ccINF_iff: "countable A \<Longrightarrow> u \<le> (INF i \<in> A. f i) \<longleftrightarrow> (\<forall>i\<in>A. u \<le> f i)"
using le_ccInf_iff [of "f ` A"] by simp
lemma ccSup_le_iff: "countable A \<Longrightarrow> Sup A \<le> b \<longleftrightarrow> (\<forall>a\<in>A. a \<le> b)"
by (auto intro: ccSup_least dest: ccSup_upper)
-lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i :A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
+lemma ccSUP_le_iff: "countable A \<Longrightarrow> (SUP i \<in> A. f i) \<le> u \<longleftrightarrow> (\<forall>i\<in>A. f i \<le> u)"
using ccSup_le_iff [of "f ` A"] by simp
lemma ccInf_insert [simp]: "countable A \<Longrightarrow> Inf (insert a A) = inf a (Inf A)"
by (force intro: le_infI le_infI1 le_infI2 antisym ccInf_greatest ccInf_lower)
-lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x:insert a A. f x) = inf (f a) (INFIMUM A f)"
+lemma ccINF_insert [simp]: "countable A \<Longrightarrow> (INF x\<in>insert a A. f x) = inf (f a) (INFIMUM A f)"
unfolding image_insert by simp
lemma ccSup_insert [simp]: "countable A \<Longrightarrow> Sup (insert a A) = sup a (Sup A)"
by (force intro: le_supI le_supI1 le_supI2 antisym ccSup_least ccSup_upper)
-lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x:insert a A. f x) = sup (f a) (SUPREMUM A f)"
+lemma ccSUP_insert [simp]: "countable A \<Longrightarrow> (SUP x\<in>insert a A. f x) = sup (f a) (SUPREMUM A f)"
unfolding image_insert by simp
-lemma ccINF_empty [simp]: "(INF x:{}. f x) = top"
+lemma ccINF_empty [simp]: "(INF x\<in>{}. f x) = top"
unfolding image_empty by simp
-lemma ccSUP_empty [simp]: "(SUP x:{}. f x) = bot"
+lemma ccSUP_empty [simp]: "(SUP x\<in>{}. f x) = bot"
unfolding image_empty by simp
lemma ccInf_superset_mono: "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> Inf A \<le> Inf B"
@@ -99,7 +99,7 @@
qed auto
lemma ccINF_mono:
- "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n:A. f n) \<le> (INF n:B. g n)"
+ "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>m. m \<in> B \<Longrightarrow> \<exists>n\<in>A. f n \<le> g m) \<Longrightarrow> (INF n\<in>A. f n) \<le> (INF n\<in>B. g n)"
using ccInf_mono [of "g ` B" "f ` A"] by auto
lemma ccSup_mono:
@@ -114,15 +114,15 @@
qed auto
lemma ccSUP_mono:
- "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n:A. f n) \<le> (SUP n:B. g n)"
+ "countable A \<Longrightarrow> countable B \<Longrightarrow> (\<And>n. n \<in> A \<Longrightarrow> \<exists>m\<in>B. f n \<le> g m) \<Longrightarrow> (SUP n\<in>A. f n) \<le> (SUP n\<in>B. g n)"
using ccSup_mono [of "g ` B" "f ` A"] by auto
lemma ccINF_superset_mono:
- "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x:A. f x) \<le> (INF x:B. g x)"
+ "countable A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (INF x\<in>A. f x) \<le> (INF x\<in>B. g x)"
by (blast intro: ccINF_mono countable_subset dest: subsetD)
lemma ccSUP_subset_mono:
- "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x:A. f x) \<le> (SUP x:B. g x)"
+ "countable B \<Longrightarrow> A \<subseteq> B \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<le> g x) \<Longrightarrow> (SUP x\<in>A. f x) \<le> (SUP x\<in>B. g x)"
by (blast intro: ccSUP_mono countable_subset dest: subsetD)
@@ -136,38 +136,38 @@
by (rule antisym) (auto intro: ccInf_greatest ccInf_lower le_infI1 le_infI2)
lemma ccINF_union:
- "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A \<union> B. M i) = inf (INF i:A. M i) (INF i:B. M i)"
+ "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A \<union> B. M i) = inf (INF i\<in>A. M i) (INF i\<in>B. M i)"
by (auto intro!: antisym ccINF_mono intro: le_infI1 le_infI2 ccINF_greatest ccINF_lower)
lemma ccSup_union_distrib: "countable A \<Longrightarrow> countable B \<Longrightarrow> Sup (A \<union> B) = sup (Sup A) (Sup B)"
by (rule antisym) (auto intro: ccSup_least ccSup_upper le_supI1 le_supI2)
lemma ccSUP_union:
- "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A \<union> B. M i) = sup (SUP i:A. M i) (SUP i:B. M i)"
+ "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A \<union> B. M i) = sup (SUP i\<in>A. M i) (SUP i\<in>B. M i)"
by (auto intro!: antisym ccSUP_mono intro: le_supI1 le_supI2 ccSUP_least ccSUP_upper)
-lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a:A. f a) (INF a:A. g a) = (INF a:A. inf (f a) (g a))"
+lemma ccINF_inf_distrib: "countable A \<Longrightarrow> inf (INF a\<in>A. f a) (INF a\<in>A. g a) = (INF a\<in>A. inf (f a) (g a))"
by (rule antisym) (rule ccINF_greatest, auto intro: le_infI1 le_infI2 ccINF_lower ccINF_mono)
-lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a:A. f a) (SUP a:A. g a) = (SUP a:A. sup (f a) (g a))"
+lemma ccSUP_sup_distrib: "countable A \<Longrightarrow> sup (SUP a\<in>A. f a) (SUP a\<in>A. g a) = (SUP a\<in>A. sup (f a) (g a))"
by (rule antisym[rotated]) (rule ccSUP_least, auto intro: le_supI1 le_supI2 ccSUP_upper ccSUP_mono)
-lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i :A. f) = f"
+lemma ccINF_const [simp]: "A \<noteq> {} \<Longrightarrow> (INF i \<in> A. f) = f"
unfolding image_constant_conv by auto
-lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i :A. f) = f"
+lemma ccSUP_const [simp]: "A \<noteq> {} \<Longrightarrow> (SUP i \<in> A. f) = f"
unfolding image_constant_conv by auto
-lemma ccINF_top [simp]: "(INF x:A. top) = top"
+lemma ccINF_top [simp]: "(INF x\<in>A. top) = top"
by (cases "A = {}") simp_all
-lemma ccSUP_bot [simp]: "(SUP x:A. bot) = bot"
+lemma ccSUP_bot [simp]: "(SUP x\<in>A. bot) = bot"
by (cases "A = {}") simp_all
-lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i:A. INF j:B. f i j) = (INF j:B. INF i:A. f i j)"
+lemma ccINF_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (INF i\<in>A. INF j\<in>B. f i j) = (INF j\<in>B. INF i\<in>A. f i j)"
by (iprover intro: ccINF_lower ccINF_greatest order_trans antisym)
-lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i:A. SUP j:B. f i j) = (SUP j:B. SUP i:A. f i j)"
+lemma ccSUP_commute: "countable A \<Longrightarrow> countable B \<Longrightarrow> (SUP i\<in>A. SUP j\<in>B. f i j) = (SUP j\<in>B. SUP i\<in>A. f i j)"
by (iprover intro: ccSUP_upper ccSUP_least order_trans antisym)
end
@@ -179,61 +179,61 @@
lemma less_ccSup_iff: "countable S \<Longrightarrow> a < Sup S \<longleftrightarrow> (\<exists>x\<in>S. a < x)"
unfolding not_le [symmetric] by (subst ccSup_le_iff) auto
-lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i:A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
+lemma less_ccSUP_iff: "countable A \<Longrightarrow> a < (SUP i\<in>A. f i) \<longleftrightarrow> (\<exists>x\<in>A. a < f x)"
using less_ccSup_iff [of "f ` A"] by simp
lemma ccInf_less_iff: "countable S \<Longrightarrow> Inf S < a \<longleftrightarrow> (\<exists>x\<in>S. x < a)"
unfolding not_le [symmetric] by (subst le_ccInf_iff) auto
-lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i:A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
+lemma ccINF_less_iff: "countable A \<Longrightarrow> (INF i\<in>A. f i) < a \<longleftrightarrow> (\<exists>x\<in>A. f x < a)"
using ccInf_less_iff [of "f ` A"] by simp
end
class countable_complete_distrib_lattice = countable_complete_lattice +
- assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b:B. sup a b)"
- assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b:B. inf a b)"
+ assumes sup_ccInf: "countable B \<Longrightarrow> sup a (Inf B) = (INF b\<in>B. sup a b)"
+ assumes inf_ccSup: "countable B \<Longrightarrow> inf a (Sup B) = (SUP b\<in>B. inf a b)"
begin
lemma sup_ccINF:
- "countable B \<Longrightarrow> sup a (INF b:B. f b) = (INF b:B. sup a (f b))"
+ "countable B \<Longrightarrow> sup a (INF b\<in>B. f b) = (INF b\<in>B. sup a (f b))"
by (simp only: sup_ccInf image_image countable_image)
lemma inf_ccSUP:
- "countable B \<Longrightarrow> inf a (SUP b:B. f b) = (SUP b:B. inf a (f b))"
+ "countable B \<Longrightarrow> inf a (SUP b\<in>B. f b) = (SUP b\<in>B. inf a (f b))"
by (simp only: inf_ccSup image_image countable_image)
subclass distrib_lattice
proof
fix a b c
- from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d:{b, c}. sup a d)"
+ from sup_ccInf[of "{b, c}" a] have "sup a (Inf {b, c}) = (INF d\<in>{b, c}. sup a d)"
by simp
then show "sup a (inf b c) = inf (sup a b) (sup a c)"
by simp
qed
lemma ccInf_sup:
- "countable B \<Longrightarrow> sup (Inf B) a = (INF b:B. sup b a)"
+ "countable B \<Longrightarrow> sup (Inf B) a = (INF b\<in>B. sup b a)"
by (simp add: sup_ccInf sup_commute)
lemma ccSup_inf:
- "countable B \<Longrightarrow> inf (Sup B) a = (SUP b:B. inf b a)"
+ "countable B \<Longrightarrow> inf (Sup B) a = (SUP b\<in>B. inf b a)"
by (simp add: inf_ccSup inf_commute)
lemma ccINF_sup:
- "countable B \<Longrightarrow> sup (INF b:B. f b) a = (INF b:B. sup (f b) a)"
+ "countable B \<Longrightarrow> sup (INF b\<in>B. f b) a = (INF b\<in>B. sup (f b) a)"
by (simp add: sup_ccINF sup_commute)
lemma ccSUP_inf:
- "countable B \<Longrightarrow> inf (SUP b:B. f b) a = (SUP b:B. inf (f b) a)"
+ "countable B \<Longrightarrow> inf (SUP b\<in>B. f b) a = (SUP b\<in>B. inf (f b) a)"
by (simp add: inf_ccSUP inf_commute)
lemma ccINF_sup_distrib2:
- "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a:A. f a) (INF b:B. g b) = (INF a:A. INF b:B. sup (f a) (g b))"
+ "countable A \<Longrightarrow> countable B \<Longrightarrow> sup (INF a\<in>A. f a) (INF b\<in>B. g b) = (INF a\<in>A. INF b\<in>B. sup (f a) (g b))"
by (subst ccINF_commute) (simp_all add: sup_ccINF ccINF_sup)
lemma ccSUP_inf_distrib2:
- "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a:A. f a) (SUP b:B. g b) = (SUP a:A. SUP b:B. inf (f a) (g b))"
+ "countable A \<Longrightarrow> countable B \<Longrightarrow> inf (SUP a\<in>A. f a) (SUP b\<in>B. g b) = (SUP a\<in>A. SUP b\<in>B. inf (f a) (g b))"
by (subst ccSUP_commute) (simp_all add: inf_ccSUP ccSUP_inf)
context
@@ -242,20 +242,20 @@
begin
lemma mono_ccInf:
- "countable A \<Longrightarrow> f (Inf A) \<le> (INF x:A. f x)"
+ "countable A \<Longrightarrow> f (Inf A) \<le> (INF x\<in>A. f x)"
using \<open>mono f\<close>
by (auto intro!: countable_complete_lattice_class.ccINF_greatest intro: ccInf_lower dest: monoD)
lemma mono_ccSup:
- "countable A \<Longrightarrow> (SUP x:A. f x) \<le> f (Sup A)"
+ "countable A \<Longrightarrow> (SUP x\<in>A. f x) \<le> f (Sup A)"
using \<open>mono f\<close> by (auto intro: countable_complete_lattice_class.ccSUP_least ccSup_upper dest: monoD)
lemma mono_ccINF:
- "countable I \<Longrightarrow> f (INF i : I. A i) \<le> (INF x : I. f (A x))"
+ "countable I \<Longrightarrow> f (INF i \<in> I. A i) \<le> (INF x \<in> I. f (A x))"
by (intro countable_complete_lattice_class.ccINF_greatest monoD[OF \<open>mono f\<close>] ccINF_lower)
lemma mono_ccSUP:
- "countable I \<Longrightarrow> (SUP x : I. f (A x)) \<le> f (SUP i : I. A i)"
+ "countable I \<Longrightarrow> (SUP x \<in> I. f (A x)) \<le> f (SUP i \<in> I. A i)"
by (intro countable_complete_lattice_class.ccSUP_least monoD[OF \<open>mono f\<close>] ccSUP_upper)
end
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Nov 08 09:11:52 2018 +0100
@@ -108,12 +108,12 @@
lemma sup_continuous_SUP[order_continuous_intros]:
fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
assumes M: "\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)"
- shows "sup_continuous (SUP i:I. M i)"
+ shows "sup_continuous (SUP i\<in>I. M i)"
unfolding sup_continuous_def by (auto simp add: sup_continuousD[OF M] intro: SUP_commute)
lemma sup_continuous_apply_SUP[order_continuous_intros]:
fixes M :: "_ \<Rightarrow> _ \<Rightarrow> 'a::complete_lattice"
- shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i:I. M i x)"
+ shows "(\<And>i. i \<in> I \<Longrightarrow> sup_continuous (M i)) \<Longrightarrow> sup_continuous (\<lambda>x. SUP i\<in>I. M i x)"
unfolding SUP_apply[symmetric] by (rule sup_continuous_SUP)
lemma sup_continuous_lfp'[order_continuous_intros]:
@@ -145,7 +145,7 @@
qed
lemma mono_INF_fun:
- "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y : X x. F x y z :: 'a :: complete_lattice)"
+ "(\<And>x y. mono (F x y)) \<Longrightarrow> mono (\<lambda>z x. INF y \<in> X x. F x y z :: 'a :: complete_lattice)"
by (auto intro!: INF_mono[OF bexI] simp: le_fun_def mono_def)
lemma continuous_on_max:
@@ -160,22 +160,22 @@
lemma real_of_nat_Sup:
assumes "A \<noteq> {}" "bdd_above A"
- shows "of_nat (Sup A) = (SUP a:A. of_nat a :: real)"
+ shows "of_nat (Sup A) = (SUP a\<in>A. of_nat a :: real)"
proof (intro antisym)
- show "(SUP a:A. of_nat a::real) \<le> of_nat (Sup A)"
+ show "(SUP a\<in>A. of_nat a::real) \<le> of_nat (Sup A)"
using assms by (intro cSUP_least of_nat_mono) (auto intro: cSup_upper)
have "Sup A \<in> A"
unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
- then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::real)"
+ then show "of_nat (Sup A) \<le> (SUP a\<in>A. of_nat a::real)"
by (intro cSUP_upper bdd_above_image_mono assms) (auto simp: mono_def)
qed
lemma (in complete_lattice) SUP_sup_const1:
- "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup c (f i)) = sup c (SUP i:I. f i)"
+ "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. sup c (f i)) = sup c (SUP i\<in>I. f i)"
using SUP_sup_distrib[of "\<lambda>_. c" I f] by simp
lemma (in complete_lattice) SUP_sup_const2:
- "I \<noteq> {} \<Longrightarrow> (SUP i:I. sup (f i) c) = sup (SUP i:I. f i) c"
+ "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. sup (f i) c) = sup (SUP i\<in>I. f i) c"
using SUP_sup_distrib[of f I "\<lambda>_. c"] by simp
lemma one_less_of_natD:
@@ -350,7 +350,7 @@
lemma rel_fun_limsup[transfer_rule]: "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal limsup limsup"
proof -
- have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i:{n..}. x i)) limsup"
+ have "rel_fun (rel_fun (=) pcr_ennreal) pcr_ennreal (\<lambda>x. INF n. sup 0 (SUP i\<in>{n..}. x i)) limsup"
unfolding limsup_INF_SUP[abs_def] by (transfer_prover_start, transfer_step+; simp)
then show ?thesis
unfolding limsup_INF_SUP[abs_def]
@@ -1140,13 +1140,13 @@
lemma of_nat_less_ennreal_of_nat[simp]: "of_nat n \<le> ennreal_of_enat x \<longleftrightarrow> of_nat n \<le> x"
by (cases x) (auto simp: of_nat_eq_enat)
-lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x:X. ennreal_of_enat x)"
+lemma ennreal_of_enat_Sup: "ennreal_of_enat (Sup X) = (SUP x\<in>X. ennreal_of_enat x)"
proof -
- have "ennreal_of_enat (Sup X) \<le> (SUP x : X. ennreal_of_enat x)"
+ have "ennreal_of_enat (Sup X) \<le> (SUP x \<in> X. ennreal_of_enat x)"
unfolding Sup_enat_def
proof (clarsimp, intro conjI impI)
fix x assume "finite X" "X \<noteq> {}"
- then show "ennreal_of_enat (Max X) \<le> (SUP x : X. ennreal_of_enat x)"
+ then show "ennreal_of_enat (Max X) \<le> (SUP x \<in> X. ennreal_of_enat x)"
by (intro SUP_upper Max_in)
next
assume "infinite X" "X \<noteq> {}"
@@ -1162,9 +1162,9 @@
with x show ?thesis
by (auto intro!: bexI[of _ x] less_le_trans[OF n])
qed
- then have "(SUP x : X. ennreal_of_enat x) = top"
+ then have "(SUP x \<in> X. ennreal_of_enat x) = top"
by simp
- then show "top \<le> (SUP x : X. ennreal_of_enat x)"
+ then show "top \<le> (SUP x \<in> X. ennreal_of_enat x)"
unfolding top_unique by simp
qed
then show ?thesis
@@ -1395,7 +1395,7 @@
lemma ennreal_suminf_SUP_eq_directed:
fixes f :: "'a \<Rightarrow> nat \<Rightarrow> ennreal"
assumes *: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
- shows "(\<Sum>n. SUP i:I. f i n) = (SUP i:I. \<Sum>n. f i n)"
+ shows "(\<Sum>n. SUP i\<in>I. f i n) = (SUP i\<in>I. \<Sum>n. f i n)"
proof cases
assume "I \<noteq> {}"
then obtain i where "i \<in> I" by auto
@@ -1417,16 +1417,16 @@
shows "(INF i. c + f i) = c + (INF i. f i)"
using INF_ennreal_add_const[of f c] by (simp add: ac_simps)
-lemma SUP_mult_left_ennreal: "c * (SUP i:I. f i) = (SUP i:I. c * f i ::ennreal)"
+lemma SUP_mult_left_ennreal: "c * (SUP i\<in>I. f i) = (SUP i\<in>I. c * f i ::ennreal)"
proof cases
assume "I \<noteq> {}" then show ?thesis
by transfer (auto simp add: SUP_ereal_mult_left max_absorb2 SUP_upper2)
qed (simp add: bot_ennreal)
-lemma SUP_mult_right_ennreal: "(SUP i:I. f i) * c = (SUP i:I. f i * c ::ennreal)"
+lemma SUP_mult_right_ennreal: "(SUP i\<in>I. f i) * c = (SUP i\<in>I. f i * c ::ennreal)"
using SUP_mult_left_ennreal by (simp add: mult.commute)
-lemma SUP_divide_ennreal: "(SUP i:I. f i) / c = (SUP i:I. f i / c ::ennreal)"
+lemma SUP_divide_ennreal: "(SUP i\<in>I. f i) / c = (SUP i\<in>I. f i / c ::ennreal)"
using SUP_mult_right_ennreal by (simp add: divide_ennreal_def)
lemma ennreal_SUP_of_nat_eq_top: "(SUP x. of_nat x :: ennreal) = top"
@@ -1442,9 +1442,9 @@
lemma ennreal_SUP_eq_top:
fixes f :: "'a \<Rightarrow> ennreal"
assumes "\<And>n. \<exists>i\<in>I. of_nat n \<le> f i"
- shows "(SUP i : I. f i) = top"
+ shows "(SUP i \<in> I. f i) = top"
proof -
- have "(SUP x. of_nat x :: ennreal) \<le> (SUP i : I. f i)"
+ have "(SUP x. of_nat x :: ennreal) \<le> (SUP i \<in> I. f i)"
using assms by (auto intro!: SUP_least intro: SUP_upper2)
then show ?thesis
by (auto simp: ennreal_SUP_of_nat_eq_top top_unique)
@@ -1452,19 +1452,19 @@
lemma ennreal_INF_const_minus:
fixes f :: "'a \<Rightarrow> ennreal"
- shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
+ shows "I \<noteq> {} \<Longrightarrow> (SUP x\<in>I. c - f x) = c - (INF x\<in>I. f x)"
by (transfer fixing: I)
(simp add: sup_max[symmetric] SUP_sup_const1 SUP_ereal_minus_right del: sup_ereal_def)
lemma of_nat_Sup_ennreal:
assumes "A \<noteq> {}" "bdd_above A"
- shows "of_nat (Sup A) = (SUP a:A. of_nat a :: ennreal)"
+ shows "of_nat (Sup A) = (SUP a\<in>A. of_nat a :: ennreal)"
proof (intro antisym)
- show "(SUP a:A. of_nat a::ennreal) \<le> of_nat (Sup A)"
+ show "(SUP a\<in>A. of_nat a::ennreal) \<le> of_nat (Sup A)"
by (intro SUP_least of_nat_mono) (auto intro: cSup_upper assms)
have "Sup A \<in> A"
unfolding Sup_nat_def using assms by (intro Max_in) (auto simp: bdd_above_nat)
- then show "of_nat (Sup A) \<le> (SUP a:A. of_nat a::ennreal)"
+ then show "of_nat (Sup A) \<le> (SUP a\<in>A. of_nat a::ennreal)"
by (intro SUP_upper)
qed
@@ -1601,18 +1601,18 @@
lemma SUP_sup_continuous_ennreal:
fixes f :: "ennreal \<Rightarrow> 'a::complete_lattice"
assumes f: "sup_continuous f" and "I \<noteq> {}"
- shows "(SUP i:I. f (g i)) = f (SUP i:I. g i)"
+ shows "(SUP i\<in>I. f (g i)) = f (SUP i\<in>I. g i)"
proof (rule antisym)
- show "(SUP i:I. f (g i)) \<le> f (SUP i:I. g i)"
+ show "(SUP i\<in>I. f (g i)) \<le> f (SUP i\<in>I. g i)"
by (rule mono_SUP[OF sup_continuous_mono[OF f]])
from ennreal_Sup_countable_SUP[of "g`I"] \<open>I \<noteq> {}\<close>
- obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i : I. g i) = (SUP i. M i)"
+ obtain M :: "nat \<Rightarrow> ennreal" where "incseq M" and M: "range M \<subseteq> g ` I" and eq: "(SUP i \<in> I. g i) = (SUP i. M i)"
by auto
- have "f (SUP i : I. g i) = (SUP i : range M. f i)"
+ have "f (SUP i \<in> I. g i) = (SUP i \<in> range M. f i)"
unfolding eq sup_continuousD[OF f \<open>mono M\<close>] by simp
- also have "\<dots> \<le> (SUP i : I. f (g i))"
+ also have "\<dots> \<le> (SUP i \<in> I. f (g i))"
by (insert M, drule SUP_subset_mono) auto
- finally show "f (SUP i : I. g i) \<le> (SUP i : I. f (g i))" .
+ finally show "f (SUP i \<in> I. g i) \<le> (SUP i \<in> I. f (g i))" .
qed
lemma ennreal_suminf_SUP_eq:
@@ -1625,7 +1625,7 @@
lemma ennreal_SUP_add_left:
fixes c :: ennreal
- shows "I \<noteq> {} \<Longrightarrow> (SUP i:I. f i + c) = (SUP i:I. f i) + c"
+ shows "I \<noteq> {} \<Longrightarrow> (SUP i\<in>I. f i + c) = (SUP i\<in>I. f i) + c"
apply transfer
apply (simp add: SUP_ereal_add_left)
apply (subst (1 2) max.absorb2)
@@ -1634,7 +1634,7 @@
lemma ennreal_SUP_const_minus: (* TODO: rename: ennreal_SUP_const_minus *)
fixes f :: "'a \<Rightarrow> ennreal"
- shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x:I. c - f x) = c - (SUP x:I. f x)"
+ shows "I \<noteq> {} \<Longrightarrow> c < top \<Longrightarrow> (INF x\<in>I. c - f x) = c - (SUP x\<in>I. f x)"
apply (transfer fixing: I)
unfolding ex_in_conv[symmetric]
apply (auto simp add: sup_max[symmetric] SUP_upper2 sup_absorb2
@@ -1648,11 +1648,11 @@
lemma INF_approx_ennreal:
fixes x::ennreal and e::real
assumes "e > 0"
- assumes INF: "x = (INF i : A. f i)"
+ assumes INF: "x = (INF i \<in> A. f i)"
assumes "x \<noteq> \<infinity>"
shows "\<exists>i \<in> A. f i < x + e"
proof -
- have "(INF i : A. f i) < x + e"
+ have "(INF i \<in> A. f i) < x + e"
unfolding INF[symmetric] using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
then show ?thesis
unfolding INF_less_iff .
@@ -1661,13 +1661,13 @@
lemma SUP_approx_ennreal:
fixes x::ennreal and e::real
assumes "e > 0" "A \<noteq> {}"
- assumes SUP: "x = (SUP i : A. f i)"
+ assumes SUP: "x = (SUP i \<in> A. f i)"
assumes "x \<noteq> \<infinity>"
shows "\<exists>i \<in> A. x < f i + e"
proof -
have "x < x + e"
using \<open>0<e\<close> \<open>x \<noteq> \<infinity>\<close> by (cases x) auto
- also have "x + e = (SUP i : A. f i + e)"
+ also have "x + e = (SUP i \<in> A. f i + e)"
unfolding SUP ennreal_SUP_add_left[OF \<open>A \<noteq> {}\<close>] ..
finally show ?thesis
unfolding less_SUP_iff .
@@ -1677,17 +1677,17 @@
fixes x::ennreal
assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
- shows "x = (SUP i : A. f i)"
+ shows "x = (SUP i \<in> A. f i)"
proof (rule antisym)
- show "x \<le> (SUP i:A. f i)"
+ 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"
by simp
- also have "\<dots> \<le> (SUP i:A. f i) + e"
+ also have "\<dots> \<le> (SUP i\<in>A. f i) + e"
by (intro add_mono \<open>i \<in> A\<close> SUP_upper order_refl)
- finally show "x \<le> (SUP i:A. f i) + e" .
+ finally show "x \<le> (SUP i\<in>A. f i) + e" .
qed
qed (intro SUP_least f_bound)
@@ -1695,17 +1695,17 @@
fixes x::ennreal
assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
- shows "x = (INF i : A. f i)"
+ shows "x = (INF i \<in> A. f i)"
proof (rule antisym)
- show "(INF i:A. f i) \<le> x"
+ 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
- then have "(INF i:A. f i) \<le> f i"
+ then have "(INF i\<in>A. f i) \<le> f i"
by (intro INF_lower)
also have "\<dots> \<le> x + e"
by fact
- finally show "(INF i:A. f i) \<le> x + e" .
+ finally show "(INF i\<in>A. f i) \<le> x + e" .
qed
qed (intro INF_greatest f_bound)
@@ -1786,7 +1786,7 @@
by (cases "0 \<le> x") (auto simp: ennreal_neg ennreal_less_iff simp flip: ennreal_1)
lemma SUP_const_minus_ennreal:
- fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x:I. c - f x) = c - (INF x:I. f x)"
+ fixes f :: "'a \<Rightarrow> ennreal" shows "I \<noteq> {} \<Longrightarrow> (SUP x\<in>I. c - f x) = c - (INF x\<in>I. f x)"
including ennreal.lifting
by (transfer fixing: I)
(simp add: SUP_sup_distrib[symmetric] SUP_ereal_minus_right
@@ -1929,18 +1929,18 @@
done
lemma SUP_diff_ennreal:
- "c < top \<Longrightarrow> (SUP i:I. f i - c :: ennreal) = (SUP i:I. f i) - c"
+ "c < top \<Longrightarrow> (SUP i\<in>I. f i - c :: ennreal) = (SUP i\<in>I. f i) - c"
by (auto intro!: SUP_eqI ennreal_minus_mono SUP_least intro: SUP_upper
simp: ennreal_minus_cancel_iff ennreal_minus_le_iff less_top[symmetric])
lemma ennreal_SUP_add_right:
- fixes c :: ennreal shows "I \<noteq> {} \<Longrightarrow> c + (SUP i:I. f i) = (SUP i:I. c + f i)"
+ fixes c :: ennreal shows "I \<noteq> {} \<Longrightarrow> c + (SUP i\<in>I. f i) = (SUP i\<in>I. c + f i)"
using ennreal_SUP_add_left[of I f c] by (simp add: add.commute)
lemma SUP_add_directed_ennreal:
fixes f g :: "_ \<Rightarrow> ennreal"
assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
- shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
+ shows "(SUP i\<in>I. f i + g i) = (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
proof cases
assume "I = {}" then show ?thesis
by (simp add: bot_ereal_def)
@@ -1948,16 +1948,16 @@
assume "I \<noteq> {}"
show ?thesis
proof (rule antisym)
- show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
+ show "(SUP i\<in>I. f i + g i) \<le> (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
by (rule SUP_least; intro add_mono SUP_upper)
next
- have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
+ have "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) = (SUP i\<in>I. f i + (SUP i\<in>I. g i))"
by (intro ennreal_SUP_add_left[symmetric] \<open>I \<noteq> {}\<close>)
- also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
+ also have "\<dots> = (SUP i\<in>I. (SUP j\<in>I. f i + g j))"
by (intro SUP_cong refl ennreal_SUP_add_right \<open>I \<noteq> {}\<close>)
- also have "\<dots> \<le> (SUP i:I. f i + g i)"
+ also have "\<dots> \<le> (SUP i\<in>I. f i + g i)"
using directed by (intro SUP_least) (blast intro: SUP_upper2)
- finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
+ finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
qed
qed
--- a/src/HOL/Library/Extended_Real.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy Thu Nov 08 09:11:52 2018 +0100
@@ -2149,23 +2149,23 @@
unfolding continuous_def by auto
lemma ereal_Sup:
- assumes *: "\<bar>SUP a:A. ereal a\<bar> \<noteq> \<infinity>"
- shows "ereal (Sup A) = (SUP a:A. ereal a)"
+ assumes *: "\<bar>SUP a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
+ shows "ereal (Sup A) = (SUP a\<in>A. ereal a)"
proof (rule continuous_at_Sup_mono)
- obtain r where r: "ereal r = (SUP a:A. ereal a)" "A \<noteq> {}"
+ obtain r where r: "ereal r = (SUP a\<in>A. ereal a)" "A \<noteq> {}"
using * by (force simp: bot_ereal_def)
then show "bdd_above A" "A \<noteq> {}"
by (auto intro!: SUP_upper bdd_aboveI[of _ r] simp flip: ereal_less_eq)
qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ereal)
-lemma ereal_SUP: "\<bar>SUP a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a:A. f a) = (SUP a:A. ereal (f a))"
+lemma ereal_SUP: "\<bar>SUP a\<in>A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (SUP a\<in>A. f a) = (SUP a\<in>A. ereal (f a))"
using ereal_Sup[of "f`A"] by auto
lemma ereal_Inf:
- assumes *: "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
- shows "ereal (Inf A) = (INF a:A. ereal a)"
+ assumes *: "\<bar>INF a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
+ shows "ereal (Inf A) = (INF a\<in>A. ereal a)"
proof (rule continuous_at_Inf_mono)
- obtain r where r: "ereal r = (INF a:A. ereal a)" "A \<noteq> {}"
+ obtain r where r: "ereal r = (INF a\<in>A. ereal a)" "A \<noteq> {}"
using * by (force simp: top_ereal_def)
then show "bdd_below A" "A \<noteq> {}"
by (auto intro!: INF_lower bdd_belowI[of _ r] simp flip: ereal_less_eq)
@@ -2173,17 +2173,17 @@
lemma ereal_Inf':
assumes *: "bdd_below A" "A \<noteq> {}"
- shows "ereal (Inf A) = (INF a:A. ereal a)"
+ shows "ereal (Inf A) = (INF a\<in>A. ereal a)"
proof (rule ereal_Inf)
from * obtain l u where "x \<in> A \<Longrightarrow> l \<le> x" "u \<in> A" for x
by (auto simp: bdd_below_def)
- then have "l \<le> (INF x:A. ereal x)" "(INF x:A. ereal x) \<le> u"
+ then have "l \<le> (INF x\<in>A. ereal x)" "(INF x\<in>A. ereal x) \<le> u"
by (auto intro!: INF_greatest INF_lower)
- then show "\<bar>INF a:A. ereal a\<bar> \<noteq> \<infinity>"
+ then show "\<bar>INF a\<in>A. ereal a\<bar> \<noteq> \<infinity>"
by auto
qed
-lemma ereal_INF: "\<bar>INF a:A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a:A. f a) = (INF a:A. ereal (f a))"
+lemma ereal_INF: "\<bar>INF a\<in>A. ereal (f a)\<bar> \<noteq> \<infinity> \<Longrightarrow> ereal (INF a\<in>A. f a) = (INF a\<in>A. ereal (f a))"
using ereal_Inf[of "f`A"] by auto
lemma ereal_Sup_uminus_image_eq: "Sup (uminus ` S::ereal set) = - Inf S"
@@ -2193,7 +2193,7 @@
lemma ereal_SUP_uminus_eq:
fixes f :: "'a \<Rightarrow> ereal"
- shows "(SUP x:S. uminus (f x)) = - (INF x:S. f x)"
+ shows "(SUP x\<in>S. uminus (f x)) = - (INF x\<in>S. f x)"
using ereal_Sup_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
lemma ereal_inj_on_uminus[intro, simp]: "inj_on uminus (A :: ereal set)"
@@ -2204,12 +2204,12 @@
lemma ereal_INF_uminus_eq:
fixes f :: "'a \<Rightarrow> ereal"
- shows "(INF x:S. - f x) = - (SUP x:S. f x)"
+ shows "(INF x\<in>S. - f x) = - (SUP x\<in>S. f x)"
using ereal_Inf_uminus_image_eq [of "f ` S"] by (simp add: comp_def)
lemma ereal_SUP_uminus:
fixes f :: "'a \<Rightarrow> ereal"
- shows "(SUP i : R. - f i) = - (INF i : R. f i)"
+ shows "(SUP i \<in> R. - f i) = - (INF i \<in> R. f i)"
using ereal_Sup_uminus_image_eq[of "f`R"]
by (simp add: image_image)
@@ -2278,17 +2278,17 @@
qed
lemma SUP_PInfty:
- "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i:A. f i :: ereal) = \<infinity>"
+ "(\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i) \<Longrightarrow> (SUP i\<in>A. f i :: ereal) = \<infinity>"
unfolding top_ereal_def[symmetric] SUP_eq_top_iff
by (metis MInfty_neq_PInfty(2) PInfty_neq_ereal(2) less_PInf_Ex_of_nat less_ereal.elims(2) less_le_trans)
-lemma SUP_nat_Infty: "(SUP i::nat. ereal (real i)) = \<infinity>"
+lemma SUP_nat_Infty: "(SUP i. ereal (real i)) = \<infinity>"
by (rule SUP_PInfty) auto
lemma SUP_ereal_add_left:
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
- shows "(SUP i:I. f i + c :: ereal) = (SUP i:I. f i) + c"
-proof (cases "(SUP i:I. f i) = - \<infinity>")
+ shows "(SUP i\<in>I. f i + c :: ereal) = (SUP i\<in>I. f i) + c"
+proof (cases "(SUP i\<in>I. f i) = - \<infinity>")
case True
then have "\<And>i. i \<in> I \<Longrightarrow> f i = -\<infinity>"
unfolding Sup_eq_MInfty by auto
@@ -2303,23 +2303,23 @@
lemma SUP_ereal_add_right:
fixes c :: ereal
- shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i:I. c + f i) = c + (SUP i:I. f i)"
+ shows "I \<noteq> {} \<Longrightarrow> c \<noteq> -\<infinity> \<Longrightarrow> (SUP i\<in>I. c + f i) = c + (SUP i\<in>I. f i)"
using SUP_ereal_add_left[of I c f] by (simp add: add.commute)
lemma SUP_ereal_minus_right:
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>"
- shows "(SUP i:I. c - f i :: ereal) = c - (INF i:I. f i)"
+ shows "(SUP i\<in>I. c - f i :: ereal) = c - (INF i\<in>I. f i)"
using SUP_ereal_add_right[OF assms, of "\<lambda>i. - f i"]
by (simp add: ereal_SUP_uminus minus_ereal_def)
lemma SUP_ereal_minus_left:
assumes "I \<noteq> {}" "c \<noteq> \<infinity>"
- shows "(SUP i:I. f i - c:: ereal) = (SUP i:I. f i) - c"
+ shows "(SUP i\<in>I. f i - c:: ereal) = (SUP i\<in>I. f i) - c"
using SUP_ereal_add_left[OF \<open>I \<noteq> {}\<close>, of "-c" f] by (simp add: \<open>c \<noteq> \<infinity>\<close> minus_ereal_def)
lemma INF_ereal_minus_right:
assumes "I \<noteq> {}" and "\<bar>c\<bar> \<noteq> \<infinity>"
- shows "(INF i:I. c - f i) = c - (SUP i:I. f i::ereal)"
+ shows "(INF i\<in>I. c - f i) = c - (SUP i\<in>I. f i::ereal)"
proof -
{ fix b have "(-c) + b = - (c - b)"
using \<open>\<bar>c\<bar> \<noteq> \<infinity>\<close> by (cases c b rule: ereal2_cases) auto }
@@ -2339,7 +2339,7 @@
lemma SUP_combine:
fixes f :: "'a::semilattice_sup \<Rightarrow> 'a::semilattice_sup \<Rightarrow> 'b::complete_lattice"
assumes mono: "\<And>a b c d. a \<le> b \<Longrightarrow> c \<le> d \<Longrightarrow> f a c \<le> f b d"
- shows "(SUP i:UNIV. SUP j:UNIV. f i j) = (SUP i. f i i)"
+ shows "(SUP i\<in>UNIV. SUP j\<in>UNIV. f i j) = (SUP i. f i i)"
proof (rule antisym)
show "(SUP i j. f i j) \<le> (SUP i. f i i)"
by (rule SUP_least SUP_upper2[where i="sup i j" for i j] UNIV_I mono sup_ge1 sup_ge2)+
@@ -2360,14 +2360,14 @@
apply (rule SUP_combine[symmetric] add_mono inc[THEN monoD] | assumption)+
done
-lemma INF_eq_minf: "(INF i:I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
+lemma INF_eq_minf: "(INF i\<in>I. f i::ereal) \<noteq> -\<infinity> \<longleftrightarrow> (\<exists>b>-\<infinity>. \<forall>i\<in>I. b \<le> f i)"
unfolding bot_ereal_def[symmetric] INF_eq_bot_iff by (auto simp: not_less)
lemma INF_ereal_add_left:
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
- shows "(INF i:I. f i + c :: ereal) = (INF i:I. f i) + c"
+ shows "(INF i\<in>I. f i + c :: ereal) = (INF i\<in>I. f i) + c"
proof -
- have "(INF i:I. f i) \<noteq> -\<infinity>"
+ have "(INF i\<in>I. f i) \<noteq> -\<infinity>"
unfolding INF_eq_minf using assms by (intro exI[of _ 0]) auto
then show ?thesis
by (subst continuous_at_Inf_mono[where f="\<lambda>x. x + c"])
@@ -2376,14 +2376,14 @@
lemma INF_ereal_add_right:
assumes "I \<noteq> {}" "c \<noteq> -\<infinity>" "\<And>x. x \<in> I \<Longrightarrow> 0 \<le> f x"
- shows "(INF i:I. c + f i :: ereal) = c + (INF i:I. f i)"
+ shows "(INF i\<in>I. c + f i :: ereal) = c + (INF i\<in>I. f i)"
using INF_ereal_add_left[OF assms] by (simp add: ac_simps)
lemma INF_ereal_add_directed:
fixes f g :: "'a \<Rightarrow> ereal"
assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<ge> f k + g k"
- shows "(INF i:I. f i + g i) = (INF i:I. f i) + (INF i:I. g i)"
+ shows "(INF i\<in>I. f i + g i) = (INF i\<in>I. f i) + (INF i\<in>I. g i)"
proof cases
assume "I = {}" then show ?thesis
by (simp add: top_ereal_def)
@@ -2391,16 +2391,16 @@
assume "I \<noteq> {}"
show ?thesis
proof (rule antisym)
- show "(INF i:I. f i) + (INF i:I. g i) \<le> (INF i:I. f i + g i)"
+ show "(INF i\<in>I. f i) + (INF i\<in>I. g i) \<le> (INF i\<in>I. f i + g i)"
by (rule INF_greatest; intro add_mono INF_lower)
next
- have "(INF i:I. f i + g i) \<le> (INF i:I. (INF j:I. f i + g j))"
+ have "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. (INF j\<in>I. f i + g j))"
using directed by (intro INF_greatest) (blast intro: INF_lower2)
- also have "\<dots> = (INF i:I. f i + (INF i:I. g i))"
+ also have "\<dots> = (INF i\<in>I. f i + (INF i\<in>I. g i))"
using nonneg by (intro INF_cong refl INF_ereal_add_right \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
- also have "\<dots> = (INF i:I. f i) + (INF i:I. g i)"
+ also have "\<dots> = (INF i\<in>I. f i) + (INF i\<in>I. g i)"
using nonneg by (intro INF_ereal_add_left \<open>I \<noteq> {}\<close>) (auto simp: INF_eq_minf intro!: exI[of _ 0])
- finally show "(INF i:I. f i + g i) \<le> (INF i:I. f i) + (INF i:I. g i)" .
+ finally show "(INF i\<in>I. f i + g i) \<le> (INF i\<in>I. f i) + (INF i\<in>I. g i)" .
qed
qed
@@ -2454,8 +2454,8 @@
fixes f :: "'a \<Rightarrow> ereal"
assumes "I \<noteq> {}"
assumes f: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" and c: "0 \<le> c"
- shows "(SUP i:I. c * f i) = c * (SUP i:I. f i)"
-proof (cases "(SUP i: I. f i) = 0")
+ shows "(SUP i\<in>I. c * f i) = c * (SUP i\<in>I. f i)"
+proof (cases "(SUP i \<in> I. f i) = 0")
case True
then have "\<And>i. i \<in> I \<Longrightarrow> f i = 0"
by (metis SUP_upper f antisym)
@@ -2595,9 +2595,9 @@
by(cases n) simp_all
lemma ereal_of_enat_Sup:
- assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a : A. ereal_of_enat a)"
+ assumes "A \<noteq> {}" shows "ereal_of_enat (Sup A) = (SUP a \<in> A. ereal_of_enat a)"
proof (intro antisym mono_Sup)
- show "ereal_of_enat (Sup A) \<le> (SUP a : A. ereal_of_enat a)"
+ show "ereal_of_enat (Sup A) \<le> (SUP a \<in> A. ereal_of_enat a)"
proof cases
assume "finite A"
with \<open>A \<noteq> {}\<close> obtain a where "a \<in> A" "ereal_of_enat (Sup A) = ereal_of_enat a"
@@ -2606,7 +2606,7 @@
by (auto intro: SUP_upper)
next
assume "\<not> finite A"
- have [simp]: "(SUP a : A. ereal_of_enat a) = top"
+ have [simp]: "(SUP a \<in> A. ereal_of_enat a) = top"
unfolding SUP_eq_top_iff
proof safe
fix x :: ereal assume "x < top"
@@ -2626,7 +2626,7 @@
qed (simp add: mono_def)
lemma ereal_of_enat_SUP:
- "A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a:A. f a) = (SUP a : A. ereal_of_enat (f a))"
+ "A \<noteq> {} \<Longrightarrow> ereal_of_enat (SUP a\<in>A. f a) = (SUP a \<in> A. ereal_of_enat (f a))"
using ereal_of_enat_Sup[of "f`A"] by auto
subsection "Limits on @{typ ereal}"
@@ -3225,43 +3225,43 @@
let ?INF = "\<lambda>P g. INFIMUM (Collect P) g"
show "?F \<noteq> {}"
by (auto intro: eventually_True)
- show "(SUP P:?F. ?INF P g) \<noteq> - \<infinity>"
+ show "(SUP P\<in>?F. ?INF P g) \<noteq> - \<infinity>"
unfolding bot_ereal_def[symmetric] SUP_bot_conv INF_eq_bot_iff
by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
- have "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. (SUP P':?F. ?INF P f + ?INF P' g))"
+ have "(SUP P\<in>?F. ?INF P f + (SUP P\<in>?F. ?INF P g)) \<le> (SUP P\<in>?F. (SUP P'\<in>?F. ?INF P f + ?INF P' g))"
proof (safe intro!: SUP_mono bexI[of _ "\<lambda>x. P x \<and> 0 \<le> f x" for P])
fix P let ?P' = "\<lambda>x. P x \<and> 0 \<le> f x"
assume "eventually P F"
with ev show "eventually ?P' F"
by eventually_elim auto
- have "?INF P f + (SUP P:?F. ?INF P g) \<le> ?INF ?P' f + (SUP P:?F. ?INF P g)"
+ have "?INF P f + (SUP P\<in>?F. ?INF P g) \<le> ?INF ?P' f + (SUP P\<in>?F. ?INF P g)"
by (intro add_mono INF_mono) auto
- also have "\<dots> = (SUP P':?F. ?INF ?P' f + ?INF P' g)"
+ also have "\<dots> = (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)"
proof (rule SUP_ereal_add_right[symmetric])
show "INFIMUM {x. P x \<and> 0 \<le> f x} f \<noteq> - \<infinity>"
unfolding bot_ereal_def[symmetric] INF_eq_bot_iff
by (auto intro!: exI[of _ 0] ev simp: bot_ereal_def)
qed fact
- finally show "?INF P f + (SUP P:?F. ?INF P g) \<le> (SUP P':?F. ?INF ?P' f + ?INF P' g)" .
+ finally show "?INF P f + (SUP P\<in>?F. ?INF P g) \<le> (SUP P'\<in>?F. ?INF ?P' f + ?INF P' g)" .
qed
- also have "\<dots> \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
+ also have "\<dots> \<le> (SUP P\<in>?F. INF x\<in>Collect P. f x + g x)"
proof (safe intro!: SUP_least)
fix P Q assume *: "eventually P F" "eventually Q F"
- show "?INF P f + ?INF Q g \<le> (SUP P:?F. INF x:Collect P. f x + g x)"
+ show "?INF P f + ?INF Q g \<le> (SUP P\<in>?F. INF x\<in>Collect P. f x + g x)"
proof (rule SUP_upper2)
show "(\<lambda>x. P x \<and> Q x) \<in> ?F"
using * by (auto simp: eventually_conj)
- show "?INF P f + ?INF Q g \<le> (INF x:{x. P x \<and> Q x}. f x + g x)"
+ show "?INF P f + ?INF Q g \<le> (INF x\<in>{x. P x \<and> Q x}. f x + g x)"
by (intro INF_greatest add_mono) (auto intro: INF_lower)
qed
qed
- finally show "(SUP P:?F. ?INF P f + (SUP P:?F. ?INF P g)) \<le> (SUP P:?F. INF x:Collect P. f x + g x)" .
+ finally show "(SUP P\<in>?F. ?INF P f + (SUP P\<in>?F. ?INF P g)) \<le> (SUP P\<in>?F. INF x\<in>Collect P. f x + g x)" .
qed
lemma Sup_ereal_mult_right':
assumes nonempty: "Y \<noteq> {}"
and x: "x \<ge> 0"
- shows "(SUP i:Y. f i) * ereal x = (SUP i:Y. f i * ereal x)" (is "?lhs = ?rhs")
+ shows "(SUP i\<in>Y. f i) * ereal x = (SUP i\<in>Y. f i * ereal x)" (is "?lhs = ?rhs")
proof(cases "x = 0")
case True thus ?thesis by(auto simp add: nonempty zero_ereal_def[symmetric])
next
@@ -3271,8 +3271,8 @@
show "?rhs \<le> ?lhs"
by(rule SUP_least)(simp add: ereal_mult_right_mono SUP_upper x)
next
- have "?lhs / ereal x = (SUP i:Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
- also have "\<dots> = (SUP i:Y. f i)" using False by simp
+ have "?lhs / ereal x = (SUP i\<in>Y. f i) * (ereal x / ereal x)" by(simp only: ereal_times_divide_eq)
+ also have "\<dots> = (SUP i\<in>Y. f i)" using False by simp
also have "\<dots> \<le> ?rhs / x"
proof(rule SUP_least)
fix i
@@ -3292,7 +3292,7 @@
qed
lemma Sup_ereal_mult_left':
- "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i:Y. f i) = (SUP i:Y. ereal x * f i)"
+ "\<lbrakk> Y \<noteq> {}; x \<ge> 0 \<rbrakk> \<Longrightarrow> ereal x * (SUP i\<in>Y. f i) = (SUP i\<in>Y. ereal x * f i)"
by(subst (1 2) mult.commute)(rule Sup_ereal_mult_right')
lemma sup_continuous_add[order_continuous_intros]:
@@ -3676,7 +3676,7 @@
fixes f g :: "'a \<Rightarrow> ereal"
assumes nonneg: "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> f i" "\<And>i. i \<in> I \<Longrightarrow> 0 \<le> g i"
assumes directed: "\<And>i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. f i + g j \<le> f k + g k"
- shows "(SUP i:I. f i + g i) = (SUP i:I. f i) + (SUP i:I. g i)"
+ shows "(SUP i\<in>I. f i + g i) = (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
proof cases
assume "I = {}" then show ?thesis
by (simp add: bot_ereal_def)
@@ -3684,18 +3684,18 @@
assume "I \<noteq> {}"
show ?thesis
proof (rule antisym)
- show "(SUP i:I. f i + g i) \<le> (SUP i:I. f i) + (SUP i:I. g i)"
+ show "(SUP i\<in>I. f i + g i) \<le> (SUP i\<in>I. f i) + (SUP i\<in>I. g i)"
by (rule SUP_least; intro add_mono SUP_upper)
next
- have "bot < (SUP i:I. g i)"
+ have "bot < (SUP i\<in>I. g i)"
using \<open>I \<noteq> {}\<close> nonneg(2) by (auto simp: bot_ereal_def less_SUP_iff)
- then have "(SUP i:I. f i) + (SUP i:I. g i) = (SUP i:I. f i + (SUP i:I. g i))"
+ then have "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) = (SUP i\<in>I. f i + (SUP i\<in>I. g i))"
by (intro SUP_ereal_add_left[symmetric] \<open>I \<noteq> {}\<close>) auto
- also have "\<dots> = (SUP i:I. (SUP j:I. f i + g j))"
+ also have "\<dots> = (SUP i\<in>I. (SUP j\<in>I. f i + g j))"
using nonneg(1) by (intro SUP_cong refl SUP_ereal_add_right[symmetric] \<open>I \<noteq> {}\<close>) auto
- also have "\<dots> \<le> (SUP i:I. f i + g i)"
+ also have "\<dots> \<le> (SUP i\<in>I. f i + g i)"
using directed by (intro SUP_least) (blast intro: SUP_upper2)
- finally show "(SUP i:I. f i) + (SUP i:I. g i) \<le> (SUP i:I. f i + g i)" .
+ finally show "(SUP i\<in>I. f i) + (SUP i\<in>I. g i) \<le> (SUP i\<in>I. f i + g i)" .
qed
qed
@@ -3704,12 +3704,12 @@
assumes "I \<noteq> {}"
assumes directed: "\<And>N i j. N \<subseteq> A \<Longrightarrow> i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f n i \<le> f n k \<and> f n j \<le> f n k"
assumes nonneg: "\<And>n i. i \<in> I \<Longrightarrow> n \<in> A \<Longrightarrow> 0 \<le> f n i"
- shows "(SUP i:I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i:I. f n i)"
+ shows "(SUP i\<in>I. \<Sum>n\<in>A. f n i) = (\<Sum>n\<in>A. SUP i\<in>I. f n i)"
proof -
- have "N \<subseteq> A \<Longrightarrow> (SUP i:I. \<Sum>n\<in>N. f n i) = (\<Sum>n\<in>N. SUP i:I. f n i)" for N
+ 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:I. f n i + (\<Sum>l\<in>N. f l i)) = (SUP i:I. f n i) + (SUP i:I. \<Sum>l\<in>N. f l i)"
+ 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)"
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)
@@ -3730,11 +3730,11 @@
assumes "I \<noteq> {}"
assumes directed: "\<And>N i j. i \<in> I \<Longrightarrow> j \<in> I \<Longrightarrow> finite N \<Longrightarrow> \<exists>k\<in>I. \<forall>n\<in>N. f i n \<le> f k n \<and> f j n \<le> f k n"
assumes nonneg: "\<And>n i. 0 \<le> f n i"
- shows "(\<Sum>i. SUP n:I. f n i) = (SUP n:I. \<Sum>i. f n i)"
+ shows "(\<Sum>i. SUP n\<in>I. f n i) = (SUP n\<in>I. \<Sum>i. f n i)"
proof (subst (1 2) suminf_ereal_eq_SUP)
- show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n:I. f n i)"
+ show "\<And>n i. 0 \<le> f n i" "\<And>i. 0 \<le> (SUP n\<in>I. f n i)"
using \<open>I \<noteq> {}\<close> nonneg by (auto intro: SUP_upper2)
- show "(SUP n. \<Sum>i<n. SUP n:I. f n i) = (SUP n:I. SUP j. \<Sum>i<j. f n i)"
+ show "(SUP n. \<Sum>i<n. SUP n\<in>I. f n i) = (SUP n\<in>I. SUP j. \<Sum>i<j. f n i)"
apply (subst SUP_commute)
apply (subst SUP_ereal_sum_directed)
apply (auto intro!: assms simp: finite_subset)
@@ -4223,11 +4223,11 @@
fixes f :: "_ \<Rightarrow> ereal" and A
assumes nonneg: "\<forall>x\<in>A. f x \<ge> 0"
and A:"A \<noteq> {}"
- shows "(SUP x:A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> ?rhs")
+ shows "(SUP x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>x\<in>A. f x = 0)" (is "?lhs \<longleftrightarrow> ?rhs")
proof(intro iffI ballI)
fix x
assume "?lhs" "x \<in> A"
- from \<open>x \<in> A\<close> have "f x \<le> (SUP x:A. f x)" by(rule SUP_upper)
+ from \<open>x \<in> A\<close> have "f x \<le> (SUP x\<in>A. f x)" by(rule SUP_upper)
with \<open>?lhs\<close> show "f x = 0" using nonneg \<open>x \<in> A\<close> by auto
qed(simp cong: SUP_cong add: A)
--- a/src/HOL/Library/Finite_Lattice.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Finite_Lattice.thy Thu Nov 08 09:11:52 2018 +0100
@@ -159,12 +159,12 @@
distrib_lattice + finite_lattice_complete
lemma finite_distrib_lattice_complete_sup_Inf:
- "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y:A. sup x y)"
+ "sup (x::'a::finite_distrib_lattice_complete) (Inf A) = (INF y\<in>A. sup x y)"
using finite
by (induct A rule: finite_induct) (simp_all add: sup_inf_distrib1)
lemma finite_distrib_lattice_complete_inf_Sup:
- "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y:A. inf x y)"
+ "inf (x::'a::finite_distrib_lattice_complete) (Sup A) = (SUP y\<in>A. inf x y)"
using finite [of A] by induct (simp_all add: inf_sup_distrib1)
context finite_distrib_lattice_complete
--- a/src/HOL/Library/Liminf_Limsup.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Thu Nov 08 09:11:52 2018 +0100
@@ -25,13 +25,13 @@
lemma le_cSup_iff_less:
fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
- shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
+ shows "A \<noteq> {} \<Longrightarrow> bdd_above (f`A) \<Longrightarrow> x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)"
by (simp add: le_cSUP_iff)
(blast intro: less_imp_le less_trans less_le_trans dest: dense)
lemma le_Sup_iff_less:
fixes x :: "'a :: {complete_linorder, dense_linorder}"
- shows "x \<le> (SUP i:A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
+ shows "x \<le> (SUP i\<in>A. f i) \<longleftrightarrow> (\<forall>y<x. \<exists>i\<in>A. y \<le> f i)" (is "?lhs = ?rhs")
unfolding le_SUP_iff
by (blast intro: less_imp_le less_trans less_le_trans dest: dense)
@@ -51,38 +51,38 @@
lemma cInf_le_iff_less:
fixes x :: "'a :: {conditionally_complete_linorder, dense_linorder}"
- shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+ shows "A \<noteq> {} \<Longrightarrow> bdd_below (f`A) \<Longrightarrow> (INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
by (simp add: cINF_le_iff)
(blast intro: less_imp_le less_trans le_less_trans dest: dense)
lemma Inf_le_iff_less:
fixes x :: "'a :: {complete_linorder, dense_linorder}"
- shows "(INF i:A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
+ shows "(INF i\<in>A. f i) \<le> x \<longleftrightarrow> (\<forall>y>x. \<exists>i\<in>A. f i \<le> y)"
unfolding INF_le_iff
by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
lemma SUP_pair:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
- shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
+ shows "(SUP i \<in> A. SUP j \<in> B. f i j) = (SUP p \<in> A \<times> B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: SUP_least SUP_upper2)
lemma INF_pair:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
- shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
+ shows "(INF i \<in> A. INF j \<in> B. f i j) = (INF p \<in> A \<times> B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: INF_greatest INF_lower2)
lemma INF_Sigma:
fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
- shows "(INF i : A. INF j : B i. f i j) = (INF p : Sigma A B. f (fst p) (snd p))"
+ shows "(INF i \<in> A. INF j \<in> B i. f i j) = (INF p \<in> Sigma A B. f (fst p) (snd p))"
by (rule antisym) (auto intro!: INF_greatest INF_lower2)
subsubsection \<open>\<open>Liminf\<close> and \<open>Limsup\<close>\<close>
definition Liminf :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
- "Liminf F f = (SUP P:{P. eventually P F}. INF x:{x. P x}. f x)"
+ "Liminf F f = (SUP P\<in>{P. eventually P F}. INF x\<in>{x. P x}. f x)"
definition Limsup :: "'a filter \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'b :: complete_lattice" where
- "Limsup F f = (INF P:{P. eventually P F}. SUP x:{x. P x}. f x)"
+ "Limsup F f = (INF P\<in>{P. eventually P F}. SUP x\<in>{x. P x}. f x)"
abbreviation "liminf \<equiv> Liminf sequentially"
@@ -98,11 +98,11 @@
(\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPREMUM (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
unfolding Limsup_def by (auto intro!: INF_eqI)
-lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
+lemma liminf_SUP_INF: "liminf f = (SUP n. INF m\<in>{n..}. f m)"
unfolding Liminf_def eventually_sequentially
by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
-lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
+lemma limsup_INF_SUP: "limsup f = (INF n. SUP m\<in>{n..}. f m)"
unfolding Limsup_def eventually_sequentially
by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
@@ -111,7 +111,7 @@
shows "Limsup F (\<lambda>x. c) = c"
proof -
have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
- have "\<And>P. eventually P F \<Longrightarrow> (SUP x : {x. P x}. c) = c"
+ have "\<And>P. eventually P F \<Longrightarrow> (SUP x \<in> {x. P x}. c) = c"
using ntriv by (intro SUP_const) (auto simp: eventually_False *)
then show ?thesis
unfolding Limsup_def using eventually_True
@@ -124,7 +124,7 @@
shows "Liminf F (\<lambda>x. c) = c"
proof -
have *: "\<And>P. Ex P \<longleftrightarrow> P \<noteq> (\<lambda>x. False)" by auto
- have "\<And>P. eventually P F \<Longrightarrow> (INF x : {x. P x}. c) = c"
+ have "\<And>P. eventually P F \<Longrightarrow> (INF x \<in> {x. P x}. c) = c"
using ntriv by (intro INF_const) (auto simp: eventually_False *)
then show ?thesis
unfolding Liminf_def using eventually_True
@@ -387,7 +387,7 @@
assumes "strict_mono r"
shows "liminf X \<le> liminf (X \<circ> r) "
proof-
- have "\<And>n. (INF m:{n..}. X m) \<le> (INF m:{n..}. (X \<circ> r) m)"
+ have "\<And>n. (INF m\<in>{n..}. X m) \<le> (INF m\<in>{n..}. (X \<circ> r) m)"
proof (safe intro!: INF_mono)
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
using seq_suble[OF \<open>strict_mono r\<close>, of m] by (intro bexI[of _ "r m"]) auto
@@ -400,7 +400,7 @@
assumes "strict_mono r"
shows "limsup (X \<circ> r) \<le> limsup X"
proof-
- have "(SUP m:{n..}. (X \<circ> r) m) \<le> (SUP m:{n..}. X m)" for n
+ have "(SUP m\<in>{n..}. (X \<circ> r) m) \<le> (SUP m\<in>{n..}. X m)" for n
proof (safe intro!: SUP_mono)
fix m :: nat
assume "n \<le> m"
@@ -431,11 +431,11 @@
qed }
note * = this
- have "f (Liminf F g) = (SUP P : {P. eventually P F}. f (Inf (g ` Collect P)))"
+ have "f (Liminf F g) = (SUP P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
unfolding Liminf_def
by (subst continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+ also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
by (intro SUP_cong refl continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis by (auto simp: Liminf_def)
@@ -456,11 +456,11 @@
qed }
note * = this
- have "f (Limsup F g) = (INF P : {P. eventually P F}. f (Sup (g ` Collect P)))"
+ have "f (Limsup F g) = (INF P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
unfolding Limsup_def
by (subst continuous_at_Inf_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
+ also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
by (intro INF_cong refl continuous_at_Sup_mono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis by (auto simp: Limsup_def)
@@ -480,11 +480,11 @@
with \<open>eventually P F\<close> F show False
by auto
qed
- have "f (Limsup F g) = (SUP P : {P. eventually P F}. f (Sup (g ` Collect P)))"
+ have "f (Limsup F g) = (SUP P \<in> {P. eventually P F}. f (Sup (g ` Collect P)))"
unfolding Limsup_def
by (subst continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (SUP P : {P. eventually P F}. INFIMUM (g ` Collect P) f)"
+ also have "\<dots> = (SUP P \<in> {P. eventually P F}. INFIMUM (g ` Collect P) f)"
by (intro SUP_cong refl continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis
@@ -506,11 +506,11 @@
qed }
note * = this
- have "f (Liminf F g) = (INF P : {P. eventually P F}. f (Inf (g ` Collect P)))"
+ have "f (Liminf F g) = (INF P \<in> {P. eventually P F}. f (Inf (g ` Collect P)))"
unfolding Liminf_def
by (subst continuous_at_Sup_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto intro: eventually_True)
- also have "\<dots> = (INF P : {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
+ also have "\<dots> = (INF P \<in> {P. eventually P F}. SUPREMUM (g ` Collect P) f)"
by (intro INF_cong refl continuous_at_Inf_antimono[OF am continuous_on_imp_continuous_within[OF c]])
(auto dest!: eventually_happens simp: F)
finally show ?thesis
@@ -527,10 +527,10 @@
by (subst Limsup_def)
(auto simp add: SUP_upper Limsup_bounded eventually_filtermap eventually_mono intro!: INF_greatest)
-lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x:Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
+lemma Liminf_least: "(\<And>P. eventually P F \<Longrightarrow> (INF x\<in>Collect P. f x) \<le> x) \<Longrightarrow> Liminf F f \<le> x"
by (auto intro!: SUP_least simp: Liminf_def)
-lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x:Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
+lemma Limsup_greatest: "(\<And>P. eventually P F \<Longrightarrow> x \<le> (SUP x\<in>Collect P. f x)) \<Longrightarrow> Limsup F f \<ge> x"
by (auto intro!: INF_greatest simp: Limsup_def)
lemma Liminf_filtermap_ge: "inj f \<Longrightarrow> Liminf (filtermap f F) g \<ge> Liminf F (\<lambda>x. g (f x))"
--- a/src/HOL/Library/Multiset.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Multiset.thy Thu Nov 08 09:11:52 2018 +0100
@@ -1035,7 +1035,7 @@
ultimately have "finite {i. Inf ((\<lambda>f. f i) ` A) > 0}" by (rule finite_subset)
with False show ?thesis by simp
qed simp_all
- thus "(\<lambda>i. if A = {} then 0 else INF f:A. f i) \<in> multiset" by (simp add: multiset_def)
+ thus "(\<lambda>i. if A = {} then 0 else INF f\<in>A. f i) \<in> multiset" by (simp add: multiset_def)
qed
instance ..
@@ -1094,17 +1094,17 @@
lemma Sup_multiset_in_multiset:
assumes "A \<noteq> {}" "subset_mset.bdd_above A"
- shows "(\<lambda>i. SUP X:A. count X i) \<in> multiset"
+ shows "(\<lambda>i. SUP X\<in>A. count X i) \<in> multiset"
unfolding multiset_def
proof
have "{i. Sup ((\<lambda>X. count X i) ` A) > 0} \<subseteq> (\<Union>X\<in>A. {i. 0 < count X i})"
proof safe
- fix i assume pos: "(SUP X:A. count X i) > 0"
+ fix i assume pos: "(SUP X\<in>A. count X i) > 0"
show "i \<in> (\<Union>X\<in>A. {i. 0 < count X i})"
proof (rule ccontr)
assume "i \<notin> (\<Union>X\<in>A. {i. 0 < count X i})"
hence "\<forall>X\<in>A. count X i \<le> 0" by (auto simp: count_eq_zero_iff)
- with assms have "(SUP X:A. count X i) \<le> 0"
+ with assms have "(SUP X\<in>A. count X i) \<le> 0"
by (intro cSup_least bdd_above_multiset_imp_bdd_above_count) auto
with pos show False by simp
qed
@@ -1115,7 +1115,7 @@
lemma count_Sup_multiset_nonempty:
assumes "A \<noteq> {}" "subset_mset.bdd_above A"
- shows "count (Sup A) x = (SUP X:A. count X x)"
+ shows "count (Sup A) x = (SUP X\<in>A. count X x)"
using assms by (simp add: Sup_multiset_def Abs_multiset_inverse Sup_multiset_in_multiset)
@@ -1127,7 +1127,7 @@
proof (rule mset_subset_eqI)
fix x
from \<open>X \<in> A\<close> have "A \<noteq> {}" by auto
- hence "count (Inf A) x = (INF X:A. count X x)"
+ hence "count (Inf A) x = (INF X\<in>A. count X x)"
by (simp add: count_Inf_multiset_nonempty)
also from \<open>X \<in> A\<close> have "\<dots> \<le> count X x"
by (intro cInf_lower) simp_all
@@ -1139,7 +1139,7 @@
show "X \<subseteq># Inf A"
proof (rule mset_subset_eqI)
fix x
- from nonempty have "count X x \<le> (INF X:A. count X x)"
+ from nonempty have "count X x \<le> (INF X\<in>A. count X x)"
by (intro cInf_greatest) (auto intro: mset_subset_eq_count le)
also from nonempty have "\<dots> = count (Inf A) x" by (simp add: count_Inf_multiset_nonempty)
finally show "count X x \<le> count (Inf A) x" .
@@ -1151,10 +1151,10 @@
proof (rule mset_subset_eqI)
fix x
from X have "A \<noteq> {}" by auto
- have "count X x \<le> (SUP X:A. count X x)"
+ have "count X x \<le> (SUP X\<in>A. count X x)"
by (intro cSUP_upper X bdd_above_multiset_imp_bdd_above_count bdd)
also from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
- have "(SUP X:A. count X x) = count (Sup A) x" by simp
+ have "(SUP X\<in>A. count X x) = count (Sup A) x" by simp
finally show "count X x \<le> count (Sup A) x" .
qed
next
@@ -1165,7 +1165,7 @@
proof (rule mset_subset_eqI)
fix x
from count_Sup_multiset_nonempty[OF \<open>A \<noteq> {}\<close> bdd]
- have "count (Sup A) x = (SUP X:A. count X x)" .
+ have "count (Sup A) x = (SUP X\<in>A. count X x)" .
also from nonempty have "\<dots> \<le> count X x"
by (intro cSup_least) (auto intro: mset_subset_eq_count ge)
finally show "count (Sup A) x \<le> count X x" .
--- a/src/HOL/Library/Product_Order.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Library/Product_Order.thy Thu Nov 08 09:11:52 2018 +0100
@@ -161,7 +161,7 @@
instantiation prod :: (Inf, Inf) Inf
begin
-definition "Inf A = (INF x:A. fst x, INF x:A. snd x)"
+definition "Inf A = (INF x\<in>A. fst x, INF x\<in>A. snd x)"
instance ..
@@ -170,7 +170,7 @@
instantiation prod :: (Sup, Sup) Sup
begin
-definition "Sup A = (SUP x:A. fst x, SUP x:A. snd x)"
+definition "Sup A = (SUP x\<in>A. fst x, SUP x\<in>A. snd x)"
instance ..
@@ -185,34 +185,34 @@
by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
-lemma fst_Sup: "fst (Sup A) = (SUP x:A. fst x)"
+lemma fst_Sup: "fst (Sup A) = (SUP x\<in>A. fst x)"
unfolding Sup_prod_def by simp
-lemma snd_Sup: "snd (Sup A) = (SUP x:A. snd x)"
+lemma snd_Sup: "snd (Sup A) = (SUP x\<in>A. snd x)"
unfolding Sup_prod_def by simp
-lemma fst_Inf: "fst (Inf A) = (INF x:A. fst x)"
+lemma fst_Inf: "fst (Inf A) = (INF x\<in>A. fst x)"
unfolding Inf_prod_def by simp
-lemma snd_Inf: "snd (Inf A) = (INF x:A. snd x)"
+lemma snd_Inf: "snd (Inf A) = (INF x\<in>A. snd x)"
unfolding Inf_prod_def by simp
-lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
+lemma fst_SUP: "fst (SUP x\<in>A. f x) = (SUP x\<in>A. fst (f x))"
using fst_Sup [of "f ` A", symmetric] by (simp add: comp_def)
-lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
+lemma snd_SUP: "snd (SUP x\<in>A. f x) = (SUP x\<in>A. snd (f x))"
using snd_Sup [of "f ` A", symmetric] by (simp add: comp_def)
-lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
+lemma fst_INF: "fst (INF x\<in>A. f x) = (INF x\<in>A. fst (f x))"
using fst_Inf [of "f ` A", symmetric] by (simp add: comp_def)
-lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
+lemma snd_INF: "snd (INF x\<in>A. f x) = (INF x\<in>A. snd (f x))"
using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
-lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
+lemma SUP_Pair: "(SUP x\<in>A. (f x, g x)) = (SUP x\<in>A. f x, SUP x\<in>A. g x)"
unfolding Sup_prod_def by (simp add: comp_def)
-lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
+lemma INF_Pair: "(INF x\<in>A. (f x, g x)) = (INF x\<in>A. f x, INF x\<in>A. g x)"
unfolding Inf_prod_def by (simp add: comp_def)
--- a/src/HOL/Probability/Discrete_Topology.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Discrete_Topology.thy Thu Nov 08 09:11:52 2018 +0100
@@ -19,7 +19,7 @@
where "dist_discrete n m = (if n = m then 0 else 1)"
definition uniformity_discrete :: "('a discrete \<times> 'a discrete) filter" where
- "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ "(uniformity::('a discrete \<times> 'a discrete) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition "open_discrete" :: "'a discrete set \<Rightarrow> bool" where
"(open::'a discrete set \<Rightarrow> bool) U \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
--- a/src/HOL/Probability/Distribution_Functions.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Distribution_Functions.thy Thu Nov 08 09:11:52 2018 +0100
@@ -220,13 +220,13 @@
and finite_borel_measure_interval_measure: "finite_borel_measure (interval_measure F)"
proof -
let ?F = "interval_measure F"
- { have "ennreal (m - 0) = (SUP i::nat. ennreal (F (real i) - F (- real i)))"
+ { have "ennreal (m - 0) = (SUP i. ennreal (F (real i) - F (- real i)))"
by (intro LIMSEQ_unique[OF _ LIMSEQ_SUP] tendsto_ennrealI tendsto_intros
lim_F_at_bot[THEN filterlim_compose] lim_F_at_top[THEN filterlim_compose]
lim_F_at_bot[THEN filterlim_compose] filterlim_real_sequentially
filterlim_uminus_at_top[THEN iffD1])
(auto simp: incseq_def nondecF intro!: diff_mono)
- also have "\<dots> = (SUP i::nat. emeasure ?F {- real i<..real i})"
+ also have "\<dots> = (SUP i. emeasure ?F {- real i<..real i})"
by (subst emeasure_interval_measure_Ioc) (simp_all add: nondecF right_cont_F)
also have "\<dots> = emeasure ?F (\<Union>i::nat. {- real i<..real i})"
by (rule SUP_emeasure_incseq) (auto simp: incseq_def)
--- a/src/HOL/Probability/Essential_Supremum.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Essential_Supremum.thy Thu Nov 08 09:11:52 2018 +0100
@@ -30,13 +30,13 @@
fix y assume "AE x in M. f x \<le> y"
then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}"
by simp
- then show "(INF P:{P. AE x in M. P x}. SUP x:Collect P. f x) \<le> y"
+ then show "(INF P\<in>{P. AE x in M. P x}. SUP x\<in>Collect P. f x) \<le> y"
by (rule INF_lower2) (auto intro: SUP_least)
next
fix P assume P: "AE x in M. P x"
- show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x:Collect P. f x)"
+ show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x\<in>Collect P. f x)"
proof (rule Inf_lower; clarsimp)
- show "AE x in M. f x \<le> (SUP x:Collect P. f x)"
+ show "AE x in M. f x \<le> (SUP x\<in>Collect P. f x)"
using P by (auto elim: eventually_mono simp: SUP_upper)
qed
qed
--- a/src/HOL/Probability/Fin_Map.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Fin_Map.thy Thu Nov 08 09:11:52 2018 +0100
@@ -258,7 +258,7 @@
definition [code del]:
"(uniformity :: (('a, 'b) fmap \<times> ('a \<Rightarrow>\<^sub>F 'b)) filter) =
- (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
instance
by standard (rule uniformity_fmap_def)
--- a/src/HOL/Probability/Giry_Monad.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy Thu Nov 08 09:11:52 2018 +0100
@@ -165,7 +165,7 @@
definition subprob_algebra :: "'a measure \<Rightarrow> 'a measure measure" where
"subprob_algebra K =
- (SUP A : sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
+ (SUP A \<in> sets K. vimage_algebra {M. subprob_space M \<and> sets M = sets K} (\<lambda>M. emeasure M A) borel)"
lemma space_subprob_algebra: "space (subprob_algebra A) = {M. subprob_space M \<and> sets M = sets A}"
by (auto simp add: subprob_algebra_def space_Sup_eq_UN)
--- a/src/HOL/Probability/Helly_Selection.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Helly_Selection.thy Thu Nov 08 09:11:52 2018 +0100
@@ -87,7 +87,7 @@
by auto
define F where "F x = Inf {lim (?f n) |n. x < r n}" for x
- have F_eq: "ereal (F x) = (INF n:{n. x < r n}. ereal (lim (?f n)))" for x
+ have F_eq: "ereal (F x) = (INF n\<in>{n. x < r n}. ereal (lim (?f n)))" for x
unfolding F_def by (subst ereal_Inf'[OF bdd_below nonempty]) (simp add: setcompr_eq_image)
have mono_F: "mono F"
using nonempty by (auto intro!: cInf_superset_mono simp: F_def bdd_below mono_def)
--- a/src/HOL/Probability/Projective_Family.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Projective_Family.thy Thu Nov 08 09:11:52 2018 +0100
@@ -470,7 +470,7 @@
next
assume *: "{i. J i \<subseteq> {0..< n}} \<noteq> {}"
have "(INF i. CI (J i) (X' i)) \<le>
- (INF i:{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
+ (INF i\<in>{i. J i \<subseteq> {0..<n}}. C 0 n (\<lambda>_. undefined) (PF.emb {0..<n} (J i) (X' i)))"
by (intro INF_superset_mono) (auto simp: emeasure_CI)
also have "\<dots> = C 0 n (\<lambda>_. undefined) (\<Inter>i\<in>{i. J i \<subseteq> {0..<n}}. (PF.emb {0..<n} (J i) (X' i)))"
using * by (intro emeasure_INT_decseq_subset[symmetric]) (auto intro!: dec_X' del: subsetI simp: sets_C)
--- a/src/HOL/Probability/Projective_Limit.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Projective_Limit.thy Thu Nov 08 09:11:52 2018 +0100
@@ -141,7 +141,7 @@
unfolding P'_def mapmeasure_def using J
by (auto intro!: prob_space_distr fm_measurable simp: measurable_cong_sets[OF sets_P])
- let ?SUP = "\<lambda>n. SUP K : {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"
+ let ?SUP = "\<lambda>n. SUP K \<in> {K. K \<subseteq> fm n ` (B n) \<and> compact K}. emeasure (P' n) K"
{ fix n
have "emeasure (P (J n)) (B n) = emeasure (P' n) (fm n ` (B n))"
using J by (auto simp: P'_def mapmeasure_PiM space_P sets_P)
@@ -169,7 +169,7 @@
have "?SUP n + 0 < ?SUP n + 2 powr (-n) * ?a"
using R[of n] unfolding ennreal_add_left_cancel_less ennreal_zero_less_mult_iff
by (auto intro: \<open>0 < ?a\<close>)
- also have "\<dots> = (SUP K:{K. K \<subseteq> fm n ` B n \<and> compact K}. emeasure (P' n) K + 2 powr (-n) * ?a)"
+ also have "\<dots> = (SUP K\<in>{K. K \<subseteq> fm n ` B n \<and> compact K}. emeasure (P' n) K + 2 powr (-n) * ?a)"
by (rule ennreal_SUP_add_left[symmetric]) auto
also have "\<dots> \<le> ?SUP n"
proof (intro SUP_least)
--- a/src/HOL/Probability/SPMF.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/SPMF.thy Thu Nov 08 09:11:52 2018 +0100
@@ -10,7 +10,7 @@
subsection \<open>Auxiliary material\<close>
-lemma cSUP_singleton [simp]: "(SUP x:{x}. f x :: _ :: conditionally_complete_lattice) = f x"
+lemma cSUP_singleton [simp]: "(SUP x\<in>{x}. f x :: _ :: conditionally_complete_lattice) = f x"
by (metis cSup_singleton image_empty image_insert)
subsubsection \<open>More about extended reals\<close>
@@ -33,18 +33,18 @@
unfolding continuous_def by auto
lemma ennreal_Sup:
- assumes *: "(SUP a:A. ennreal a) \<noteq> \<top>"
+ assumes *: "(SUP a\<in>A. ennreal a) \<noteq> \<top>"
and "A \<noteq> {}"
- shows "ennreal (Sup A) = (SUP a:A. ennreal a)"
+ shows "ennreal (Sup A) = (SUP a\<in>A. ennreal a)"
proof (rule continuous_at_Sup_mono)
- obtain r where r: "ennreal r = (SUP a:A. ennreal a)" "r \<ge> 0"
- using * by(cases "(SUP a:A. ennreal a)") simp_all
+ obtain r where r: "ennreal r = (SUP a\<in>A. ennreal a)" "r \<ge> 0"
+ using * by(cases "(SUP a\<in>A. ennreal a)") simp_all
then show "bdd_above A"
by(auto intro!: SUP_upper bdd_aboveI[of _ r] simp add: ennreal_le_iff[symmetric])
qed (auto simp: mono_def continuous_at_imp_continuous_at_within continuous_at_ennreal ennreal_leI assms)
lemma ennreal_SUP:
- "\<lbrakk> (SUP a:A. ennreal (f a)) \<noteq> \<top>; A \<noteq> {} \<rbrakk> \<Longrightarrow> ennreal (SUP a:A. f a) = (SUP a:A. ennreal (f a))"
+ "\<lbrakk> (SUP a\<in>A. ennreal (f a)) \<noteq> \<top>; A \<noteq> {} \<rbrakk> \<Longrightarrow> ennreal (SUP a\<in>A. f a) = (SUP a\<in>A. ennreal (f a))"
using ennreal_Sup[of "f ` A"] by auto
lemma ennreal_lt_0: "x < 0 \<Longrightarrow> ennreal x = 0"
@@ -333,9 +333,9 @@
lemma nn_integral_spmf_neq_top: "(\<integral>\<^sup>+ x. spmf p x \<partial>count_space UNIV) \<noteq> \<top>"
using nn_integral_measure_spmf[where f="\<lambda>_. 1", of p, symmetric] by simp
-lemma SUP_spmf_neq_top': "(SUP p:Y. ennreal (spmf p x)) \<noteq> \<top>"
+lemma SUP_spmf_neq_top': "(SUP p\<in>Y. ennreal (spmf p x)) \<noteq> \<top>"
proof(rule neq_top_trans)
- show "(SUP p:Y. ennreal (spmf p x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
+ show "(SUP p\<in>Y. ennreal (spmf p x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
qed simp
lemma SUP_spmf_neq_top: "(SUP i. ennreal (spmf (Y i) x)) \<noteq> \<top>"
@@ -343,9 +343,9 @@
show "(SUP i. ennreal (spmf (Y i) x)) \<le> 1" by(rule SUP_least)(simp add: pmf_le_1)
qed simp
-lemma SUP_emeasure_spmf_neq_top: "(SUP p:Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
+lemma SUP_emeasure_spmf_neq_top: "(SUP p\<in>Y. emeasure (measure_spmf p) A) \<noteq> \<top>"
proof(rule neq_top_trans)
- show "(SUP p:Y. emeasure (measure_spmf p) A) \<le> 1"
+ show "(SUP p\<in>Y. emeasure (measure_spmf p) A) \<le> 1"
by(rule SUP_least)(simp add: measure_spmf.subprob_emeasure_le_1)
qed simp
@@ -1228,7 +1228,7 @@
context fixes Y :: "'a spmf set" begin
definition lub_spmf :: "'a spmf"
-where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p : Y. ennreal (spmf p x)))"
+where "lub_spmf = embed_spmf (\<lambda>x. enn2real (SUP p \<in> Y. ennreal (spmf p x)))"
\<comment> \<open>We go through @{typ ennreal} to have a sensible definition even if @{term Y} is empty.\<close>
lemma lub_spmf_empty [simp]: "SPMF.lub_spmf {} = return_pmf None"
@@ -1339,7 +1339,7 @@
qed
qed simp
-lemma lub_spmf_subprob: "(\<integral>\<^sup>+ x. (SUP p : Y. ennreal (spmf p x)) \<partial>count_space UNIV) \<le> 1"
+lemma lub_spmf_subprob: "(\<integral>\<^sup>+ x. (SUP p \<in> Y. ennreal (spmf p x)) \<partial>count_space UNIV) \<le> 1"
proof(cases "Y = {}")
case True
thus ?thesis by(simp add: bot_ennreal)
@@ -1348,13 +1348,13 @@
let ?B = "\<Union>p\<in>Y. set_spmf p"
have countable: "countable ?B" by(rule spmf_chain_countable)
- have "(\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
- (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
+ have "(\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x)) \<partial>count_space UNIV) =
+ (\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x) * indicator ?B x) \<partial>count_space UNIV)"
by(intro nn_integral_cong SUP_cong)(auto split: split_indicator simp add: spmf_eq_0_set_spmf)
- also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x)) \<partial>count_space ?B)"
+ also have "\<dots> = (\<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x)) \<partial>count_space ?B)"
unfolding ennreal_indicator[symmetric] using False
by(subst SUP_mult_right_ennreal[symmetric])(simp add: ennreal_indicator nn_integral_count_space_indicator)
- also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B)" using False _ countable
+ also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ x. spmf p x \<partial>count_space ?B)" using False _ countable
by(rule nn_integral_monotone_convergence_SUP_countable)(rule chain_ord_spmf_eqD)
also have "\<dots> \<le> 1"
proof(rule SUP_least)
@@ -1373,23 +1373,23 @@
lemma spmf_lub_spmf:
assumes "Y \<noteq> {}"
- shows "spmf lub_spmf x = (SUP p : Y. spmf p x)"
+ shows "spmf lub_spmf x = (SUP p \<in> Y. spmf p x)"
proof -
from assms obtain p where "p \<in> Y" by auto
- have "spmf lub_spmf x = max 0 (enn2real (SUP p:Y. ennreal (spmf p x)))" unfolding lub_spmf_def
+ have "spmf lub_spmf x = max 0 (enn2real (SUP p\<in>Y. ennreal (spmf p x)))" unfolding lub_spmf_def
by(rule spmf_embed_spmf)(simp del: SUP_eq_top_iff Sup_eq_top_iff add: ennreal_enn2real_if SUP_spmf_neq_top' lub_spmf_subprob)
- also have "\<dots> = enn2real (SUP p:Y. ennreal (spmf p x))"
+ also have "\<dots> = enn2real (SUP p\<in>Y. ennreal (spmf p x))"
by(rule max_absorb2)(simp)
- also have "\<dots> = enn2real (ennreal (SUP p : Y. spmf p x))" using assms
+ also have "\<dots> = enn2real (ennreal (SUP p \<in> Y. spmf p x))" using assms
by(subst ennreal_SUP[symmetric])(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
also have "0 \<le> (\<Squnion>p\<in>Y. spmf p x)" using assms
by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] simp add: pmf_le_1)
- then have "enn2real (ennreal (SUP p : Y. spmf p x)) = (SUP p : Y. spmf p x)"
+ then have "enn2real (ennreal (SUP p \<in> Y. spmf p x)) = (SUP p \<in> Y. spmf p x)"
by(rule enn2real_ennreal)
finally show ?thesis .
qed
-lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
+lemma ennreal_spmf_lub_spmf: "Y \<noteq> {} \<Longrightarrow> ennreal (spmf lub_spmf x) = (SUP p\<in>Y. ennreal (spmf p x))"
unfolding spmf_lub_spmf by(subst ennreal_SUP)(simp_all add: SUP_spmf_neq_top' del: SUP_eq_top_iff Sup_eq_top_iff)
lemma lub_spmf_upper:
@@ -1398,7 +1398,7 @@
proof(rule ord_pmf_increaseI)
fix x
from p have [simp]: "Y \<noteq> {}" by auto
- from p have "ennreal (spmf p x) \<le> (SUP p:Y. ennreal (spmf p x))" by(rule SUP_upper)
+ from p have "ennreal (spmf p x) \<le> (SUP p\<in>Y. ennreal (spmf p x))" by(rule SUP_upper)
also have "\<dots> = ennreal (spmf lub_spmf x)" using p
by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' simp del: SUP_eq_top_iff Sup_eq_top_iff)
finally show "spmf p x \<le> spmf lub_spmf x" by simp
@@ -1413,7 +1413,7 @@
proof(rule ord_pmf_increaseI)
fix x
from nonempty obtain p where p: "p \<in> Y" by auto
- have "ennreal (spmf lub_spmf x) = (SUP p:Y. ennreal (spmf p x))"
+ have "ennreal (spmf lub_spmf x) = (SUP p\<in>Y. ennreal (spmf p x))"
by(subst spmf_lub_spmf)(auto simp add: ennreal_SUP SUP_spmf_neq_top' nonempty simp del: SUP_eq_top_iff Sup_eq_top_iff)
also have "\<dots> \<le> ennreal (spmf z x)" by(rule SUP_least)(simp add: ord_spmf_eq_leD z)
finally show "spmf lub_spmf x \<le> spmf z x" by simp
@@ -1438,16 +1438,16 @@
lemma emeasure_lub_spmf:
assumes Y: "Y \<noteq> {}"
- shows "emeasure (measure_spmf lub_spmf) A = (SUP y:Y. emeasure (measure_spmf y) A)"
+ shows "emeasure (measure_spmf lub_spmf) A = (SUP y\<in>Y. emeasure (measure_spmf y) A)"
(is "?lhs = ?rhs")
proof -
let ?M = "count_space (set_spmf lub_spmf)"
have "?lhs = \<integral>\<^sup>+ x. ennreal (spmf lub_spmf x) * indicator A x \<partial>?M"
by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf')
- also have "\<dots> = \<integral>\<^sup>+ x. (SUP y:Y. ennreal (spmf y x) * indicator A x) \<partial>?M"
+ also have "\<dots> = \<integral>\<^sup>+ x. (SUP y\<in>Y. ennreal (spmf y x) * indicator A x) \<partial>?M"
unfolding ennreal_indicator[symmetric]
by(simp add: spmf_lub_spmf assms ennreal_SUP[OF SUP_spmf_neq_top'] SUP_mult_right_ennreal)
- also from assms have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
+ also from assms have "\<dots> = (SUP y\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>?M)"
proof(rule nn_integral_monotone_convergence_SUP_countable)
have "(\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y = (\<lambda>f x. f x * indicator A x) ` (\<lambda>p x. ennreal (spmf p x)) ` Y"
by(simp add: image_image)
@@ -1455,7 +1455,7 @@
by(rule chain_imageI)(auto simp add: le_fun_def split: split_indicator)
finally show "Complete_Partial_Order.chain (\<le>) ((\<lambda>i x. ennreal (spmf i x) * indicator A x) ` Y)" .
qed simp
- also have "\<dots> = (SUP y:Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
+ also have "\<dots> = (SUP y\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf y x) * indicator A x \<partial>count_space UNIV)"
by(auto simp add: nn_integral_count_space_indicator set_lub_spmf spmf_eq_0_set_spmf split: split_indicator intro!: SUP_cong nn_integral_cong)
also have "\<dots> = ?rhs"
by(auto simp add: nn_integral_indicator[symmetric] nn_integral_measure_spmf)
@@ -1464,7 +1464,7 @@
lemma measure_lub_spmf:
assumes Y: "Y \<noteq> {}"
- shows "measure (measure_spmf lub_spmf) A = (SUP y:Y. measure (measure_spmf y) A)" (is "?lhs = ?rhs")
+ shows "measure (measure_spmf lub_spmf) A = (SUP y\<in>Y. measure (measure_spmf y) A)" (is "?lhs = ?rhs")
proof -
have "ennreal ?lhs = ennreal ?rhs"
using emeasure_lub_spmf[OF assms] SUP_emeasure_spmf_neq_top[of A Y] Y
@@ -1476,12 +1476,12 @@
lemma weight_lub_spmf:
assumes Y: "Y \<noteq> {}"
- shows "weight_spmf lub_spmf = (SUP y:Y. weight_spmf y)"
+ shows "weight_spmf lub_spmf = (SUP y\<in>Y. weight_spmf y)"
unfolding weight_spmf_def by(rule measure_lub_spmf) fact
lemma measure_spmf_lub_spmf:
assumes Y: "Y \<noteq> {}"
- shows "measure_spmf lub_spmf = (SUP p:Y. measure_spmf p)" (is "?lhs = ?rhs")
+ shows "measure_spmf lub_spmf = (SUP p\<in>Y. measure_spmf p)" (is "?lhs = ?rhs")
proof(rule measure_eqI)
from assms obtain p where p: "p \<in> Y" by auto
from chain have chain': "Complete_Partial_Order.chain (\<le>) (measure_spmf ` Y)"
@@ -1583,11 +1583,11 @@
let ?M = "count_space (set_spmf (lub_spmf Y))"
have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ x. ennreal (spmf (lub_spmf Y) x) * ennreal (spmf (f x) i) \<partial>?M"
by(auto simp add: ennreal_spmf_lub_spmf ennreal_spmf_bind nn_integral_measure_spmf')
- also have "\<dots> = \<integral>\<^sup>+ x. (SUP p:Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"
+ also have "\<dots> = \<integral>\<^sup>+ x. (SUP p\<in>Y. ennreal (spmf p x * spmf (f x) i)) \<partial>?M"
by(subst ennreal_spmf_lub_spmf[OF chain Y])(subst SUP_mult_right_ennreal, simp_all add: ennreal_mult Y)
- also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
+ also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ x. ennreal (spmf p x * spmf (f x) i) \<partial>?M)"
using Y chain' by(rule nn_integral_monotone_convergence_SUP_countable) simp
- also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf p f) i))"
+ also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf p f) i))"
by(auto simp add: ennreal_spmf_bind nn_integral_measure_spmf nn_integral_count_space_indicator set_lub_spmf[OF chain] in_set_spmf_iff_spmf ennreal_mult intro!: SUP_cong nn_integral_cong split: split_indicator)
also have "\<dots> = ennreal (spmf ?rhs i)" using chain'' by(simp add: ennreal_spmf_lub_spmf Y)
finally show "spmf ?lhs i = spmf ?rhs i" by simp
@@ -1619,12 +1619,12 @@
have chain''': "Complete_Partial_Order.chain (ord_spmf (=)) ((\<lambda>p. bind_spmf x (\<lambda>y. g y p)) ` Y)"
using chain by(rule chain_imageI)(rule monotone_bind_spmf2[OF g, THEN monotoneD])
- have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p:Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
+ have "ennreal (spmf ?lhs i) = \<integral>\<^sup>+ y. (SUP p\<in>Y. ennreal (spmf x y * spmf (g y p) i)) \<partial>count_space (set_spmf x)"
by(simp add: ennreal_spmf_bind ennreal_spmf_lub_spmf[OF chain'] Y nn_integral_measure_spmf' SUP_mult_left_ennreal ennreal_mult)
- also have "\<dots> = (SUP p:Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
+ also have "\<dots> = (SUP p\<in>Y. \<integral>\<^sup>+ y. ennreal (spmf x y * spmf (g y p) i) \<partial>count_space (set_spmf x))"
unfolding nn_integral_measure_spmf' using Y chain''
by(rule nn_integral_monotone_convergence_SUP_countable) simp
- also have "\<dots> = (SUP p:Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
+ also have "\<dots> = (SUP p\<in>Y. ennreal (spmf (bind_spmf x (\<lambda>y. g y p)) i))"
by(simp add: ennreal_spmf_bind nn_integral_measure_spmf' ennreal_mult)
also have "\<dots> = ennreal (spmf ?rhs i)" using chain'''
by(auto simp add: ennreal_spmf_lub_spmf Y)
@@ -1775,9 +1775,9 @@
by(auto simp add: weight_lub_spmf chain1 chain2 Y rel_spmf_weightD[OF R, symmetric] intro!: cSUP_least intro: cSUP_upper2[OF bdd_aboveI2[OF weight_spmf_le_1]])
fix A
- have "measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y:fst ` Y. measure (measure_spmf y) A)"
+ have "measure (measure_spmf (lub_spmf (fst ` Y))) A = (SUP y\<in>fst ` Y. measure (measure_spmf y) A)"
using chain1 Y1 by(rule measure_lub_spmf)
- also have "\<dots> \<le> (SUP y:snd ` Y. measure (measure_spmf y) {y. \<exists>x\<in>A. R x y})" using Y1
+ also have "\<dots> \<le> (SUP y\<in>snd ` Y. measure (measure_spmf y) {y. \<exists>x\<in>A. R x y})" using Y1
by(rule cSUP_least)(auto intro!: cSUP_upper2[OF bdd_aboveI2[OF measure_spmf.subprob_measure_le_1]] rel_spmf_measureD R)
also have "\<dots> = measure (measure_spmf (lub_spmf (snd ` Y))) {y. \<exists>x\<in>A. R x y}"
using chain2 Y2 by(rule measure_lub_spmf[symmetric])
--- a/src/HOL/Probability/Stream_Space.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Stream_Space.thy Thu Nov 08 09:11:52 2018 +0100
@@ -279,7 +279,7 @@
simp add: sets_PiM_eq_proj snth_in space sets cong: measurable_cong_sets)
lemma sets_stream_space_eq: "sets (stream_space M) =
- sets (SUP i:UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
+ sets (SUP i\<in>UNIV. vimage_algebra (streams (space M)) (\<lambda>s. s !! i) M)"
by (auto intro!: sets_stream_space_in_sets sets_Sup_in_sets sets_image_in_sets
measurable_Sup1 snth_in measurable_vimage_algebra1 del: subsetI
simp: space_Sup_eq_UN space_stream_space)
--- a/src/HOL/Probability/Weak_Convergence.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Probability/Weak_Convergence.thy Thu Nov 08 09:11:52 2018 +0100
@@ -53,7 +53,7 @@
by (auto intro!: cInf_lower bdd)
{ assume *: "I \<omega> \<le> x"
- have "\<omega> \<le> (INF s:{x. \<omega> \<le> f x}. f s)"
+ have "\<omega> \<le> (INF s\<in>{x. \<omega> \<le> f x}. f s)"
by (rule cINF_greatest[OF ne]) auto
also have "\<dots> = f (I \<omega>)"
using continuous_at_Inf_mono[OF mono cont ne bdd] ..
--- a/src/HOL/Real_Vector_Spaces.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy Thu Nov 08 09:11:52 2018 +0100
@@ -597,7 +597,7 @@
assumes dist_norm: "dist x y = norm (x - y)"
class uniformity_dist = dist + uniformity +
- assumes uniformity_dist: "uniformity = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ assumes uniformity_dist: "uniformity = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
begin
lemma eventually_uniformity_metric:
@@ -1133,7 +1133,7 @@
definition dist_real_def: "dist x y = \<bar>x - y\<bar>"
definition uniformity_real_def [code del]:
- "(uniformity :: (real \<times> real) filter) = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
+ "(uniformity :: (real \<times> real) filter) = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
definition open_real_def [code del]:
"open (U :: real set) \<longleftrightarrow> (\<forall>x\<in>U. eventually (\<lambda>(x', y). x' = x \<longrightarrow> y \<in> U) uniformity)"
@@ -1611,7 +1611,7 @@
subsection \<open>Filters and Limits on Metric Space\<close>
-lemma (in metric_space) nhds_metric: "nhds x = (INF e:{0 <..}. principal {y. dist y x < e})"
+lemma (in metric_space) nhds_metric: "nhds x = (INF e\<in>{0 <..}. principal {y. dist y x < e})"
unfolding nhds_def
proof (safe intro!: INF_eq)
fix S
--- a/src/HOL/Topological_Spaces.thy Wed Nov 07 23:03:45 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy Thu Nov 08 09:11:52 2018 +0100
@@ -517,7 +517,7 @@
by (auto simp: nhds_discrete filterlim_principal)
lemma (in topological_space) at_within_eq:
- "at x within s = (INF S:{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
+ "at x within s = (INF S\<in>{S. open S \<and> x \<in> S}. principal (S \<inter> s - {x}))"
unfolding nhds_def at_within_def
by (subst INF_inf_const2[symmetric]) (auto simp: Diff_Int_distrib)
@@ -575,7 +575,7 @@
by (simp add: at_eq_bot_iff not_open_singleton)
lemma (in order_topology) nhds_order:
- "nhds x = inf (INF a:{x <..}. principal {..< a}) (INF a:{..< x}. principal {a <..})"
+ "nhds x = inf (INF a\<in>{x <..}. principal {..< a}) (INF a\<in>{..< x}. principal {a <..})"
proof -
have 1: "{S \<in> range lessThan \<union> range greaterThan. x \<in> S} =
(\<lambda>a. {..< a}) ` {x <..} \<union> (\<lambda>a. {a <..}) ` {..< x}"
@@ -616,8 +616,8 @@
lemma (in linorder_topology) at_within_order:
assumes "UNIV \<noteq> {x}"
shows "at x within s =
- inf (INF a:{x <..}. principal ({..< a} \<inter> s - {x}))
- (INF a:{..< x}. principal ({a <..} \<inter> s - {x}))"
+ inf (INF a\<in>{x <..}. principal ({..< a} \<inter> s - {x}))
+ (INF a\<in>{..< x}. principal ({a <..} \<inter> s - {x}))"
proof (cases "{x <..} = {}" "{..< x} = {}" rule: case_split [case_product case_split])
case True_True
have "UNIV = {..< x} \<union> {x} \<union> {x <..}"
@@ -628,7 +628,7 @@
inf_principal[symmetric] INF_inf_const2 inf_sup_aci[where 'a="'a filter"])
lemma (in linorder_topology) at_left_eq:
- "y < x \<Longrightarrow> at_left x = (INF a:{..< x}. principal {a <..< x})"
+ "y < x \<Longrightarrow> at_left x = (INF a\<in>{..< x}. principal {a <..< x})"
by (subst at_within_order)
(auto simp: greaterThan_Int_greaterThan greaterThanLessThan_eq[symmetric] min.absorb2 INF_constant
intro!: INF_lower2 inf_absorb2)
@@ -639,7 +639,7 @@
by (subst eventually_INF_base) (auto simp: eventually_principal Ball_def)
lemma (in linorder_topology) at_right_eq:
- "x < y \<Longrightarrow> at_right x = (INF a:{x <..}. principal {x <..< a})"
+ "x < y \<Longrightarrow> at_right x = (INF a\<in>{x <..}. principal {x <..< a})"
by (subst at_within_order)
(auto simp: lessThan_Int_lessThan greaterThanLessThan_eq[symmetric] max.absorb2 INF_constant Int_commute
intro!: INF_lower2 inf_absorb1)
@@ -3039,11 +3039,11 @@
assumes "mono f"
and cont: "continuous (at_left (Sup S)) f"
and S: "S \<noteq> {}" "bdd_above S"
- shows "f (Sup S) = (SUP s:S. f s)"
+ shows "f (Sup S) = (SUP s\<in>S. f s)"
proof (rule antisym)
have f: "(f \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
using cont unfolding continuous_within .
- show "f (Sup S) \<le> (SUP s:S. f s)"
+ show "f (Sup S) \<le> (SUP s\<in>S. f s)"
proof cases
assume "Sup S \<in> S"
then show ?thesis
@@ -3057,8 +3057,8 @@
show ?thesis
proof (rule ccontr)
assume "\<not> ?thesis"
- with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "b < Sup S"
- and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s:S. f s) < f y"
+ with order_tendstoD(1)[OF f, of "SUP s\<in>S. f s"] obtain b where "b < Sup S"
+ and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> (SUP s\<in>S. f s) < f y"
by (auto simp: not_le eventually_at_left[OF \<open>s < Sup S\<close>])
with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "b < c"
using less_cSupD[of S b] by auto
@@ -3077,11 +3077,11 @@
assumes "antimono f"
and cont: "continuous (at_left (Sup S)) f"
and S: "S \<noteq> {}" "bdd_above S"
- shows "f (Sup S) = (INF s:S. f s)"
+ shows "f (Sup S) = (INF s\<in>S. f s)"
proof (rule antisym)
have f: "(f \<longlongrightarrow> f (Sup S)) (at_left (Sup S))"
using cont unfolding continuous_within .
- show "(INF s:S. f s) \<le> f (Sup S)"
+ show "(INF s\<in>S. f s) \<le> f (Sup S)"
proof cases
assume "Sup S \<in> S"
then show ?thesis
@@ -3095,8 +3095,8 @@
show ?thesis
proof (rule ccontr)
assume "\<not> ?thesis"
- with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "b < Sup S"
- and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s:S. f s)"
+ with order_tendstoD(2)[OF f, of "INF s\<in>S. f s"] obtain b where "b < Sup S"
+ and *: "\<And>y. b < y \<Longrightarrow> y < Sup S \<Longrightarrow> f y < (INF s\<in>S. f s)"
by (auto simp: not_le eventually_at_left[OF \<open>s < Sup S\<close>])
with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "b < c"
using less_cSupD[of S b] by auto
@@ -3115,11 +3115,11 @@
assumes "mono f"
and cont: "continuous (at_right (Inf S)) f"
and S: "S \<noteq> {}" "bdd_below S"
- shows "f (Inf S) = (INF s:S. f s)"
+ shows "f (Inf S) = (INF s\<in>S. f s)"
proof (rule antisym)
have f: "(f \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
using cont unfolding continuous_within .
- show "(INF s:S. f s) \<le> f (Inf S)"
+ show "(INF s\<in>S. f s) \<le> f (Inf S)"
proof cases
assume "Inf S \<in> S"
then show ?thesis
@@ -3133,8 +3133,8 @@
show ?thesis
proof (rule ccontr)
assume "\<not> ?thesis"
- with order_tendstoD(2)[OF f, of "INF s:S. f s"] obtain b where "Inf S < b"
- and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s:S. f s)"
+ with order_tendstoD(2)[OF f, of "INF s\<in>S. f s"] obtain b where "Inf S < b"
+ and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> f y < (INF s\<in>S. f s)"
by (auto simp: not_le eventually_at_right[OF \<open>Inf S < s\<close>])
with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "c < b"
using cInf_lessD[of S b] by auto
@@ -3153,11 +3153,11 @@
assumes "antimono f"
and cont: "continuous (at_right (Inf S)) f"
and S: "S \<noteq> {}" "bdd_below S"
- shows "f (Inf S) = (SUP s:S. f s)"
+ shows "f (Inf S) = (SUP s\<in>S. f s)"
proof (rule antisym)
have f: "(f \<longlongrightarrow> f (Inf S)) (at_right (Inf S))"
using cont unfolding continuous_within .
- show "f (Inf S) \<le> (SUP s:S. f s)"
+ show "f (Inf S) \<le> (SUP s\<in>S. f s)"
proof cases
assume "Inf S \<in> S"
then show ?thesis
@@ -3171,8 +3171,8 @@
show ?thesis
proof (rule ccontr)
assume "\<not> ?thesis"
- with order_tendstoD(1)[OF f, of "SUP s:S. f s"] obtain b where "Inf S < b"
- and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s:S. f s) < f y"
+ with order_tendstoD(1)[OF f, of "SUP s\<in>S. f s"] obtain b where "Inf S < b"
+ and *: "\<And>y. Inf S < y \<Longrightarrow> y < b \<Longrightarrow> (SUP s\<in>S. f s) < f y"
by (auto simp: not_le eventually_at_right[OF \<open>Inf S < s\<close>])
with \<open>S \<noteq> {}\<close> obtain c where "c \<in> S" "c < b"
using cInf_lessD[of S b] by auto
@@ -3529,14 +3529,14 @@
proof (subst prod_filter_INF, auto intro!: antisym INF_greatest simp: principal_prod_principal)
fix S T
assume "open S" "a \<in> S" "open T" "b \<in> T"
- then show "(INF x : {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
+ then show "(INF x \<in> {S. open S \<and> (a, b) \<in> S}. principal x) \<le> principal (S \<times> T)"
by (intro INF_lower) (auto intro!: open_Times)
next
fix S'
assume "open S'" "(a, b) \<in> S'"
then obtain S T where "open S" "a \<in> S" "open T" "b \<in> T" "S \<times> T \<subseteq> S'"
by (auto elim: open_prod_elim)
- then show "(INF x : {S. open S \<and> a \<in> S}. INF y : {S. open S \<and> b \<in> S}.
+ then show "(INF x \<in> {S. open S \<and> a \<in> S}. INF y \<in> {S. open S \<and> b \<in> S}.
principal (x \<times> y)) \<le> principal S'"
by (auto intro!: INF_lower2)
qed