consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
authorhaftmann
Tue Mar 18 22:11:46 2014 +0100 (2014-03-18)
changeset 562123253aaf73a01
parent 56211 3250d70c8d0b
child 56213 e5720d3c18f0
child 56215 fcf90317383d
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly
NEWS
src/HOL/Complete_Lattices.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Liminf_Limsup.thy
src/HOL/Library/Product_Order.thy
src/HOL/Library/RBT_Set.thy
src/HOL/Lifting_Set.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Predicate.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Measure_Space.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Probability/Regularity.thy
     1.1 --- a/NEWS	Tue Mar 18 21:02:33 2014 +0100
     1.2 +++ b/NEWS	Tue Mar 18 22:11:46 2014 +0100
     1.3 @@ -98,8 +98,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Consolidated theorem names containing INFI and SUPR: have INF
     1.8 +and SUP instead uniformly.  INCOMPATIBILITY.
     1.9 +
    1.10  * More aggressive normalization of expressions involving INF and Inf
    1.11 -or SUP and Sup. INCOMPATIBILITY.
    1.12 +or SUP and Sup.  INCOMPATIBILITY.
    1.13  
    1.14  * INF_image and SUP_image do not unfold composition.
    1.15  INCOMPATIBILITY.
     2.1 --- a/src/HOL/Complete_Lattices.thy	Tue Mar 18 21:02:33 2014 +0100
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Tue Mar 18 22:11:46 2014 +0100
     2.3 @@ -293,13 +293,13 @@
     2.4    ultimately show ?thesis by (rule Sup_upper2)
     2.5  qed
     2.6  
     2.7 -lemma SUPR_eq:
     2.8 +lemma SUP_eq:
     2.9    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<le> g j"
    2.10    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<le> f i"
    2.11    shows "(\<Squnion>i\<in>A. f i) = (\<Squnion>j\<in>B. g j)"
    2.12    by (intro antisym SUP_least) (blast intro: SUP_upper2 dest: assms)+
    2.13  
    2.14 -lemma INFI_eq:
    2.15 +lemma INF_eq:
    2.16    assumes "\<And>i. i \<in> A \<Longrightarrow> \<exists>j\<in>B. f i \<ge> g j"
    2.17    assumes "\<And>j. j \<in> B \<Longrightarrow> \<exists>i\<in>A. g j \<ge> f i"
    2.18    shows "(\<Sqinter>i\<in>A. f i) = (\<Sqinter>j\<in>B. g j)"
     3.1 --- a/src/HOL/Library/Extended_Real.thy	Tue Mar 18 21:02:33 2014 +0100
     3.2 +++ b/src/HOL/Library/Extended_Real.thy	Tue Mar 18 22:11:46 2014 +0100
     3.3 @@ -1421,16 +1421,16 @@
     3.4    using INF_lower2[of _ A f u] INF_greatest[of A l f]
     3.5    by (cases "INFI A f") auto
     3.6  
     3.7 -lemma ereal_SUPR_uminus:
     3.8 +lemma ereal_SUP_uminus:
     3.9    fixes f :: "'a \<Rightarrow> ereal"
    3.10    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
    3.11    using ereal_Sup_uminus_image_eq[of "f`R"]
    3.12    by (simp add: image_image)
    3.13  
    3.14 -lemma ereal_INFI_uminus:
    3.15 +lemma ereal_INF_uminus:
    3.16    fixes f :: "'a \<Rightarrow> ereal"
    3.17    shows "(INF i : R. - f i) = - (SUP i : R. f i)"
    3.18 -  using ereal_SUPR_uminus[of _ "\<lambda>x. - f x"] by simp
    3.19 +  using ereal_SUP_uminus [of _ "\<lambda>x. - f x"] by simp
    3.20  
    3.21  lemma ereal_image_uminus_shift:
    3.22    fixes X Y :: "ereal set"
    3.23 @@ -1539,7 +1539,7 @@
    3.24      using real by (simp add: ereal_le_minus_iff)
    3.25  qed (insert assms, auto)
    3.26  
    3.27 -lemma SUPR_ereal_add:
    3.28 +lemma SUP_ereal_add:
    3.29    fixes f g :: "nat \<Rightarrow> ereal"
    3.30    assumes "incseq f"
    3.31      and "incseq g"
    3.32 @@ -1575,18 +1575,18 @@
    3.33      by (simp add: ac_simps)
    3.34  qed (auto intro!: add_mono SUP_upper)
    3.35  
    3.36 -lemma SUPR_ereal_add_pos:
    3.37 +lemma SUP_ereal_add_pos:
    3.38    fixes f g :: "nat \<Rightarrow> ereal"
    3.39    assumes inc: "incseq f" "incseq g"
    3.40      and pos: "\<And>i. 0 \<le> f i" "\<And>i. 0 \<le> g i"
    3.41    shows "(SUP i. f i + g i) = SUPR UNIV f + SUPR UNIV g"
    3.42 -proof (intro SUPR_ereal_add inc)
    3.43 +proof (intro SUP_ereal_add inc)
    3.44    fix i
    3.45    show "f i \<noteq> -\<infinity>" "g i \<noteq> -\<infinity>"
    3.46      using pos[of i] by auto
    3.47  qed
    3.48  
    3.49 -lemma SUPR_ereal_setsum:
    3.50 +lemma SUP_ereal_setsum:
    3.51    fixes f g :: "'a \<Rightarrow> nat \<Rightarrow> ereal"
    3.52    assumes "\<And>n. n \<in> A \<Longrightarrow> incseq (f n)"
    3.53      and pos: "\<And>n i. n \<in> A \<Longrightarrow> 0 \<le> f n i"
    3.54 @@ -1594,13 +1594,13 @@
    3.55  proof (cases "finite A")
    3.56    case True
    3.57    then show ?thesis using assms
    3.58 -    by induct (auto simp: incseq_setsumI2 setsum_nonneg SUPR_ereal_add_pos)
    3.59 +    by induct (auto simp: incseq_setsumI2 setsum_nonneg SUP_ereal_add_pos)
    3.60  next
    3.61    case False
    3.62    then show ?thesis by simp
    3.63  qed
    3.64  
    3.65 -lemma SUPR_ereal_cmult:
    3.66 +lemma SUP_ereal_cmult:
    3.67    fixes f :: "nat \<Rightarrow> ereal"
    3.68    assumes "\<And>i. 0 \<le> f i"
    3.69      and "0 \<le> c"
    3.70 @@ -1675,7 +1675,7 @@
    3.71    qed
    3.72  qed
    3.73  
    3.74 -lemma Sup_countable_SUPR:
    3.75 +lemma Sup_countable_SUP:
    3.76    assumes "A \<noteq> {}"
    3.77    shows "\<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> A \<and> Sup A = SUPR UNIV f"
    3.78  proof (cases "Sup A")
    3.79 @@ -1770,9 +1770,9 @@
    3.80      using MInf by (auto intro!: exI[of _ "\<lambda>x. -\<infinity>"])
    3.81  qed
    3.82  
    3.83 -lemma SUPR_countable_SUPR:
    3.84 +lemma SUP_countable_SUP:
    3.85    "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
    3.86 -  using Sup_countable_SUPR[of "g`A"]
    3.87 +  using Sup_countable_SUP [of "g`A"]
    3.88    by auto
    3.89  
    3.90  lemma Sup_ereal_cadd:
    3.91 @@ -1807,7 +1807,7 @@
    3.92    using Sup_ereal_cadd [of "uminus ` A" a] assms
    3.93    unfolding image_image minus_ereal_def by (simp add: ereal_SUP_uminus_eq)
    3.94  
    3.95 -lemma SUPR_ereal_cminus:
    3.96 +lemma SUP_ereal_cminus:
    3.97    fixes f :: "'i \<Rightarrow> ereal"
    3.98    fixes A
    3.99    assumes "A \<noteq> {}"
   3.100 @@ -1834,7 +1834,7 @@
   3.101      by (auto simp add: ereal_INF_uminus_eq ereal_SUP_uminus_eq)
   3.102  qed
   3.103  
   3.104 -lemma INFI_ereal_cminus:
   3.105 +lemma INF_ereal_cminus:
   3.106    fixes a :: ereal
   3.107    assumes "A \<noteq> {}"
   3.108      and "\<bar>a\<bar> \<noteq> \<infinity>"
   3.109 @@ -1848,7 +1848,7 @@
   3.110    shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
   3.111    by (cases rule: ereal2_cases[of a b]) auto
   3.112  
   3.113 -lemma INFI_ereal_add:
   3.114 +lemma INF_ereal_add:
   3.115    fixes f :: "nat \<Rightarrow> ereal"
   3.116    assumes "decseq f" "decseq g"
   3.117      and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   3.118 @@ -1864,10 +1864,10 @@
   3.119    then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   3.120      by simp
   3.121    also have "\<dots> = INFI UNIV f + INFI UNIV g"
   3.122 -    unfolding ereal_INFI_uminus
   3.123 +    unfolding ereal_INF_uminus
   3.124      using assms INF_less
   3.125 -    by (subst SUPR_ereal_add)
   3.126 -       (auto simp: ereal_SUPR_uminus intro!: uminus_ereal_add_uminus_uminus)
   3.127 +    by (subst SUP_ereal_add)
   3.128 +       (auto simp: ereal_SUP_uminus intro!: uminus_ereal_add_uminus_uminus)
   3.129    finally show ?thesis .
   3.130  qed
   3.131  
   3.132 @@ -2430,7 +2430,7 @@
   3.133  lemma ereal_Limsup_uminus:
   3.134    fixes f :: "'a \<Rightarrow> ereal"
   3.135    shows "Limsup net (\<lambda>x. - (f x)) = - Liminf net f"
   3.136 -  unfolding Limsup_def Liminf_def ereal_SUPR_uminus ereal_INFI_uminus ..
   3.137 +  unfolding Limsup_def Liminf_def ereal_SUP_uminus ereal_INF_uminus ..
   3.138  
   3.139  lemma liminf_bounded_iff:
   3.140    fixes x :: "nat \<Rightarrow> ereal"
     4.1 --- a/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 18 21:02:33 2014 +0100
     4.2 +++ b/src/HOL/Library/Liminf_Limsup.thy	Tue Mar 18 22:11:46 2014 +0100
     4.3 @@ -20,12 +20,12 @@
     4.4    unfolding INF_le_iff
     4.5    by (blast intro: less_imp_le less_trans le_less_trans dest: dense)
     4.6  
     4.7 -lemma SUPR_pair:
     4.8 +lemma SUP_pair:
     4.9    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    4.10    shows "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
    4.11    by (rule antisym) (auto intro!: SUP_least SUP_upper2)
    4.12  
    4.13 -lemma INFI_pair:
    4.14 +lemma INF_pair:
    4.15    fixes f :: "_ \<Rightarrow> _ \<Rightarrow> _ :: complete_lattice"
    4.16    shows "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    4.17    by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    4.18 @@ -52,13 +52,13 @@
    4.19      (\<And>y. (\<And>P. eventually P F \<Longrightarrow> y \<le> SUPR (Collect P) f) \<Longrightarrow> y \<le> x) \<Longrightarrow> Limsup F f = x"
    4.20    unfolding Limsup_def by (auto intro!: INF_eqI)
    4.21  
    4.22 -lemma liminf_SUPR_INFI: "liminf f = (SUP n. INF m:{n..}. f m)"
    4.23 +lemma liminf_SUP_INF: "liminf f = (SUP n. INF m:{n..}. f m)"
    4.24    unfolding Liminf_def eventually_sequentially
    4.25 -  by (rule SUPR_eq) (auto simp: atLeast_def intro!: INF_mono)
    4.26 +  by (rule SUP_eq) (auto simp: atLeast_def intro!: INF_mono)
    4.27  
    4.28 -lemma limsup_INFI_SUPR: "limsup f = (INF n. SUP m:{n..}. f m)"
    4.29 +lemma limsup_INF_SUP: "limsup f = (INF n. SUP m:{n..}. f m)"
    4.30    unfolding Limsup_def eventually_sequentially
    4.31 -  by (rule INFI_eq) (auto simp: atLeast_def intro!: SUP_mono)
    4.32 +  by (rule INF_eq) (auto simp: atLeast_def intro!: SUP_mono)
    4.33  
    4.34  lemma Limsup_const: 
    4.35    assumes ntriv: "\<not> trivial_limit F"
    4.36 @@ -292,7 +292,7 @@
    4.37      fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. X ma \<le> (X \<circ> r) m"
    4.38        using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
    4.39    qed
    4.40 -  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUPR_INFI comp_def)
    4.41 +  then show ?thesis by (auto intro!: SUP_mono simp: liminf_SUP_INF comp_def)
    4.42  qed
    4.43  
    4.44  lemma limsup_subseq_mono:
    4.45 @@ -305,7 +305,7 @@
    4.46      fix n m :: nat assume "n \<le> m" then show "\<exists>ma\<in>{n..}. (X \<circ> r) m \<le> X ma"
    4.47        using seq_suble[OF `subseq r`, of m] by (intro bexI[of _ "r m"]) auto
    4.48    qed
    4.49 -  then show ?thesis by (auto intro!: INF_mono simp: limsup_INFI_SUPR comp_def)
    4.50 +  then show ?thesis by (auto intro!: INF_mono simp: limsup_INF_SUP comp_def)
    4.51  qed
    4.52  
    4.53  end
     5.1 --- a/src/HOL/Library/Product_Order.thy	Tue Mar 18 21:02:33 2014 +0100
     5.2 +++ b/src/HOL/Library/Product_Order.thy	Tue Mar 18 22:11:46 2014 +0100
     5.3 @@ -218,26 +218,14 @@
     5.4  text {* Alternative formulations for set infima and suprema over the product
     5.5  of two complete lattices: *}
     5.6  
     5.7 -lemma Inf_prod_alt_def: "Inf A = (Inf (fst ` A), Inf (snd ` A))"
     5.8 -by (auto simp: Inf_prod_def)
     5.9 -
    5.10 -lemma Sup_prod_alt_def: "Sup A = (Sup (fst ` A), Sup (snd ` A))"
    5.11 -by (auto simp: Sup_prod_def)
    5.12 -
    5.13 -lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
    5.14 +lemma INF_prod_alt_def:
    5.15 +  "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
    5.16    unfolding INF_def Inf_prod_def by simp
    5.17  
    5.18 -lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
    5.19 +lemma SUP_prod_alt_def:
    5.20 +  "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
    5.21    unfolding SUP_def Sup_prod_def by simp
    5.22  
    5.23 -lemma INF_prod_alt_def:
    5.24 -  "(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"
    5.25 -  by (simp add: INFI_prod_alt_def comp_def)
    5.26 -
    5.27 -lemma SUP_prod_alt_def:
    5.28 -  "(SUP x:A. f x) = (SUP x:A. fst (f x), SUP x:A. snd (f x))"
    5.29 -  by (simp add: SUPR_prod_alt_def comp_def)
    5.30 -
    5.31  
    5.32  subsection {* Complete distributive lattices *}
    5.33  
    5.34 @@ -247,10 +235,10 @@
    5.35    (complete_distrib_lattice, complete_distrib_lattice) complete_distrib_lattice
    5.36  proof
    5.37    case goal1 thus ?case
    5.38 -    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF)
    5.39 +    by (auto simp: sup_prod_def Inf_prod_def INF_prod_alt_def sup_Inf sup_INF comp_def)
    5.40  next
    5.41    case goal2 thus ?case
    5.42 -    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP)
    5.43 +    by (auto simp: inf_prod_def Sup_prod_def SUP_prod_alt_def inf_Sup inf_SUP comp_def)
    5.44  qed
    5.45  
    5.46  end
     6.1 --- a/src/HOL/Library/RBT_Set.thy	Tue Mar 18 21:02:33 2014 +0100
     6.2 +++ b/src/HOL/Library/RBT_Set.thy	Tue Mar 18 22:11:46 2014 +0100
     6.3 @@ -757,7 +757,7 @@
     6.4  declare Inf'_def[symmetric, code_unfold]
     6.5  declare Inf_Set_fold[folded Inf'_def, code]
     6.6  
     6.7 -lemma INFI_Set_fold [code]:
     6.8 +lemma INF_Set_fold [code]:
     6.9    fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
    6.10    shows "INFI (Set t) f = fold_keys (inf \<circ> f) t top"
    6.11  proof -
    6.12 @@ -798,7 +798,7 @@
    6.13  declare Sup'_def[symmetric, code_unfold]
    6.14  declare Sup_Set_fold[folded Sup'_def, code]
    6.15  
    6.16 -lemma SUPR_Set_fold [code]:
    6.17 +lemma SUP_Set_fold [code]:
    6.18    fixes f :: "_ \<Rightarrow> 'a::complete_lattice"
    6.19    shows "SUPR (Set t) f = fold_keys (sup \<circ> f) t bot"
    6.20  proof -
     7.1 --- a/src/HOL/Lifting_Set.thy	Tue Mar 18 21:02:33 2014 +0100
     7.2 +++ b/src/HOL/Lifting_Set.thy	Tue Mar 18 22:11:46 2014 +0100
     7.3 @@ -149,14 +149,14 @@
     7.4      rel_set rel_set"
     7.5    unfolding rel_fun_def rel_set_def by fast
     7.6  
     7.7 -lemma SUPR_parametric [transfer_rule]:
     7.8 +lemma SUP_parametric [transfer_rule]:
     7.9    "(rel_set R ===> (R ===> op =) ===> op =) SUPR (SUPR :: _ \<Rightarrow> _ \<Rightarrow> _::complete_lattice)"
    7.10  proof(rule rel_funI)+
    7.11    fix A B f and g :: "'b \<Rightarrow> 'c"
    7.12    assume AB: "rel_set R A B"
    7.13      and fg: "(R ===> op =) f g"
    7.14    show "SUPR A f = SUPR B g"
    7.15 -    by(rule SUPR_eq)(auto 4 4 dest: rel_setD1[OF AB] rel_setD2[OF AB] rel_funD[OF fg] intro: rev_bexI)
    7.16 +    by (rule SUP_eq) (auto 4 4 dest: rel_setD1 [OF AB] rel_setD2 [OF AB] rel_funD [OF fg] intro: rev_bexI)
    7.17  qed
    7.18  
    7.19  lemma bind_transfer [transfer_rule]:
     8.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 18 21:02:33 2014 +0100
     8.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Tue Mar 18 22:11:46 2014 +0100
     8.3 @@ -537,10 +537,10 @@
     8.4  next
     8.5    case (real r)
     8.6    then show ?thesis
     8.7 -    unfolding liminf_SUPR_INFI limsup_INFI_SUPR
     8.8 -    apply (subst INFI_ereal_cminus)
     8.9 +    unfolding liminf_SUP_INF limsup_INF_SUP
    8.10 +    apply (subst INF_ereal_cminus)
    8.11      apply auto
    8.12 -    apply (subst SUPR_ereal_cminus)
    8.13 +    apply (subst SUP_ereal_cminus)
    8.14      apply auto
    8.15      done
    8.16  qed (insert `c \<noteq> -\<infinity>`, simp)
    8.17 @@ -874,7 +874,7 @@
    8.18    unfolding summable_def
    8.19    by auto
    8.20  
    8.21 -lemma suminf_ereal_eq_SUPR:
    8.22 +lemma suminf_ereal_eq_SUP:
    8.23    fixes f :: "nat \<Rightarrow> ereal"
    8.24    assumes "\<And>i. 0 \<le> f i"
    8.25    shows "(\<Sum>x. f x) = (SUP n. \<Sum>i<n. f i)"
    8.26 @@ -917,7 +917,7 @@
    8.27    fixes f :: "nat \<Rightarrow> ereal"
    8.28    assumes "\<And>n. 0 \<le> f n"
    8.29    shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
    8.30 -  unfolding suminf_ereal_eq_SUPR[OF assms]
    8.31 +  unfolding suminf_ereal_eq_SUP [OF assms]
    8.32    by (auto intro: complete_lattice_class.SUP_upper)
    8.33  
    8.34  lemma suminf_0_le:
    8.35 @@ -956,9 +956,9 @@
    8.36    assumes "\<And>i. 0 \<le> f i"
    8.37      and "\<And>i. 0 \<le> g i"
    8.38    shows "(\<Sum>i. f i + g i) = suminf f + suminf g"
    8.39 -  apply (subst (1 2 3) suminf_ereal_eq_SUPR)
    8.40 +  apply (subst (1 2 3) suminf_ereal_eq_SUP)
    8.41    unfolding setsum_addf
    8.42 -  apply (intro assms ereal_add_nonneg_nonneg SUPR_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
    8.43 +  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
    8.44    done
    8.45  
    8.46  lemma suminf_cmult_ereal:
    8.47 @@ -967,8 +967,8 @@
    8.48      and "0 \<le> a"
    8.49    shows "(\<Sum>i. a * f i) = a * suminf f"
    8.50    by (auto simp: setsum_ereal_right_distrib[symmetric] assms
    8.51 -       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUPR
    8.52 -       intro!: SUPR_ereal_cmult )
    8.53 +       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
    8.54 +       intro!: SUP_ereal_cmult)
    8.55  
    8.56  lemma suminf_PInfty:
    8.57    fixes f :: "nat \<Rightarrow> ereal"
    8.58 @@ -1107,12 +1107,12 @@
    8.59      fix n :: nat
    8.60      have "(\<Sum>i<n. SUP k. f k i) = (SUP k. \<Sum>i<n. f k i)"
    8.61        using assms
    8.62 -      by (auto intro!: SUPR_ereal_setsum[symmetric])
    8.63 +      by (auto intro!: SUP_ereal_setsum [symmetric])
    8.64    }
    8.65    note * = this
    8.66    show ?thesis
    8.67      using assms
    8.68 -    apply (subst (1 2) suminf_ereal_eq_SUPR)
    8.69 +    apply (subst (1 2) suminf_ereal_eq_SUP)
    8.70      unfolding *
    8.71      apply (auto intro!: SUP_upper2)
    8.72      apply (subst SUP_commute)
    8.73 @@ -1161,7 +1161,7 @@
    8.74    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
    8.75    shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S \<inter> ball x e - {x}). f y)"
    8.76    unfolding Liminf_def eventually_at
    8.77 -proof (rule SUPR_eq, simp_all add: Ball_def Bex_def, safe)
    8.78 +proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
    8.79    fix P d
    8.80    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
    8.81    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
    8.82 @@ -1181,7 +1181,7 @@
    8.83    fixes f :: "'a::metric_space \<Rightarrow> 'b::complete_lattice"
    8.84    shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S \<inter> ball x e - {x}). f y)"
    8.85    unfolding Limsup_def eventually_at
    8.86 -proof (rule INFI_eq, simp_all add: Ball_def Bex_def, safe)
    8.87 +proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
    8.88    fix P d
    8.89    assume "0 < d" and "\<forall>y. y \<in> S \<longrightarrow> y \<noteq> x \<and> dist y x < d \<longrightarrow> P y"
    8.90    then have "S \<inter> ball x d - {x} \<subseteq> {x. P x}"
     9.1 --- a/src/HOL/Predicate.thy	Tue Mar 18 21:02:33 2014 +0100
     9.2 +++ b/src/HOL/Predicate.thy	Tue Mar 18 22:11:46 2014 +0100
     9.3 @@ -83,11 +83,11 @@
     9.4  
     9.5  end
     9.6  
     9.7 -lemma eval_INFI [simp]:
     9.8 +lemma eval_INF [simp]:
     9.9    "eval (INFI A f) = INFI A (eval \<circ> f)"
    9.10    using eval_Inf [of "f ` A"] by simp
    9.11  
    9.12 -lemma eval_SUPR [simp]:
    9.13 +lemma eval_SUP [simp]:
    9.14    "eval (SUPR A f) = SUPR A (eval \<circ> f)"
    9.15    using eval_Sup [of "f ` A"] by simp
    9.16  
    10.1 --- a/src/HOL/Probability/Borel_Space.thy	Tue Mar 18 21:02:33 2014 +0100
    10.2 +++ b/src/HOL/Probability/Borel_Space.thy	Tue Mar 18 22:11:46 2014 +0100
    10.3 @@ -1111,7 +1111,7 @@
    10.4    assumes "\<And>i. f i \<in> borel_measurable M"
    10.5    shows borel_measurable_liminf: "(\<lambda>x. liminf (\<lambda>i. f i x)) \<in> borel_measurable M"
    10.6      and borel_measurable_limsup: "(\<lambda>x. limsup (\<lambda>i. f i x)) \<in> borel_measurable M"
    10.7 -  unfolding liminf_SUPR_INFI limsup_INFI_SUPR using assms by auto
    10.8 +  unfolding liminf_SUP_INF limsup_INF_SUP using assms by auto
    10.9  
   10.10  lemma sets_Collect_eventually_sequentially[measurable]:
   10.11    "(\<And>i. {x\<in>space M. P x i} \<in> sets M) \<Longrightarrow> {x\<in>space M. eventually (P x) sequentially} \<in> sets M"
    11.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 18 21:02:33 2014 +0100
    11.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 18 22:11:46 2014 +0100
    11.3 @@ -40,9 +40,9 @@
    11.4        by (auto intro!: setsum_mono3 simp: pos) }
    11.5    ultimately
    11.6    show ?thesis unfolding g_def using pos
    11.7 -    by (auto intro!: SUPR_eq  simp: setsum_cartesian_product reindex SUP_upper2
    11.8 -                     setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair
    11.9 -                     SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
   11.10 +    by (auto intro!: SUP_eq  simp: setsum_cartesian_product reindex SUP_upper2
   11.11 +                     setsum_nonneg suminf_ereal_eq_SUP SUP_pair
   11.12 +                     SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
   11.13  qed
   11.14  
   11.15  subsection {* Measure Spaces *}
    12.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 18 21:02:33 2014 +0100
    12.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Tue Mar 18 22:11:46 2014 +0100
    12.3 @@ -946,18 +946,18 @@
    12.4  
    12.5    have "integral\<^sup>S M u = (SUP i. integral\<^sup>S M (?uB i))"
    12.6      unfolding simple_integral_indicator[OF B `simple_function M u`]
    12.7 -  proof (subst SUPR_ereal_setsum, safe)
    12.8 +  proof (subst SUP_ereal_setsum, safe)
    12.9      fix x n assume "x \<in> space M"
   12.10      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)"
   12.11        using B_mono B_u by (auto intro!: emeasure_mono ereal_mult_left_mono incseq_SucI simp: ereal_zero_le_0_iff)
   12.12    next
   12.13      show "integral\<^sup>S M u = (\<Sum>i\<in>u ` space M. SUP n. i * (emeasure M) (?B' i n))"
   12.14        using measure_conv u_range B_u unfolding simple_integral_def
   12.15 -      by (auto intro!: setsum_cong SUPR_ereal_cmult[symmetric])
   12.16 +      by (auto intro!: setsum_cong SUP_ereal_cmult [symmetric])
   12.17    qed
   12.18    moreover
   12.19    have "a * (SUP i. integral\<^sup>S M (?uB i)) \<le> ?S"
   12.20 -    apply (subst SUPR_ereal_cmult[symmetric])
   12.21 +    apply (subst SUP_ereal_cmult [symmetric])
   12.22    proof (safe intro!: SUP_mono bexI)
   12.23      fix i
   12.24      have "a * integral\<^sup>S M (?uB i) = (\<integral>\<^sup>Sx. a * ?uB i x \<partial>M)"
   12.25 @@ -1120,8 +1120,8 @@
   12.26            by auto }
   12.27        then have "(SUP i. a * u i x + v i x) = a * (SUP i. u i x) + (SUP i. v i x)"
   12.28          using `0 \<le> a` u(3) v(3) u(6)[of _ x] v(6)[of _ x]
   12.29 -        by (subst SUPR_ereal_cmult[symmetric, OF u(6) `0 \<le> a`])
   12.30 -           (auto intro!: SUPR_ereal_add
   12.31 +        by (subst SUP_ereal_cmult [symmetric, OF u(6) `0 \<le> a`])
   12.32 +           (auto intro!: SUP_ereal_add
   12.33                   simp: incseq_Suc_iff le_fun_def add_mono ereal_mult_left_mono ereal_add_nonneg_nonneg) }
   12.34      then show "AE x in M. (SUP i. l i x) = (SUP i. ?L' i x)"
   12.35        unfolding l(5) using `0 \<le> a` u(5) v(5) l(5) f(2) g(2)
   12.36 @@ -1132,8 +1132,8 @@
   12.37    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)"
   12.38      unfolding l(5)[symmetric] u(5)[symmetric] v(5)[symmetric]
   12.39      unfolding l(1)[symmetric] u(1)[symmetric] v(1)[symmetric]
   12.40 -    apply (subst SUPR_ereal_cmult[symmetric, OF pos(1) `0 \<le> a`])
   12.41 -    apply (subst SUPR_ereal_add[symmetric, OF inc not_MInf]) .
   12.42 +    apply (subst SUP_ereal_cmult [symmetric, OF pos(1) `0 \<le> a`])
   12.43 +    apply (subst SUP_ereal_add [symmetric, OF inc not_MInf]) .
   12.44    then show ?thesis by (simp add: positive_integral_max_0)
   12.45  qed
   12.46  
   12.47 @@ -1277,14 +1277,14 @@
   12.48    have all_pos: "AE x in M. \<forall>i. 0 \<le> f i x"
   12.49      using assms by (auto simp: AE_all_countable)
   12.50    have "(\<Sum>i. integral\<^sup>P M (f i)) = (SUP n. \<Sum>i<n. integral\<^sup>P M (f i))"
   12.51 -    using positive_integral_positive by (rule suminf_ereal_eq_SUPR)
   12.52 +    using positive_integral_positive by (rule suminf_ereal_eq_SUP)
   12.53    also have "\<dots> = (SUP n. \<integral>\<^sup>+x. (\<Sum>i<n. f i x) \<partial>M)"
   12.54      unfolding positive_integral_setsum[OF f] ..
   12.55    also have "\<dots> = \<integral>\<^sup>+x. (SUP n. \<Sum>i<n. f i x) \<partial>M" using f all_pos
   12.56      by (intro positive_integral_monotone_convergence_SUP_AE[symmetric])
   12.57         (elim AE_mp, auto simp: setsum_nonneg simp del: setsum_lessThan_Suc intro!: AE_I2 setsum_mono3)
   12.58    also have "\<dots> = \<integral>\<^sup>+x. (\<Sum>i. f i x) \<partial>M" using all_pos
   12.59 -    by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUPR)
   12.60 +    by (intro positive_integral_cong_AE) (auto simp: suminf_ereal_eq_SUP)
   12.61    finally show ?thesis by simp
   12.62  qed
   12.63  
   12.64 @@ -1297,11 +1297,11 @@
   12.65    have pos: "AE x in M. \<forall>i. 0 \<le> u i x" using u by (auto simp: AE_all_countable)
   12.66    have "(\<integral>\<^sup>+ x. liminf (\<lambda>n. u n x) \<partial>M) =
   12.67      (SUP n. \<integral>\<^sup>+ x. (INF i:{n..}. u i x) \<partial>M)"
   12.68 -    unfolding liminf_SUPR_INFI using pos u
   12.69 +    unfolding liminf_SUP_INF using pos u
   12.70      by (intro positive_integral_monotone_convergence_SUP_AE)
   12.71         (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_superset_mono)
   12.72    also have "\<dots> \<le> liminf (\<lambda>n. integral\<^sup>P M (u n))"
   12.73 -    unfolding liminf_SUPR_INFI
   12.74 +    unfolding liminf_SUP_INF
   12.75      by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
   12.76    finally show ?thesis .
   12.77  qed
   12.78 @@ -2749,7 +2749,7 @@
   12.79  next
   12.80    case (seq U)
   12.81    from f(2) have eq: "AE x in M. f x * (SUP i. U i x) = (SUP i. f x * U i x)"
   12.82 -    by eventually_elim (simp add: SUPR_ereal_cmult seq)
   12.83 +    by eventually_elim (simp add: SUP_ereal_cmult seq)
   12.84    from seq f show ?case
   12.85      apply (simp add: positive_integral_monotone_convergence_SUP)
   12.86      apply (subst positive_integral_cong_AE[OF eq])
    13.1 --- a/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 21:02:33 2014 +0100
    13.2 +++ b/src/HOL/Probability/Measure_Space.thy	Tue Mar 18 22:11:46 2014 +0100
    13.3 @@ -55,7 +55,7 @@
    13.4      from this[of "Suc i"] show "f i \<le> y" by auto
    13.5    qed (insert assms, simp)
    13.6    ultimately show ?thesis using assms
    13.7 -    by (subst suminf_ereal_eq_SUPR) (auto simp: indicator_def)
    13.8 +    by (subst suminf_ereal_eq_SUP) (auto simp: indicator_def)
    13.9  qed
   13.10  
   13.11  lemma suminf_indicator:
   13.12 @@ -375,7 +375,7 @@
   13.13      by auto
   13.14    ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
   13.15      using A(4) f_fin f_Int_fin
   13.16 -    by (subst INFI_ereal_add) (auto simp: decseq_f)
   13.17 +    by (subst INF_ereal_add) (auto simp: decseq_f)
   13.18    moreover {
   13.19      fix n
   13.20      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))"
   13.21 @@ -543,10 +543,10 @@
   13.22    have A0: "0 \<le> emeasure M (A 0)" using A by auto
   13.23  
   13.24    have "emeasure M (A 0) - (INF n. emeasure M (A n)) = emeasure M (A 0) + (SUP n. - emeasure M (A n))"
   13.25 -    by (simp add: ereal_SUPR_uminus minus_ereal_def)
   13.26 +    by (simp add: ereal_SUP_uminus minus_ereal_def)
   13.27    also have "\<dots> = (SUP n. emeasure M (A 0) - emeasure M (A n))"
   13.28      unfolding minus_ereal_def using A0 assms
   13.29 -    by (subst SUPR_ereal_add) (auto simp add: decseq_emeasure)
   13.30 +    by (subst SUP_ereal_add) (auto simp add: decseq_emeasure)
   13.31    also have "\<dots> = (SUP n. emeasure M (A 0 - A n))"
   13.32      using A finite `decseq A`[unfolded decseq_def] by (subst emeasure_Diff) auto
   13.33    also have "\<dots> = emeasure M (\<Union>i. A 0 - A i)"
    14.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 18 21:02:33 2014 +0100
    14.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Tue Mar 18 22:11:46 2014 +0100
    14.3 @@ -354,7 +354,7 @@
    14.4      from this[THEN bspec, OF sets.top] show "integral\<^sup>P M g \<le> N (space M)"
    14.5        by (simp cong: positive_integral_cong)
    14.6    qed
    14.7 -  from SUPR_countable_SUPR[OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
    14.8 +  from SUP_countable_SUP [OF `G \<noteq> {}`, of "integral\<^sup>P M"] guess ys .. note ys = this
    14.9    then have "\<forall>n. \<exists>g. g\<in>G \<and> integral\<^sup>P M g = ys n"
   14.10    proof safe
   14.11      fix n assume "range ys \<subseteq> integral\<^sup>P M ` G"
   14.12 @@ -540,7 +540,7 @@
   14.13      by (auto intro!: SUP_least emeasure_mono)
   14.14    then have "?a \<noteq> \<infinity>" using finite_emeasure_space
   14.15      by auto
   14.16 -  from SUPR_countable_SUPR[OF Q_not_empty, of "emeasure M"]
   14.17 +  from SUP_countable_SUP [OF Q_not_empty, of "emeasure M"]
   14.18    obtain Q'' where "range Q'' \<subseteq> emeasure M ` ?Q" and a: "?a = (SUP i::nat. Q'' i)"
   14.19      by auto
   14.20    then have "\<forall>i. \<exists>Q'. Q'' i = emeasure M Q' \<and> Q' \<in> ?Q" by auto
    15.1 --- a/src/HOL/Probability/Regularity.thy	Tue Mar 18 21:02:33 2014 +0100
    15.2 +++ b/src/HOL/Probability/Regularity.thy	Tue Mar 18 22:11:46 2014 +0100
    15.3 @@ -312,7 +312,7 @@
    15.4      case 2
    15.5      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
    15.6      also have "\<dots> = (INF K:{K. K \<subseteq> B \<and> compact K}. M (space M) -  M K)"
    15.7 -      unfolding inner by (subst INFI_ereal_cminus) force+
    15.8 +      unfolding inner by (subst INF_ereal_cminus) force+
    15.9      also have "\<dots> = (INF U:{U. U \<subseteq> B \<and> compact U}. M (space M - U))"
   15.10        by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   15.11      also have "\<dots> \<ge> (INF U:{U. U \<subseteq> B \<and> closed U}. M (space M - U))"
   15.12 @@ -331,7 +331,7 @@
   15.13      case 1
   15.14      have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl)
   15.15      also have "\<dots> = (SUP U: {U. B \<subseteq> U \<and> open U}. M (space M) -  M U)"
   15.16 -      unfolding outer by (subst SUPR_ereal_cminus) auto
   15.17 +      unfolding outer by (subst SUP_ereal_cminus) auto
   15.18      also have "\<dots> = (SUP U:{U. B \<subseteq> U \<and> open U}. M (space M - U))"
   15.19        by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed)
   15.20      also have "\<dots> = (SUP K:{K. K \<subseteq> space M - B \<and> closed K}. emeasure M K)"