# HG changeset patch
# User haftmann
# Date 1395177106 -3600
# Node ID 3253aaf73a0161fc5ba7ebd8c9fe46e3c28c0521
# Parent  3250d70c8d0bf646452ac0fa8101d31cb26551ab
consolidated theorem names containing INFI and SUPR: have INF and SUP instead uniformly

diff -r 3250d70c8d0b -r 3253aaf73a01 NEWS
--- 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.
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Complete_Lattices.thy
--- 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)"
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Library/Extended_Real.thy
--- 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"
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Library/Liminf_Limsup.thy
--- 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
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Library/Product_Order.thy
--- 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
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Library/RBT_Set.thy
--- 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 -
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Lifting_Set.thy
--- 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]:
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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}"
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Predicate.thy
--- 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
 
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Probability/Borel_Space.thy
--- 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"
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Probability/Caratheodory.thy
--- 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 *}
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Probability/Lebesgue_Integration.thy
--- 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])
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Probability/Measure_Space.thy
--- 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)"
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Probability/Radon_Nikodym.thy
--- 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
diff -r 3250d70c8d0b -r 3253aaf73a01 src/HOL/Probability/Regularity.thy
--- 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)"