--- a/src/HOL/Complete_Lattices.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Complete_Lattices.thy Wed Sep 14 10:08:52 2011 -0400
@@ -1150,19 +1150,6 @@
"\<Squnion>{a, b} = a \<squnion> b"
by simp
-lemmas (in complete_lattice) INFI_def = INF_def
-lemmas (in complete_lattice) SUPR_def = SUP_def
-lemmas (in complete_lattice) INF_leI = INF_lower
-lemmas (in complete_lattice) INF_leI2 = INF_lower2
-lemmas (in complete_lattice) le_INFI = INF_greatest
-lemmas (in complete_lattice) le_SUPI = SUP_upper
-lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
-lemmas (in complete_lattice) SUP_leI = SUP_least
-lemmas (in complete_lattice) less_INFD = less_INF_D
-
-lemmas INFI_apply = INF_apply
-lemmas SUPR_apply = SUP_apply
-
text {* Grep and put to news from here *}
lemma (in complete_lattice) INF_eq:
@@ -1196,9 +1183,6 @@
"\<Inter>S = (\<Inter>x\<in>S. x)"
by (simp add: INTER_eq_Inter_image image_def)
-lemmas INTER_def = INTER_eq
-lemmas UNION_def = UNION_eq
-
lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
by (fact INF_eq)
--- a/src/HOL/Finite_Set.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Finite_Set.thy Wed Sep 14 10:08:52 2011 -0400
@@ -784,7 +784,7 @@
interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?inf"
by (induct A arbitrary: B)
- (simp_all add: INFI_def inf_left_commute)
+ (simp_all add: INF_def inf_left_commute)
qed
lemma sup_SUPR_fold_sup:
@@ -795,7 +795,7 @@
interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
from `finite A` show "?fold = ?sup"
by (induct A arbitrary: B)
- (simp_all add: SUPR_def sup_left_commute)
+ (simp_all add: SUP_def sup_left_commute)
qed
lemma INFI_fold_inf:
--- a/src/HOL/Fun.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Fun.thy Wed Sep 14 10:08:52 2011 -0400
@@ -181,7 +181,7 @@
assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
shows "inj_on f (\<Union> i \<in> I. A i)"
-proof(unfold inj_on_def UNION_def, auto)
+proof(unfold inj_on_def UNION_eq, auto)
fix i j x y
assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
and ***: "f x = f y"
--- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Wed Sep 14 10:08:52 2011 -0400
@@ -270,7 +270,7 @@
lemmas my_simp_list = list_lemmas fst_conv snd_conv
not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
Collect_mem_eq ball_simps option.simps primrecdef_list
-lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length
+lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
ML {*
val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}])
--- a/src/HOL/Library/Continuity.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/Continuity.thy Wed Sep 14 10:08:52 2011 -0400
@@ -21,12 +21,12 @@
lemma SUP_nat_conv:
"(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
apply(rule order_antisym)
- apply(rule SUP_leI)
+ apply(rule SUP_least)
apply(case_tac n)
apply simp
- apply (fast intro:le_SUPI le_supI2)
+ apply (fast intro:SUP_upper le_supI2)
apply(simp)
-apply (blast intro:SUP_leI le_SUPI)
+apply (blast intro:SUP_least SUP_upper)
done
lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
@@ -61,7 +61,7 @@
also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
finally show ?case .
qed }
- hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
+ hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least)
moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
proof (rule lfp_lowerbound)
have "chain(%i. (F ^^ i) bot)"
@@ -75,7 +75,7 @@
thus ?thesis by(auto simp add:chain_def)
qed
hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
- also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
+ also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper)
finally show "F ?U \<le> ?U" .
qed
ultimately show ?thesis by (blast intro:order_antisym)
--- a/src/HOL/Library/Extended_Real.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/Extended_Real.thy Wed Sep 14 10:08:52 2011 -0400
@@ -30,11 +30,11 @@
lemma SUPR_pair:
"(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_leI le_SUPI2)
+ by (rule antisym) (auto intro!: SUP_least SUP_upper2)
lemma INFI_pair:
"(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
- by (rule antisym) (auto intro!: le_INFI INF_leI2)
+ by (rule antisym) (auto intro!: INF_greatest INF_lower2)
subsection {* Definition and basic properties *}
@@ -1252,7 +1252,7 @@
lemma ereal_SUPR_uminus:
fixes f :: "'a => ereal"
shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
- unfolding SUPR_def INFI_def
+ unfolding SUP_def INF_def
using ereal_Sup_uminus_image_eq[of "f`R"]
by (simp add: image_image)
@@ -1313,7 +1313,7 @@
assumes "!!i. i : A ==> f i <= x"
assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
shows "(SUP i:A. f i) = x"
- unfolding SUPR_def Sup_ereal_def
+ unfolding SUP_def Sup_ereal_def
using assms by (auto intro!: Least_equality)
lemma ereal_INFI:
@@ -1321,7 +1321,7 @@
assumes "!!i. i : A ==> f i >= x"
assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
shows "(INF i:A. f i) = x"
- unfolding INFI_def Inf_ereal_def
+ unfolding INF_def Inf_ereal_def
using assms by (auto intro!: Greatest_equality)
lemma Sup_ereal_close:
@@ -1364,13 +1364,13 @@
{ assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
from this obtain i where "i : A & y <= f i" using `?rhs` by auto
- hence "y <= (SUP i:A. f i)" using le_SUPI[of i A f] by auto
+ hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
hence False using y_def by auto
} hence "?lhs" by auto
}
moreover
{ assume "?lhs" hence "?rhs"
- by (metis SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
+ by (metis SUP_least assms atLeastatMost_empty atLeastatMost_empty_iff
inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
} ultimately show ?thesis by auto
qed
@@ -1384,13 +1384,13 @@
{ assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
from this obtain i where "i : A & f i <= y" using `?rhs` by auto
- hence "(INF i:A. f i) <= y" using INF_leI[of i A f] by auto
+ hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
hence False using y_def by auto
} hence "?lhs" by auto
}
moreover
{ assume "?lhs" hence "?rhs"
- by (metis le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
+ by (metis INF_greatest assms atLeastatMost_empty atLeastatMost_empty_iff
inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
} ultimately show ?thesis by auto
qed
@@ -1402,7 +1402,7 @@
proof(rule ccontr)
assume "~ (EX i. i : A & f i <= x)"
hence "ALL i:A. f i > x" by auto
- hence "(INF i:A. f i) >= x" apply (subst le_INFI) by auto
+ hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto
thus False using assms by auto
qed
@@ -1411,7 +1411,7 @@
shows "(INF e:A. f e) = (INF e:A. g e)"
proof-
have "f ` A = g ` A" unfolding image_def using assms by auto
-thus ?thesis unfolding INFI_def by auto
+thus ?thesis unfolding INF_def by auto
qed
lemma same_SUP:
@@ -1419,7 +1419,7 @@
shows "(SUP e:A. f e) = (SUP e:A. g e)"
proof-
have "f ` A = g ` A" unfolding image_def using assms by auto
-thus ?thesis unfolding SUPR_def by auto
+thus ?thesis unfolding SUP_def by auto
qed
lemma SUPR_eq:
@@ -1428,9 +1428,9 @@
shows "(SUP i:A. f i) = (SUP j:B. g j)"
proof (intro antisym)
show "(SUP i:A. f i) \<le> (SUP j:B. g j)"
- using assms by (metis SUP_leI le_SUPI2)
+ using assms by (metis SUP_least SUP_upper2)
show "(SUP i:B. g i) \<le> (SUP j:A. f j)"
- using assms by (metis SUP_leI le_SUPI2)
+ using assms by (metis SUP_least SUP_upper2)
qed
lemma SUP_ereal_le_addI:
@@ -1440,7 +1440,7 @@
proof (cases y)
case (real r)
then have "\<And>i. f i \<le> z - y" using assms by (simp add: ereal_le_minus_iff)
- then have "SUPR UNIV f \<le> z - y" by (rule SUP_leI)
+ then have "SUPR UNIV f \<le> z - y" by (rule SUP_least)
then show ?thesis using real by (simp add: ereal_le_minus_iff)
qed (insert assms, auto)
@@ -1451,7 +1451,7 @@
proof (rule ereal_SUPI)
fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
- unfolding SUPR_def Sup_eq_MInfty by (auto dest: image_eqD)
+ unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
{ fix j
{ fix i
have "f i + g j \<le> f i + g (max i j)"
@@ -1466,7 +1466,7 @@
then have "SUPR UNIV g + SUPR UNIV f \<le> y"
using f by (rule SUP_ereal_le_addI)
then show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
-qed (auto intro!: add_mono le_SUPI)
+qed (auto intro!: add_mono SUP_upper)
lemma SUPR_ereal_add_pos:
fixes f g :: "nat \<Rightarrow> ereal"
@@ -1489,7 +1489,7 @@
fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
shows "(SUP i. c * f i) = c * SUPR UNIV f"
proof (rule ereal_SUPI)
- fix i have "f i \<le> SUPR UNIV f" by (rule le_SUPI) auto
+ fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
then show "c * f i \<le> c * SUPR UNIV f"
using `0 \<le> c` by (rule ereal_mult_left_mono)
next
@@ -1498,7 +1498,7 @@
proof cases
assume c: "0 < c \<and> c \<noteq> \<infinity>"
with * have "SUPR UNIV f \<le> y / c"
- by (intro SUP_leI) (auto simp: ereal_le_divide_pos)
+ by (intro SUP_least) (auto simp: ereal_le_divide_pos)
with c show ?thesis
by (auto simp: ereal_le_divide_pos)
next
@@ -1507,7 +1507,7 @@
assume "\<forall>i. f i = 0"
moreover then have "range f = {0}" by auto
ultimately show "c * SUPR UNIV f \<le> y" using *
- by (auto simp: SUPR_def min_max.sup_absorb1)
+ by (auto simp: SUP_def min_max.sup_absorb1)
next
assume "\<not> (\<forall>i. f i = 0)"
then obtain i where "f i \<noteq> 0" by auto
@@ -1522,7 +1522,7 @@
fixes f :: "'a \<Rightarrow> ereal"
assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
shows "(SUP i:A. f i) = \<infinity>"
- unfolding SUPR_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
+ unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
apply simp
proof safe
fix x :: ereal assume "x \<noteq> \<infinity>"
@@ -1616,7 +1616,7 @@
lemma SUPR_countable_SUPR:
"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"] by (auto simp: SUPR_def)
+ using Sup_countable_SUPR[of "g`A"] by (auto simp: SUP_def)
lemma Sup_ereal_cadd:
fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
@@ -1649,7 +1649,7 @@
fixes A assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
using Sup_ereal_cminus[of "f`A" a] assms
- unfolding SUPR_def INFI_def image_image by auto
+ unfolding SUP_def INF_def image_image by auto
lemma Inf_ereal_cminus:
fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
@@ -1667,7 +1667,7 @@
fixes a :: ereal assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
using Inf_ereal_cminus[of "f`A" a] assms
- unfolding SUPR_def INFI_def image_image
+ unfolding SUP_def INF_def image_image
by auto
lemma uminus_ereal_add_uminus_uminus:
@@ -2358,14 +2358,14 @@
fix y assume "y < x"
with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
- also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro le_SUPI) auto
+ also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro SUP_upper) auto
finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
qed
next
show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
- proof (unfold SUPR_def, safe intro!: Sup_mono bexI)
+ proof (unfold SUP_def, safe intro!: Sup_mono bexI)
fix y n assume "y < INFI {n..} f"
- from less_INFD[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
+ from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
qed (rule order_refl)
qed
@@ -2418,14 +2418,14 @@
fix B assume "B < C" "C \<le> liminf x"
then have "B < liminf x" by auto
then obtain N where "B < (INF m:{N..}. x m)"
- unfolding liminf_SUPR_INFI SUPR_def less_Sup_iff by auto
- from less_INFD[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
+ unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
+ from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
next
assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
{ fix B assume "B<C"
then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
- hence "B \<le> (INF m:{N..}. x m)" by (intro le_INFI) auto
- also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro le_SUPI) simp
+ hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
+ also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
finally have "B \<le> liminf x" .
} then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
qed
--- a/src/HOL/Library/Kleene_Algebra.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/Kleene_Algebra.thy Wed Sep 14 10:08:52 2011 -0400
@@ -360,10 +360,10 @@
subsection {* Complete lattices are Kleene algebras *}
-lemma (in complete_lattice) le_SUPI':
+lemma (in complete_lattice) SUP_upper':
assumes "l \<le> M i"
shows "l \<le> (SUP i. M i)"
- using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
+ using assms by (rule order_trans) (rule SUP_upper [OF UNIV_I])
class kleene_by_complete_lattice = pre_kleene
+ complete_lattice + power + star +
@@ -376,12 +376,12 @@
have [simp]: "1 \<le> star a"
unfolding star_cont[of 1 a 1, simplified]
- by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
+ by (subst power_0[symmetric]) (rule SUP_upper [OF UNIV_I])
have "a * star a \<le> star a"
using star_cont[of a a 1] star_cont[of 1 a 1]
by (auto simp add: power_Suc[symmetric] simp del: power_Suc
- intro: SUP_leI le_SUPI)
+ intro: SUP_least SUP_upper)
then show "1 + a * star a \<le> star a"
by simp
@@ -422,7 +422,7 @@
show "star a * x \<le> x"
unfolding star_cont[of 1 a x, simplified]
- by (rule SUP_leI) (rule b)
+ by (rule SUP_least) (rule b)
qed
show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
@@ -457,7 +457,7 @@
show "x * star a \<le> x"
unfolding star_cont[of x a 1, simplified]
- by (rule SUP_leI) (rule b)
+ by (rule SUP_least) (rule b)
qed
qed
--- a/src/HOL/Library/More_List.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/More_List.thy Wed Sep 14 10:08:52 2011 -0400
@@ -262,11 +262,11 @@
lemma (in complete_lattice) INFI_set_fold:
"INFI (set xs) f = fold (inf \<circ> f) xs top"
- unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..
+ unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
lemma (in complete_lattice) SUPR_set_fold:
"SUPR (set xs) f = fold (sup \<circ> f) xs bot"
- unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
+ unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
text {* @{text nth_map} *}
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Wed Sep 14 10:08:52 2011 -0400
@@ -41,7 +41,7 @@
declare Int_def[code_pred_inline]
declare eq_reflection[OF Un_def, code_pred_inline]
-declare eq_reflection[OF UNION_def, code_pred_inline]
+declare eq_reflection[OF UNION_eq, code_pred_inline]
lemma Diff[code_pred_inline]:
"(A - B) = (%x. A x \<and> \<not> B x)"
--- a/src/HOL/Library/Product_Lattice.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Library/Product_Lattice.thy Wed Sep 14 10:08:52 2011 -0400
@@ -161,7 +161,7 @@
instance
by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
- INF_leI le_SUPI le_INF_iff SUP_le_iff)
+ INF_lower SUP_upper le_INF_iff SUP_le_iff)
end
@@ -178,21 +178,21 @@
unfolding Inf_prod_def by simp
lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
- by (simp add: SUPR_def fst_Sup image_image)
+ by (simp add: SUP_def fst_Sup image_image)
lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
- by (simp add: SUPR_def snd_Sup image_image)
+ by (simp add: SUP_def snd_Sup image_image)
lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
- by (simp add: INFI_def fst_Inf image_image)
+ by (simp add: INF_def fst_Inf image_image)
lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
- by (simp add: INFI_def snd_Inf image_image)
+ by (simp add: INF_def snd_Inf image_image)
lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
- by (simp add: SUPR_def Sup_prod_def image_image)
+ by (simp add: SUP_def Sup_prod_def image_image)
lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
- by (simp add: INFI_def Inf_prod_def image_image)
+ by (simp add: INF_def Inf_prod_def image_image)
end
--- a/src/HOL/List.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/List.thy Wed Sep 14 10:08:52 2011 -0400
@@ -2549,12 +2549,12 @@
lemma (in complete_lattice) INFI_set_fold:
"INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
- unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
+ unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map
by (simp add: inf_commute)
lemma (in complete_lattice) SUPR_set_fold:
"SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
- unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
+ unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map
by (simp add: sup_commute)
@@ -4987,8 +4987,8 @@
"x \<in> set xs \<longleftrightarrow> member xs x"
by (simp add: member_def)
-declare INFI_def [code_unfold]
-declare SUPR_def [code_unfold]
+declare INF_def [code_unfold]
+declare SUP_def [code_unfold]
declare set_map [symmetric, code_unfold]
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Wed Sep 14 10:08:52 2011 -0400
@@ -653,7 +653,7 @@
unfolding less_SUP_iff by auto
{ fix y assume "y:S & 0 < dist y x & dist y x < d"
hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
- hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
+ hence "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
} hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
} ultimately show ?thesis by auto
qed
@@ -669,8 +669,8 @@
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
by (metis dist_eq_0_iff real_less_def zero_le_dist)
hence "B <= f y" using d_def by auto
- } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto
- also have "...<=?l" apply (subst le_SUPI) using d_def by auto
+ } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst INF_greatest) by auto
+ also have "...<=?l" apply (subst SUP_upper) using d_def by auto
finally have "B<=?l" by auto
} hence "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
}
@@ -700,7 +700,7 @@
unfolding INF_less_iff by auto
{ fix y assume "y:S & 0 < dist y x & dist y x < d"
hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
- hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
+ hence "f y:T" using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
} hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
} ultimately show ?thesis by auto
qed
@@ -716,8 +716,8 @@
hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
by (metis dist_eq_0_iff real_less_def zero_le_dist)
hence "f y <= B" using d_def by auto
- } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto
- moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto
+ } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_least) by auto
+ moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_lower) using d_def by auto
ultimately have "?l<=B" by auto
} hence "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
}
@@ -1149,7 +1149,7 @@
lemma suminf_upper:
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] SUPR_def
+ unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
by (auto intro: complete_lattice_class.Sup_upper image_eqI)
lemma suminf_0_le:
@@ -1291,7 +1291,7 @@
show ?thesis using assms
apply (subst (1 2) suminf_ereal_eq_SUPR)
unfolding *
- apply (auto intro!: le_SUPI2)
+ apply (auto intro!: SUP_upper2)
apply (subst SUP_commute) ..
qed
--- a/src/HOL/Predicate.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Predicate.thy Wed Sep 14 10:08:52 2011 -0400
@@ -184,61 +184,61 @@
subsubsection {* Intersections of families *}
lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
- by (simp add: INFI_apply)
+ by (simp add: INF_apply)
lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
- by (simp add: INFI_apply)
+ by (simp add: INF_apply)
lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
- by (auto simp add: INFI_apply)
+ by (auto simp add: INF_apply)
lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
- by (auto simp add: INFI_apply)
+ by (auto simp add: INF_apply)
lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
- by (auto simp add: INFI_apply)
+ by (auto simp add: INF_apply)
lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
- by (auto simp add: INFI_apply)
+ by (auto simp add: INF_apply)
lemma INF1_E [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> (B a b \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: INFI_apply)
+ by (auto simp add: INF_apply)
lemma INF2_E [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: INFI_apply)
+ by (auto simp add: INF_apply)
lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
- by (simp add: INFI_apply fun_eq_iff)
+ by (simp add: INF_apply fun_eq_iff)
lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
- by (simp add: INFI_apply fun_eq_iff)
+ by (simp add: INF_apply fun_eq_iff)
subsubsection {* Unions of families *}
lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
- by (simp add: SUPR_apply)
+ by (simp add: SUP_apply)
lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
- by (simp add: SUPR_apply)
+ by (simp add: SUP_apply)
lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
- by (auto simp add: SUPR_apply)
+ by (auto simp add: SUP_apply)
lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
- by (auto simp add: SUPR_apply)
+ by (auto simp add: SUP_apply)
lemma SUP1_E [elim!]: "(\<Squnion>x\<in>A. B x) b \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: SUPR_apply)
+ by (auto simp add: SUP_apply)
lemma SUP2_E [elim!]: "(\<Squnion>x\<in>A. B x) b c \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> B x b c \<Longrightarrow> R) \<Longrightarrow> R"
- by (auto simp add: SUPR_apply)
+ by (auto simp add: SUP_apply)
lemma SUP_UN_eq: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
- by (simp add: SUPR_apply fun_eq_iff)
+ by (simp add: SUP_apply fun_eq_iff)
lemma SUP_UN_eq2: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
- by (simp add: SUPR_apply fun_eq_iff)
+ by (simp add: SUP_apply fun_eq_iff)
subsection {* Predicates as relations *}
@@ -469,11 +469,11 @@
lemma eval_INFI [simp]:
"eval (INFI A f) = INFI A (eval \<circ> f)"
- by (simp only: INFI_def eval_Inf image_compose)
+ by (simp only: INF_def eval_Inf image_compose)
lemma eval_SUPR [simp]:
"eval (SUPR A f) = SUPR A (eval \<circ> f)"
- by (simp only: SUPR_def eval_Sup image_compose)
+ by (simp only: SUP_def eval_Sup image_compose)
instantiation pred :: (type) complete_boolean_algebra
begin
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Wed Sep 14 10:08:52 2011 -0400
@@ -1017,7 +1017,7 @@
code_pred [inductify] Image .
thm Image.equation
declare singleton_iff[code_pred_inline]
-declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
+declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
code_pred (expected_modes:
(o => bool) => o => bool,
--- a/src/HOL/Probability/Borel_Space.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Borel_Space.thy Wed Sep 14 10:08:52 2011 -0400
@@ -1414,7 +1414,7 @@
proof
fix a
have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
- by (auto simp: less_SUP_iff SUPR_apply)
+ by (auto simp: less_SUP_iff SUP_apply)
then show "?sup -` {a<..} \<inter> space M \<in> sets M"
using assms by auto
qed
@@ -1427,7 +1427,7 @@
proof
fix a
have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
- by (auto simp: INF_less_iff INFI_apply)
+ by (auto simp: INF_less_iff INF_apply)
then show "?inf -` {..<a} \<inter> space M \<in> sets M"
using assms by auto
qed
--- a/src/HOL/Probability/Caratheodory.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Wed Sep 14 10:08:52 2011 -0400
@@ -46,7 +46,7 @@
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 le_SUPI2
+ 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)
qed
--- a/src/HOL/Probability/Finite_Product_Measure.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy Wed Sep 14 10:08:52 2011 -0400
@@ -716,9 +716,9 @@
unfolding positive_integral_def simple_function_def simple_integral_def_raw
proof (simp add: P_empty, intro antisym)
show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
- by (intro le_SUPI) (auto simp: le_fun_def split: split_max)
+ by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
- by (intro SUP_leI) (auto simp: le_fun_def simp: max_def split: split_if_asm)
+ by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm)
qed
qed
--- a/src/HOL/Probability/Infinite_Product_Measure.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Infinite_Product_Measure.thy Wed Sep 14 10:08:52 2011 -0400
@@ -503,7 +503,7 @@
proof (rule ccontr)
assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0")
moreover have "0 \<le> ?a"
- using A positive_\<mu>G by (auto intro!: le_INFI simp: positive_def)
+ using A positive_\<mu>G by (auto intro!: INF_greatest simp: positive_def)
ultimately have "0 < ?a" by auto
have "\<forall>n. \<exists>J X. J \<noteq> {} \<and> finite J \<and> J \<subseteq> I \<and> X \<in> sets (Pi\<^isub>M J M) \<and> A n = emb I J X \<and> \<mu>G (A n) = measure (Pi\<^isub>M J M) X"
@@ -525,7 +525,7 @@
have a_le_1: "?a \<le> 1"
using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
- by (auto intro!: INF_leI2[of 0] J.measure_le_1)
+ by (auto intro!: INF_lower2[of 0] J.measure_le_1)
let "?M K Z y" = "merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
@@ -544,7 +544,7 @@
note Q_sets = this
have "?a / 2^(k+1) \<le> (INF n. measure (Pi\<^isub>M J' M) (?Q n))"
- proof (intro le_INFI)
+ proof (intro INF_greatest)
fix n
have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
also have "\<dots> \<le> (\<integral>\<^isup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^isub>M J' M)"
@@ -592,7 +592,7 @@
let "?q k n y" = "\<mu>G (?M (J k) (A n) y)"
- have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_leI)
+ have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
let "?P k wk w" =
--- a/src/HOL/Probability/Lebesgue_Integration.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Sep 14 10:08:52 2011 -0400
@@ -888,13 +888,13 @@
lemma (in measure_space) positive_integral_positive:
"0 \<le> integral\<^isup>P M f"
- by (auto intro!: le_SUPI2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
+ by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
lemma (in measure_space) positive_integral_def_finite:
"integral\<^isup>P M f = (SUP g : {g. simple_function M g \<and> g \<le> max 0 \<circ> f \<and> range g \<subseteq> {0 ..< \<infinity>}}. integral\<^isup>S M g)"
(is "_ = SUPR ?A ?f")
unfolding positive_integral_def
-proof (safe intro!: antisym SUP_leI)
+proof (safe intro!: antisym SUP_least)
fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
note gM = g(1)[THEN borel_measurable_simple_function]
@@ -910,7 +910,7 @@
assume "\<mu> ?G = 0"
with gM have "AE x. x \<notin> ?G" by (simp add: AE_iff_null_set)
with gM g show ?thesis
- by (intro le_SUPI2[OF g0] simple_integral_mono_AE)
+ by (intro SUP_upper2[OF g0] simple_integral_mono_AE)
(auto simp: max_def intro!: simple_function_If)
next
assume \<mu>G: "\<mu> ?G \<noteq> 0"
@@ -932,7 +932,7 @@
qed
then show ?thesis by simp
qed
-qed (auto intro: le_SUPI)
+qed (auto intro: SUP_upper)
lemma (in measure_space) positive_integral_mono_AE:
assumes ae: "AE x. u x \<le> v x" shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
@@ -979,10 +979,10 @@
with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
by (auto simp: fun_eq_iff max_def split: split_indicator)
have "integral\<^isup>P M ?f \<le> integral\<^isup>S M ?f" using f'
- by (force intro!: SUP_leI simple_integral_mono simp: le_fun_def positive_integral_def)
+ by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)
moreover have "integral\<^isup>S M ?f \<le> integral\<^isup>P M ?f"
unfolding positive_integral_def
- using f' by (auto intro!: le_SUPI)
+ using f' by (auto intro!: SUP_upper)
ultimately show ?thesis
by (simp cong: positive_integral_cong simple_integral_cong)
qed
@@ -1004,7 +1004,7 @@
shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S")
proof (rule ereal_le_mult_one_interval)
have "0 \<le> (SUP i. integral\<^isup>P M (f i))"
- using f(3) by (auto intro!: le_SUPI2 positive_integral_positive)
+ using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)
then show "(SUP i. integral\<^isup>P M (f i)) \<noteq> -\<infinity>" by auto
have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
using u(3) by auto
@@ -1044,8 +1044,8 @@
with `a < 1` u_range[OF `x \<in> space M`]
have "a * u x < 1 * u x"
by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
- also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUPR_apply)
- finally obtain i where "a * u x < f i x" unfolding SUPR_def
+ also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUP_apply)
+ finally obtain i where "a * u x < f i x" unfolding SUP_def
by (auto simp add: less_Sup_iff)
hence "a * u x \<le> f i x" by auto
thus ?thesis using `x \<in> space M` by auto
@@ -1104,18 +1104,18 @@
shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
proof (rule antisym)
show "(SUP j. integral\<^isup>P M (f j)) \<le> (\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M)"
- by (auto intro!: SUP_leI le_SUPI positive_integral_mono)
+ by (auto intro!: SUP_least SUP_upper positive_integral_mono)
next
show "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^isup>P M (f j))"
unfolding positive_integral_def_finite[of "\<lambda>x. SUP i. f i x"]
- proof (safe intro!: SUP_leI)
+ proof (safe intro!: SUP_least)
fix g assume g: "simple_function M g"
and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
- using f by (auto intro!: le_SUPI2)
+ using f by (auto intro!: SUP_upper2)
ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
by (intro positive_integral_SUP_approx[OF f g _ g'])
- (auto simp: le_fun_def max_def SUPR_apply)
+ (auto simp: le_fun_def max_def SUP_apply)
qed
qed
@@ -1419,10 +1419,10 @@
(SUP n. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>M)"
unfolding liminf_SUPR_INFI using pos u
by (intro positive_integral_monotone_convergence_SUP_AE)
- (elim AE_mp, auto intro!: AE_I2 intro: le_INFI INF_subset)
+ (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_subset)
also have "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
unfolding liminf_SUPR_INFI
- by (auto intro!: SUP_mono exI le_INFI positive_integral_mono INF_leI)
+ by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
finally show ?thesis .
qed
--- a/src/HOL/Probability/Lebesgue_Measure.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Lebesgue_Measure.thy Wed Sep 14 10:08:52 2011 -0400
@@ -125,7 +125,7 @@
fix A assume "A \<in> sets lebesgue"
then show "0 \<le> measure lebesgue A"
unfolding lebesgue_def
- by (auto intro!: le_SUPI2 integral_nonneg)
+ by (auto intro!: SUP_upper2 integral_nonneg)
qed
next
show "countably_additive lebesgue (measure lebesgue)"
@@ -146,7 +146,7 @@
next
fix i n show "0 \<le> ereal (?m n i)"
using rA unfolding lebesgue_def
- by (auto intro!: le_SUPI2 integral_nonneg)
+ by (auto intro!: SUP_upper2 integral_nonneg)
next
show "(SUP n. \<Sum>i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))"
proof (intro arg_cong[where f="SUPR UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
@@ -642,7 +642,7 @@
{ fix i
note u_eq
also have "integral\<^isup>P lebesgue (u i) \<le> (\<integral>\<^isup>+x. max 0 (f x) \<partial>lebesgue)"
- by (intro lebesgue.positive_integral_mono) (auto intro: le_SUPI simp: u(4)[symmetric])
+ by (intro lebesgue.positive_integral_mono) (auto intro: SUP_upper simp: u(4)[symmetric])
finally have "integral\<^isup>S lebesgue (u i) \<noteq> \<infinity>"
unfolding positive_integral_max_0 using f by auto }
note u_fin = this
@@ -687,7 +687,7 @@
using lebesgue.positive_integral_eq_simple_integral[OF u(1,5)] by simp
also have "\<dots> \<le> real (integral\<^isup>P lebesgue f)" using f
by (auto intro!: real_of_ereal_positive_mono lebesgue.positive_integral_positive
- lebesgue.positive_integral_mono le_SUPI simp: SUP_eq[symmetric])
+ lebesgue.positive_integral_mono SUP_upper simp: SUP_eq[symmetric])
finally show "\<bar>integral UNIV (u' k)\<bar> \<le> real (integral\<^isup>P lebesgue f)" .
qed
qed
--- a/src/HOL/Probability/Measure.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Measure.thy Wed Sep 14 10:08:52 2011 -0400
@@ -590,7 +590,7 @@
lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
proof -
have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
- unfolding SUPR_def image_compose
+ unfolding SUP_def image_compose
unfolding surj_from_nat ..
then show ?thesis by simp
qed
--- a/src/HOL/Probability/Radon_Nikodym.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Probability/Radon_Nikodym.thy Wed Sep 14 10:08:52 2011 -0400
@@ -358,7 +358,7 @@
show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
using f by (auto simp: G_def)
{ fix x show "0 \<le> (SUP i. f i x)"
- using f by (auto simp: G_def intro: le_SUPI2) }
+ using f by (auto simp: G_def intro: SUP_upper2) }
next
fix A assume "A \<in> sets M"
have "(\<integral>\<^isup>+x. (SUP i. f i x) * indicator A x \<partial>M) =
@@ -369,12 +369,12 @@
by (intro positive_integral_monotone_convergence_SUP)
(auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
finally show "(\<integral>\<^isup>+x. (SUP i. f i x) * indicator A x \<partial>M) \<le> \<nu> A"
- using f `A \<in> sets M` by (auto intro!: SUP_leI simp: G_def)
+ using f `A \<in> sets M` by (auto intro!: SUP_least simp: G_def)
qed }
note SUP_in_G = this
let ?y = "SUP g : G. integral\<^isup>P M g"
have "?y \<le> \<nu> (space M)" unfolding G_def
- proof (safe intro!: SUP_leI)
+ proof (safe intro!: SUP_least)
fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> \<nu> A"
from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> \<nu> (space M)"
by (simp cong: positive_integral_cong)
@@ -413,14 +413,14 @@
show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y"
using g_in_G
using [[simp_trace]]
- by (auto intro!: exI Sup_mono simp: SUPR_def)
+ by (auto intro!: exI Sup_mono simp: SUP_def)
show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq
by (auto intro!: SUP_mono positive_integral_mono Max_ge)
qed
finally have int_f_eq_y: "integral\<^isup>P M f = ?y" .
have "\<And>x. 0 \<le> f x"
unfolding f_def using `\<And>i. gs i \<in> G`
- by (auto intro!: le_SUPI2 Max_ge_iff[THEN iffD2] simp: G_def)
+ by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
let ?M = "M\<lparr> measure := ?t\<rparr>"
interpret M: sigma_algebra ?M
@@ -591,11 +591,11 @@
hence "0 < b * \<mu> A0" using b by (auto simp: ereal_zero_less_0_iff)
with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * \<mu> A0" unfolding int_f_eq_y
using `f \<in> G`
- by (intro ereal_add_strict_mono) (auto intro!: le_SUPI2 positive_integral_positive)
+ by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
by (simp cong: positive_integral_cong)
finally have "?y < integral\<^isup>P M ?f0" by simp
- moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: le_SUPI)
+ moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
ultimately show False by auto
qed
show ?thesis
@@ -628,7 +628,7 @@
have "{} \<in> ?Q" using v.empty_measure by auto
then have Q_not_empty: "?Q \<noteq> {}" by blast
have "?a \<le> \<mu> (space M)" using sets_into_space
- by (auto intro!: SUP_leI measure_mono top)
+ by (auto intro!: SUP_least measure_mono top)
then have "?a \<noteq> \<infinity>" using finite_measure_of_space
by auto
from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>]
@@ -661,7 +661,7 @@
proof (rule antisym)
show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
- show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
+ show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUP_def
proof (safe intro!: Sup_mono, unfold bex_simps)
fix i
have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
@@ -701,7 +701,7 @@
using `\<nu> A \<noteq> \<infinity>` O_sets A by auto
qed (fastforce intro!: incseq_SucI)
also have "\<dots> \<le> ?a"
- proof (safe intro!: SUP_leI)
+ proof (safe intro!: SUP_least)
fix i have "?O i \<union> A \<in> ?Q"
proof (safe del: notI)
show "?O i \<union> A \<in> sets M" using O_sets A by auto
@@ -711,7 +711,7 @@
ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
using `\<nu> A \<noteq> \<infinity>` by auto
qed
- then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
+ then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule SUP_upper)
qed
finally have "\<mu> A = 0"
unfolding a_eq using real_measure[OF `?O_0 \<in> sets M`] real_measure[OF A(1)] by auto
--- a/src/HOL/Quotient_Examples/Cset.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/Quotient_Examples/Cset.thy Wed Sep 14 10:08:52 2011 -0400
@@ -97,6 +97,6 @@
hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
forall_def exists_def card_def set_def subset_def psubset_def
inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
- UNION_def
+ UNION_eq
end
--- a/src/HOL/UNITY/Union.thy Wed Sep 14 10:55:07 2011 +0200
+++ b/src/HOL/UNITY/Union.thy Wed Sep 14 10:08:52 2011 -0400
@@ -246,7 +246,7 @@
by (simp add: invariant_def, blast)
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
-by (simp add: FP_def JN_stable INTER_def)
+by (simp add: FP_def JN_stable INTER_eq)
subsection{*Progress: transient, ensures*}