consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
--- a/NEWS Tue Mar 18 21:02:33 2014 +0100
+++ b/NEWS Tue Mar 18 22:11:46 2014 +0100
@@ -98,8 +98,11 @@
*** HOL ***
+* Consolidated theorem names containing INFI and SUPR: have INF
+and SUP instead uniformly. INCOMPATIBILITY.
+
* More aggressive normalization of expressions involving INF and Inf
-or SUP and Sup. INCOMPATIBILITY.
+or SUP and Sup. INCOMPATIBILITY.
* INF_image and SUP_image do not unfold composition.
INCOMPATIBILITY.
--- a/src/HOL/Complete_Lattices.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy Tue Mar 18 22:11:46 2014 +0100
@@ -293,13 +293,13 @@
ultimately show ?thesis by (rule Sup_upper2)
qed
-lemma SUPR_eq:
+lemma SUP_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
-lemma INFI_eq:
+lemma INF_eq:
assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
--- a/src/HOL/Library/Extended_Real.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Library/Extended_Real.thy Tue Mar 18 22:11:46 2014 +0100
@@ -1421,16 +1421,16 @@
using INF_lower2[of _ A f u] INF_greatest[of A l f]
by (cases "INFI A f") auto
-lemma ereal_SUPR_uminus:
+lemma ereal_SUP_uminus:
fixes f :: "'a \<Rightarrow> ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
using ereal_Sup_uminus_image_eq[of "f`R"]
by (simp add: image_image)
-lemma ereal_INFI_uminus:
+lemma ereal_INF_uminus:
fixes f :: "'a \<Rightarrow> ereal"
shows "(INF i : R. - f i) = - (SUP i : R. f i)"
- using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
+ using ereal_SUP_uminus [of _ "\<lambda>x. - f x"] by simp
lemma ereal_image_uminus_shift:
fixes X Y :: "ereal set"
@@ -1539,7 +1539,7 @@
using real by (simp add: ereal_le_minus_iff)
qed (insert assms, auto)
-lemma SUPR_ereal_add:
+lemma SUP_ereal_add:
fixes f g :: "nat \<Rightarrow> ereal"
assumes "incseq f"
and "incseq g"
@@ -1575,18 +1575,18 @@
by (simp add: ac_simps)
qed (auto intro!: add_mono SUP_upper)
-lemma SUPR_ereal_add_pos:
+lemma SUP_ereal_add_pos:
fixes f g :: "nat \<Rightarrow> ereal"
assumes inc: "incseq f" "incseq g"
and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
-proof (intro SUPR_ereal_add inc)
+proof (intro SUP_ereal_add inc)
fix i
show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
using pos[of i] by auto
qed
-lemma SUPR_ereal_setsum:
+lemma SUP_ereal_setsum:
fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
@@ -1594,13 +1594,13 @@
proof (cases "finite A")
case True
then show ?thesis using assms
- by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
+ by induct (auto simp: incseq_setsumI2 setsum_nonneg SUP_ereal_add_pos)
next
case False
then show ?thesis by simp
qed
-lemma SUPR_ereal_cmult:
+lemma SUP_ereal_cmult:
fixes f :: "nat \<Rightarrow> ereal"
assumes "\<And>i. 0 \<le> f i"
and "0 \<le> c"
@@ -1675,7 +1675,7 @@
qed
qed
-lemma Sup_countable_SUPR:
+lemma Sup_countable_SUP:
assumes "A \<noteq> {}"
shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
proof (cases "Sup A")
@@ -1770,9 +1770,9 @@
using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
qed
-lemma SUPR_countable_SUPR:
+lemma SUP_countable_SUP:
"A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
- using Sup_countable_SUPR[of "g`A"]
+ using Sup_countable_SUP [of "g`A"]
by auto
lemma Sup_ereal_cadd:
@@ -1807,7 +1807,7 @@
using Sup_ereal_cadd [of "uminus ` A" a] assms
unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
-lemma SUPR_ereal_cminus:
+lemma SUP_ereal_cminus:
fixes f :: "'i \<Rightarrow> ereal"
fixes A
assumes "A \<noteq> {}"
@@ -1834,7 +1834,7 @@
by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
qed
-lemma INFI_ereal_cminus:
+lemma INF_ereal_cminus:
fixes a :: ereal
assumes "A \<noteq> {}"
and "\<bar>a\<bar> \<noteq> \<infinity>"
@@ -1848,7 +1848,7 @@
shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
by (cases rule: ereal2_cases[of a b]) auto
-lemma INFI_ereal_add:
+lemma INF_ereal_add:
fixes f :: "nat \<Rightarrow> ereal"
assumes "decseq f" "decseq g"
and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
@@ -1864,10 +1864,10 @@
then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
by simp
also have "\<dots> = INFI UNIV f + INFI UNIV g"
- unfolding ereal_INFI_uminus
+ unfolding ereal_INF_uminus
using assms INF_less
- by (subst SUPR_ereal_add)
- (auto simp: ereal_SUPR_uminus intro!: uminus_ereal_add_uminus_uminus)
+ by (subst SUP_ereal_add)
+ (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
finally show ?thesis .
qed
@@ -2430,7 +2430,7 @@
lemma ereal_Limsup_uminus:
fixes f :: "'a \<Rightarrow> ereal"
shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
- unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
+ unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
lemma liminf_bounded_iff:
fixes x :: "nat \<Rightarrow> ereal"
--- a/src/HOL/Library/Liminf_Limsup.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Library/Liminf_Limsup.thy Tue Mar 18 22:11:46 2014 +0100
@@ -20,12 +20,12 @@
unfolding INF_le_iff
by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
-lemma SUPR_pair:
+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))"
by (rule antisym) (auto intro!: SUP_least SUP_upper2)
-lemma INFI_pair:
+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))"
by (rule antisym) (auto intro!: INF_greatest INF_lower2)
@@ -52,13 +52,13 @@
(\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
unfolding Limsup_def by (auto intro!: INF_eqI)
-lemma liminf_SUPR_INFI: "liminf f = (SUP n. INF m:{n..}. f m)"
+lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
unfolding Liminf_def eventually_sequentially
- by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
+ by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
-lemma limsup_INFI_SUPR: "limsup f = (INF n. SUP m:{n..}. f m)"
+lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
unfolding Limsup_def eventually_sequentially
- by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
+ by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
lemma Limsup_const:
assumes ntriv: "\<not> trivial_limit F"
@@ -292,7 +292,7 @@
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 `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
qed
- then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
+ then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
qed
lemma limsup_subseq_mono:
@@ -305,7 +305,7 @@
fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
qed
- then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
+ then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
qed
end
--- a/src/HOL/Library/Product_Order.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy Tue Mar 18 22:11:46 2014 +0100
@@ -218,26 +218,14 @@
text {* Alternative formulations for set infima and suprema over the product
of two complete lattices: *}
-lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
-by (auto simp: Inf_prod_def)
-
-lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
-by (auto simp: Sup_prod_def)
-
-lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
+lemma INF_prod_alt_def:
+ "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
unfolding INF_def Inf_prod_def by simp
-lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
+lemma SUP_prod_alt_def:
+ "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
unfolding SUP_def Sup_prod_def by simp
-lemma INF_prod_alt_def:
- "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
- by (simp add: INFI_prod_alt_def comp_def)
-
-lemma SUP_prod_alt_def:
- "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
- by (simp add: SUPR_prod_alt_def comp_def)
-
subsection {* Complete distributive lattices *}
@@ -247,10 +235,10 @@
(complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
proof
case goal1 thus ?case
- by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
+ by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
next
case goal2 thus ?case
- by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
+ by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
qed
end
--- a/src/HOL/Library/RBT_Set.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Library/RBT_Set.thy Tue Mar 18 22:11:46 2014 +0100
@@ -757,7 +757,7 @@
declare Inf'_def[symmetric, code_unfold]
declare Inf_Set_fold[folded Inf'_def, code]
-lemma INFI_Set_fold [code]:
+lemma INF_Set_fold [code]:
fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
proof -
@@ -798,7 +798,7 @@
declare Sup'_def[symmetric, code_unfold]
declare Sup_Set_fold[folded Sup'_def, code]
-lemma SUPR_Set_fold [code]:
+lemma SUP_Set_fold [code]:
fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
proof -
--- a/src/HOL/Lifting_Set.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Lifting_Set.thy Tue Mar 18 22:11:46 2014 +0100
@@ -149,14 +149,14 @@
rel_set rel_set"
unfolding rel_fun_def rel_set_def by fast
-lemma SUPR_parametric [transfer_rule]:
+lemma SUP_parametric [transfer_rule]:
"(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
proof(rule rel_funI)+
fix A B f and g :: "'b \<Rightarrow> 'c"
assume AB: "rel_set R A B"
and fg: "(R ===> op =) f g"
show "SUPR A f = SUPR B g"
- by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] rel_funD[OF fg] intro: rev_bexI)
+ by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
qed
lemma bind_transfer [transfer_rule]:
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Tue Mar 18 22:11:46 2014 +0100
@@ -537,10 +537,10 @@
next
case (real r)
then show ?thesis
- unfolding liminf_SUPR_INFI limsup_INFI_SUPR
- apply (subst INFI_ereal_cminus)
+ unfolding liminf_SUP_INF limsup_INF_SUP
+ apply (subst INF_ereal_cminus)
apply auto
- apply (subst SUPR_ereal_cminus)
+ apply (subst SUP_ereal_cminus)
apply auto
done
qed (insert `c \<noteq> -\<infinity>`, simp)
@@ -874,7 +874,7 @@
unfolding summable_def
by auto
-lemma suminf_ereal_eq_SUPR:
+lemma suminf_ereal_eq_SUP:
fixes f :: "nat \<Rightarrow> ereal"
assumes "\<And>i. 0 \<le> f i"
shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
@@ -917,7 +917,7 @@
fixes f :: "nat \<Rightarrow> ereal"
assumes "\<And>n. 0 \<le> f n"
shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
- unfolding suminf_ereal_eq_SUPR[OF assms]
+ unfolding suminf_ereal_eq_SUP [OF assms]
by (auto intro: complete_lattice_class.SUP_upper)
lemma suminf_0_le:
@@ -956,9 +956,9 @@
assumes "\<And>i. 0 \<le> f i"
and "\<And>i. 0 \<le> g i"
shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
- apply (subst (1 2 3) suminf_ereal_eq_SUPR)
+ apply (subst (1 2 3) suminf_ereal_eq_SUP)
unfolding setsum_addf
- apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
+ apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
done
lemma suminf_cmult_ereal:
@@ -967,8 +967,8 @@
and "0 \<le> a"
shows "(\<Sum>i. a * f i) = a * suminf f"
by (auto simp: setsum_ereal_right_distrib[symmetric] assms
- ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
- intro!: SUPR_ereal_cmult )
+ ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
+ intro!: SUP_ereal_cmult)
lemma suminf_PInfty:
fixes f :: "nat \<Rightarrow> ereal"
@@ -1107,12 +1107,12 @@
fix n :: nat
have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
using assms
- by (auto intro!: SUPR_ereal_setsum[symmetric])
+ by (auto intro!: SUP_ereal_setsum [symmetric])
}
note * = this
show ?thesis
using assms
- apply (subst (1 2) suminf_ereal_eq_SUPR)
+ apply (subst (1 2) suminf_ereal_eq_SUP)
unfolding *
apply (auto intro!: SUP_upper2)
apply (subst SUP_commute)
@@ -1161,7 +1161,7 @@
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)"
unfolding Liminf_def eventually_at
-proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
+proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
fix P d
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
@@ -1181,7 +1181,7 @@
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)"
unfolding Limsup_def eventually_at
-proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
+proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
fix P d
assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
--- a/src/HOL/Predicate.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Predicate.thy Tue Mar 18 22:11:46 2014 +0100
@@ -83,11 +83,11 @@
end
-lemma eval_INFI [simp]:
+lemma eval_INF [simp]:
"eval (INFI A f) = INFI A (eval \<circ> f)"
using eval_Inf [of "f ` A"] by simp
-lemma eval_SUPR [simp]:
+lemma eval_SUP [simp]:
"eval (SUPR A f) = SUPR A (eval \<circ> f)"
using eval_Sup [of "f ` A"] by simp
--- a/src/HOL/Probability/Borel_Space.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Borel_Space.thy Tue Mar 18 22:11:46 2014 +0100
@@ -1111,7 +1111,7 @@
assumes "\<And>i. f i \<in> borel_measurable M"
shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
- unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
+ unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
lemma sets_Collect_eventually_sequentially[measurable]:
"(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
--- a/src/HOL/Probability/Caratheodory.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Caratheodory.thy Tue Mar 18 22:11:46 2014 +0100
@@ -40,9 +40,9 @@
by (auto intro!: setsum_mono3 simp: pos) }
ultimately
show ?thesis unfolding g_def using pos
- by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex SUP_upper2
- setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair
- SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
+ by (auto intro!: SUP_eq simp: setsum_cartesian_product reindex SUP_upper2
+ setsum_nonneg suminf_ereal_eq_SUP SUP_pair
+ SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
qed
subsection {* Measure Spaces *}
--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 18 22:11:46 2014 +0100
@@ -946,18 +946,18 @@
have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB i))"
unfolding simple_integral_indicator[OF B `simple_function M u`]
- proof (subst SUPR_ereal_setsum, safe)
+ proof (subst SUP_ereal_setsum, safe)
fix x n assume "x \<in> space M"
with u_range show "incseq (\<lambda>i. u x * (emeasure M) (?B' (u x) i))" "\<And>i. 0 \<le> u x * (emeasure M) (?B' (u x) i)"
using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff)
next
show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
using measure_conv u_range B_u unfolding simple_integral_def
- by (auto intro!: setsum_cong SUPR_ereal_cmult[symmetric])
+ by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric])
qed
moreover
have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
- apply (subst SUPR_ereal_cmult[symmetric])
+ apply (subst SUP_ereal_cmult [symmetric])
proof (safe intro!: SUP_mono bexI)
fix i
have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
@@ -1120,8 +1120,8 @@
by auto }
then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
- by (subst SUPR_ereal_cmult[symmetric, OF u(6) `0 \<le> a`])
- (auto intro!: SUPR_ereal_add
+ by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
+ (auto intro!: SUP_ereal_add
simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) }
then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
@@ -1132,8 +1132,8 @@
finally have "(\<integral>\<^sup>+ x. max 0 (a * f x + g x) \<partial>M) = a * (\<integral>\<^sup>+x. max 0 (f x) \<partial>M) + (\<integral>\<^sup>+x. max 0 (g x) \<partial>M)"
unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
- apply (subst SUPR_ereal_cmult[symmetric, OF pos(1) `0 \<le> a`])
- apply (subst SUPR_ereal_add[symmetric, OF inc not_MInf]) .
+ apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
+ apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
then show ?thesis by (simp add: positive_integral_max_0)
qed
@@ -1277,14 +1277,14 @@
have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x"
using assms by (auto simp: AE_all_countable)
have "(\<Sum>i. integral\<^sup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>P M (f i))"
- using positive_integral_positive by (rule suminf_ereal_eq_SUPR)
+ using positive_integral_positive by (rule suminf_ereal_eq_SUP)
also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)"
unfolding positive_integral_setsum[OF f] ..
also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
(elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
- by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUPR)
+ by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
finally show ?thesis by simp
qed
@@ -1297,11 +1297,11 @@
have pos: "AE x in M. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
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)"
- unfolding liminf_SUPR_INFI using pos u
+ unfolding liminf_SUP_INF using pos u
by (intro positive_integral_monotone_convergence_SUP_AE)
(elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
- unfolding liminf_SUPR_INFI
+ unfolding liminf_SUP_INF
by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
finally show ?thesis .
qed
@@ -2749,7 +2749,7 @@
next
case (seq U)
from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
- by eventually_elim (simp add: SUPR_ereal_cmult seq)
+ by eventually_elim (simp add: SUP_ereal_cmult seq)
from seq f show ?case
apply (simp add: positive_integral_monotone_convergence_SUP)
apply (subst positive_integral_cong_AE[OF eq])
--- a/src/HOL/Probability/Measure_Space.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Measure_Space.thy Tue Mar 18 22:11:46 2014 +0100
@@ -55,7 +55,7 @@
from this[of "Suc i"] show "f i \<le> y" by auto
qed (insert assms, simp)
ultimately show ?thesis using assms
- by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def)
+ by (subst suminf_ereal_eq_SUP) (auto simp: indicator_def)
qed
lemma suminf_indicator:
@@ -375,7 +375,7 @@
by auto
ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
using A(4) f_fin f_Int_fin
- by (subst INFI_ereal_add) (auto simp: decseq_f)
+ by (subst INF_ereal_add) (auto simp: decseq_f)
moreover {
fix n
have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
@@ -543,10 +543,10 @@
have A0: "0 \<le> emeasure M (A 0)" using A by auto
have "emeasure M (A 0) - (INF n. emeasure M (A n)) = emeasure M (A 0) + (SUP n. - emeasure M (A n))"
- by (simp add: ereal_SUPR_uminus minus_ereal_def)
+ by (simp add: ereal_SUP_uminus minus_ereal_def)
also have "\<dots> = (SUP n. emeasure M (A 0) - emeasure M (A n))"
unfolding minus_ereal_def using A0 assms
- by (subst SUPR_ereal_add) (auto simp add: decseq_emeasure)
+ by (subst SUP_ereal_add) (auto simp add: decseq_emeasure)
also have "\<dots> = (SUP n. emeasure M (A 0 - A n))"
using A finite `decseq A`[unfolded decseq_def] by (subst emeasure_Diff) auto
also have "\<dots> = emeasure M (\<Union>i. A 0 - A i)"
--- a/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Radon_Nikodym.thy Tue Mar 18 22:11:46 2014 +0100
@@ -354,7 +354,7 @@
from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \<le> N (space M)"
by (simp cong: positive_integral_cong)
qed
- from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
+ from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n"
proof safe
fix n assume "range ys \<subseteq> integral\<^sup>P M ` G"
@@ -540,7 +540,7 @@
by (auto intro!: SUP_least emeasure_mono)
then have "?a \<noteq> \<infinity>" using finite_emeasure_space
by auto
- from SUPR_countable_SUPR[OF Q_not_empty, of "emeasure M"]
+ from SUP_countable_SUP [OF Q_not_empty, of "emeasure M"]
obtain Q'' where "range Q'' \<subseteq> emeasure M ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
by auto
then have "\<forall>i. \<exists>Q'. Q'' i = emeasure M Q' \<and> Q' \<in> ?Q" by auto
--- a/src/HOL/Probability/Regularity.thy Tue Mar 18 21:02:33 2014 +0100
+++ b/src/HOL/Probability/Regularity.thy Tue Mar 18 22:11:46 2014 +0100
@@ -312,7 +312,7 @@
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)"
- unfolding inner by (subst INFI_ereal_cminus) force+
+ unfolding inner by (subst INF_ereal_cminus) force+
also have "\<dots> = (INF U:{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))"
@@ -331,7 +331,7 @@
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)"
- unfolding outer by (subst SUPR_ereal_cminus) auto
+ unfolding outer by (subst SUP_ereal_cminus) auto
also have "\<dots> = (SUP U:{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)"