src/HOL/Probability/Regularity.thy

   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x"
   assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
   assumes f_nonneg: "\<And>i. 0 \<le> f i"
   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
   shows "x = (SUP i : A. f i)"
-proof (subst eq_commute, rule ereal_SUPI)
+proof (subst eq_commute, rule SUP_eqI)
   show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
 next
   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
   with A_notempty f_nonneg have "y \<ge> 0" by auto (metis order_trans)
   show "x \<le> y"

   assumes f_bound: "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i"
   assumes f_fin: "\<And>i. i \<in> A \<Longrightarrow> f i \<noteq> \<infinity>"
   assumes f_nonneg: "\<And>i. 0 \<le> f i"
   assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
   shows "x = (INF i : A. f i)"
-proof (subst eq_commute, rule ereal_INFI)
+proof (subst eq_commute, rule INF_eqI)
   show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
 next
   fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
   with A_notempty f_fin have "y \<noteq> \<infinity>" by force
   show "y \<le> x"

   assume "\<forall>i\<in>A. \<not> f i < x + e"
   moreover
   from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
   ultimately
   have "(INF i : A. f i) = x + e" using `e > 0`
-    by (intro ereal_INFI)
+    by (intro INF_eqI)
       (force, metis add.comm_neutral add_left_mono ereal_less(1)
         linorder_not_le not_less_iff_gr_or_eq)
   thus False using assms by auto
 qed
 

   assume "\<forall>i\<in>A. \<not> x \<le> f i + e"
   moreover
   from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
   ultimately
   have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
-    by (intro ereal_SUPI)
+    by (intro SUP_eqI)
        (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
         metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
   thus False using assms by auto
 qed
 

       qed
       moreover
       have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
         by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
       ultimately show ?thesis by simp
-    qed (auto intro!: ereal_INFI)
+    qed (auto intro!: INF_eqI)
     note `?inner A` `?outer A` }
   note closed_in_D = this
   from `B \<in> sets borel`
   have "Int_stable (Collect closed)" "Collect closed \<subseteq> Pow UNIV" "B \<in> sigma_sets UNIV (Collect closed)" 
     by (auto simp: Int_stable_def borel_eq_closed)
   then show "?inner B" "?outer B"
   proof (induct B rule: sigma_sets_induct_disjoint)
     case empty
-    { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
-    { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
+    { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
+    { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
   next
     case (basic B)
     { case 1 from basic closed_in_D show ?case by auto }
     { case 2 from basic closed_in_D show ?case by auto }
   next