# HG changeset patch
# User hoelzl
# Date 1316009332 14400
# Node ID 7ef6505bde7f8f752715eac7ebeb5756da4debe8
# Parent  8bf41f8cf71d10038bb24fa8bcb25998cc242dcb
renamed Complete_Lattices lemmas, removed legacy names

diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Complete_Lattices.thy
--- 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)
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Finite_Set.thy
--- 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:
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Fun.thy
--- 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"
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Hoare_Parallel/OG_Tactics.thy
--- 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}])
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/Continuity.thy
--- 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)
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/Extended_Real.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/Kleene_Algebra.thy
--- 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
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/More_List.thy
--- 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} *}
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- 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)"
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Library/Product_Lattice.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/List.thy
--- 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]
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- 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
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Predicate.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
--- 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,
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Borel_Space.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Caratheodory.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Finite_Product_Measure.thy
--- 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
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Infinite_Product_Measure.thy
--- 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" =
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Lebesgue_Integration.thy
--- 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
 
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Lebesgue_Measure.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Measure.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Probability/Radon_Nikodym.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/Quotient_Examples/Cset.thy
--- 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
diff -r 8bf41f8cf71d -r 7ef6505bde7f src/HOL/UNITY/Union.thy
--- 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*}