src/HOL/Probability/Regularity.thy
changeset 51000 c9adb50f74ad
parent 50881 ae630bab13da
child 52141 eff000cab70f
     1.1 --- a/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:27 2013 +0100
     1.2 +++ b/src/HOL/Probability/Regularity.thy	Thu Jan 31 11:31:30 2013 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    assumes f_nonneg: "\<And>i. 0 \<le> f i"
     1.5    assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. x \<le> f i + e"
     1.6    shows "x = (SUP i : A. f i)"
     1.7 -proof (subst eq_commute, rule ereal_SUPI)
     1.8 +proof (subst eq_commute, rule SUP_eqI)
     1.9    show "\<And>i. i \<in> A \<Longrightarrow> f i \<le> x" using f_bound by simp
    1.10  next
    1.11    fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> f i \<le> y)"
    1.12 @@ -45,7 +45,7 @@
    1.13    assumes f_nonneg: "\<And>i. 0 \<le> f i"
    1.14    assumes approx: "\<And>e. (e::real) > 0 \<Longrightarrow> \<exists>i \<in> A. f i \<le> x + e"
    1.15    shows "x = (INF i : A. f i)"
    1.16 -proof (subst eq_commute, rule ereal_INFI)
    1.17 +proof (subst eq_commute, rule INF_eqI)
    1.18    show "\<And>i. i \<in> A \<Longrightarrow> x \<le> f i" using f_bound by simp
    1.19  next
    1.20    fix y :: ereal assume f_le_y: "(\<And>i::'a. i \<in> A \<Longrightarrow> y \<le> f i)"
    1.21 @@ -79,7 +79,7 @@
    1.22    from INF have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> y \<le> f i) \<Longrightarrow> y \<le> x" by (auto intro: INF_greatest)
    1.23    ultimately
    1.24    have "(INF i : A. f i) = x + e" using `e > 0`
    1.25 -    by (intro ereal_INFI)
    1.26 +    by (intro INF_eqI)
    1.27        (force, metis add.comm_neutral add_left_mono ereal_less(1)
    1.28          linorder_not_le not_less_iff_gr_or_eq)
    1.29    thus False using assms by auto
    1.30 @@ -97,7 +97,7 @@
    1.31    from SUP have "\<And>y. (\<And>i. i \<in> A \<Longrightarrow> f i \<le> y) \<Longrightarrow> y \<ge> x" by (auto intro: SUP_least)
    1.32    ultimately
    1.33    have "(SUP i : A. f i) = x - e" using `e > 0` `\<bar>x\<bar> \<noteq> \<infinity>`
    1.34 -    by (intro ereal_SUPI)
    1.35 +    by (intro SUP_eqI)
    1.36         (metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
    1.37          metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
    1.38    thus False using assms by auto
    1.39 @@ -290,7 +290,7 @@
    1.40        have "emeasure M A \<le> (INF U:{U. A \<subseteq> U \<and> open U}. emeasure M U)"
    1.41          by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb)
    1.42        ultimately show ?thesis by simp
    1.43 -    qed (auto intro!: ereal_INFI)
    1.44 +    qed (auto intro!: INF_eqI)
    1.45      note `?inner A` `?outer A` }
    1.46    note closed_in_D = this
    1.47    from `B \<in> sets borel`
    1.48 @@ -299,8 +299,8 @@
    1.49    then show "?inner B" "?outer B"
    1.50    proof (induct B rule: sigma_sets_induct_disjoint)
    1.51      case empty
    1.52 -    { case 1 show ?case by (intro ereal_SUPI[symmetric]) auto }
    1.53 -    { case 2 show ?case by (intro ereal_INFI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
    1.54 +    { case 1 show ?case by (intro SUP_eqI[symmetric]) auto }
    1.55 +    { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) }
    1.56    next
    1.57      case (basic B)
    1.58      { case 1 from basic closed_in_D show ?case by auto }