renamed Complete_Lattices lemmas, removed legacy names
authorhoelzl
Wed Sep 14 10:08:52 2011 -0400 (2011-09-14)
changeset 449287ef6505bde7f
parent 44927 8bf41f8cf71d
child 44929 1886cddaf8a5
renamed Complete_Lattices lemmas, removed legacy names
src/HOL/Complete_Lattices.thy
src/HOL/Finite_Set.thy
src/HOL/Fun.thy
src/HOL/Hoare_Parallel/OG_Tactics.thy
src/HOL/Library/Continuity.thy
src/HOL/Library/Extended_Real.thy
src/HOL/Library/Kleene_Algebra.thy
src/HOL/Library/More_List.thy
src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
src/HOL/Library/Product_Lattice.thy
src/HOL/List.thy
src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
src/HOL/Predicate.thy
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy
src/HOL/Probability/Borel_Space.thy
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Finite_Product_Measure.thy
src/HOL/Probability/Infinite_Product_Measure.thy
src/HOL/Probability/Lebesgue_Integration.thy
src/HOL/Probability/Lebesgue_Measure.thy
src/HOL/Probability/Measure.thy
src/HOL/Probability/Radon_Nikodym.thy
src/HOL/Quotient_Examples/Cset.thy
src/HOL/UNITY/Union.thy
     1.1 --- a/src/HOL/Complete_Lattices.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattices.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -1150,19 +1150,6 @@
     1.4    "\<Squnion>{a, b} = a \<squnion> b"
     1.5    by simp
     1.6  
     1.7 -lemmas (in complete_lattice) INFI_def = INF_def
     1.8 -lemmas (in complete_lattice) SUPR_def = SUP_def
     1.9 -lemmas (in complete_lattice) INF_leI = INF_lower
    1.10 -lemmas (in complete_lattice) INF_leI2 = INF_lower2
    1.11 -lemmas (in complete_lattice) le_INFI = INF_greatest
    1.12 -lemmas (in complete_lattice) le_SUPI = SUP_upper
    1.13 -lemmas (in complete_lattice) le_SUPI2 = SUP_upper2
    1.14 -lemmas (in complete_lattice) SUP_leI = SUP_least
    1.15 -lemmas (in complete_lattice) less_INFD = less_INF_D
    1.16 -
    1.17 -lemmas INFI_apply = INF_apply
    1.18 -lemmas SUPR_apply = SUP_apply
    1.19 -
    1.20  text {* Grep and put to news from here *}
    1.21  
    1.22  lemma (in complete_lattice) INF_eq:
    1.23 @@ -1196,9 +1183,6 @@
    1.24    "\<Inter>S = (\<Inter>x\<in>S. x)"
    1.25    by (simp add: INTER_eq_Inter_image image_def)
    1.26  
    1.27 -lemmas INTER_def = INTER_eq
    1.28 -lemmas UNION_def = UNION_eq
    1.29 -
    1.30  lemma INT_eq: "(\<Inter>x\<in>A. B x) = \<Inter>({Y. \<exists>x\<in>A. Y = B x})"
    1.31    by (fact INF_eq)
    1.32  
     2.1 --- a/src/HOL/Finite_Set.thy	Wed Sep 14 10:55:07 2011 +0200
     2.2 +++ b/src/HOL/Finite_Set.thy	Wed Sep 14 10:08:52 2011 -0400
     2.3 @@ -784,7 +784,7 @@
     2.4    interpret comp_fun_idem "inf \<circ> f" by (fact comp_comp_fun_idem)
     2.5    from `finite A` show "?fold = ?inf"
     2.6      by (induct A arbitrary: B)
     2.7 -      (simp_all add: INFI_def inf_left_commute)
     2.8 +      (simp_all add: INF_def inf_left_commute)
     2.9  qed
    2.10  
    2.11  lemma sup_SUPR_fold_sup:
    2.12 @@ -795,7 +795,7 @@
    2.13    interpret comp_fun_idem "sup \<circ> f" by (fact comp_comp_fun_idem)
    2.14    from `finite A` show "?fold = ?sup"
    2.15      by (induct A arbitrary: B)
    2.16 -      (simp_all add: SUPR_def sup_left_commute)
    2.17 +      (simp_all add: SUP_def sup_left_commute)
    2.18  qed
    2.19  
    2.20  lemma INFI_fold_inf:
     3.1 --- a/src/HOL/Fun.thy	Wed Sep 14 10:55:07 2011 +0200
     3.2 +++ b/src/HOL/Fun.thy	Wed Sep 14 10:08:52 2011 -0400
     3.3 @@ -181,7 +181,7 @@
     3.4    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
     3.5           INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
     3.6    shows "inj_on f (\<Union> i \<in> I. A i)"
     3.7 -proof(unfold inj_on_def UNION_def, auto)
     3.8 +proof(unfold inj_on_def UNION_eq, auto)
     3.9    fix i j x y
    3.10    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    3.11           and ***: "f x = f y"
     4.1 --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Wed Sep 14 10:55:07 2011 +0200
     4.2 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Wed Sep 14 10:08:52 2011 -0400
     4.3 @@ -270,7 +270,7 @@
     4.4  lemmas my_simp_list = list_lemmas fst_conv snd_conv
     4.5  not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc nat.inject
     4.6  Collect_mem_eq ball_simps option.simps primrecdef_list
     4.7 -lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length
     4.8 +lemmas ParallelConseq_list = INTER_eq Collect_conj_eq length_map length_upt length_append list_length
     4.9  
    4.10  ML {*
    4.11  val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}])
     5.1 --- a/src/HOL/Library/Continuity.thy	Wed Sep 14 10:55:07 2011 +0200
     5.2 +++ b/src/HOL/Library/Continuity.thy	Wed Sep 14 10:08:52 2011 -0400
     5.3 @@ -21,12 +21,12 @@
     5.4  lemma SUP_nat_conv:
     5.5    "(SUP n. M n) = sup (M 0) (SUP n. M(Suc n))"
     5.6  apply(rule order_antisym)
     5.7 - apply(rule SUP_leI)
     5.8 + apply(rule SUP_least)
     5.9   apply(case_tac n)
    5.10    apply simp
    5.11 - apply (fast intro:le_SUPI le_supI2)
    5.12 + apply (fast intro:SUP_upper le_supI2)
    5.13  apply(simp)
    5.14 -apply (blast intro:SUP_leI le_SUPI)
    5.15 +apply (blast intro:SUP_least SUP_upper)
    5.16  done
    5.17  
    5.18  lemma continuous_mono: fixes F :: "'a::complete_lattice \<Rightarrow> 'a::complete_lattice"
    5.19 @@ -61,7 +61,7 @@
    5.20        also have "\<dots> = lfp F" by(simp add:lfp_unfold[OF mono, symmetric])
    5.21        finally show ?case .
    5.22      qed }
    5.23 -  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_leI)
    5.24 +  hence "(SUP i. (F ^^ i) bot) \<le> lfp F" by (blast intro!:SUP_least)
    5.25    moreover have "lfp F \<le> (SUP i. (F ^^ i) bot)" (is "_ \<le> ?U")
    5.26    proof (rule lfp_lowerbound)
    5.27      have "chain(%i. (F ^^ i) bot)"
    5.28 @@ -75,7 +75,7 @@
    5.29        thus ?thesis by(auto simp add:chain_def)
    5.30      qed
    5.31      hence "F ?U = (SUP i. (F ^^ (i+1)) bot)" using `continuous F` by (simp add:continuous_def)
    5.32 -    also have "\<dots> \<le> ?U" by(fast intro:SUP_leI le_SUPI)
    5.33 +    also have "\<dots> \<le> ?U" by(fast intro:SUP_least SUP_upper)
    5.34      finally show "F ?U \<le> ?U" .
    5.35    qed
    5.36    ultimately show ?thesis by (blast intro:order_antisym)
     6.1 --- a/src/HOL/Library/Extended_Real.thy	Wed Sep 14 10:55:07 2011 +0200
     6.2 +++ b/src/HOL/Library/Extended_Real.thy	Wed Sep 14 10:08:52 2011 -0400
     6.3 @@ -30,11 +30,11 @@
     6.4  
     6.5  lemma SUPR_pair:
     6.6    "(SUP i : A. SUP j : B. f i j) = (SUP p : A \<times> B. f (fst p) (snd p))"
     6.7 -  by (rule antisym) (auto intro!: SUP_leI le_SUPI2)
     6.8 +  by (rule antisym) (auto intro!: SUP_least SUP_upper2)
     6.9  
    6.10  lemma INFI_pair:
    6.11    "(INF i : A. INF j : B. f i j) = (INF p : A \<times> B. f (fst p) (snd p))"
    6.12 -  by (rule antisym) (auto intro!: le_INFI INF_leI2)
    6.13 +  by (rule antisym) (auto intro!: INF_greatest INF_lower2)
    6.14  
    6.15  subsection {* Definition and basic properties *}
    6.16  
    6.17 @@ -1252,7 +1252,7 @@
    6.18  lemma ereal_SUPR_uminus:
    6.19    fixes f :: "'a => ereal"
    6.20    shows "(SUP i : R. -(f i)) = -(INF i : R. f i)"
    6.21 -  unfolding SUPR_def INFI_def
    6.22 +  unfolding SUP_def INF_def
    6.23    using ereal_Sup_uminus_image_eq[of "f`R"]
    6.24    by (simp add: image_image)
    6.25  
    6.26 @@ -1313,7 +1313,7 @@
    6.27    assumes "!!i. i : A ==> f i <= x"
    6.28    assumes "!!y. (!!i. i : A ==> f i <= y) ==> x <= y"
    6.29    shows "(SUP i:A. f i) = x"
    6.30 -  unfolding SUPR_def Sup_ereal_def
    6.31 +  unfolding SUP_def Sup_ereal_def
    6.32    using assms by (auto intro!: Least_equality)
    6.33  
    6.34  lemma ereal_INFI:
    6.35 @@ -1321,7 +1321,7 @@
    6.36    assumes "!!i. i : A ==> f i >= x"
    6.37    assumes "!!y. (!!i. i : A ==> f i >= y) ==> x >= y"
    6.38    shows "(INF i:A. f i) = x"
    6.39 -  unfolding INFI_def Inf_ereal_def
    6.40 +  unfolding INF_def Inf_ereal_def
    6.41    using assms by (auto intro!: Greatest_equality)
    6.42  
    6.43  lemma Sup_ereal_close:
    6.44 @@ -1364,13 +1364,13 @@
    6.45    { assume "~(x <= (SUP i:A. f i))" hence "(SUP i:A. f i)<x" by (simp add: not_le)
    6.46      from this obtain y where y_def: "(SUP i:A. f i)<y & y<x" using ereal_dense by auto
    6.47      from this obtain i where "i : A & y <= f i" using `?rhs` by auto
    6.48 -    hence "y <= (SUP i:A. f i)" using le_SUPI[of i A f] by auto
    6.49 +    hence "y <= (SUP i:A. f i)" using SUP_upper[of i A f] by auto
    6.50      hence False using y_def by auto
    6.51    } hence "?lhs" by auto
    6.52  }
    6.53  moreover
    6.54  { assume "?lhs" hence "?rhs"
    6.55 -  by (metis SUP_leI assms atLeastatMost_empty atLeastatMost_empty_iff
    6.56 +  by (metis SUP_least assms atLeastatMost_empty atLeastatMost_empty_iff
    6.57        inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
    6.58  } ultimately show ?thesis by auto
    6.59  qed
    6.60 @@ -1384,13 +1384,13 @@
    6.61    { assume "~((INF i:A. f i) <= x)" hence "x < (INF i:A. f i)" by (simp add: not_le)
    6.62      from this obtain y where y_def: "x<y & y<(INF i:A. f i)" using ereal_dense by auto
    6.63      from this obtain i where "i : A & f i <= y" using `?rhs` by auto
    6.64 -    hence "(INF i:A. f i) <= y" using INF_leI[of i A f] by auto
    6.65 +    hence "(INF i:A. f i) <= y" using INF_lower[of i A f] by auto
    6.66      hence False using y_def by auto
    6.67    } hence "?lhs" by auto
    6.68  }
    6.69  moreover
    6.70  { assume "?lhs" hence "?rhs"
    6.71 -  by (metis le_INFI assms atLeastatMost_empty atLeastatMost_empty_iff
    6.72 +  by (metis INF_greatest assms atLeastatMost_empty atLeastatMost_empty_iff
    6.73        inf_sup_ord(4) linorder_le_cases sup_absorb1 xt1(8))
    6.74  } ultimately show ?thesis by auto
    6.75  qed
    6.76 @@ -1402,7 +1402,7 @@
    6.77  proof(rule ccontr)
    6.78    assume "~ (EX i. i : A & f i <= x)"
    6.79    hence "ALL i:A. f i > x" by auto
    6.80 -  hence "(INF i:A. f i) >= x" apply (subst le_INFI) by auto
    6.81 +  hence "(INF i:A. f i) >= x" apply (subst INF_greatest) by auto
    6.82    thus False using assms by auto
    6.83  qed
    6.84  
    6.85 @@ -1411,7 +1411,7 @@
    6.86    shows "(INF e:A. f e) = (INF e:A. g e)"
    6.87  proof-
    6.88  have "f ` A = g ` A" unfolding image_def using assms by auto
    6.89 -thus ?thesis unfolding INFI_def by auto
    6.90 +thus ?thesis unfolding INF_def by auto
    6.91  qed
    6.92  
    6.93  lemma same_SUP:
    6.94 @@ -1419,7 +1419,7 @@
    6.95    shows "(SUP e:A. f e) = (SUP e:A. g e)"
    6.96  proof-
    6.97  have "f ` A = g ` A" unfolding image_def using assms by auto
    6.98 -thus ?thesis unfolding SUPR_def by auto
    6.99 +thus ?thesis unfolding SUP_def by auto
   6.100  qed
   6.101  
   6.102  lemma SUPR_eq:
   6.103 @@ -1428,9 +1428,9 @@
   6.104    shows "(SUP i:A. f i) = (SUP j:B. g j)"
   6.105  proof (intro antisym)
   6.106    show "(SUP i:A. f i) \<le> (SUP j:B. g j)"
   6.107 -    using assms by (metis SUP_leI le_SUPI2)
   6.108 +    using assms by (metis SUP_least SUP_upper2)
   6.109    show "(SUP i:B. g i) \<le> (SUP j:A. f j)"
   6.110 -    using assms by (metis SUP_leI le_SUPI2)
   6.111 +    using assms by (metis SUP_least SUP_upper2)
   6.112  qed
   6.113  
   6.114  lemma SUP_ereal_le_addI:
   6.115 @@ -1440,7 +1440,7 @@
   6.116  proof (cases y)
   6.117    case (real r)
   6.118    then have "\<And>i. f i \<le> z - y" using assms by (simp add: ereal_le_minus_iff)
   6.119 -  then have "SUPR UNIV f \<le> z - y" by (rule SUP_leI)
   6.120 +  then have "SUPR UNIV f \<le> z - y" by (rule SUP_least)
   6.121    then show ?thesis using real by (simp add: ereal_le_minus_iff)
   6.122  qed (insert assms, auto)
   6.123  
   6.124 @@ -1451,7 +1451,7 @@
   6.125  proof (rule ereal_SUPI)
   6.126    fix y assume *: "\<And>i. i \<in> UNIV \<Longrightarrow> f i + g i \<le> y"
   6.127    have f: "SUPR UNIV f \<noteq> -\<infinity>" using pos
   6.128 -    unfolding SUPR_def Sup_eq_MInfty by (auto dest: image_eqD)
   6.129 +    unfolding SUP_def Sup_eq_MInfty by (auto dest: image_eqD)
   6.130    { fix j
   6.131      { fix i
   6.132        have "f i + g j \<le> f i + g (max i j)"
   6.133 @@ -1466,7 +1466,7 @@
   6.134    then have "SUPR UNIV g + SUPR UNIV f \<le> y"
   6.135      using f by (rule SUP_ereal_le_addI)
   6.136    then show "SUPR UNIV f + SUPR UNIV g \<le> y" by (simp add: ac_simps)
   6.137 -qed (auto intro!: add_mono le_SUPI)
   6.138 +qed (auto intro!: add_mono SUP_upper)
   6.139  
   6.140  lemma SUPR_ereal_add_pos:
   6.141    fixes f g :: "nat \<Rightarrow> ereal"
   6.142 @@ -1489,7 +1489,7 @@
   6.143    fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>i. 0 \<le> f i" "0 \<le> c"
   6.144    shows "(SUP i. c * f i) = c * SUPR UNIV f"
   6.145  proof (rule ereal_SUPI)
   6.146 -  fix i have "f i \<le> SUPR UNIV f" by (rule le_SUPI) auto
   6.147 +  fix i have "f i \<le> SUPR UNIV f" by (rule SUP_upper) auto
   6.148    then show "c * f i \<le> c * SUPR UNIV f"
   6.149      using `0 \<le> c` by (rule ereal_mult_left_mono)
   6.150  next
   6.151 @@ -1498,7 +1498,7 @@
   6.152    proof cases
   6.153      assume c: "0 < c \<and> c \<noteq> \<infinity>"
   6.154      with * have "SUPR UNIV f \<le> y / c"
   6.155 -      by (intro SUP_leI) (auto simp: ereal_le_divide_pos)
   6.156 +      by (intro SUP_least) (auto simp: ereal_le_divide_pos)
   6.157      with c show ?thesis
   6.158        by (auto simp: ereal_le_divide_pos)
   6.159    next
   6.160 @@ -1507,7 +1507,7 @@
   6.161          assume "\<forall>i. f i = 0"
   6.162          moreover then have "range f = {0}" by auto
   6.163          ultimately show "c * SUPR UNIV f \<le> y" using *
   6.164 -          by (auto simp: SUPR_def min_max.sup_absorb1)
   6.165 +          by (auto simp: SUP_def min_max.sup_absorb1)
   6.166        next
   6.167          assume "\<not> (\<forall>i. f i = 0)"
   6.168          then obtain i where "f i \<noteq> 0" by auto
   6.169 @@ -1522,7 +1522,7 @@
   6.170    fixes f :: "'a \<Rightarrow> ereal"
   6.171    assumes "\<And>n::nat. \<exists>i\<in>A. ereal (real n) \<le> f i"
   6.172    shows "(SUP i:A. f i) = \<infinity>"
   6.173 -  unfolding SUPR_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
   6.174 +  unfolding SUP_def Sup_eq_top_iff[where 'a=ereal, unfolded top_ereal_def]
   6.175    apply simp
   6.176  proof safe
   6.177    fix x :: ereal assume "x \<noteq> \<infinity>"
   6.178 @@ -1616,7 +1616,7 @@
   6.179  
   6.180  lemma SUPR_countable_SUPR:
   6.181    "A \<noteq> {} \<Longrightarrow> \<exists>f::nat \<Rightarrow> ereal. range f \<subseteq> g`A \<and> SUPR A g = SUPR UNIV f"
   6.182 -  using Sup_countable_SUPR[of "g`A"] by (auto simp: SUPR_def)
   6.183 +  using Sup_countable_SUPR[of "g`A"] by (auto simp: SUP_def)
   6.184  
   6.185  lemma Sup_ereal_cadd:
   6.186    fixes A :: "ereal set" assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
   6.187 @@ -1649,7 +1649,7 @@
   6.188    fixes A assumes "A \<noteq> {}" and "a \<noteq> -\<infinity>"
   6.189    shows "(SUP x:A. a - f x) = a - (INF x:A. f x)"
   6.190    using Sup_ereal_cminus[of "f`A" a] assms
   6.191 -  unfolding SUPR_def INFI_def image_image by auto
   6.192 +  unfolding SUP_def INF_def image_image by auto
   6.193  
   6.194  lemma Inf_ereal_cminus:
   6.195    fixes A :: "ereal set" assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
   6.196 @@ -1667,7 +1667,7 @@
   6.197    fixes a :: ereal assumes "A \<noteq> {}" and "\<bar>a\<bar> \<noteq> \<infinity>"
   6.198    shows "(INF x:A. a - f x) = a - (SUP x:A. f x)"
   6.199    using Inf_ereal_cminus[of "f`A" a] assms
   6.200 -  unfolding SUPR_def INFI_def image_image
   6.201 +  unfolding SUP_def INF_def image_image
   6.202    by auto
   6.203  
   6.204  lemma uminus_ereal_add_uminus_uminus:
   6.205 @@ -2358,14 +2358,14 @@
   6.206      fix y assume "y < x"
   6.207      with * obtain N where "\<And>n. N \<le> n \<Longrightarrow> y < f n" by auto
   6.208      then have "y \<le> (INF m:{N..}. f m)" by (force simp: le_INF_iff)
   6.209 -    also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro le_SUPI) auto
   6.210 +    also have "\<dots> \<le> (SUP n. INF m:{n..}. f m)" by (intro SUP_upper) auto
   6.211      finally show "y \<le> (SUP n. INF m:{n..}. f m)" .
   6.212    qed
   6.213  next
   6.214    show "(SUP n. INF m:{n..}. f m) \<le> Sup {l. \<forall>y<l. \<exists>N. \<forall>n\<ge>N. y < f n}"
   6.215 -  proof (unfold SUPR_def, safe intro!: Sup_mono bexI)
   6.216 +  proof (unfold SUP_def, safe intro!: Sup_mono bexI)
   6.217      fix y n assume "y < INFI {n..} f"
   6.218 -    from less_INFD[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
   6.219 +    from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. y < f n" by (intro exI[of _ n]) auto
   6.220    qed (rule order_refl)
   6.221  qed
   6.222  
   6.223 @@ -2418,14 +2418,14 @@
   6.224    fix B assume "B < C" "C \<le> liminf x"
   6.225    then have "B < liminf x" by auto
   6.226    then obtain N where "B < (INF m:{N..}. x m)"
   6.227 -    unfolding liminf_SUPR_INFI SUPR_def less_Sup_iff by auto
   6.228 -  from less_INFD[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
   6.229 +    unfolding liminf_SUPR_INFI SUP_def less_Sup_iff by auto
   6.230 +  from less_INF_D[OF this] show "\<exists>N. \<forall>n\<ge>N. B < x n" by auto
   6.231  next
   6.232    assume *: "\<forall>B<C. \<exists>N. \<forall>n\<ge>N. B < x n"
   6.233    { fix B assume "B<C"
   6.234      then obtain N where "\<forall>n\<ge>N. B < x n" using `?rhs` by auto
   6.235 -    hence "B \<le> (INF m:{N..}. x m)" by (intro le_INFI) auto
   6.236 -    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro le_SUPI) simp
   6.237 +    hence "B \<le> (INF m:{N..}. x m)" by (intro INF_greatest) auto
   6.238 +    also have "... \<le> liminf x" unfolding liminf_SUPR_INFI by (intro SUP_upper) simp
   6.239      finally have "B \<le> liminf x" .
   6.240    } then show "?lhs" by (metis * leD liminf_bounded linorder_le_less_linear)
   6.241  qed
     7.1 --- a/src/HOL/Library/Kleene_Algebra.thy	Wed Sep 14 10:55:07 2011 +0200
     7.2 +++ b/src/HOL/Library/Kleene_Algebra.thy	Wed Sep 14 10:08:52 2011 -0400
     7.3 @@ -360,10 +360,10 @@
     7.4  
     7.5  subsection {* Complete lattices are Kleene algebras *}
     7.6  
     7.7 -lemma (in complete_lattice) le_SUPI':
     7.8 +lemma (in complete_lattice) SUP_upper':
     7.9    assumes "l \<le> M i"
    7.10    shows "l \<le> (SUP i. M i)"
    7.11 -  using assms by (rule order_trans) (rule le_SUPI [OF UNIV_I])
    7.12 +  using assms by (rule order_trans) (rule SUP_upper [OF UNIV_I])
    7.13  
    7.14  class kleene_by_complete_lattice = pre_kleene
    7.15    + complete_lattice + power + star +
    7.16 @@ -376,12 +376,12 @@
    7.17    
    7.18    have [simp]: "1 \<le> star a"
    7.19      unfolding star_cont[of 1 a 1, simplified] 
    7.20 -    by (subst power_0[symmetric]) (rule le_SUPI [OF UNIV_I])
    7.21 +    by (subst power_0[symmetric]) (rule SUP_upper [OF UNIV_I])
    7.22  
    7.23    have "a * star a \<le> star a"
    7.24      using star_cont[of a a 1] star_cont[of 1 a 1]
    7.25      by (auto simp add: power_Suc[symmetric] simp del: power_Suc
    7.26 -      intro: SUP_leI le_SUPI)
    7.27 +      intro: SUP_least SUP_upper)
    7.28  
    7.29    then show "1 + a * star a \<le> star a"
    7.30      by simp
    7.31 @@ -422,7 +422,7 @@
    7.32      
    7.33      show "star a * x \<le> x"
    7.34        unfolding star_cont[of 1 a x, simplified]
    7.35 -      by (rule SUP_leI) (rule b)
    7.36 +      by (rule SUP_least) (rule b)
    7.37    qed
    7.38  
    7.39    show "x * a \<le> x \<Longrightarrow> x * star a \<le> x" (* symmetric *)
    7.40 @@ -457,7 +457,7 @@
    7.41      
    7.42      show "x * star a \<le> x"
    7.43        unfolding star_cont[of x a 1, simplified]
    7.44 -      by (rule SUP_leI) (rule b)
    7.45 +      by (rule SUP_least) (rule b)
    7.46    qed
    7.47  qed
    7.48  
     8.1 --- a/src/HOL/Library/More_List.thy	Wed Sep 14 10:55:07 2011 +0200
     8.2 +++ b/src/HOL/Library/More_List.thy	Wed Sep 14 10:08:52 2011 -0400
     8.3 @@ -262,11 +262,11 @@
     8.4  
     8.5  lemma (in complete_lattice) INFI_set_fold:
     8.6    "INFI (set xs) f = fold (inf \<circ> f) xs top"
     8.7 -  unfolding INFI_def set_map [symmetric] Inf_set_fold fold_map ..
     8.8 +  unfolding INF_def set_map [symmetric] Inf_set_fold fold_map ..
     8.9  
    8.10  lemma (in complete_lattice) SUPR_set_fold:
    8.11    "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
    8.12 -  unfolding SUPR_def set_map [symmetric] Sup_set_fold fold_map ..
    8.13 +  unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
    8.14  
    8.15  text {* @{text nth_map} *}
    8.16  
     9.1 --- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Sep 14 10:55:07 2011 +0200
     9.2 +++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Sep 14 10:08:52 2011 -0400
     9.3 @@ -41,7 +41,7 @@
     9.4  
     9.5  declare Int_def[code_pred_inline]
     9.6  declare eq_reflection[OF Un_def, code_pred_inline]
     9.7 -declare eq_reflection[OF UNION_def, code_pred_inline]
     9.8 +declare eq_reflection[OF UNION_eq, code_pred_inline]
     9.9  
    9.10  lemma Diff[code_pred_inline]:
    9.11    "(A - B) = (%x. A x \<and> \<not> B x)"
    10.1 --- a/src/HOL/Library/Product_Lattice.thy	Wed Sep 14 10:55:07 2011 +0200
    10.2 +++ b/src/HOL/Library/Product_Lattice.thy	Wed Sep 14 10:08:52 2011 -0400
    10.3 @@ -161,7 +161,7 @@
    10.4  
    10.5  instance
    10.6    by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
    10.7 -    INF_leI le_SUPI le_INF_iff SUP_le_iff)
    10.8 +    INF_lower SUP_upper le_INF_iff SUP_le_iff)
    10.9  
   10.10  end
   10.11  
   10.12 @@ -178,21 +178,21 @@
   10.13    unfolding Inf_prod_def by simp
   10.14  
   10.15  lemma fst_SUP: "fst (SUP x:A. f x) = (SUP x:A. fst (f x))"
   10.16 -  by (simp add: SUPR_def fst_Sup image_image)
   10.17 +  by (simp add: SUP_def fst_Sup image_image)
   10.18  
   10.19  lemma snd_SUP: "snd (SUP x:A. f x) = (SUP x:A. snd (f x))"
   10.20 -  by (simp add: SUPR_def snd_Sup image_image)
   10.21 +  by (simp add: SUP_def snd_Sup image_image)
   10.22  
   10.23  lemma fst_INF: "fst (INF x:A. f x) = (INF x:A. fst (f x))"
   10.24 -  by (simp add: INFI_def fst_Inf image_image)
   10.25 +  by (simp add: INF_def fst_Inf image_image)
   10.26  
   10.27  lemma snd_INF: "snd (INF x:A. f x) = (INF x:A. snd (f x))"
   10.28 -  by (simp add: INFI_def snd_Inf image_image)
   10.29 +  by (simp add: INF_def snd_Inf image_image)
   10.30  
   10.31  lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
   10.32 -  by (simp add: SUPR_def Sup_prod_def image_image)
   10.33 +  by (simp add: SUP_def Sup_prod_def image_image)
   10.34  
   10.35  lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
   10.36 -  by (simp add: INFI_def Inf_prod_def image_image)
   10.37 +  by (simp add: INF_def Inf_prod_def image_image)
   10.38  
   10.39  end
    11.1 --- a/src/HOL/List.thy	Wed Sep 14 10:55:07 2011 +0200
    11.2 +++ b/src/HOL/List.thy	Wed Sep 14 10:08:52 2011 -0400
    11.3 @@ -2549,12 +2549,12 @@
    11.4  
    11.5  lemma (in complete_lattice) INFI_set_fold:
    11.6    "INFI (set xs) f = foldl (\<lambda>y x. inf (f x) y) top xs"
    11.7 -  unfolding INFI_def set_map [symmetric] Inf_set_fold foldl_map
    11.8 +  unfolding INF_def set_map [symmetric] Inf_set_fold foldl_map
    11.9      by (simp add: inf_commute)
   11.10  
   11.11  lemma (in complete_lattice) SUPR_set_fold:
   11.12    "SUPR (set xs) f = foldl (\<lambda>y x. sup (f x) y) bot xs"
   11.13 -  unfolding SUPR_def set_map [symmetric] Sup_set_fold foldl_map
   11.14 +  unfolding SUP_def set_map [symmetric] Sup_set_fold foldl_map
   11.15      by (simp add: sup_commute)
   11.16  
   11.17  
   11.18 @@ -4987,8 +4987,8 @@
   11.19    "x \<in> set xs \<longleftrightarrow> member xs x"
   11.20    by (simp add: member_def)
   11.21  
   11.22 -declare INFI_def [code_unfold]
   11.23 -declare SUPR_def [code_unfold]
   11.24 +declare INF_def [code_unfold]
   11.25 +declare SUP_def [code_unfold]
   11.26  
   11.27  declare set_map [symmetric, code_unfold]
   11.28  
    12.1 --- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Sep 14 10:55:07 2011 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Sep 14 10:08:52 2011 -0400
    12.3 @@ -653,7 +653,7 @@
    12.4        unfolding less_SUP_iff by auto
    12.5      { fix y assume "y:S & 0 < dist y x & dist y x < d"
    12.6        hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
    12.7 -      hence "f y:T" using d_def INF_leI[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
    12.8 +      hence "f y:T" using d_def INF_lower[of y "S Int ball x d - {x}" f] `T={B<..}` by auto
    12.9      } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
   12.10    } ultimately show ?thesis by auto
   12.11    qed
   12.12 @@ -669,8 +669,8 @@
   12.13        hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
   12.14           by (metis dist_eq_0_iff real_less_def zero_le_dist)
   12.15        hence "B <= f y" using d_def by auto
   12.16 -    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst le_INFI) by auto
   12.17 -    also have "...<=?l" apply (subst le_SUPI) using d_def by auto
   12.18 +    } hence "B <= INFI (S Int ball x d - {x}) f" apply (subst INF_greatest) by auto
   12.19 +    also have "...<=?l" apply (subst SUP_upper) using d_def by auto
   12.20      finally have "B<=?l" by auto
   12.21    } hence "z <= ?l" using ereal_le_ereal[of z "?l"] by auto
   12.22  }
   12.23 @@ -700,7 +700,7 @@
   12.24        unfolding INF_less_iff by auto
   12.25      { fix y assume "y:S & 0 < dist y x & dist y x < d"
   12.26        hence "y:(S Int ball x d - {x})" unfolding ball_def by (auto simp add: dist_commute)
   12.27 -      hence "f y:T" using d_def le_SUPI[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
   12.28 +      hence "f y:T" using d_def SUP_upper[of y "S Int ball x d - {x}" f] `T={..<B}` by auto
   12.29      } hence ?thesis apply(rule_tac x="d" in exI) using d_def by auto
   12.30    } ultimately show ?thesis by auto
   12.31    qed
   12.32 @@ -716,8 +716,8 @@
   12.33        hence "y:S & 0 < dist y x & dist y x < d" unfolding ball_def apply (simp add: dist_commute)
   12.34           by (metis dist_eq_0_iff real_less_def zero_le_dist)
   12.35        hence "f y <= B" using d_def by auto
   12.36 -    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_leI) by auto
   12.37 -    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_leI) using d_def by auto
   12.38 +    } hence "SUPR (S Int ball x d - {x}) f <= B" apply (subst SUP_least) by auto
   12.39 +    moreover have "?l<=SUPR (S Int ball x d - {x}) f" apply (subst INF_lower) using d_def by auto
   12.40      ultimately have "?l<=B" by auto
   12.41    } hence "?l <= z" using ereal_ge_ereal[of z "?l"] by auto
   12.42  }
   12.43 @@ -1149,7 +1149,7 @@
   12.44  lemma suminf_upper:
   12.45    fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
   12.46    shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
   12.47 -  unfolding suminf_ereal_eq_SUPR[OF assms] SUPR_def
   12.48 +  unfolding suminf_ereal_eq_SUPR[OF assms] SUP_def
   12.49    by (auto intro: complete_lattice_class.Sup_upper image_eqI)
   12.50  
   12.51  lemma suminf_0_le:
   12.52 @@ -1291,7 +1291,7 @@
   12.53    show ?thesis using assms
   12.54      apply (subst (1 2) suminf_ereal_eq_SUPR)
   12.55      unfolding *
   12.56 -    apply (auto intro!: le_SUPI2)
   12.57 +    apply (auto intro!: SUP_upper2)
   12.58      apply (subst SUP_commute) ..
   12.59  qed
   12.60  
    13.1 --- a/src/HOL/Predicate.thy	Wed Sep 14 10:55:07 2011 +0200
    13.2 +++ b/src/HOL/Predicate.thy	Wed Sep 14 10:08:52 2011 -0400
    13.3 @@ -184,61 +184,61 @@
    13.4  subsubsection {* Intersections of families *}
    13.5  
    13.6  lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
    13.7 -  by (simp add: INFI_apply)
    13.8 +  by (simp add: INF_apply)
    13.9  
   13.10  lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
   13.11 -  by (simp add: INFI_apply)
   13.12 +  by (simp add: INF_apply)
   13.13  
   13.14  lemma INF1_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   13.15 -  by (auto simp add: INFI_apply)
   13.16 +  by (auto simp add: INF_apply)
   13.17  
   13.18  lemma INF2_I [intro!]: "(\<And>x. x \<in> A \<Longrightarrow> B x b c) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b c"
   13.19 -  by (auto simp add: INFI_apply)
   13.20 +  by (auto simp add: INF_apply)
   13.21  
   13.22  lemma INF1_D [elim]: "(\<Sqinter>x\<in>A. B x) b \<Longrightarrow> a \<in> A \<Longrightarrow> B a b"
   13.23 -  by (auto simp add: INFI_apply)
   13.24 +  by (auto simp add: INF_apply)
   13.25  
   13.26  lemma INF2_D [elim]: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> a \<in> A \<Longrightarrow> B a b c"
   13.27 -  by (auto simp add: INFI_apply)
   13.28 +  by (auto simp add: INF_apply)
   13.29  
   13.30  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"
   13.31 -  by (auto simp add: INFI_apply)
   13.32 +  by (auto simp add: INF_apply)
   13.33  
   13.34  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"
   13.35 -  by (auto simp add: INFI_apply)
   13.36 +  by (auto simp add: INF_apply)
   13.37  
   13.38  lemma INF_INT_eq: "(\<Sqinter>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Sqinter>i. r i))"
   13.39 -  by (simp add: INFI_apply fun_eq_iff)
   13.40 +  by (simp add: INF_apply fun_eq_iff)
   13.41  
   13.42  lemma INF_INT_eq2: "(\<Sqinter>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Sqinter>i. r i))"
   13.43 -  by (simp add: INFI_apply fun_eq_iff)
   13.44 +  by (simp add: INF_apply fun_eq_iff)
   13.45  
   13.46  
   13.47  subsubsection {* Unions of families *}
   13.48  
   13.49  lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
   13.50 -  by (simp add: SUPR_apply)
   13.51 +  by (simp add: SUP_apply)
   13.52  
   13.53  lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
   13.54 -  by (simp add: SUPR_apply)
   13.55 +  by (simp add: SUP_apply)
   13.56  
   13.57  lemma SUP1_I [intro]: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   13.58 -  by (auto simp add: SUPR_apply)
   13.59 +  by (auto simp add: SUP_apply)
   13.60  
   13.61  lemma SUP2_I [intro]: "a \<in> A \<Longrightarrow> B a b c \<Longrightarrow> (\<Squnion>x\<in>A. B x) b c"
   13.62 -  by (auto simp add: SUPR_apply)
   13.63 +  by (auto simp add: SUP_apply)
   13.64  
   13.65  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"
   13.66 -  by (auto simp add: SUPR_apply)
   13.67 +  by (auto simp add: SUP_apply)
   13.68  
   13.69  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"
   13.70 -  by (auto simp add: SUPR_apply)
   13.71 +  by (auto simp add: SUP_apply)
   13.72  
   13.73  lemma SUP_UN_eq: "(\<Squnion>i. (\<lambda>x. x \<in> r i)) = (\<lambda>x. x \<in> (\<Union>i. r i))"
   13.74 -  by (simp add: SUPR_apply fun_eq_iff)
   13.75 +  by (simp add: SUP_apply fun_eq_iff)
   13.76  
   13.77  lemma SUP_UN_eq2: "(\<Squnion>i. (\<lambda>x y. (x, y) \<in> r i)) = (\<lambda>x y. (x, y) \<in> (\<Union>i. r i))"
   13.78 -  by (simp add: SUPR_apply fun_eq_iff)
   13.79 +  by (simp add: SUP_apply fun_eq_iff)
   13.80  
   13.81  
   13.82  subsection {* Predicates as relations *}
   13.83 @@ -469,11 +469,11 @@
   13.84  
   13.85  lemma eval_INFI [simp]:
   13.86    "eval (INFI A f) = INFI A (eval \<circ> f)"
   13.87 -  by (simp only: INFI_def eval_Inf image_compose)
   13.88 +  by (simp only: INF_def eval_Inf image_compose)
   13.89  
   13.90  lemma eval_SUPR [simp]:
   13.91    "eval (SUPR A f) = SUPR A (eval \<circ> f)"
   13.92 -  by (simp only: SUPR_def eval_Sup image_compose)
   13.93 +  by (simp only: SUP_def eval_Sup image_compose)
   13.94  
   13.95  instantiation pred :: (type) complete_boolean_algebra
   13.96  begin
    14.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 14 10:55:07 2011 +0200
    14.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy	Wed Sep 14 10:08:52 2011 -0400
    14.3 @@ -1017,7 +1017,7 @@
    14.4  code_pred [inductify] Image .
    14.5  thm Image.equation
    14.6  declare singleton_iff[code_pred_inline]
    14.7 -declare Id_on_def[unfolded Bex_def UNION_def singleton_iff, code_pred_def]
    14.8 +declare Id_on_def[unfolded Bex_def UNION_eq singleton_iff, code_pred_def]
    14.9  
   14.10  code_pred (expected_modes:
   14.11    (o => bool) => o => bool,
    15.1 --- a/src/HOL/Probability/Borel_Space.thy	Wed Sep 14 10:55:07 2011 +0200
    15.2 +++ b/src/HOL/Probability/Borel_Space.thy	Wed Sep 14 10:08:52 2011 -0400
    15.3 @@ -1414,7 +1414,7 @@
    15.4  proof
    15.5    fix a
    15.6    have "?sup -` {a<..} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. a < f i x})"
    15.7 -    by (auto simp: less_SUP_iff SUPR_apply)
    15.8 +    by (auto simp: less_SUP_iff SUP_apply)
    15.9    then show "?sup -` {a<..} \<inter> space M \<in> sets M"
   15.10      using assms by auto
   15.11  qed
   15.12 @@ -1427,7 +1427,7 @@
   15.13  proof
   15.14    fix a
   15.15    have "?inf -` {..<a} \<inter> space M = (\<Union>i\<in>A. {x\<in>space M. f i x < a})"
   15.16 -    by (auto simp: INF_less_iff INFI_apply)
   15.17 +    by (auto simp: INF_less_iff INF_apply)
   15.18    then show "?inf -` {..<a} \<inter> space M \<in> sets M"
   15.19      using assms by auto
   15.20  qed
    16.1 --- a/src/HOL/Probability/Caratheodory.thy	Wed Sep 14 10:55:07 2011 +0200
    16.2 +++ b/src/HOL/Probability/Caratheodory.thy	Wed Sep 14 10:08:52 2011 -0400
    16.3 @@ -46,7 +46,7 @@
    16.4        by (auto intro!: setsum_mono3 simp: pos) }
    16.5    ultimately
    16.6    show ?thesis unfolding g_def using pos
    16.7 -    by (auto intro!: SUPR_eq  simp: setsum_cartesian_product reindex le_SUPI2
    16.8 +    by (auto intro!: SUPR_eq  simp: setsum_cartesian_product reindex SUP_upper2
    16.9                       setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair
   16.10                       SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
   16.11  qed
    17.1 --- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Sep 14 10:55:07 2011 +0200
    17.2 +++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Sep 14 10:08:52 2011 -0400
    17.3 @@ -716,9 +716,9 @@
    17.4      unfolding positive_integral_def simple_function_def simple_integral_def_raw
    17.5    proof (simp add: P_empty, intro antisym)
    17.6      show "f (\<lambda>k. undefined) \<le> (SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined))"
    17.7 -      by (intro le_SUPI) (auto simp: le_fun_def split: split_max)
    17.8 +      by (intro SUP_upper) (auto simp: le_fun_def split: split_max)
    17.9      show "(SUP f:{g. g \<le> max 0 \<circ> f}. f (\<lambda>k. undefined)) \<le> f (\<lambda>k. undefined)" using pos
   17.10 -      by (intro SUP_leI) (auto simp: le_fun_def simp: max_def split: split_if_asm)
   17.11 +      by (intro SUP_least) (auto simp: le_fun_def simp: max_def split: split_if_asm)
   17.12    qed
   17.13  qed
   17.14  
    18.1 --- a/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Sep 14 10:55:07 2011 +0200
    18.2 +++ b/src/HOL/Probability/Infinite_Product_Measure.thy	Wed Sep 14 10:08:52 2011 -0400
    18.3 @@ -503,7 +503,7 @@
    18.4      proof (rule ccontr)
    18.5        assume "(INF i. \<mu>G (A i)) \<noteq> 0" (is "?a \<noteq> 0")
    18.6        moreover have "0 \<le> ?a"
    18.7 -        using A positive_\<mu>G by (auto intro!: le_INFI simp: positive_def)
    18.8 +        using A positive_\<mu>G by (auto intro!: INF_greatest simp: positive_def)
    18.9        ultimately have "0 < ?a" by auto
   18.10  
   18.11        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"
   18.12 @@ -525,7 +525,7 @@
   18.13  
   18.14        have a_le_1: "?a \<le> 1"
   18.15          using \<mu>G_spec[of "J 0" "A 0" "X 0"] J A_eq
   18.16 -        by (auto intro!: INF_leI2[of 0] J.measure_le_1)
   18.17 +        by (auto intro!: INF_lower2[of 0] J.measure_le_1)
   18.18  
   18.19        let "?M K Z y" = "merge K y (I - K) -` Z \<inter> space (Pi\<^isub>M I M)"
   18.20  
   18.21 @@ -544,7 +544,7 @@
   18.22          note Q_sets = this
   18.23  
   18.24          have "?a / 2^(k+1) \<le> (INF n. measure (Pi\<^isub>M J' M) (?Q n))"
   18.25 -        proof (intro le_INFI)
   18.26 +        proof (intro INF_greatest)
   18.27            fix n
   18.28            have "?a / 2^k \<le> \<mu>G (Z n)" using Z by auto
   18.29            also have "\<dots> \<le> (\<integral>\<^isup>+ x. indicator (?Q n) x + ?a / 2^(k+1) \<partial>Pi\<^isub>M J' M)"
   18.30 @@ -592,7 +592,7 @@
   18.31  
   18.32        let "?q k n y" = "\<mu>G (?M (J k) (A n) y)"
   18.33  
   18.34 -      have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_leI)
   18.35 +      have "\<forall>n. ?a / 2 ^ 0 \<le> \<mu>G (A n)" by (auto intro: INF_lower)
   18.36        from Ex_w[OF A(1,2) this J(1-3), of 0] guess w0 .. note w0 = this
   18.37  
   18.38        let "?P k wk w" =
    19.1 --- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Sep 14 10:55:07 2011 +0200
    19.2 +++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Sep 14 10:08:52 2011 -0400
    19.3 @@ -888,13 +888,13 @@
    19.4  
    19.5  lemma (in measure_space) positive_integral_positive:
    19.6    "0 \<le> integral\<^isup>P M f"
    19.7 -  by (auto intro!: le_SUPI2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
    19.8 +  by (auto intro!: SUP_upper2[of "\<lambda>x. 0"] simp: positive_integral_def le_fun_def)
    19.9  
   19.10  lemma (in measure_space) positive_integral_def_finite:
   19.11    "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)"
   19.12      (is "_ = SUPR ?A ?f")
   19.13    unfolding positive_integral_def
   19.14 -proof (safe intro!: antisym SUP_leI)
   19.15 +proof (safe intro!: antisym SUP_least)
   19.16    fix g assume g: "simple_function M g" "g \<le> max 0 \<circ> f"
   19.17    let ?G = "{x \<in> space M. \<not> g x \<noteq> \<infinity>}"
   19.18    note gM = g(1)[THEN borel_measurable_simple_function]
   19.19 @@ -910,7 +910,7 @@
   19.20      assume "\<mu> ?G = 0"
   19.21      with gM have "AE x. x \<notin> ?G" by (simp add: AE_iff_null_set)
   19.22      with gM g show ?thesis
   19.23 -      by (intro le_SUPI2[OF g0] simple_integral_mono_AE)
   19.24 +      by (intro SUP_upper2[OF g0] simple_integral_mono_AE)
   19.25           (auto simp: max_def intro!: simple_function_If)
   19.26    next
   19.27      assume \<mu>G: "\<mu> ?G \<noteq> 0"
   19.28 @@ -932,7 +932,7 @@
   19.29      qed
   19.30      then show ?thesis by simp
   19.31    qed
   19.32 -qed (auto intro: le_SUPI)
   19.33 +qed (auto intro: SUP_upper)
   19.34  
   19.35  lemma (in measure_space) positive_integral_mono_AE:
   19.36    assumes ae: "AE x. u x \<le> v x" shows "integral\<^isup>P M u \<le> integral\<^isup>P M v"
   19.37 @@ -979,10 +979,10 @@
   19.38    with f(2) have [simp]: "max 0 \<circ> ?f = ?f"
   19.39      by (auto simp: fun_eq_iff max_def split: split_indicator)
   19.40    have "integral\<^isup>P M ?f \<le> integral\<^isup>S M ?f" using f'
   19.41 -    by (force intro!: SUP_leI simple_integral_mono simp: le_fun_def positive_integral_def)
   19.42 +    by (force intro!: SUP_least simple_integral_mono simp: le_fun_def positive_integral_def)
   19.43    moreover have "integral\<^isup>S M ?f \<le> integral\<^isup>P M ?f"
   19.44      unfolding positive_integral_def
   19.45 -    using f' by (auto intro!: le_SUPI)
   19.46 +    using f' by (auto intro!: SUP_upper)
   19.47    ultimately show ?thesis
   19.48      by (simp cong: positive_integral_cong simple_integral_cong)
   19.49  qed
   19.50 @@ -1004,7 +1004,7 @@
   19.51    shows "integral\<^isup>S M u \<le> (SUP i. integral\<^isup>P M (f i))" (is "_ \<le> ?S")
   19.52  proof (rule ereal_le_mult_one_interval)
   19.53    have "0 \<le> (SUP i. integral\<^isup>P M (f i))"
   19.54 -    using f(3) by (auto intro!: le_SUPI2 positive_integral_positive)
   19.55 +    using f(3) by (auto intro!: SUP_upper2 positive_integral_positive)
   19.56    then show "(SUP i. integral\<^isup>P M (f i)) \<noteq> -\<infinity>" by auto
   19.57    have u_range: "\<And>x. x \<in> space M \<Longrightarrow> 0 \<le> u x \<and> u x \<noteq> \<infinity>"
   19.58      using u(3) by auto
   19.59 @@ -1044,8 +1044,8 @@
   19.60          with `a < 1` u_range[OF `x \<in> space M`]
   19.61          have "a * u x < 1 * u x"
   19.62            by (intro ereal_mult_strict_right_mono) (auto simp: image_iff)
   19.63 -        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUPR_apply)
   19.64 -        finally obtain i where "a * u x < f i x" unfolding SUPR_def
   19.65 +        also have "\<dots> \<le> (SUP i. f i x)" using u(2) by (auto simp: le_fun_def SUP_apply)
   19.66 +        finally obtain i where "a * u x < f i x" unfolding SUP_def
   19.67            by (auto simp add: less_Sup_iff)
   19.68          hence "a * u x \<le> f i x" by auto
   19.69          thus ?thesis using `x \<in> space M` by auto
   19.70 @@ -1104,18 +1104,18 @@
   19.71    shows "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) = (SUP i. integral\<^isup>P M (f i))"
   19.72  proof (rule antisym)
   19.73    show "(SUP j. integral\<^isup>P M (f j)) \<le> (\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M)"
   19.74 -    by (auto intro!: SUP_leI le_SUPI positive_integral_mono)
   19.75 +    by (auto intro!: SUP_least SUP_upper positive_integral_mono)
   19.76  next
   19.77    show "(\<integral>\<^isup>+ x. (SUP i. f i x) \<partial>M) \<le> (SUP j. integral\<^isup>P M (f j))"
   19.78      unfolding positive_integral_def_finite[of "\<lambda>x. SUP i. f i x"]
   19.79 -  proof (safe intro!: SUP_leI)
   19.80 +  proof (safe intro!: SUP_least)
   19.81      fix g assume g: "simple_function M g"
   19.82        and "g \<le> max 0 \<circ> (\<lambda>x. SUP i. f i x)" "range g \<subseteq> {0..<\<infinity>}"
   19.83      moreover then have "\<And>x. 0 \<le> (SUP i. f i x)" and g': "g`space M \<subseteq> {0..<\<infinity>}"
   19.84 -      using f by (auto intro!: le_SUPI2)
   19.85 +      using f by (auto intro!: SUP_upper2)
   19.86      ultimately show "integral\<^isup>S M g \<le> (SUP j. integral\<^isup>P M (f j))"
   19.87        by (intro  positive_integral_SUP_approx[OF f g _ g'])
   19.88 -         (auto simp: le_fun_def max_def SUPR_apply)
   19.89 +         (auto simp: le_fun_def max_def SUP_apply)
   19.90    qed
   19.91  qed
   19.92  
   19.93 @@ -1419,10 +1419,10 @@
   19.94      (SUP n. \<integral>\<^isup>+ x. (INF i:{n..}. u i x) \<partial>M)"
   19.95      unfolding liminf_SUPR_INFI using pos u
   19.96      by (intro positive_integral_monotone_convergence_SUP_AE)
   19.97 -       (elim AE_mp, auto intro!: AE_I2 intro: le_INFI INF_subset)
   19.98 +       (elim AE_mp, auto intro!: AE_I2 intro: INF_greatest INF_subset)
   19.99    also have "\<dots> \<le> liminf (\<lambda>n. integral\<^isup>P M (u n))"
  19.100      unfolding liminf_SUPR_INFI
  19.101 -    by (auto intro!: SUP_mono exI le_INFI positive_integral_mono INF_leI)
  19.102 +    by (auto intro!: SUP_mono exI INF_greatest positive_integral_mono INF_lower)
  19.103    finally show ?thesis .
  19.104  qed
  19.105  
    20.1 --- a/src/HOL/Probability/Lebesgue_Measure.thy	Wed Sep 14 10:55:07 2011 +0200
    20.2 +++ b/src/HOL/Probability/Lebesgue_Measure.thy	Wed Sep 14 10:08:52 2011 -0400
    20.3 @@ -125,7 +125,7 @@
    20.4      fix A assume "A \<in> sets lebesgue"
    20.5      then show "0 \<le> measure lebesgue A"
    20.6        unfolding lebesgue_def
    20.7 -      by (auto intro!: le_SUPI2 integral_nonneg)
    20.8 +      by (auto intro!: SUP_upper2 integral_nonneg)
    20.9    qed
   20.10  next
   20.11    show "countably_additive lebesgue (measure lebesgue)"
   20.12 @@ -146,7 +146,7 @@
   20.13      next
   20.14        fix i n show "0 \<le> ereal (?m n i)"
   20.15          using rA unfolding lebesgue_def
   20.16 -        by (auto intro!: le_SUPI2 integral_nonneg)
   20.17 +        by (auto intro!: SUP_upper2 integral_nonneg)
   20.18      next
   20.19        show "(SUP n. \<Sum>i. ereal (?m n i)) = (SUP n. ereal (?M n UNIV))"
   20.20        proof (intro arg_cong[where f="SUPR UNIV"] ext sums_unique[symmetric] sums_ereal[THEN iffD2] sums_def[THEN iffD2])
   20.21 @@ -642,7 +642,7 @@
   20.22    { fix i
   20.23      note u_eq
   20.24      also have "integral\<^isup>P lebesgue (u i) \<le> (\<integral>\<^isup>+x. max 0 (f x) \<partial>lebesgue)"
   20.25 -      by (intro lebesgue.positive_integral_mono) (auto intro: le_SUPI simp: u(4)[symmetric])
   20.26 +      by (intro lebesgue.positive_integral_mono) (auto intro: SUP_upper simp: u(4)[symmetric])
   20.27      finally have "integral\<^isup>S lebesgue (u i) \<noteq> \<infinity>"
   20.28        unfolding positive_integral_max_0 using f by auto }
   20.29    note u_fin = this
   20.30 @@ -687,7 +687,7 @@
   20.31          using lebesgue.positive_integral_eq_simple_integral[OF u(1,5)] by simp
   20.32        also have "\<dots> \<le> real (integral\<^isup>P lebesgue f)" using f
   20.33          by (auto intro!: real_of_ereal_positive_mono lebesgue.positive_integral_positive
   20.34 -             lebesgue.positive_integral_mono le_SUPI simp: SUP_eq[symmetric])
   20.35 +             lebesgue.positive_integral_mono SUP_upper simp: SUP_eq[symmetric])
   20.36        finally show "\<bar>integral UNIV (u' k)\<bar> \<le> real (integral\<^isup>P lebesgue f)" .
   20.37      qed
   20.38    qed
    21.1 --- a/src/HOL/Probability/Measure.thy	Wed Sep 14 10:55:07 2011 +0200
    21.2 +++ b/src/HOL/Probability/Measure.thy	Wed Sep 14 10:08:52 2011 -0400
    21.3 @@ -590,7 +590,7 @@
    21.4  lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))"
    21.5  proof -
    21.6    have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)"
    21.7 -    unfolding SUPR_def image_compose
    21.8 +    unfolding SUP_def image_compose
    21.9      unfolding surj_from_nat ..
   21.10    then show ?thesis by simp
   21.11  qed
    22.1 --- a/src/HOL/Probability/Radon_Nikodym.thy	Wed Sep 14 10:55:07 2011 +0200
    22.2 +++ b/src/HOL/Probability/Radon_Nikodym.thy	Wed Sep 14 10:08:52 2011 -0400
    22.3 @@ -358,7 +358,7 @@
    22.4        show "(\<lambda>x. SUP i. f i x) \<in> borel_measurable M"
    22.5          using f by (auto simp: G_def)
    22.6        { fix x show "0 \<le> (SUP i. f i x)"
    22.7 -          using f by (auto simp: G_def intro: le_SUPI2) }
    22.8 +          using f by (auto simp: G_def intro: SUP_upper2) }
    22.9      next
   22.10        fix A assume "A \<in> sets M"
   22.11        have "(\<integral>\<^isup>+x. (SUP i. f i x) * indicator A x \<partial>M) =
   22.12 @@ -369,12 +369,12 @@
   22.13          by (intro positive_integral_monotone_convergence_SUP)
   22.14             (auto simp: G_def incseq_Suc_iff le_fun_def split: split_indicator)
   22.15        finally show "(\<integral>\<^isup>+x. (SUP i. f i x) * indicator A x \<partial>M) \<le> \<nu> A"
   22.16 -        using f `A \<in> sets M` by (auto intro!: SUP_leI simp: G_def)
   22.17 +        using f `A \<in> sets M` by (auto intro!: SUP_least simp: G_def)
   22.18      qed }
   22.19    note SUP_in_G = this
   22.20    let ?y = "SUP g : G. integral\<^isup>P M g"
   22.21    have "?y \<le> \<nu> (space M)" unfolding G_def
   22.22 -  proof (safe intro!: SUP_leI)
   22.23 +  proof (safe intro!: SUP_least)
   22.24      fix g assume "\<forall>A\<in>sets M. (\<integral>\<^isup>+x. g x * indicator A x \<partial>M) \<le> \<nu> A"
   22.25      from this[THEN bspec, OF top] show "integral\<^isup>P M g \<le> \<nu> (space M)"
   22.26        by (simp cong: positive_integral_cong)
   22.27 @@ -413,14 +413,14 @@
   22.28      show "(SUP i. integral\<^isup>P M (?g i)) \<le> ?y"
   22.29        using g_in_G
   22.30        using [[simp_trace]]
   22.31 -      by (auto intro!: exI Sup_mono simp: SUPR_def)
   22.32 +      by (auto intro!: exI Sup_mono simp: SUP_def)
   22.33      show "?y \<le> (SUP i. integral\<^isup>P M (?g i))" unfolding y_eq
   22.34        by (auto intro!: SUP_mono positive_integral_mono Max_ge)
   22.35    qed
   22.36    finally have int_f_eq_y: "integral\<^isup>P M f = ?y" .
   22.37    have "\<And>x. 0 \<le> f x"
   22.38      unfolding f_def using `\<And>i. gs i \<in> G`
   22.39 -    by (auto intro!: le_SUPI2 Max_ge_iff[THEN iffD2] simp: G_def)
   22.40 +    by (auto intro!: SUP_upper2 Max_ge_iff[THEN iffD2] simp: G_def)
   22.41    let "?t A" = "\<nu> A - (\<integral>\<^isup>+x. ?F A x \<partial>M)"
   22.42    let ?M = "M\<lparr> measure := ?t\<rparr>"
   22.43    interpret M: sigma_algebra ?M
   22.44 @@ -591,11 +591,11 @@
   22.45      hence "0 < b * \<mu> A0" using b by (auto simp: ereal_zero_less_0_iff)
   22.46      with int_f_finite have "?y + 0 < integral\<^isup>P M f + b * \<mu> A0" unfolding int_f_eq_y
   22.47        using `f \<in> G`
   22.48 -      by (intro ereal_add_strict_mono) (auto intro!: le_SUPI2 positive_integral_positive)
   22.49 +      by (intro ereal_add_strict_mono) (auto intro!: SUP_upper2 positive_integral_positive)
   22.50      also have "\<dots> = integral\<^isup>P M ?f0" using f0_eq[OF top] `A0 \<in> sets M` sets_into_space
   22.51        by (simp cong: positive_integral_cong)
   22.52      finally have "?y < integral\<^isup>P M ?f0" by simp
   22.53 -    moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: le_SUPI)
   22.54 +    moreover from `?f0 \<in> G` have "integral\<^isup>P M ?f0 \<le> ?y" by (auto intro!: SUP_upper)
   22.55      ultimately show False by auto
   22.56    qed
   22.57    show ?thesis
   22.58 @@ -628,7 +628,7 @@
   22.59    have "{} \<in> ?Q" using v.empty_measure by auto
   22.60    then have Q_not_empty: "?Q \<noteq> {}" by blast
   22.61    have "?a \<le> \<mu> (space M)" using sets_into_space
   22.62 -    by (auto intro!: SUP_leI measure_mono top)
   22.63 +    by (auto intro!: SUP_least measure_mono top)
   22.64    then have "?a \<noteq> \<infinity>" using finite_measure_of_space
   22.65      by auto
   22.66    from SUPR_countable_SUPR[OF Q_not_empty, of \<mu>]
   22.67 @@ -661,7 +661,7 @@
   22.68    proof (rule antisym)
   22.69      show "?a \<le> (SUP i. \<mu> (?O i))" unfolding a_Lim
   22.70        using Q' by (auto intro!: SUP_mono measure_mono finite_UN)
   22.71 -    show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUPR_def
   22.72 +    show "(SUP i. \<mu> (?O i)) \<le> ?a" unfolding SUP_def
   22.73      proof (safe intro!: Sup_mono, unfold bex_simps)
   22.74        fix i
   22.75        have *: "(\<Union>Q' ` {..i}) = ?O i" by auto
   22.76 @@ -701,7 +701,7 @@
   22.77                using `\<nu> A \<noteq> \<infinity>` O_sets A by auto
   22.78            qed (fastforce intro!: incseq_SucI)
   22.79            also have "\<dots> \<le> ?a"
   22.80 -          proof (safe intro!: SUP_leI)
   22.81 +          proof (safe intro!: SUP_least)
   22.82              fix i have "?O i \<union> A \<in> ?Q"
   22.83              proof (safe del: notI)
   22.84                show "?O i \<union> A \<in> sets M" using O_sets A by auto
   22.85 @@ -711,7 +711,7 @@
   22.86                ultimately show "\<nu> (?O i \<union> A) \<noteq> \<infinity>"
   22.87                  using `\<nu> A \<noteq> \<infinity>` by auto
   22.88              qed
   22.89 -            then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule le_SUPI)
   22.90 +            then show "\<mu> (?O i \<union> A) \<le> ?a" by (rule SUP_upper)
   22.91            qed
   22.92            finally have "\<mu> A = 0"
   22.93              unfolding a_eq using real_measure[OF `?O_0 \<in> sets M`] real_measure[OF A(1)] by auto
    23.1 --- a/src/HOL/Quotient_Examples/Cset.thy	Wed Sep 14 10:55:07 2011 +0200
    23.2 +++ b/src/HOL/Quotient_Examples/Cset.thy	Wed Sep 14 10:08:52 2011 -0400
    23.3 @@ -97,6 +97,6 @@
    23.4  hide_fact (open) is_empty_def insert_def remove_def map_def filter_def
    23.5    forall_def exists_def card_def set_def subset_def psubset_def
    23.6    inter_def union_def empty_def UNIV_def uminus_def minus_def Inf_def Sup_def
    23.7 -  UNION_def
    23.8 +  UNION_eq
    23.9  
   23.10  end
    24.1 --- a/src/HOL/UNITY/Union.thy	Wed Sep 14 10:55:07 2011 +0200
    24.2 +++ b/src/HOL/UNITY/Union.thy	Wed Sep 14 10:08:52 2011 -0400
    24.3 @@ -246,7 +246,7 @@
    24.4  by (simp add: invariant_def, blast)
    24.5  
    24.6  lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
    24.7 -by (simp add: FP_def JN_stable INTER_def)
    24.8 +by (simp add: FP_def JN_stable INTER_eq)
    24.9  
   24.10  
   24.11  subsection{*Progress: transient, ensures*}